Verification run
Run 1065
failed commit
ffe579a7e996 toolchain lean-v4-30-0 prover lean took 22m 56s · 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-1366-source
exit_code=Some(0) duration_ms=3551
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1366-source'...
$ git checkout ffe579a7e99607374558c3c22a3644da1c7456ba
exit_code=Some(0) duration_ms=178
stderr:
Note: switching to 'ffe579a7e99607374558c3c22a3644da1c7456ba'.
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 ffe579a Lower current product hull formula gap surface
Resolved source revision: ffe579a7e99607374558c3c22a3644da1c7456ba
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=ffe579a7e99607374558c3c22a3644da1c7456ba provenance={"branch":"master","checked_out_revision":"ffe579a7e99607374558c3c22a3644da1c7456ba","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"ffe579a7e99607374558c3c22a3644da1c7456ba","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=39313
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%, 12 KB/s], Decompressed: 0
Downloaded: 17 file(s) [attempted 17/8459 = 0%, 9 KB/s], Decompressed: 16
Downloaded: 42 file(s) [attempted 42/8459 = 0%, 123 KB/s], Decompressed: 38
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 54 KB/s], Decompressed: 46
Downloaded: 93 file(s) [attempted 93/8459 = 1%, 76 KB/s], Decompressed: 46
Downloaded: 127 file(s) [attempted 127/8459 = 1%, 247 KB/s], Decompressed: 117
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 95 KB/s], Decompressed: 117
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 163 KB/s], Decompressed: 124
Downloaded: 240 file(s) [attempted 240/8459 = 2%, 727 KB/s], Decompressed: 234
Downloaded: 278 file(s) [attempted 278/8459 = 3%, 635 KB/s], Decompressed: 268
Downloaded: 313 file(s) [attempted 313/8459 = 3%, 692 KB/s], Decompressed: 306
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 210 KB/s], Decompressed: 343
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 188 KB/s], Decompressed: 377
Downloaded: 425 file(s) [attempted 425/8459 = 5%, 139 KB/s], Decompressed: 422
Downloaded: 466 file(s) [attempted 466/8459 = 5%, 321 KB/s], Decompressed: 463
Downloaded: 506 file(s) [attempted 506/8459 = 5%, 809 KB/s], Decompressed: 501
Downloaded: 545 file(s) [attempted 545/8459 = 6%, 64 KB/s], Decompressed: 521
Downloaded: 583 file(s) [attempted 583/8459 = 6%, 186 KB/s], Decompressed: 521
Downloaded: 623 file(s) [attempted 623/8459 = 7%, 312 KB/s], Decompressed: 528
Downloaded: 660 file(s) [attempted 660/8459 = 7%, 83 KB/s], Decompressed: 655
Downloaded: 703 file(s) [attempted 703/8459 = 8%, 283 KB/s], Decompressed: 699
Downloaded: 744 file(s) [attempted 744/8459 = 8%, 435 KB/s], Decompressed: 737
Downloaded: 782 file(s) [attempted 782/8459 = 9%, 156 KB/s], Decompressed: 775
Downloaded: 819 file(s) [attempted 819/8459 = 9%, 135 KB/s], Decompressed: 816
Downloaded: 860 file(s) [attempted 860/8459 = 10%, 444 KB/s], Decompressed: 830
Downloaded: 905 file(s) [attempted 905/8459 = 10%, 46 KB/s], Decompressed: 830
Downloaded: 946 file(s) [attempted 946/8459 = 11%, 60 KB/s], Decompressed: 919
Downloaded: 987 file(s) [attempted 987/8459 = 11%, 69 KB/s], Decompressed: 919
Downloaded: 1025 file(s) [attempted 1025/8459 = 12%, 299 KB/s], Decompressed: 939
Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 141 KB/s], Decompressed: 1056
Downloaded: 1104 file(s) [attempted 1104/8459 = 13%, 609 KB/s], Decompressed: 1100
Downloaded: 1143 file(s) [attempted 1143/8459 = 13%, 156 KB/s], Decompressed: 1134
Downloaded: 1180 file(s) [attempted 1180/8459 = 13%, 353 KB/s], Decompressed: 1175
Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 375 KB/s], Decompressed: 1213
Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 202 KB/s], Decompressed: 1247
Downloaded: 1296 file(s) [attempted 1296/8459 = 15%, 746 KB/s], Decompressed: 1292
Downloaded: 1337 file(s) [attempted 1337/8459 = 15%, 948 KB/s], Decompressed: 1333
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 30 KB/s], Decompressed: 1374
Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 103 KB/s], Decompressed: 1409
Downloaded: 1453 file(s) [attempted 1453/8459 = 17%, 347 KB/s], Decompressed: 1442
Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 60 KB/s], Decompressed: 1483
Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 119 KB/s], Decompressed: 1514
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 544 KB/s], Decompressed: 1514
Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 391 KB/s], Decompressed: 1521
Downloaded: 1645 file(s) [attempted 1645/8459 = 19%, 49 KB/s], Decompressed: 1596
Downloaded: 1685 file(s) [attempted 1685/8459 = 19%, 340 KB/s], Decompressed: 1596
Downloaded: 1726 file(s) [attempted 1726/8459 = 20%, 1660 KB/s], Decompressed: 1617
Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 80 KB/s], Decompressed: 1617
Downloaded: 1812 file(s) [attempted 1812/8459 = 21%, 59 KB/s], Decompressed: 1692
Downloaded: 1846 file(s) [attempted 1846/8459 = 21%, 641 KB/s], Decompressed: 1692
Downloaded: 1880 file(s) [attempted 1880/8459 = 22%, 3355 KB/s], Decompressed: 1781
Downloaded: 1920 file(s) [attempted 1920/8459 = 22%, 120 KB/s], Decompressed: 1781
Downloaded: 1956 file(s) [attempted 1956/8459 = 23%, 169 KB/s], Decompressed: 1867
Downloaded: 1997 file(s) [attempted 1997/8459 = 23%, 104 KB/s], Decompressed: 1867
Downloaded: 2038 file(s) [attempted 2038/8459 = 24%, 399 KB/s], Decompressed: 1867
Downloaded: 2072 file(s) [attempted 2072/8459 = 24%, 2084 KB/s], Decompressed: 1867
Downloaded: 2110 file(s) [attempted 2110/8459 = 24%, 2141 KB/s], Decompressed: 2103
Downloaded: 2147 file(s) [attempted 2147/8459 = 25%, 109 KB/s], Decompressed: 2144
Downloaded: 2185 file(s) [attempted 2185/8459 = 25%, 479 KB/s], Decompressed: 2182
Downloaded: 2220 file(s) [attempted 2220/8459 = 26%, 263 KB/s], Decompressed: 2216
Downloaded: 2260 file(s) [attempted 2260/8459 = 26%, 102 KB/s], Decompressed: 2243
Downloaded: 2291 file(s) [attempted 2291/8459 = 27%, 28 KB/s], Decompressed: 2288
Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 48 KB/s], Decompressed: 2329
Downloaded: 2373 file(s) [attempted 2373/8459 = 28%, 590 KB/s], Decompressed: 2366
Downloaded: 2407 file(s) [attempted 2407/8459 = 28%, 121 KB/s], Decompressed: 2401
Downloaded: 2445 file(s) [attempted 2445/8459 = 28%, 61 KB/s], Decompressed: 2431
Downloaded: 2483 file(s) [attempted 2483/8459 = 29%, 31 KB/s], Decompressed: 2448
Downloaded: 2524 file(s) [attempted 2524/8459 = 29%, 106 KB/s], Decompressed: 2448
Downloaded: 2565 file(s) [attempted 2565/8459 = 30%, 32 KB/s], Decompressed: 2455
Downloaded: 2603 file(s) [attempted 2603/8459 = 30%, 250 KB/s], Decompressed: 2455
Downloaded: 2640 file(s) [attempted 2640/8459 = 31%, 707 KB/s], Decompressed: 2534
Downloaded: 2678 file(s) [attempted 2678/8459 = 31%, 402 KB/s], Decompressed: 2534
Downloaded: 2722 file(s) [attempted 2722/8459 = 32%, 1178 KB/s], Decompressed: 2623
Downloaded: 2763 file(s) [attempted 2763/8459 = 32%, 598 KB/s], Decompressed: 2736
Downloaded: 2801 file(s) [attempted 2801/8459 = 33%, 146 KB/s], Decompressed: 2736
Downloaded: 2839 file(s) [attempted 2839/8459 = 33%, 104 KB/s], Decompressed: 2835
Downloaded: 2881 file(s) [attempted 2881/8459 = 34%, 124 KB/s], Decompressed: 2873
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 662 KB/s], Decompressed: 2914
Downloaded: 2962 file(s) [attempted 2962/8459 = 35%, 221 KB/s], Decompressed: 2921
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 334 KB/s], Decompressed: 2921
Downloaded: 3037 file(s) [attempted 3037/8459 = 35%, 163 KB/s], Decompressed: 3034
Downloaded: 3080 file(s) [attempted 3080/8459 = 36%, 34 KB/s], Decompressed: 3075
Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 390 KB/s], Decompressed: 3109
Downloaded: 3153 file(s) [attempted 3153/8459 = 37%, 78 KB/s], Decompressed: 3130
Downloaded: 3191 file(s) [attempted 3191/8459 = 37%, 227 KB/s], Decompressed: 3130
Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 153 KB/s], Decompressed: 3130
Downloaded: 3278 file(s) [attempted 3278/8459 = 38%, 322 KB/s], Decompressed: 3236
Downloaded: 3314 file(s) [attempted 3314/8459 = 39%, 284 KB/s], Decompressed: 3236
Downloaded: 3359 file(s) [attempted 3359/8459 = 39%, 48 KB/s], Decompressed: 3352
Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 529 KB/s], Decompressed: 3390
Downloaded: 3434 file(s) [attempted 3434/8459 = 40%, 108 KB/s], Decompressed: 3427
Downloaded: 3475 file(s) [attempted 3475/8459 = 41%, 331 KB/s], Decompressed: 3427
Downloaded: 3516 file(s) [attempted 3516/8459 = 41%, 125 KB/s], Decompressed: 3427
Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 89 KB/s], Decompressed: 3434
Downloaded: 3592 file(s) [attempted 3592/8459 = 42%, 33 KB/s], Decompressed: 3434
Downloaded: 3631 file(s) [attempted 3631/8459 = 42%, 240 KB/s], Decompressed: 3622
Downloaded: 3667 file(s) [attempted 3667/8459 = 43%, 99 KB/s], Decompressed: 3660
Downloaded: 3704 file(s) [attempted 3704/8459 = 43%, 36 KB/s], Decompressed: 3687
Downloaded: 3735 file(s) [attempted 3735/8459 = 44%, 368 KB/s], Decompressed: 3732
Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 192 KB/s], Decompressed: 3780
Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 454 KB/s], Decompressed: 3824
Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 232 KB/s], Decompressed: 3824
Downloaded: 3910 file(s) [attempted 3910/8459 = 46%, 146 KB/s], Decompressed: 3828
Downloaded: 3948 file(s) [attempted 3948/8459 = 46%, 215 KB/s], Decompressed: 3937
Downloaded: 3985 file(s) [attempted 3985/8459 = 47%, 332 KB/s], Decompressed: 3979
Downloaded: 4026 file(s) [attempted 4026/8459 = 47%, 104 KB/s], Decompressed: 4023
Downloaded: 4061 file(s) [attempted 4061/8459 = 48%, 296 KB/s], Decompressed: 4047
Downloaded: 4095 file(s) [attempted 4095/8459 = 48%, 1398 KB/s], Decompressed: 4091
Downloaded: 4146 file(s) [attempted 4146/8459 = 49%, 67 KB/s], Decompressed: 4143
Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 2051 KB/s], Decompressed: 4187
Downloaded: 4242 file(s) [attempted 4242/8459 = 50%, 346 KB/s], Decompressed: 4235
Downloaded: 4290 file(s) [attempted 4290/8459 = 50%, 130 KB/s], Decompressed: 4276
Downloaded: 4328 file(s) [attempted 4328/8459 = 51%, 101 KB/s], Decompressed: 4276
Downloaded: 4365 file(s) [attempted 4365/8459 = 51%, 389 KB/s], Decompressed: 4280
Downloaded: 4407 file(s) [attempted 4407/8459 = 52%, 649 KB/s], Decompressed: 4396
Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 53 KB/s], Decompressed: 4437
Downloaded: 4492 file(s) [attempted 4492/8459 = 53%, 394 KB/s], Decompressed: 4485
Downloaded: 4526 file(s) [attempted 4526/8459 = 53%, 332 KB/s], Decompressed: 4523
Downloaded: 4567 file(s) [attempted 4567/8459 = 53%, 35 KB/s], Decompressed: 4564
Downloaded: 4612 file(s) [attempted 4612/8459 = 54%, 291 KB/s], Decompressed: 4608
Downloaded: 4650 file(s) [attempted 4650/8459 = 54%, 361 KB/s], Decompressed: 4646
Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 352 KB/s], Decompressed: 4684
Downloaded: 4728 file(s) [attempted 4728/8459 = 55%, 384 KB/s], Decompressed: 4721
Downloaded: 4766 file(s) [attempted 4766/8459 = 56%, 31 KB/s], Decompressed: 4759
Downloaded: 4810 file(s) [attempted 4810/8459 = 56%, 197 KB/s], Decompressed: 4807
Downloaded: 4858 file(s) [attempted 4858/8459 = 57%, 1498 KB/s], Decompressed: 4855
Downloaded: 4893 file(s) [attempted 4893/8459 = 57%, 464 KB/s], Decompressed: 4889
Downloaded: 4934 file(s) [attempted 4934/8459 = 58%, 267 KB/s], Decompressed: 4920
Downloaded: 4975 file(s) [attempted 4975/8459 = 58%, 488 KB/s], Decompressed: 4920
Downloaded: 5012 file(s) [attempted 5012/8459 = 59%, 85 KB/s], Decompressed: 4927
Downloaded: 5054 file(s) [attempted 5054/8459 = 59%, 372 KB/s], Decompressed: 5047
Downloaded: 5091 file(s) [attempted 5091/8459 = 60%, 819 KB/s], Decompressed: 5057
Downloaded: 5132 file(s) [attempted 5132/8459 = 60%, 69 KB/s], Decompressed: 5057
Downloaded: 5173 file(s) [attempted 5173/8459 = 61%, 111 KB/s], Decompressed: 5146
Downloaded: 5211 file(s) [attempted 5211/8459 = 61%, 538 KB/s], Decompressed: 5207
Downloaded: 5248 file(s) [attempted 5248/8459 = 62%, 422 KB/s], Decompressed: 5245
Downloaded: 5293 file(s) [attempted 5293/8459 = 62%, 144 KB/s], Decompressed: 5279
Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 191 KB/s], Decompressed: 5279
Downloaded: 5378 file(s) [attempted 5378/8459 = 63%, 381 KB/s], Decompressed: 5286
Downloaded: 5423 file(s) [attempted 5423/8459 = 64%, 119 KB/s], Decompressed: 5413
Downloaded: 5457 file(s) [attempted 5457/8459 = 64%, 56 KB/s], Decompressed: 5426
Downloaded: 5498 file(s) [attempted 5498/8459 = 64%, 286 KB/s], Decompressed: 5426
Downloaded: 5539 file(s) [attempted 5539/8459 = 65%, 305 KB/s], Decompressed: 5433
Downloaded: 5587 file(s) [attempted 5587/8459 = 66%, 42 KB/s], Decompressed: 5433
Downloaded: 5632 file(s) [attempted 5632/8459 = 66%, 143 KB/s], Decompressed: 5519
Downloaded: 5669 file(s) [attempted 5669/8459 = 67%, 452 KB/s], Decompressed: 5519
Downloaded: 5704 file(s) [attempted 5704/8459 = 67%, 79 KB/s], Decompressed: 5604
Downloaded: 5741 file(s) [attempted 5741/8459 = 67%, 255 KB/s], Decompressed: 5604
Downloaded: 5786 file(s) [attempted 5786/8459 = 68%, 248 KB/s], Decompressed: 5690
Downloaded: 5830 file(s) [attempted 5830/8459 = 68%, 89 KB/s], Decompressed: 5827
Downloaded: 5871 file(s) [attempted 5871/8459 = 69%, 154 KB/s], Decompressed: 5861
Downloaded: 5909 file(s) [attempted 5909/8459 = 69%, 459 KB/s], Decompressed: 5902
Downloaded: 5950 file(s) [attempted 5950/8459 = 70%, 529 KB/s], Decompressed: 5943
Downloaded: 5988 file(s) [attempted 5988/8459 = 70%, 288 KB/s], Decompressed: 5984
Downloaded: 6032 file(s) [attempted 6032/8459 = 71%, 389 KB/s], Decompressed: 6029
Downloaded: 6077 file(s) [attempted 6077/8459 = 71%, 107 KB/s], Decompressed: 6070
Downloaded: 6109 file(s) [attempted 6109/8459 = 72%, 557 KB/s], Decompressed: 6097
Downloaded: 6148 file(s) [attempted 6148/8459 = 72%, 1223 KB/s], Decompressed: 6097
Downloaded: 6190 file(s) [attempted 6190/8459 = 73%, 461 KB/s], Decompressed: 6107
Downloaded: 6227 file(s) [attempted 6227/8459 = 73%, 143 KB/s], Decompressed: 6107
Downloaded: 6272 file(s) [attempted 6272/8459 = 74%, 106 KB/s], Decompressed: 6107
Downloaded: 6310 file(s) [attempted 6310/8459 = 74%, 201 KB/s], Decompressed: 6303
Downloaded: 6347 file(s) [attempted 6347/8459 = 75%, 389 KB/s], Decompressed: 6340
Downloaded: 6388 file(s) [attempted 6388/8459 = 75%, 134 KB/s], Decompressed: 6382
Downloaded: 6429 file(s) [attempted 6429/8459 = 76%, 154 KB/s], Decompressed: 6422
Downloaded: 6467 file(s) [attempted 6467/8459 = 76%, 278 KB/s], Decompressed: 6463
Downloaded: 6511 file(s) [attempted 6511/8459 = 76%, 112 KB/s], Decompressed: 6491
Downloaded: 6552 file(s) [attempted 6552/8459 = 77%, 108 KB/s], Decompressed: 6491
Downloaded: 6594 file(s) [attempted 6594/8459 = 77%, 59 KB/s], Decompressed: 6580
Downloaded: 6628 file(s) [attempted 6628/8459 = 78%, 298 KB/s], Decompressed: 6580
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 80 KB/s], Decompressed: 6580
Downloaded: 6710 file(s) [attempted 6710/8459 = 79%, 418 KB/s], Decompressed: 6593
Downloaded: 6747 file(s) [attempted 6747/8459 = 79%, 237 KB/s], Decompressed: 6593
Downloaded: 6788 file(s) [attempted 6788/8459 = 80%, 72 KB/s], Decompressed: 6593
Downloaded: 6826 file(s) [attempted 6826/8459 = 80%, 253 KB/s], Decompressed: 6593
Downloaded: 6867 file(s) [attempted 6867/8459 = 81%, 140 KB/s], Decompressed: 6593
Downloaded: 6908 file(s) [attempted 6908/8459 = 81%, 26 KB/s], Decompressed: 6593
Downloaded: 6946 file(s) [attempted 6946/8459 = 82%, 36 KB/s], Decompressed: 6669
Downloaded: 6987 file(s) [attempted 6987/8459 = 82%, 157 KB/s], Decompressed: 6932
Downloaded: 7028 file(s) [attempted 7028/8459 = 83%, 465 KB/s], Decompressed: 7021
Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 1213 KB/s], Decompressed: 7062
Downloaded: 7107 file(s) [attempted 7107/8459 = 84%, 718 KB/s], Decompressed: 7097
Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 1185 KB/s], Decompressed: 7141
Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 1277 KB/s], Decompressed: 7141
Downloaded: 7230 file(s) [attempted 7230/8459 = 85%, 941 KB/s], Decompressed: 7141
Downloaded: 7272 file(s) [attempted 7272/8459 = 85%, 620 KB/s], Decompressed: 7264
Downloaded: 7306 file(s) [attempted 7306/8459 = 86%, 140 KB/s], Decompressed: 7298
Downloaded: 7344 file(s) [attempted 7344/8459 = 86%, 534 KB/s], Decompressed: 7298
Downloaded: 7384 file(s) [attempted 7384/8459 = 87%, 565 KB/s], Decompressed: 7298
Downloaded: 7425 file(s) [attempted 7425/8459 = 87%, 102 KB/s], Decompressed: 7418
Downloaded: 7459 file(s) [attempted 7459/8459 = 88%, 87 KB/s], Decompressed: 7452
Downloaded: 7496 file(s) [attempted 7496/8459 = 88%, 97 KB/s], Decompressed: 7490
Downloaded: 7535 file(s) [attempted 7535/8459 = 89%, 219 KB/s], Decompressed: 7524
Downloaded: 7579 file(s) [attempted 7579/8459 = 89%, 223 KB/s], Decompressed: 7541
Downloaded: 7617 file(s) [attempted 7617/8459 = 90%, 524 KB/s], Decompressed: 7541
Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 465 KB/s], Decompressed: 7545
Downloaded: 7689 file(s) [attempted 7689/8459 = 90%, 994 KB/s], Decompressed: 7685
Downloaded: 7730 file(s) [attempted 7730/8459 = 91%, 102 KB/s], Decompressed: 7726
Downloaded: 7771 file(s) [attempted 7771/8459 = 91%, 172 KB/s], Decompressed: 7767
Downloaded: 7812 file(s) [attempted 7812/8459 = 92%, 22 KB/s], Decompressed: 7778
Downloaded: 7856 file(s) [attempted 7856/8459 = 92%, 23 KB/s], Decompressed: 7778
Downloaded: 7894 file(s) [attempted 7894/8459 = 93%, 1136 KB/s], Decompressed: 7887
Downloaded: 7932 file(s) [attempted 7932/8459 = 93%, 623 KB/s], Decompressed: 7928
Downloaded: 7969 file(s) [attempted 7969/8459 = 94%, 1960 KB/s], Decompressed: 7962
Downloaded: 8010 file(s) [attempted 8010/8459 = 94%, 252 KB/s], Decompressed: 8007
Downloaded: 8051 file(s) [attempted 8051/8459 = 95%, 61 KB/s], Decompressed: 8048
Downloaded: 8089 file(s) [attempted 8089/8459 = 95%, 185 KB/s], Decompressed: 8084
Downloaded: 8123 file(s) [attempted 8123/8459 = 96%, 594 KB/s], Decompressed: 8120
Downloaded: 8164 file(s) [attempted 8164/8459 = 96%, 24 KB/s], Decompressed: 8161
Downloaded: 8205 file(s) [attempted 8205/8459 = 96%, 411 KB/s], Decompressed: 8202
Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 202 KB/s], Decompressed: 8240
Downloaded: 8281 file(s) [attempted 8281/8459 = 97%, 1037 KB/s], Decompressed: 8270
Downloaded: 8322 file(s) [attempted 8322/8459 = 98%, 184 KB/s], Decompressed: 8315
Downloaded: 8363 file(s) [attempted 8363/8459 = 98%, 128 KB/s], Decompressed: 8359
Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 307 KB/s], Decompressed: 8397
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 73 KB/s], Decompressed: 8438
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 128 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 128 KB/s], Decompressed: 8455
$ lake build
exit_code=Some(1) duration_ms=745111
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (69s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.5s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.6s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.5s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/764] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.5s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.6s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (95s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.0s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.6s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.5s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (113s)
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 (69s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
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 (4.8s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.1s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.4s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.9s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (26s)
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 (240s)
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=2123
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-1366-source
Cloning into '/var/lib/apodeixis/repos/job-1366-source'...
git_checkout exit 0
git checkout ffe579a7e99607374558c3c22a3644da1c7456ba
Note: switching to 'ffe579a7e99607374558c3c22a3644da1c7456ba'. 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 ffe579a Lower current product hull formula gap surface
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%, 12 KB/s], Decompressed: 0 Downloaded: 17 file(s) [attempted 17/8459 = 0%, 9 KB/s], Decompressed: 16 Downloaded: 42 file(s) [attempted 42/8459 = 0%, 123 KB/s], Decompressed: 38 Downloaded: 68 file(s) [attempted 68/8459 = 0%, 54 KB/s], Decompressed: 46 Downloaded: 93 file(s) [attempted 93/8459 = 1%, 76 KB/s], Decompressed: 46 Downloaded: 127 file(s) [attempted 127/8459 = 1%, 247 KB/s], Decompressed: 117 Downloaded: 158 file(s) [attempted 158/8459 = 1%, 95 KB/s], Decompressed: 117 Downloaded: 199 file(s) [attempted 199/8459 = 2%, 163 KB/s], Decompressed: 124 Downloaded: 240 file(s) [attempted 240/8459 = 2%, 727 KB/s], Decompressed: 234 Downloaded: 278 file(s) [attempted 278/8459 = 3%, 635 KB/s], Decompressed: 268 Downloaded: 313 file(s) [attempted 313/8459 = 3%, 692 KB/s], Decompressed: 306 Downloaded: 353 file(s) [attempted 353/8459 = 4%, 210 KB/s], Decompressed: 343 Downloaded: 391 file(s) [attempted 391/8459 = 4%, 188 KB/s], Decompressed: 377 Downloaded: 425 file(s) [attempted 425/8459 = 5%, 139 KB/s], Decompressed: 422 Downloaded: 466 file(s) [attempted 466/8459 = 5%, 321 KB/s], Decompressed: 463 Downloaded: 506 file(s) [attempted 506/8459 = 5%, 809 KB/s], Decompressed: 501 Downloaded: 545 file(s) [attempted 545/8459 = 6%, 64 KB/s], Decompressed: 521 Downloaded: 583 file(s) [attempted 583/8459 = 6%, 186 KB/s], Decompressed: 521 Downloaded: 623 file(s) [attempted 623/8459 = 7%, 312 KB/s], Decompressed: 528 Downloaded: 660 file(s) [attempted 660/8459 = 7%, 83 KB/s], Decompressed: 655 Downloaded: 703 file(s) [attempted 703/8459 = 8%, 283 KB/s], Decompressed: 699 Downloaded: 744 file(s) [attempted 744/8459 = 8%, 435 KB/s], Decompressed: 737 Downloaded: 782 file(s) [attempted 782/8459 = 9%, 156 KB/s], Decompressed: 775 Downloaded: 819 file(s) [attempted 819/8459 = 9%, 135 KB/s], Decompressed: 816 Downloaded: 860 file(s) [attempted 860/8459 = 10%, 444 KB/s], Decompressed: 830 Downloaded: 905 file(s) [attempted 905/8459 = 10%, 46 KB/s], Decompressed: 830 Downloaded: 946 file(s) [attempted 946/8459 = 11%, 60 KB/s], Decompressed: 919 Downloaded: 987 file(s) [attempted 987/8459 = 11%, 69 KB/s], Decompressed: 919 Downloaded: 1025 file(s) [attempted 1025/8459 = 12%, 299 KB/s], Decompressed: 939 Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 141 KB/s], Decompressed: 1056 Downloaded: 1104 file(s) [attempted 1104/8459 = 13%, 609 KB/s], Decompressed: 1100 Downloaded: 1143 file(s) [attempted 1143/8459 = 13%, 156 KB/s], Decompressed: 1134 Downloaded: 1180 file(s) [attempted 1180/8459 = 13%, 353 KB/s], Decompressed: 1175 Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 375 KB/s], Decompressed: 1213 Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 202 KB/s], Decompressed: 1247 Downloaded: 1296 file(s) [attempted 1296/8459 = 15%, 746 KB/s], Decompressed: 1292 Downloaded: 1337 file(s) [attempted 1337/8459 = 15%, 948 KB/s], Decompressed: 1333 Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 30 KB/s], Decompressed: 1374 Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 103 KB/s], Decompressed: 1409 Downloaded: 1453 file(s) [attempted 1453/8459 = 17%, 347 KB/s], Decompressed: 1442 Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 60 KB/s], Decompressed: 1483 Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 119 KB/s], Decompressed: 1514 Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 544 KB/s], Decompressed: 1514 Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 391 KB/s], Decompressed: 1521 Downloaded: 1645 file(s) [attempted 1645/8459 = 19%, 49 KB/s], Decompressed: 1596 Downloaded: 1685 file(s) [attempted 1685/8459 = 19%, 340 KB/s], Decompressed: 1596 Downloaded: 1726 file(s) [attempted 1726/8459 = 20%, 1660 KB/s], Decompressed: 1617 Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 80 KB/s], Decompressed: 1617 Downloaded: 1812 file(s) [attempted 1812/8459 = 21%, 59 KB/s], Decompressed: 1692 Downloaded: 1846 file(s) [attempted 1846/8459 = 21%, 641 KB/s], Decompressed: 1692 Downloaded: 1880 file(s) [attempted 1880/8459 = 22%, 3355 KB/s], Decompressed: 1781 Downloaded: 1920 file(s) [attempted 1920/8459 = 22%, 120 KB/s], Decompressed: 1781 Downloaded: 1956 file(s) [attempted 1956/8459 = 23%, 169 KB/s], Decompressed: 1867 Downloaded: 1997 file(s) [attempted 1997/8459 = 23%, 104 KB/s], Decompressed: 1867 Downloaded: 2038 file(s) [attempted 2038/8459 = 24%, 399 KB/s], Decompressed: 1867 Downloaded: 2072 file(s) [attempted 2072/8459 = 24%, 2084 KB/s], Decompressed: 1867 Downloaded: 2110 file(s) [attempted 2110/8459 = 24%, 2141 KB/s], Decompressed: 2103 Downloaded: 2147 file(s) [attempted 2147/8459 = 25%, 109 KB/s], Decompressed: 2144 Downloaded: 2185 file(s) [attempted 2185/8459 = 25%, 479 KB/s], Decompressed: 2182 Downloaded: 2220 file(s) [attempted 2220/8459 = 26%, 263 KB/s], Decompressed: 2216 Downloaded: 2260 file(s) [attempted 2260/8459 = 26%, 102 KB/s], Decompressed: 2243 Downloaded: 2291 file(s) [attempted 2291/8459 = 27%, 28 KB/s], Decompressed: 2288 Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 48 KB/s], Decompressed: 2329 Downloaded: 2373 file(s) [attempted 2373/8459 = 28%, 590 KB/s], Decompressed: 2366 Downloaded: 2407 file(s) [attempted 2407/8459 = 28%, 121 KB/s], Decompressed: 2401 Downloaded: 2445 file(s) [attempted 2445/8459 = 28%, 61 KB/s], Decompressed: 2431 Downloaded: 2483 file(s) [attempted 2483/8459 = 29%, 31 KB/s], Decompressed: 2448 Downloaded: 2524 file(s) [attempted 2524/8459 = 29%, 106 KB/s], Decompressed: 2448 Downloaded: 2565 file(s) [attempted 2565/8459 = 30%, 32 KB/s], Decompressed: 2455 Downloaded: 2603 file(s) [attempted 2603/8459 = 30%, 250 KB/s], Decompressed: 2455 Downloaded: 2640 file(s) [attempted 2640/8459 = 31%, 707 KB/s], Decompressed: 2534 Downloaded: 2678 file(s) [attempted 2678/8459 = 31%, 402 KB/s], Decompressed: 2534 Downloaded: 2722 file(s) [attempted 2722/8459 = 32%, 1178 KB/s], Decompressed: 2623 Downloaded: 2763 file(s) [attempted 2763/8459 = 32%, 598 KB/s], Decompressed: 2736 Downloaded: 2801 file(s) [attempted 2801/8459 = 33%, 146 KB/s], Decompressed: 2736 Downloaded: 2839 file(s) [attempted 2839/8459 = 33%, 104 KB/s], Decompressed: 2835 Downloaded: 2881 file(s) [attempted 2881/8459 = 34%, 124 KB/s], Decompressed: 2873 Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 662 KB/s], Decompressed: 2914 Downloaded: 2962 file(s) [attempted 2962/8459 = 35%, 221 KB/s], Decompressed: 2921 Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 334 KB/s], Decompressed: 2921 Downloaded: 3037 file(s) [attempted 3037/8459 = 35%, 163 KB/s], Decompressed: 3034 Downloaded: 3080 file(s) [attempted 3080/8459 = 36%, 34 KB/s], Decompressed: 3075 Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 390 KB/s], Decompressed: 3109 Downloaded: 3153 file(s) [attempted 3153/8459 = 37%, 78 KB/s], Decompressed: 3130 Downloaded: 3191 file(s) [attempted 3191/8459 = 37%, 227 KB/s], Decompressed: 3130 Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 153 KB/s], Decompressed: 3130 Downloaded: 3278 file(s) [attempted 3278/8459 = 38%, 322 KB/s], Decompressed: 3236 Downloaded: 3314 file(s) [attempted 3314/8459 = 39%, 284 KB/s], Decompressed: 3236 Downloaded: 3359 file(s) [attempted 3359/8459 = 39%, 48 KB/s], Decompressed: 3352 Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 529 KB/s], Decompressed: 3390 Downloaded: 3434 file(s) [attempted 3434/8459 = 40%, 108 KB/s], Decompressed: 3427 Downloaded: 3475 file(s) [attempted 3475/8459 = 41%, 331 KB/s], Decompressed: 3427 Downloaded: 3516 file(s) [attempted 3516/8459 = 41%, 125 KB/s], Decompressed: 3427 Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 89 KB/s], Decompressed: 3434 Downloaded: 3592 file(s) [attempted 3592/8459 = 42%, 33 KB/s], Decompressed: 3434 Downloaded: 3631 file(s) [attempted 3631/8459 = 42%, 240 KB/s], Decompressed: 3622 Downloaded: 3667 file(s) [attempted 3667/8459 = 43%, 99 KB/s], Decompressed: 3660 Downloaded: 3704 file(s) [attempted 3704/8459 = 43%, 36 KB/s], Decompressed: 3687 Downloaded: 3735 file(s) [attempted 3735/8459 = 44%, 368 KB/s], Decompressed: 3732 Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 192 KB/s], Decompressed: 3780 Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 454 KB/s], Decompressed: 3824 Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 232 KB/s], Decompressed: 3824 Downloaded: 3910 file(s) [attempted 3910/8459 = 46%, 146 KB/s], Decompressed: 3828 Downloaded: 3948 file(s) [attempted 3948/8459 = 46%, 215 KB/s], Decompressed: 3937 Downloaded: 3985 file(s) [attempted 3985/8459 = 47%, 332 KB/s], Decompressed: 3979 Downloaded: 4026 file(s) [attempted 4026/8459 = 47%, 104 KB/s], Decompressed: 4023 Downloaded: 4061 file(s) [attempted 4061/8459 = 48%, 296 KB/s], Decompressed: 4047 Downloaded: 4095 file(s) [attempted 4095/8459 = 48%, 1398 KB/s], Decompressed: 4091 Downloaded: 4146 file(s) [attempted 4146/8459 = 49%, 67 KB/s], Decompressed: 4143 Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 2051 KB/s], Decompressed: 4187 Downloaded: 4242 file(s) [attempted 4242/8459 = 50%, 346 KB/s], Decompressed: 4235 Downloaded: 4290 file(s) [attempted 4290/8459 = 50%, 130 KB/s], Decompressed: 4276 Downloaded: 4328 file(s) [attempted 4328/8459 = 51%, 101 KB/s], Decompressed: 4276 Downloaded: 4365 file(s) [attempted 4365/8459 = 51%, 389 KB/s], Decompressed: 4280 Downloaded: 4407 file(s) [attempted 4407/8459 = 52%, 649 KB/s], Decompressed: 4396 Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 53 KB/s], Decompressed: 4437 Downloaded: 4492 file(s) [attempted 4492/8459 = 53%, 394 KB/s], Decompressed: 4485 Downloaded: 4526 file(s) [attempted 4526/8459 = 53%, 332 KB/s], Decompressed: 4523 Downloaded: 4567 file(s) [attempted 4567/8459 = 53%, 35 KB/s], Decompressed: 4564 Downloaded: 4612 file(s) [attempted 4612/8459 = 54%, 291 KB/s], Decompressed: 4608 Downloaded: 4650 file(s) [attempted 4650/8459 = 54%, 361 KB/s], Decompressed: 4646 Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 352 KB/s], Decompressed: 4684 Downloaded: 4728 file(s) [attempted 4728/8459 = 55%, 384 KB/s], Decompressed: 4721 Downloaded: 4766 file(s) [attempted 4766/8459 = 56%, 31 KB/s], Decompressed: 4759 Downloaded: 4810 file(s) [attempted 4810/8459 = 56%, 197 KB/s], Decompressed: 4807 Downloaded: 4858 file(s) [attempted 4858/8459 = 57%, 1498 KB/s], Decompressed: 4855 Downloaded: 4893 file(s) [attempted 4893/8459 = 57%, 464 KB/s], Decompressed: 4889 Downloaded: 4934 file(s) [attempted 4934/8459 = 58%, 267 KB/s], Decompressed: 4920 Downloaded: 4975 file(s) [attempted 4975/8459 = 58%, 488 KB/s], Decompressed: 4920 Downloaded: 5012 file(s) [attempted 5012/8459 = 59%, 85 KB/s], Decompressed: 4927 Downloaded: 5054 file(s) [attempted 5054/8459 = 59%, 372 KB/s], Decompressed: 5047 Downloaded: 5091 file(s) [attempted 5091/8459 = 60%, 819 KB/s], Decompressed: 5057 Downloaded: 5132 file(s) [attempted 5132/8459 = 60%, 69 KB/s], Decompressed: 5057 Downloaded: 5173 file(s) [attempted 5173/8459 = 61%, 111 KB/s], Decompressed: 5146 Downloaded: 5211 file(s) [attempted 5211/8459 = 61%, 538 KB/s], Decompressed: 5207 Downloaded: 5248 file(s) [attempted 5248/8459 = 62%, 422 KB/s], Decompressed: 5245 Downloaded: 5293 file(s) [attempted 5293/8459 = 62%, 144 KB/s], Decompressed: 5279 Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 191 KB/s], Decompressed: 5279 Downloaded: 5378 file(s) [attempted 5378/8459 = 63%, 381 KB/s], Decompressed: 5286 Downloaded: 5423 file(s) [attempted 5423/8459 = 64%, 119 KB/s], Decompressed: 5413 Downloaded: 5457 file(s) [attempted 5457/8459 = 64%, 56 KB/s], Decompressed: 5426 Downloaded: 5498 file(s) [attempted 5498/8459 = 64%, 286 KB/s], Decompressed: 5426 Downloaded: 5539 file(s) [attempted 5539/8459 = 65%, 305 KB/s], Decompressed: 5433 Downloaded: 5587 file(s) [attempted 5587/8459 = 66%, 42 KB/s], Decompressed: 5433 Downloaded: 5632 file(s) [attempted 5632/8459 = 66%, 143 KB/s], Decompressed: 5519 Downloaded: 5669 file(s) [attempted 5669/8459 = 67%, 452 KB/s], Decompressed: 5519 Downloaded: 5704 file(s) [attempted 5704/8459 = 67%, 79 KB/s], Decompressed: 5604 Downloaded: 5741 file(s) [attempted 5741/8459 = 67%, 255 KB/s], Decompressed: 5604 Downloaded: 5786 file(s) [attempted 5786/8459 = 68%, 248 KB/s], Decompressed: 5690 Downloaded: 5830 file(s) [attempted 5830/8459 = 68%, 89 KB/s], Decompressed: 5827 Downloaded: 5871 file(s) [attempted 5871/8459 = 69%, 154 KB/s], Decompressed: 5861 Downloaded: 5909 file(s) [attempted 5909/8459 = 69%, 459 KB/s], Decompressed: 5902 Downloaded: 5950 file(s) [attempted 5950/8459 = 70%, 529 KB/s], Decompressed: 5943 Downloaded: 5988 file(s) [attempted 5988/8459 = 70%, 288 KB/s], Decompressed: 5984 Downloaded: 6032 file(s) [attempted 6032/8459 = 71%, 389 KB/s], Decompressed: 6029 Downloaded: 6077 file(s) [attempted 6077/8459 = 71%, 107 KB/s], Decompressed: 6070 Downloaded: 6109 file(s) [attempted 6109/8459 = 72%, 557 KB/s], Decompressed: 6097 Downloaded: 6148 file(s) [attempted 6148/8459 = 72%, 1223 KB/s], Decompressed: 6097 Downloaded: 6190 file(s) [attempted 6190/8459 = 73%, 461 KB/s], Decompressed: 6107 Downloaded: 6227 file(s) [attempted 6227/8459 = 73%, 143 KB/s], Decompressed: 6107 Downloaded: 6272 file(s) [attempted 6272/8459 = 74%, 106 KB/s], Decompressed: 6107 Downloaded: 6310 file(s) [attempted 6310/8459 = 74%, 201 KB/s], Decompressed: 6303 Downloaded: 6347 file(s) [attempted 6347/8459 = 75%, 389 KB/s], Decompressed: 6340 Downloaded: 6388 file(s) [attempted 6388/8459 = 75%, 134 KB/s], Decompressed: 6382 Downloaded: 6429 file(s) [attempted 6429/8459 = 76%, 154 KB/s], Decompressed: 6422 Downloaded: 6467 file(s) [attempted 6467/8459 = 76%, 278 KB/s], Decompressed: 6463 Downloaded: 6511 file(s) [attempted 6511/8459 = 76%, 112 KB/s], Decompressed: 6491 Downloaded: 6552 file(s) [attempted 6552/8459 = 77%, 108 KB/s], Decompressed: 6491 Downloaded: 6594 file(s) [attempted 6594/8459 = 77%, 59 KB/s], Decompressed: 6580 Downloaded: 6628 file(s) [attempted 6628/8459 = 78%, 298 KB/s], Decompressed: 6580 Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 80 KB/s], Decompressed: 6580 Downloaded: 6710 file(s) [attempted 6710/8459 = 79%, 418 KB/s], Decompressed: 6593 Downloaded: 6747 file(s) [attempted 6747/8459 = 79%, 237 KB/s], Decompressed: 6593 Downloaded: 6788 file(s) [attempted 6788/8459 = 80%, 72 KB/s], Decompressed: 6593 Downloaded: 6826 file(s) [attempted 6826/8459 = 80%, 253 KB/s], Decompressed: 6593 Downloaded: 6867 file(s) [attempted 6867/8459 = 81%, 140 KB/s], Decompressed: 6593 Downloaded: 6908 file(s) [attempted 6908/8459 = 81%, 26 KB/s], Decompressed: 6593 Downloaded: 6946 file(s) [attempted 6946/8459 = 82%, 36 KB/s], Decompressed: 6669 Downloaded: 6987 file(s) [attempted 6987/8459 = 82%, 157 KB/s], Decompressed: 6932 Downloaded: 7028 file(s) [attempted 7028/8459 = 83%, 465 KB/s], Decompressed: 7021 Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 1213 KB/s], Decompressed: 7062 Downloaded: 7107 file(s) [attempted 7107/8459 = 84%, 718 KB/s], Decompressed: 7097 Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 1185 KB/s], Decompressed: 7141 Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 1277 KB/s], Decompressed: 7141 Downloaded: 7230 file(s) [attempted 7230/8459 = 85%, 941 KB/s], Decompressed: 7141 Downloaded: 7272 file(s) [attempted 7272/8459 = 85%, 620 KB/s], Decompressed: 7264 Downloaded: 7306 file(s) [attempted 7306/8459 = 86%, 140 KB/s], Decompressed: 7298 Downloaded: 7344 file(s) [attempted 7344/8459 = 86%, 534 KB/s], Decompressed: 7298 Downloaded: 7384 file(s) [attempted 7384/8459 = 87%, 565 KB/s], Decompressed: 7298 Downloaded: 7425 file(s) [attempted 7425/8459 = 87%, 102 KB/s], Decompressed: 7418 Downloaded: 7459 file(s) [attempted 7459/8459 = 88%, 87 KB/s], Decompressed: 7452 Downloaded: 7496 file(s) [attempted 7496/8459 = 88%, 97 KB/s], Decompressed: 7490 Downloaded: 7535 file(s) [attempted 7535/8459 = 89%, 219 KB/s], Decompressed: 7524 Downloaded: 7579 file(s) [attempted 7579/8459 = 89%, 223 KB/s], Decompressed: 7541 Downloaded: 7617 file(s) [attempted 7617/8459 = 90%, 524 KB/s], Decompressed: 7541 Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 465 KB/s], Decompressed: 7545 Downloaded: 7689 file(s) [attempted 7689/8459 = 90%, 994 KB/s], Decompressed: 7685 Downloaded: 7730 file(s) [attempted 7730/8459 = 91%, 102 KB/s], Decompressed: 7726 Downloaded: 7771 file(s) [attempted 7771/8459 = 91%, 172 KB/s], Decompressed: 7767 Downloaded: 7812 file(s) [attempted 7812/8459 = 92%, 22 KB/s], Decompressed: 7778 Downloaded: 7856 file(s) [attempted 7856/8459 = 92%, 23 KB/s], Decompressed: 7778 Downloaded: 7894 file(s) [attempted 7894/8459 = 93%, 1136 KB/s], Decompressed: 7887 Downloaded: 7932 file(s) [attempted 7932/8459 = 93%, 623 KB/s], Decompressed: 7928 Downloaded: 7969 file(s) [attempted 7969/8459 = 94%, 1960 KB/s], Decompressed: 7962 Downloaded: 8010 file(s) [attempted 8010/8459 = 94%, 252 KB/s], Decompressed: 8007 Downloaded: 8051 file(s) [attempted 8051/8459 = 95%, 61 KB/s], Decompressed: 8048 Downloaded: 8089 file(s) [attempted 8089/8459 = 95%, 185 KB/s], Decompressed: 8084 Downloaded: 8123 file(s) [attempted 8123/8459 = 96%, 594 KB/s], Decompressed: 8120 Downloaded: 8164 file(s) [attempted 8164/8459 = 96%, 24 KB/s], Decompressed: 8161 Downloaded: 8205 file(s) [attempted 8205/8459 = 96%, 411 KB/s], Decompressed: 8202 Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 202 KB/s], Decompressed: 8240 Downloaded: 8281 file(s) [attempted 8281/8459 = 97%, 1037 KB/s], Decompressed: 8270 Downloaded: 8322 file(s) [attempted 8322/8459 = 98%, 184 KB/s], Decompressed: 8315 Downloaded: 8363 file(s) [attempted 8363/8459 = 98%, 128 KB/s], Decompressed: 8359 Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 307 KB/s], Decompressed: 8397 Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 73 KB/s], Decompressed: 8438 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 128 KB/s], Decompressed: 8455 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 128 KB/s], Decompressed: 8455
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (69s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.5s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.6s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.5s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/764] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.5s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.6s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (95s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.0s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.6s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.5s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (113s)
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 (69s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
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 (4.8s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.1s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.4s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.9s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (26s)
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 (240s)
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`