Verification run
Run 1064
failed commit
c011181bbc4a toolchain lean-v4-30-0 prover lean took 25m 14s · finished 3d ago lake build failed with exit code 1 (toolchain lean-v4-30-0, command: elan run leanprover/lean4:v4.30.0 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase lake build)
Package inputs
This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.
Trust verification
Recomputes trust checks from the recorded attestations, manifest, and command history.
(verification not run)
Manifest
Loads the published files manifest and location metadata for this job.
(manifest not loaded)
Verifier log excerpt
$ git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1365-source
exit_code=Some(0) duration_ms=3816
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1365-source'...
$ git checkout c011181bbc4ab6cdef92e729c373cfa7dfb7bcb1
exit_code=Some(0) duration_ms=160
stderr:
Note: switching to 'c011181bbc4ab6cdef92e729c373cfa7dfb7bcb1'.
You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.
If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:
git switch -c <new-branch-name>
Or undo this operation with:
git switch -
Turn off this advice by setting config variable advice.detachedHead to false
HEAD is now at c011181 Construct restriction calibrated route
Resolved source revision: c011181bbc4ab6cdef92e729c373cfa7dfb7bcb1
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=c011181bbc4ab6cdef92e729c373cfa7dfb7bcb1 provenance={"branch":"master","checked_out_revision":"c011181bbc4ab6cdef92e729c373cfa7dfb7bcb1","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"c011181bbc4ab6cdef92e729c373cfa7dfb7bcb1","used_missing_commit_fetch":false}
Resolved toolchain: lean-v4-30-0 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
Restored Lean workspace build cache
Restored 9 Lean dependency package snapshot(s)
Prepared 9 shared Lean git mirror alias(es)
Lean semantic module cache: pre-semantic phase failed; not running semantic extraction
$ lake exe cache get
exit_code=Some(0) duration_ms=92781
stdout:
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
Downloaded: 1 file(s) [attempted 1/8459 = 0%, 11 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 34 KB/s], Decompressed: 12
Downloaded: 41 file(s) [attempted 41/8459 = 0%, 25 KB/s], Decompressed: 39
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 29 KB/s], Decompressed: 61
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 195 KB/s], Decompressed: 71
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 35 KB/s], Decompressed: 71
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 96 KB/s], Decompressed: 76
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 430 KB/s], Decompressed: 76
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 251 KB/s], Decompressed: 141
Downloaded: 268 file(s) [attempted 268/8459 = 3%, 248 KB/s], Decompressed: 141
Downloaded: 306 file(s) [attempted 306/8459 = 3%, 524 KB/s], Decompressed: 223
Downloaded: 343 file(s) [attempted 343/8459 = 4%, 422 KB/s], Decompressed: 223
Downloaded: 377 file(s) [attempted 377/8459 = 4%, 113 KB/s], Decompressed: 223
Downloaded: 412 file(s) [attempted 412/8459 = 4%, 301 KB/s], Decompressed: 408
Downloaded: 450 file(s) [attempted 450/8459 = 5%, 67 KB/s], Decompressed: 446
Downloaded: 494 file(s) [attempted 494/8459 = 5%, 276 KB/s], Decompressed: 490
Downloaded: 538 file(s) [attempted 538/8459 = 6%, 440 KB/s], Decompressed: 535
Downloaded: 573 file(s) [attempted 573/8459 = 6%, 22 KB/s], Decompressed: 569
Downloaded: 614 file(s) [attempted 614/8459 = 7%, 78 KB/s], Decompressed: 610
Downloaded: 651 file(s) [attempted 651/8459 = 7%, 336 KB/s], Decompressed: 614
Downloaded: 696 file(s) [attempted 696/8459 = 8%, 152 KB/s], Decompressed: 614
Downloaded: 741 file(s) [attempted 741/8459 = 8%, 310 KB/s], Decompressed: 617
Downloaded: 775 file(s) [attempted 775/8459 = 9%, 167 KB/s], Decompressed: 617
Downloaded: 812 file(s) [attempted 812/8459 = 9%, 657 KB/s], Decompressed: 795
Downloaded: 854 file(s) [attempted 854/8459 = 10%, 234 KB/s], Decompressed: 850
Downloaded: 895 file(s) [attempted 895/8459 = 10%, 71 KB/s], Decompressed: 891
Downloaded: 932 file(s) [attempted 932/8459 = 11%, 133 KB/s], Decompressed: 925
Downloaded: 973 file(s) [attempted 973/8459 = 11%, 768 KB/s], Decompressed: 967
Downloaded: 1015 file(s) [attempted 1015/8459 = 11%, 169 KB/s], Decompressed: 984
Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 66 KB/s], Decompressed: 984
Downloaded: 1094 file(s) [attempted 1094/8459 = 12%, 568 KB/s], Decompressed: 1090
Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 74 KB/s], Decompressed: 1124
Downloaded: 1186 file(s) [attempted 1186/8459 = 14%, 38 KB/s], Decompressed: 1124
Downloaded: 1234 file(s) [attempted 1234/8459 = 14%, 205 KB/s], Decompressed: 1230
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 58 KB/s], Decompressed: 1268
Downloaded: 1312 file(s) [attempted 1312/8459 = 15%, 795 KB/s], Decompressed: 1271
Downloaded: 1353 file(s) [attempted 1353/8459 = 15%, 149 KB/s], Decompressed: 1271
Downloaded: 1394 file(s) [attempted 1394/8459 = 16%, 44 KB/s], Decompressed: 1281
Downloaded: 1435 file(s) [attempted 1435/8459 = 16%, 501 KB/s], Decompressed: 1281
Downloaded: 1477 file(s) [attempted 1477/8459 = 17%, 132 KB/s], Decompressed: 1367
Downloaded: 1514 file(s) [attempted 1514/8459 = 17%, 376 KB/s], Decompressed: 1367
Downloaded: 1555 file(s) [attempted 1555/8459 = 18%, 178 KB/s], Decompressed: 1459
Downloaded: 1596 file(s) [attempted 1596/8459 = 18%, 21 KB/s], Decompressed: 1459
Downloaded: 1637 file(s) [attempted 1637/8459 = 19%, 241 KB/s], Decompressed: 1531
Downloaded: 1678 file(s) [attempted 1678/8459 = 19%, 478 KB/s], Decompressed: 1531
Downloaded: 1716 file(s) [attempted 1716/8459 = 20%, 284 KB/s], Decompressed: 1620
Downloaded: 1757 file(s) [attempted 1757/8459 = 20%, 78 KB/s], Decompressed: 1750
Downloaded: 1802 file(s) [attempted 1802/8459 = 21%, 46 KB/s], Decompressed: 1750
Downloaded: 1839 file(s) [attempted 1839/8459 = 21%, 110 KB/s], Decompressed: 1754
Downloaded: 1877 file(s) [attempted 1877/8459 = 22%, 262 KB/s], Decompressed: 1754
Downloaded: 1915 file(s) [attempted 1915/8459 = 22%, 497 KB/s], Decompressed: 1836
Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 2876 KB/s], Decompressed: 1915
Downloaded: 2004 file(s) [attempted 2004/8459 = 23%, 379 KB/s], Decompressed: 1915
Downloaded: 2045 file(s) [attempted 2045/8459 = 24%, 250 KB/s], Decompressed: 1928
Downloaded: 2081 file(s) [attempted 2081/8459 = 24%, 1170 KB/s], Decompressed: 1928
Downloaded: 2123 file(s) [attempted 2123/8459 = 25%, 202 KB/s], Decompressed: 2106
Downloaded: 2168 file(s) [attempted 2168/8459 = 25%, 1380 KB/s], Decompressed: 2106
Downloaded: 2209 file(s) [attempted 2209/8459 = 26%, 265 KB/s], Decompressed: 2106
Downloaded: 2250 file(s) [attempted 2250/8459 = 26%, 868 KB/s], Decompressed: 2123
Downloaded: 2288 file(s) [attempted 2288/8459 = 27%, 321 KB/s], Decompressed: 2212
Downloaded: 2325 file(s) [attempted 2325/8459 = 27%, 39 KB/s], Decompressed: 2212
Downloaded: 2366 file(s) [attempted 2366/8459 = 27%, 141 KB/s], Decompressed: 2253
Downloaded: 2411 file(s) [attempted 2411/8459 = 28%, 182 KB/s], Decompressed: 2253
Downloaded: 2448 file(s) [attempted 2448/8459 = 28%, 269 KB/s], Decompressed: 2339
Downloaded: 2490 file(s) [attempted 2490/8459 = 29%, 285 KB/s], Decompressed: 2339
Downloaded: 2531 file(s) [attempted 2531/8459 = 29%, 339 KB/s], Decompressed: 2339
Downloaded: 2572 file(s) [attempted 2572/8459 = 30%, 618 KB/s], Decompressed: 2339
Downloaded: 2616 file(s) [attempted 2616/8459 = 30%, 1910 KB/s], Decompressed: 2438
Downloaded: 2655 file(s) [attempted 2655/8459 = 31%, 251 KB/s], Decompressed: 2647
Downloaded: 2695 file(s) [attempted 2695/8459 = 31%, 58 KB/s], Decompressed: 2685
Downloaded: 2736 file(s) [attempted 2736/8459 = 32%, 41 KB/s], Decompressed: 2685
Downloaded: 2777 file(s) [attempted 2777/8459 = 32%, 160 KB/s], Decompressed: 2688
Downloaded: 2822 file(s) [attempted 2822/8459 = 33%, 227 KB/s], Decompressed: 2811
Downloaded: 2859 file(s) [attempted 2859/8459 = 33%, 32 KB/s], Decompressed: 2811
Downloaded: 2899 file(s) [attempted 2899/8459 = 34%, 160 KB/s], Decompressed: 2815
Downloaded: 2938 file(s) [attempted 2938/8459 = 34%, 646 KB/s], Decompressed: 2931
Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 1052 KB/s], Decompressed: 2979
Downloaded: 3023 file(s) [attempted 3023/8459 = 35%, 120 KB/s], Decompressed: 3020
Downloaded: 3064 file(s) [attempted 3064/8459 = 36%, 187 KB/s], Decompressed: 3058
Downloaded: 3106 file(s) [attempted 3106/8459 = 36%, 157 KB/s], Decompressed: 3099
Downloaded: 3143 file(s) [attempted 3143/8459 = 37%, 1124 KB/s], Decompressed: 3140
Downloaded: 3184 file(s) [attempted 3184/8459 = 37%, 177 KB/s], Decompressed: 3157
Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 174 KB/s], Decompressed: 3157
Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 2922 KB/s], Decompressed: 3160
Downloaded: 3314 file(s) [attempted 3314/8459 = 39%, 282 KB/s], Decompressed: 3160
Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 228 KB/s], Decompressed: 3349
Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 51 KB/s], Decompressed: 3393
Downloaded: 3441 file(s) [attempted 3441/8459 = 40%, 347 KB/s], Decompressed: 3438
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 250 KB/s], Decompressed: 3479
Downloaded: 3523 file(s) [attempted 3523/8459 = 41%, 391 KB/s], Decompressed: 3479
Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 122 KB/s], Decompressed: 3479
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 120 KB/s], Decompressed: 3598
Downloaded: 3646 file(s) [attempted 3646/8459 = 43%, 338 KB/s], Decompressed: 3643
Downloaded: 3691 file(s) [attempted 3691/8459 = 43%, 78 KB/s], Decompressed: 3687
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 289 KB/s], Decompressed: 3728
Downloaded: 3771 file(s) [attempted 3771/8459 = 44%, 94 KB/s], Decompressed: 3763
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 361 KB/s], Decompressed: 3800
Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 240 KB/s], Decompressed: 3845
Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 934 KB/s], Decompressed: 3889
Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 930 KB/s], Decompressed: 3934
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 343 KB/s], Decompressed: 3975
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 44 KB/s], Decompressed: 3989
Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 453 KB/s], Decompressed: 3989
Downloaded: 4095 file(s) [attempted 4095/8459 = 48%, 36 KB/s], Decompressed: 4091
Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 83 KB/s], Decompressed: 4136
Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 49 KB/s], Decompressed: 4149
Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 310 KB/s], Decompressed: 4149
Downloaded: 4262 file(s) [attempted 4262/8459 = 50%, 425 KB/s], Decompressed: 4242
Downloaded: 4300 file(s) [attempted 4300/8459 = 50%, 115 KB/s], Decompressed: 4262
Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 221 KB/s], Decompressed: 4262
Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 853 KB/s], Decompressed: 4269
Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 471 KB/s], Decompressed: 4269
Downloaded: 4468 file(s) [attempted 4468/8459 = 52%, 365 KB/s], Decompressed: 4464
Downloaded: 4512 file(s) [attempted 4512/8459 = 53%, 277 KB/s], Decompressed: 4505
Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 48 KB/s], Decompressed: 4550
Downloaded: 4594 file(s) [attempted 4594/8459 = 54%, 379 KB/s], Decompressed: 4584
Downloaded: 4632 file(s) [attempted 4632/8459 = 54%, 94 KB/s], Decompressed: 4629
Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 74 KB/s], Decompressed: 4652
Downloaded: 4717 file(s) [attempted 4717/8459 = 55%, 24 KB/s], Decompressed: 4652
Downloaded: 4759 file(s) [attempted 4759/8459 = 56%, 133 KB/s], Decompressed: 4738
Downloaded: 4800 file(s) [attempted 4800/8459 = 56%, 395 KB/s], Decompressed: 4738
Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 1900 KB/s], Decompressed: 4738
Downloaded: 4882 file(s) [attempted 4882/8459 = 57%, 243 KB/s], Decompressed: 4759
Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 407 KB/s], Decompressed: 4759
Downloaded: 4964 file(s) [attempted 4964/8459 = 58%, 88 KB/s], Decompressed: 4848
Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 138 KB/s], Decompressed: 4848
Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 89 KB/s], Decompressed: 4943
Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 330 KB/s], Decompressed: 4943
Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 640 KB/s], Decompressed: 4943
Downloaded: 5176 file(s) [attempted 5176/8459 = 61%, 110 KB/s], Decompressed: 5039
Downloaded: 5217 file(s) [attempted 5217/8459 = 61%, 102 KB/s], Decompressed: 5039
Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 84 KB/s], Decompressed: 5248
Downloaded: 5292 file(s) [attempted 5292/8459 = 62%, 417 KB/s], Decompressed: 5248
Downloaded: 5330 file(s) [attempted 5330/8459 = 63%, 304 KB/s], Decompressed: 5248
Downloaded: 5375 file(s) [attempted 5375/8459 = 63%, 377 KB/s], Decompressed: 5334
Downloaded: 5412 file(s) [attempted 5412/8459 = 63%, 788 KB/s], Decompressed: 5334
Downloaded: 5457 file(s) [attempted 5457/8459 = 64%, 831 KB/s], Decompressed: 5440
Downloaded: 5494 file(s) [attempted 5494/8459 = 64%, 118 KB/s], Decompressed: 5491
Downloaded: 5535 file(s) [attempted 5535/8459 = 65%, 578 KB/s], Decompressed: 5532
Downloaded: 5577 file(s) [attempted 5577/8459 = 65%, 1424 KB/s], Decompressed: 5549
Downloaded: 5621 file(s) [attempted 5621/8459 = 66%, 336 KB/s], Decompressed: 5549
Downloaded: 5662 file(s) [attempted 5662/8459 = 66%, 1019 KB/s], Decompressed: 5559
Downloaded: 5700 file(s) [attempted 5700/8459 = 67%, 90 KB/s], Decompressed: 5559
Downloaded: 5741 file(s) [attempted 5741/8459 = 67%, 98 KB/s], Decompressed: 5645
Downloaded: 5778 file(s) [attempted 5778/8459 = 68%, 521 KB/s], Decompressed: 5645
Downloaded: 5823 file(s) [attempted 5823/8459 = 68%, 86 KB/s], Decompressed: 5645
Downloaded: 5867 file(s) [attempted 5867/8459 = 69%, 166 KB/s], Decompressed: 5734
Downloaded: 5902 file(s) [attempted 5902/8459 = 69%, 344 KB/s], Decompressed: 5734
Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 309 KB/s], Decompressed: 5929
Downloaded: 5994 file(s) [attempted 5994/8459 = 70%, 625 KB/s], Decompressed: 5980
Downloaded: 6035 file(s) [attempted 6035/8459 = 71%, 1109 KB/s], Decompressed: 5980
Downloaded: 6076 file(s) [attempted 6076/8459 = 71%, 102 KB/s], Decompressed: 5984
Downloaded: 6124 file(s) [attempted 6124/8459 = 72%, 399 KB/s], Decompressed: 6117
Downloaded: 6169 file(s) [attempted 6169/8459 = 72%, 269 KB/s], Decompressed: 6160
Downloaded: 6199 file(s) [attempted 6199/8459 = 73%, 75 KB/s], Decompressed: 6193
Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 103 KB/s], Decompressed: 6237
Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 127 KB/s], Decompressed: 6278
Downloaded: 6329 file(s) [attempted 6329/8459 = 74%, 113 KB/s], Decompressed: 6326
Downloaded: 6374 file(s) [attempted 6374/8459 = 75%, 337 KB/s], Decompressed: 6336
Downloaded: 6412 file(s) [attempted 6412/8459 = 75%, 71 KB/s], Decompressed: 6336
Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 37 KB/s], Decompressed: 6343
Downloaded: 6490 file(s) [attempted 6490/8459 = 76%, 165 KB/s], Decompressed: 6343
Downloaded: 6535 file(s) [attempted 6535/8459 = 77%, 86 KB/s], Decompressed: 6521
Downloaded: 6576 file(s) [attempted 6576/8459 = 77%, 517 KB/s], Decompressed: 6572
Downloaded: 6613 file(s) [attempted 6613/8459 = 78%, 57 KB/s], Decompressed: 6607
Downloaded: 6651 file(s) [attempted 6651/8459 = 78%, 468 KB/s], Decompressed: 6648
Downloaded: 6692 file(s) [attempted 6692/8459 = 79%, 528 KB/s], Decompressed: 6689
Downloaded: 6737 file(s) [attempted 6737/8459 = 79%, 72 KB/s], Decompressed: 6733
Downloaded: 6781 file(s) [attempted 6781/8459 = 80%, 169 KB/s], Decompressed: 6778
Downloaded: 6822 file(s) [attempted 6822/8459 = 80%, 597 KB/s], Decompressed: 6815
Downloaded: 6860 file(s) [attempted 6860/8459 = 81%, 79 KB/s], Decompressed: 6850
Downloaded: 6898 file(s) [attempted 6898/8459 = 81%, 123 KB/s], Decompressed: 6891
Downloaded: 6939 file(s) [attempted 6939/8459 = 82%, 436 KB/s], Decompressed: 6935
Downloaded: 6987 file(s) [attempted 6987/8459 = 82%, 889 KB/s], Decompressed: 6983
Downloaded: 7034 file(s) [attempted 7034/8459 = 83%, 1010 KB/s], Decompressed: 7028
Downloaded: 7082 file(s) [attempted 7082/8459 = 83%, 40 KB/s], Decompressed: 7075
Downloaded: 7123 file(s) [attempted 7123/8459 = 84%, 243 KB/s], Decompressed: 7086
Downloaded: 7164 file(s) [attempted 7164/8459 = 84%, 479 KB/s], Decompressed: 7086
Downloaded: 7202 file(s) [attempted 7202/8459 = 85%, 147 KB/s], Decompressed: 7199
Downloaded: 7243 file(s) [attempted 7243/8459 = 85%, 41 KB/s], Decompressed: 7202
Downloaded: 7284 file(s) [attempted 7284/8459 = 86%, 842 KB/s], Decompressed: 7202
Downloaded: 7325 file(s) [attempted 7325/8459 = 86%, 305 KB/s], Decompressed: 7212
Downloaded: 7370 file(s) [attempted 7370/8459 = 87%, 116 KB/s], Decompressed: 7212
Downloaded: 7407 file(s) [attempted 7407/8459 = 87%, 1122 KB/s], Decompressed: 7295
Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 988 KB/s], Decompressed: 7295
Downloaded: 7493 file(s) [attempted 7493/8459 = 88%, 471 KB/s], Decompressed: 7295
Downloaded: 7537 file(s) [attempted 7537/8459 = 89%, 194 KB/s], Decompressed: 7295
Downloaded: 7579 file(s) [attempted 7579/8459 = 89%, 871 KB/s], Decompressed: 7390
Downloaded: 7616 file(s) [attempted 7616/8459 = 90%, 537 KB/s], Decompressed: 7390
Downloaded: 7657 file(s) [attempted 7657/8459 = 90%, 479 KB/s], Decompressed: 7551
Downloaded: 7702 file(s) [attempted 7702/8459 = 91%, 58 KB/s], Decompressed: 7551
Downloaded: 7739 file(s) [attempted 7739/8459 = 91%, 166 KB/s], Decompressed: 7551
Downloaded: 7780 file(s) [attempted 7780/8459 = 91%, 314 KB/s], Decompressed: 7657
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 162 KB/s], Decompressed: 7657
Downloaded: 7869 file(s) [attempted 7869/8459 = 93%, 61 KB/s], Decompressed: 7757
Downloaded: 7904 file(s) [attempted 7904/8459 = 93%, 73 KB/s], Decompressed: 7856
Downloaded: 7945 file(s) [attempted 7945/8459 = 93%, 239 KB/s], Decompressed: 7856
Downloaded: 7986 file(s) [attempted 7986/8459 = 94%, 208 KB/s], Decompressed: 7876
Downloaded: 8030 file(s) [attempted 8030/8459 = 94%, 562 KB/s], Decompressed: 7876
Downloaded: 8076 file(s) [attempted 8076/8459 = 95%, 639 KB/s], Decompressed: 7969
Downloaded: 8112 file(s) [attempted 8112/8459 = 95%, 295 KB/s], Decompressed: 8106
Downloaded: 8150 file(s) [attempted 8150/8459 = 96%, 213 KB/s], Decompressed: 8140
Downloaded: 8191 file(s) [attempted 8191/8459 = 96%, 102 KB/s], Decompressed: 8140
Downloaded: 8232 file(s) [attempted 8232/8459 = 97%, 569 KB/s], Decompressed: 8143
Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 756 KB/s], Decompressed: 8232
Downloaded: 8325 file(s) [attempted 8325/8459 = 98%, 183 KB/s], Decompressed: 8232
Downloaded: 8366 file(s) [attempted 8366/8459 = 98%, 406 KB/s], Decompressed: 8253
Downloaded: 8403 file(s) [attempted 8403/8459 = 99%, 607 KB/s], Decompressed: 8253
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 502 KB/s], Decompressed: 8338
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 502 KB/s], Decompressed: 8451
$ lake build
exit_code=Some(1) duration_ms=762593
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (95s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.9s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.7s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.8s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.7s)
✔ [763/772] Built Iut.Foundations.QualitativeData (2.2s)
✔ [3382/3392] Built Iut.Foundations.AlgorithmicOutput (1.8s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (3.1s)
✔ [3389/3394] Built Iut.Stage1.CorollarySchema (114s)
✔ [3390/3397] Built Iut.Stage1.SourceObligations (3.1s)
✔ [3392/3398] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3394/3401] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (117s)
warning: Iut/Stage1/IUTStage1SourceCore.lean:19880:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotient_card_eq_pow_finrank`:
[FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [FiniteDimensional ℚ_[p] K] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20063:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotientCosetHaarCharacterEndpoint`:
[FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [FiniteDimensional ℚ_[p] K] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20130:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.unitBallHaarCharacterEndpoint`:
[FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [FiniteDimensional ℚ_[p] K] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20532:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20533:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20537:4: `have hinteger_eq : (integer : ℚ_[p]) = (p : ℚ_[p]) * (preimage : ℚ_[p]) := by
simpa [IUTStage1PadicIntegerUnitBallSource.padicIntAddEquivIntegerAddSubgroup, hpreimage_eq] using
hpoint_eq.symm` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20547:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20572:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20573:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20576:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20577:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20578:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
✔ [3411/3425] Built Iut.Stage1.IUTStage1Remark312Absorption (59s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (18s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (5.3s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (6.3s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (13s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (10s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (28s)
warning: Iut/Stage1/IUTStage1Theorem311.lean:4518:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4523:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4655:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4687:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4692:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4735:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4789:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4824:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4829:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4961:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4995:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5000:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5138:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5172:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5177:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5320:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5352:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5357:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5470:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:7525:6: try 'simp' instead of 'simpa'
Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15277:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15618:4: try 'simp' instead of 'simpa'
Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:16875:4: try 'simp' instead of 'simpa'
Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:17353:5: unused variable `targetSource`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:18439:5: unused variable `data`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:21472:5: unused variable `obligations`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
✖ [3418/3425] Building Iut.Stage1.IUTStage1StepXI (196s)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean /apx/source/Iut/Stage1/IUTStage1StepXI.lean -o /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI.olean -i /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI.ilean -c /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI.c --setup /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI.setup.json --json
error: Lean exited with code 137
Some required targets logged failures:
- Iut.Stage1.IUTStage1StepXI
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: build failed
$ lake build :blueprint
exit_code=Some(1) duration_ms=21236
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: unknown package facet `blueprint`
blueprint_build failed; continuing (non-fatal phase).
Command runs
git_clone exit 0
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1365-source
Cloning into '/var/lib/apodeixis/repos/job-1365-source'...
git_checkout exit 0
git checkout c011181bbc4ab6cdef92e729c373cfa7dfb7bcb1
Note: switching to 'c011181bbc4ab6cdef92e729c373cfa7dfb7bcb1'. You are in 'detached HEAD' state. You can look around, make experimental changes and commit them, and you can discard any commits you make in this state without impacting any branches by switching back to a branch. If you want to create a new branch to retain commits you create, you may do so (now or later) by using -c with the switch command. Example: git switch -c <new-branch-name> Or undo this operation with: git switch - Turn off this advice by setting config variable advice.detachedHead to false HEAD is now at c011181 Construct restriction calibrated route
lake_cache exit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache Decompressed 8459 file(s) Already decompressed 8459 file(s)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes Downloaded: 1 file(s) [attempted 1/8459 = 0%, 11 KB/s], Decompressed: 0 Downloaded: 16 file(s) [attempted 16/8459 = 0%, 34 KB/s], Decompressed: 12 Downloaded: 41 file(s) [attempted 41/8459 = 0%, 25 KB/s], Decompressed: 39 Downloaded: 65 file(s) [attempted 65/8459 = 0%, 29 KB/s], Decompressed: 61 Downloaded: 89 file(s) [attempted 89/8459 = 1%, 195 KB/s], Decompressed: 71 Downloaded: 124 file(s) [attempted 124/8459 = 1%, 35 KB/s], Decompressed: 71 Downloaded: 158 file(s) [attempted 158/8459 = 1%, 96 KB/s], Decompressed: 76 Downloaded: 196 file(s) [attempted 196/8459 = 2%, 430 KB/s], Decompressed: 76 Downloaded: 230 file(s) [attempted 230/8459 = 2%, 251 KB/s], Decompressed: 141 Downloaded: 268 file(s) [attempted 268/8459 = 3%, 248 KB/s], Decompressed: 141 Downloaded: 306 file(s) [attempted 306/8459 = 3%, 524 KB/s], Decompressed: 223 Downloaded: 343 file(s) [attempted 343/8459 = 4%, 422 KB/s], Decompressed: 223 Downloaded: 377 file(s) [attempted 377/8459 = 4%, 113 KB/s], Decompressed: 223 Downloaded: 412 file(s) [attempted 412/8459 = 4%, 301 KB/s], Decompressed: 408 Downloaded: 450 file(s) [attempted 450/8459 = 5%, 67 KB/s], Decompressed: 446 Downloaded: 494 file(s) [attempted 494/8459 = 5%, 276 KB/s], Decompressed: 490 Downloaded: 538 file(s) [attempted 538/8459 = 6%, 440 KB/s], Decompressed: 535 Downloaded: 573 file(s) [attempted 573/8459 = 6%, 22 KB/s], Decompressed: 569 Downloaded: 614 file(s) [attempted 614/8459 = 7%, 78 KB/s], Decompressed: 610 Downloaded: 651 file(s) [attempted 651/8459 = 7%, 336 KB/s], Decompressed: 614 Downloaded: 696 file(s) [attempted 696/8459 = 8%, 152 KB/s], Decompressed: 614 Downloaded: 741 file(s) [attempted 741/8459 = 8%, 310 KB/s], Decompressed: 617 Downloaded: 775 file(s) [attempted 775/8459 = 9%, 167 KB/s], Decompressed: 617 Downloaded: 812 file(s) [attempted 812/8459 = 9%, 657 KB/s], Decompressed: 795 Downloaded: 854 file(s) [attempted 854/8459 = 10%, 234 KB/s], Decompressed: 850 Downloaded: 895 file(s) [attempted 895/8459 = 10%, 71 KB/s], Decompressed: 891 Downloaded: 932 file(s) [attempted 932/8459 = 11%, 133 KB/s], Decompressed: 925 Downloaded: 973 file(s) [attempted 973/8459 = 11%, 768 KB/s], Decompressed: 967 Downloaded: 1015 file(s) [attempted 1015/8459 = 11%, 169 KB/s], Decompressed: 984 Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 66 KB/s], Decompressed: 984 Downloaded: 1094 file(s) [attempted 1094/8459 = 12%, 568 KB/s], Decompressed: 1090 Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 74 KB/s], Decompressed: 1124 Downloaded: 1186 file(s) [attempted 1186/8459 = 14%, 38 KB/s], Decompressed: 1124 Downloaded: 1234 file(s) [attempted 1234/8459 = 14%, 205 KB/s], Decompressed: 1230 Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 58 KB/s], Decompressed: 1268 Downloaded: 1312 file(s) [attempted 1312/8459 = 15%, 795 KB/s], Decompressed: 1271 Downloaded: 1353 file(s) [attempted 1353/8459 = 15%, 149 KB/s], Decompressed: 1271 Downloaded: 1394 file(s) [attempted 1394/8459 = 16%, 44 KB/s], Decompressed: 1281 Downloaded: 1435 file(s) [attempted 1435/8459 = 16%, 501 KB/s], Decompressed: 1281 Downloaded: 1477 file(s) [attempted 1477/8459 = 17%, 132 KB/s], Decompressed: 1367 Downloaded: 1514 file(s) [attempted 1514/8459 = 17%, 376 KB/s], Decompressed: 1367 Downloaded: 1555 file(s) [attempted 1555/8459 = 18%, 178 KB/s], Decompressed: 1459 Downloaded: 1596 file(s) [attempted 1596/8459 = 18%, 21 KB/s], Decompressed: 1459 Downloaded: 1637 file(s) [attempted 1637/8459 = 19%, 241 KB/s], Decompressed: 1531 Downloaded: 1678 file(s) [attempted 1678/8459 = 19%, 478 KB/s], Decompressed: 1531 Downloaded: 1716 file(s) [attempted 1716/8459 = 20%, 284 KB/s], Decompressed: 1620 Downloaded: 1757 file(s) [attempted 1757/8459 = 20%, 78 KB/s], Decompressed: 1750 Downloaded: 1802 file(s) [attempted 1802/8459 = 21%, 46 KB/s], Decompressed: 1750 Downloaded: 1839 file(s) [attempted 1839/8459 = 21%, 110 KB/s], Decompressed: 1754 Downloaded: 1877 file(s) [attempted 1877/8459 = 22%, 262 KB/s], Decompressed: 1754 Downloaded: 1915 file(s) [attempted 1915/8459 = 22%, 497 KB/s], Decompressed: 1836 Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 2876 KB/s], Decompressed: 1915 Downloaded: 2004 file(s) [attempted 2004/8459 = 23%, 379 KB/s], Decompressed: 1915 Downloaded: 2045 file(s) [attempted 2045/8459 = 24%, 250 KB/s], Decompressed: 1928 Downloaded: 2081 file(s) [attempted 2081/8459 = 24%, 1170 KB/s], Decompressed: 1928 Downloaded: 2123 file(s) [attempted 2123/8459 = 25%, 202 KB/s], Decompressed: 2106 Downloaded: 2168 file(s) [attempted 2168/8459 = 25%, 1380 KB/s], Decompressed: 2106 Downloaded: 2209 file(s) [attempted 2209/8459 = 26%, 265 KB/s], Decompressed: 2106 Downloaded: 2250 file(s) [attempted 2250/8459 = 26%, 868 KB/s], Decompressed: 2123 Downloaded: 2288 file(s) [attempted 2288/8459 = 27%, 321 KB/s], Decompressed: 2212 Downloaded: 2325 file(s) [attempted 2325/8459 = 27%, 39 KB/s], Decompressed: 2212 Downloaded: 2366 file(s) [attempted 2366/8459 = 27%, 141 KB/s], Decompressed: 2253 Downloaded: 2411 file(s) [attempted 2411/8459 = 28%, 182 KB/s], Decompressed: 2253 Downloaded: 2448 file(s) [attempted 2448/8459 = 28%, 269 KB/s], Decompressed: 2339 Downloaded: 2490 file(s) [attempted 2490/8459 = 29%, 285 KB/s], Decompressed: 2339 Downloaded: 2531 file(s) [attempted 2531/8459 = 29%, 339 KB/s], Decompressed: 2339 Downloaded: 2572 file(s) [attempted 2572/8459 = 30%, 618 KB/s], Decompressed: 2339 Downloaded: 2616 file(s) [attempted 2616/8459 = 30%, 1910 KB/s], Decompressed: 2438 Downloaded: 2655 file(s) [attempted 2655/8459 = 31%, 251 KB/s], Decompressed: 2647 Downloaded: 2695 file(s) [attempted 2695/8459 = 31%, 58 KB/s], Decompressed: 2685 Downloaded: 2736 file(s) [attempted 2736/8459 = 32%, 41 KB/s], Decompressed: 2685 Downloaded: 2777 file(s) [attempted 2777/8459 = 32%, 160 KB/s], Decompressed: 2688 Downloaded: 2822 file(s) [attempted 2822/8459 = 33%, 227 KB/s], Decompressed: 2811 Downloaded: 2859 file(s) [attempted 2859/8459 = 33%, 32 KB/s], Decompressed: 2811 Downloaded: 2899 file(s) [attempted 2899/8459 = 34%, 160 KB/s], Decompressed: 2815 Downloaded: 2938 file(s) [attempted 2938/8459 = 34%, 646 KB/s], Decompressed: 2931 Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 1052 KB/s], Decompressed: 2979 Downloaded: 3023 file(s) [attempted 3023/8459 = 35%, 120 KB/s], Decompressed: 3020 Downloaded: 3064 file(s) [attempted 3064/8459 = 36%, 187 KB/s], Decompressed: 3058 Downloaded: 3106 file(s) [attempted 3106/8459 = 36%, 157 KB/s], Decompressed: 3099 Downloaded: 3143 file(s) [attempted 3143/8459 = 37%, 1124 KB/s], Decompressed: 3140 Downloaded: 3184 file(s) [attempted 3184/8459 = 37%, 177 KB/s], Decompressed: 3157 Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 174 KB/s], Decompressed: 3157 Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 2922 KB/s], Decompressed: 3160 Downloaded: 3314 file(s) [attempted 3314/8459 = 39%, 282 KB/s], Decompressed: 3160 Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 228 KB/s], Decompressed: 3349 Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 51 KB/s], Decompressed: 3393 Downloaded: 3441 file(s) [attempted 3441/8459 = 40%, 347 KB/s], Decompressed: 3438 Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 250 KB/s], Decompressed: 3479 Downloaded: 3523 file(s) [attempted 3523/8459 = 41%, 391 KB/s], Decompressed: 3479 Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 122 KB/s], Decompressed: 3479 Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 120 KB/s], Decompressed: 3598 Downloaded: 3646 file(s) [attempted 3646/8459 = 43%, 338 KB/s], Decompressed: 3643 Downloaded: 3691 file(s) [attempted 3691/8459 = 43%, 78 KB/s], Decompressed: 3687 Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 289 KB/s], Decompressed: 3728 Downloaded: 3771 file(s) [attempted 3771/8459 = 44%, 94 KB/s], Decompressed: 3763 Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 361 KB/s], Decompressed: 3800 Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 240 KB/s], Decompressed: 3845 Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 934 KB/s], Decompressed: 3889 Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 930 KB/s], Decompressed: 3934 Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 343 KB/s], Decompressed: 3975 Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 44 KB/s], Decompressed: 3989 Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 453 KB/s], Decompressed: 3989 Downloaded: 4095 file(s) [attempted 4095/8459 = 48%, 36 KB/s], Decompressed: 4091 Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 83 KB/s], Decompressed: 4136 Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 49 KB/s], Decompressed: 4149 Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 310 KB/s], Decompressed: 4149 Downloaded: 4262 file(s) [attempted 4262/8459 = 50%, 425 KB/s], Decompressed: 4242 Downloaded: 4300 file(s) [attempted 4300/8459 = 50%, 115 KB/s], Decompressed: 4262 Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 221 KB/s], Decompressed: 4262 Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 853 KB/s], Decompressed: 4269 Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 471 KB/s], Decompressed: 4269 Downloaded: 4468 file(s) [attempted 4468/8459 = 52%, 365 KB/s], Decompressed: 4464 Downloaded: 4512 file(s) [attempted 4512/8459 = 53%, 277 KB/s], Decompressed: 4505 Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 48 KB/s], Decompressed: 4550 Downloaded: 4594 file(s) [attempted 4594/8459 = 54%, 379 KB/s], Decompressed: 4584 Downloaded: 4632 file(s) [attempted 4632/8459 = 54%, 94 KB/s], Decompressed: 4629 Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 74 KB/s], Decompressed: 4652 Downloaded: 4717 file(s) [attempted 4717/8459 = 55%, 24 KB/s], Decompressed: 4652 Downloaded: 4759 file(s) [attempted 4759/8459 = 56%, 133 KB/s], Decompressed: 4738 Downloaded: 4800 file(s) [attempted 4800/8459 = 56%, 395 KB/s], Decompressed: 4738 Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 1900 KB/s], Decompressed: 4738 Downloaded: 4882 file(s) [attempted 4882/8459 = 57%, 243 KB/s], Decompressed: 4759 Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 407 KB/s], Decompressed: 4759 Downloaded: 4964 file(s) [attempted 4964/8459 = 58%, 88 KB/s], Decompressed: 4848 Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 138 KB/s], Decompressed: 4848 Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 89 KB/s], Decompressed: 4943 Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 330 KB/s], Decompressed: 4943 Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 640 KB/s], Decompressed: 4943 Downloaded: 5176 file(s) [attempted 5176/8459 = 61%, 110 KB/s], Decompressed: 5039 Downloaded: 5217 file(s) [attempted 5217/8459 = 61%, 102 KB/s], Decompressed: 5039 Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 84 KB/s], Decompressed: 5248 Downloaded: 5292 file(s) [attempted 5292/8459 = 62%, 417 KB/s], Decompressed: 5248 Downloaded: 5330 file(s) [attempted 5330/8459 = 63%, 304 KB/s], Decompressed: 5248 Downloaded: 5375 file(s) [attempted 5375/8459 = 63%, 377 KB/s], Decompressed: 5334 Downloaded: 5412 file(s) [attempted 5412/8459 = 63%, 788 KB/s], Decompressed: 5334 Downloaded: 5457 file(s) [attempted 5457/8459 = 64%, 831 KB/s], Decompressed: 5440 Downloaded: 5494 file(s) [attempted 5494/8459 = 64%, 118 KB/s], Decompressed: 5491 Downloaded: 5535 file(s) [attempted 5535/8459 = 65%, 578 KB/s], Decompressed: 5532 Downloaded: 5577 file(s) [attempted 5577/8459 = 65%, 1424 KB/s], Decompressed: 5549 Downloaded: 5621 file(s) [attempted 5621/8459 = 66%, 336 KB/s], Decompressed: 5549 Downloaded: 5662 file(s) [attempted 5662/8459 = 66%, 1019 KB/s], Decompressed: 5559 Downloaded: 5700 file(s) [attempted 5700/8459 = 67%, 90 KB/s], Decompressed: 5559 Downloaded: 5741 file(s) [attempted 5741/8459 = 67%, 98 KB/s], Decompressed: 5645 Downloaded: 5778 file(s) [attempted 5778/8459 = 68%, 521 KB/s], Decompressed: 5645 Downloaded: 5823 file(s) [attempted 5823/8459 = 68%, 86 KB/s], Decompressed: 5645 Downloaded: 5867 file(s) [attempted 5867/8459 = 69%, 166 KB/s], Decompressed: 5734 Downloaded: 5902 file(s) [attempted 5902/8459 = 69%, 344 KB/s], Decompressed: 5734 Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 309 KB/s], Decompressed: 5929 Downloaded: 5994 file(s) [attempted 5994/8459 = 70%, 625 KB/s], Decompressed: 5980 Downloaded: 6035 file(s) [attempted 6035/8459 = 71%, 1109 KB/s], Decompressed: 5980 Downloaded: 6076 file(s) [attempted 6076/8459 = 71%, 102 KB/s], Decompressed: 5984 Downloaded: 6124 file(s) [attempted 6124/8459 = 72%, 399 KB/s], Decompressed: 6117 Downloaded: 6169 file(s) [attempted 6169/8459 = 72%, 269 KB/s], Decompressed: 6160 Downloaded: 6199 file(s) [attempted 6199/8459 = 73%, 75 KB/s], Decompressed: 6193 Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 103 KB/s], Decompressed: 6237 Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 127 KB/s], Decompressed: 6278 Downloaded: 6329 file(s) [attempted 6329/8459 = 74%, 113 KB/s], Decompressed: 6326 Downloaded: 6374 file(s) [attempted 6374/8459 = 75%, 337 KB/s], Decompressed: 6336 Downloaded: 6412 file(s) [attempted 6412/8459 = 75%, 71 KB/s], Decompressed: 6336 Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 37 KB/s], Decompressed: 6343 Downloaded: 6490 file(s) [attempted 6490/8459 = 76%, 165 KB/s], Decompressed: 6343 Downloaded: 6535 file(s) [attempted 6535/8459 = 77%, 86 KB/s], Decompressed: 6521 Downloaded: 6576 file(s) [attempted 6576/8459 = 77%, 517 KB/s], Decompressed: 6572 Downloaded: 6613 file(s) [attempted 6613/8459 = 78%, 57 KB/s], Decompressed: 6607 Downloaded: 6651 file(s) [attempted 6651/8459 = 78%, 468 KB/s], Decompressed: 6648 Downloaded: 6692 file(s) [attempted 6692/8459 = 79%, 528 KB/s], Decompressed: 6689 Downloaded: 6737 file(s) [attempted 6737/8459 = 79%, 72 KB/s], Decompressed: 6733 Downloaded: 6781 file(s) [attempted 6781/8459 = 80%, 169 KB/s], Decompressed: 6778 Downloaded: 6822 file(s) [attempted 6822/8459 = 80%, 597 KB/s], Decompressed: 6815 Downloaded: 6860 file(s) [attempted 6860/8459 = 81%, 79 KB/s], Decompressed: 6850 Downloaded: 6898 file(s) [attempted 6898/8459 = 81%, 123 KB/s], Decompressed: 6891 Downloaded: 6939 file(s) [attempted 6939/8459 = 82%, 436 KB/s], Decompressed: 6935 Downloaded: 6987 file(s) [attempted 6987/8459 = 82%, 889 KB/s], Decompressed: 6983 Downloaded: 7034 file(s) [attempted 7034/8459 = 83%, 1010 KB/s], Decompressed: 7028 Downloaded: 7082 file(s) [attempted 7082/8459 = 83%, 40 KB/s], Decompressed: 7075 Downloaded: 7123 file(s) [attempted 7123/8459 = 84%, 243 KB/s], Decompressed: 7086 Downloaded: 7164 file(s) [attempted 7164/8459 = 84%, 479 KB/s], Decompressed: 7086 Downloaded: 7202 file(s) [attempted 7202/8459 = 85%, 147 KB/s], Decompressed: 7199 Downloaded: 7243 file(s) [attempted 7243/8459 = 85%, 41 KB/s], Decompressed: 7202 Downloaded: 7284 file(s) [attempted 7284/8459 = 86%, 842 KB/s], Decompressed: 7202 Downloaded: 7325 file(s) [attempted 7325/8459 = 86%, 305 KB/s], Decompressed: 7212 Downloaded: 7370 file(s) [attempted 7370/8459 = 87%, 116 KB/s], Decompressed: 7212 Downloaded: 7407 file(s) [attempted 7407/8459 = 87%, 1122 KB/s], Decompressed: 7295 Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 988 KB/s], Decompressed: 7295 Downloaded: 7493 file(s) [attempted 7493/8459 = 88%, 471 KB/s], Decompressed: 7295 Downloaded: 7537 file(s) [attempted 7537/8459 = 89%, 194 KB/s], Decompressed: 7295 Downloaded: 7579 file(s) [attempted 7579/8459 = 89%, 871 KB/s], Decompressed: 7390 Downloaded: 7616 file(s) [attempted 7616/8459 = 90%, 537 KB/s], Decompressed: 7390 Downloaded: 7657 file(s) [attempted 7657/8459 = 90%, 479 KB/s], Decompressed: 7551 Downloaded: 7702 file(s) [attempted 7702/8459 = 91%, 58 KB/s], Decompressed: 7551 Downloaded: 7739 file(s) [attempted 7739/8459 = 91%, 166 KB/s], Decompressed: 7551 Downloaded: 7780 file(s) [attempted 7780/8459 = 91%, 314 KB/s], Decompressed: 7657 Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 162 KB/s], Decompressed: 7657 Downloaded: 7869 file(s) [attempted 7869/8459 = 93%, 61 KB/s], Decompressed: 7757 Downloaded: 7904 file(s) [attempted 7904/8459 = 93%, 73 KB/s], Decompressed: 7856 Downloaded: 7945 file(s) [attempted 7945/8459 = 93%, 239 KB/s], Decompressed: 7856 Downloaded: 7986 file(s) [attempted 7986/8459 = 94%, 208 KB/s], Decompressed: 7876 Downloaded: 8030 file(s) [attempted 8030/8459 = 94%, 562 KB/s], Decompressed: 7876 Downloaded: 8076 file(s) [attempted 8076/8459 = 95%, 639 KB/s], Decompressed: 7969 Downloaded: 8112 file(s) [attempted 8112/8459 = 95%, 295 KB/s], Decompressed: 8106 Downloaded: 8150 file(s) [attempted 8150/8459 = 96%, 213 KB/s], Decompressed: 8140 Downloaded: 8191 file(s) [attempted 8191/8459 = 96%, 102 KB/s], Decompressed: 8140 Downloaded: 8232 file(s) [attempted 8232/8459 = 97%, 569 KB/s], Decompressed: 8143 Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 756 KB/s], Decompressed: 8232 Downloaded: 8325 file(s) [attempted 8325/8459 = 98%, 183 KB/s], Decompressed: 8232 Downloaded: 8366 file(s) [attempted 8366/8459 = 98%, 406 KB/s], Decompressed: 8253 Downloaded: 8403 file(s) [attempted 8403/8459 = 99%, 607 KB/s], Decompressed: 8253 Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 502 KB/s], Decompressed: 8338 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 502 KB/s], Decompressed: 8451
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (95s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.9s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.7s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.8s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.7s)
✔ [763/772] Built Iut.Foundations.QualitativeData (2.2s)
✔ [3382/3392] Built Iut.Foundations.AlgorithmicOutput (1.8s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (3.1s)
✔ [3389/3394] Built Iut.Stage1.CorollarySchema (114s)
✔ [3390/3397] Built Iut.Stage1.SourceObligations (3.1s)
✔ [3392/3398] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3394/3401] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (117s)
warning: Iut/Stage1/IUTStage1SourceCore.lean:19880:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotient_card_eq_pow_finrank`:
[FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [FiniteDimensional ℚ_[p] K] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20063:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotientCosetHaarCharacterEndpoint`:
[FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [FiniteDimensional ℚ_[p] K] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20130:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.unitBallHaarCharacterEndpoint`:
[FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [FiniteDimensional ℚ_[p] K] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20532:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20533:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20537:4: `have hinteger_eq : (integer : ℚ_[p]) = (p : ℚ_[p]) * (preimage : ℚ_[p]) := by
simpa [IUTStage1PadicIntegerUnitBallSource.padicIntAddEquivIntegerAddSubgroup, hpreimage_eq] using
hpoint_eq.symm` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20547:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20572:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20573:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20576:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20577:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20578:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
✔ [3411/3425] Built Iut.Stage1.IUTStage1Remark312Absorption (59s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (18s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (5.3s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (6.3s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (13s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (10s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (28s)
warning: Iut/Stage1/IUTStage1Theorem311.lean:4518:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4523:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4655:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4687:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4692:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4735:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4789:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4824:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4829:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4961:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4995:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5000:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5138:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5172:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5177:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5320:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5352:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5357:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5470:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:7525:6: try 'simp' instead of 'simpa'
Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15277:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15618:4: try 'simp' instead of 'simpa'
Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:16875:4: try 'simp' instead of 'simpa'
Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:17353:5: unused variable `targetSource`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:18439:5: unused variable `data`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:21472:5: unused variable `obligations`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
✖ [3418/3425] Building Iut.Stage1.IUTStage1StepXI (196s)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean /apx/source/Iut/Stage1/IUTStage1StepXI.lean -o /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI.olean -i /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI.ilean -c /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI.c --setup /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI.setup.json --json
error: Lean exited with code 137
Some required targets logged failures:
- Iut.Stage1.IUTStage1StepXI
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes error: build failed
blueprint_build exit 1
lake build :blueprint
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes error: unknown package facet `blueprint`