Verification run
Run 1071
failed commit
825e75ac440b toolchain lean-v4-30-0 prover lean took 11m 13s · finished 4d 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-1373-source
exit_code=Some(0) duration_ms=3443
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1373-source'...
$ git checkout 825e75ac440b2d03baa53fbe21b4d14ef6b7f33c
exit_code=Some(0) duration_ms=179
stderr:
Note: switching to '825e75ac440b2d03baa53fbe21b4d14ef6b7f33c'.
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 825e75a Construct packet localized CTheta source
Resolved source revision: 825e75ac440b2d03baa53fbe21b4d14ef6b7f33c
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=825e75ac440b2d03baa53fbe21b4d14ef6b7f33c provenance={"branch":"master","checked_out_revision":"825e75ac440b2d03baa53fbe21b4d14ef6b7f33c","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"825e75ac440b2d03baa53fbe21b4d14ef6b7f33c","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=33432
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%, 10 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 2 KB/s], Decompressed: 12
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 16 KB/s], Decompressed: 33
Downloaded: 64 file(s) [attempted 64/8459 = 0%, 47 KB/s], Decompressed: 57
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 407 KB/s], Decompressed: 83
Downloaded: 117 file(s) [attempted 117/8459 = 1%, 140 KB/s], Decompressed: 114
Downloaded: 153 file(s) [attempted 153/8459 = 1%, 179 KB/s], Decompressed: 148
Downloaded: 182 file(s) [attempted 182/8459 = 2%, 530 KB/s], Decompressed: 175
Downloaded: 220 file(s) [attempted 220/8459 = 2%, 339 KB/s], Decompressed: 216
Downloaded: 254 file(s) [attempted 254/8459 = 3%, 439 KB/s], Decompressed: 247
Downloaded: 288 file(s) [attempted 288/8459 = 3%, 83 KB/s], Decompressed: 282
Downloaded: 324 file(s) [attempted 324/8459 = 3%, 345 KB/s], Decompressed: 319
Downloaded: 365 file(s) [attempted 365/8459 = 4%, 1210 KB/s], Decompressed: 360
Downloaded: 398 file(s) [attempted 398/8459 = 4%, 67 KB/s], Decompressed: 395
Downloaded: 433 file(s) [attempted 433/8459 = 5%, 264 KB/s], Decompressed: 429
Downloaded: 469 file(s) [attempted 469/8459 = 5%, 715 KB/s], Decompressed: 463
Downloaded: 508 file(s) [attempted 508/8459 = 6%, 772 KB/s], Decompressed: 504
Downloaded: 546 file(s) [attempted 546/8459 = 6%, 28 KB/s], Decompressed: 542
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 65 KB/s], Decompressed: 583
Downloaded: 626 file(s) [attempted 626/8459 = 7%, 438 KB/s], Decompressed: 617
Downloaded: 665 file(s) [attempted 665/8459 = 7%, 500 KB/s], Decompressed: 662
Downloaded: 703 file(s) [attempted 703/8459 = 8%, 28 KB/s], Decompressed: 693
Downloaded: 741 file(s) [attempted 741/8459 = 8%, 174 KB/s], Decompressed: 737
Downloaded: 782 file(s) [attempted 782/8459 = 9%, 147 KB/s], Decompressed: 775
Downloaded: 819 file(s) [attempted 819/8459 = 9%, 1844 KB/s], Decompressed: 816
Downloaded: 864 file(s) [attempted 864/8459 = 10%, 423 KB/s], Decompressed: 860
Downloaded: 902 file(s) [attempted 902/8459 = 10%, 29 KB/s], Decompressed: 898
Downloaded: 939 file(s) [attempted 939/8459 = 11%, 178 KB/s], Decompressed: 932
Downloaded: 975 file(s) [attempted 975/8459 = 11%, 451 KB/s], Decompressed: 970
Downloaded: 1018 file(s) [attempted 1018/8459 = 12%, 233 KB/s], Decompressed: 1015
Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 41 KB/s], Decompressed: 1059
Downloaded: 1100 file(s) [attempted 1100/8459 = 13%, 237 KB/s], Decompressed: 1083
Downloaded: 1134 file(s) [attempted 1134/8459 = 13%, 283 KB/s], Decompressed: 1127
Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 100 KB/s], Decompressed: 1172
Downloaded: 1213 file(s) [attempted 1213/8459 = 14%, 635 KB/s], Decompressed: 1210
Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 43 KB/s], Decompressed: 1254
Downloaded: 1292 file(s) [attempted 1292/8459 = 15%, 102 KB/s], Decompressed: 1285
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 155 KB/s], Decompressed: 1326
Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 1243 KB/s], Decompressed: 1367
Downloaded: 1406 file(s) [attempted 1406/8459 = 16%, 346 KB/s], Decompressed: 1401
Downloaded: 1446 file(s) [attempted 1446/8459 = 17%, 175 KB/s], Decompressed: 1439
Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 129 KB/s], Decompressed: 1480
Downloaded: 1529 file(s) [attempted 1529/8459 = 18%, 26 KB/s], Decompressed: 1524
Downloaded: 1566 file(s) [attempted 1566/8459 = 18%, 1023 KB/s], Decompressed: 1562
Downloaded: 1603 file(s) [attempted 1603/8459 = 18%, 1052 KB/s], Decompressed: 1600
Downloaded: 1641 file(s) [attempted 1641/8459 = 19%, 654 KB/s], Decompressed: 1637
Downloaded: 1682 file(s) [attempted 1682/8459 = 19%, 346 KB/s], Decompressed: 1675
Downloaded: 1718 file(s) [attempted 1718/8459 = 20%, 296 KB/s], Decompressed: 1713
Downloaded: 1757 file(s) [attempted 1757/8459 = 20%, 441 KB/s], Decompressed: 1754
Downloaded: 1795 file(s) [attempted 1795/8459 = 21%, 34 KB/s], Decompressed: 1791
Downloaded: 1838 file(s) [attempted 1838/8459 = 21%, 481 KB/s], Decompressed: 1832
Downloaded: 1874 file(s) [attempted 1874/8459 = 22%, 435 KB/s], Decompressed: 1870
Downloaded: 1915 file(s) [attempted 1915/8459 = 22%, 498 KB/s], Decompressed: 1911
Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 746 KB/s], Decompressed: 1945
Downloaded: 1990 file(s) [attempted 1990/8459 = 23%, 677 KB/s], Decompressed: 1986
Downloaded: 2034 file(s) [attempted 2034/8459 = 24%, 180 KB/s], Decompressed: 2031
Downloaded: 2082 file(s) [attempted 2082/8459 = 24%, 227 KB/s], Decompressed: 2075
Downloaded: 2127 file(s) [attempted 2127/8459 = 25%, 89 KB/s], Decompressed: 2120
Downloaded: 2163 file(s) [attempted 2163/8459 = 25%, 100 KB/s], Decompressed: 2154
Downloaded: 2195 file(s) [attempted 2195/8459 = 25%, 453 KB/s], Decompressed: 2192
Downloaded: 2236 file(s) [attempted 2236/8459 = 26%, 194 KB/s], Decompressed: 2233
Downloaded: 2277 file(s) [attempted 2277/8459 = 26%, 345 KB/s], Decompressed: 2274
Downloaded: 2318 file(s) [attempted 2318/8459 = 27%, 392 KB/s], Decompressed: 2315
Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 283 KB/s], Decompressed: 2353
Downloaded: 2393 file(s) [attempted 2393/8459 = 28%, 88 KB/s], Decompressed: 2387
Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 577 KB/s], Decompressed: 2425
Downloaded: 2472 file(s) [attempted 2472/8459 = 29%, 213 KB/s], Decompressed: 2469
Downloaded: 2520 file(s) [attempted 2520/8459 = 29%, 80 KB/s], Decompressed: 2517
Downloaded: 2568 file(s) [attempted 2568/8459 = 30%, 728 KB/s], Decompressed: 2565
Downloaded: 2609 file(s) [attempted 2609/8459 = 30%, 119 KB/s], Decompressed: 2585
Downloaded: 2649 file(s) [attempted 2649/8459 = 31%, 147 KB/s], Decompressed: 2640
Downloaded: 2685 file(s) [attempted 2685/8459 = 31%, 359 KB/s], Decompressed: 2674
Downloaded: 2724 file(s) [attempted 2724/8459 = 32%, 409 KB/s], Decompressed: 2715
Downloaded: 2764 file(s) [attempted 2764/8459 = 32%, 445 KB/s], Decompressed: 2760
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 673 KB/s], Decompressed: 2801
Downloaded: 2846 file(s) [attempted 2846/8459 = 33%, 75 KB/s], Decompressed: 2835
Downloaded: 2884 file(s) [attempted 2884/8459 = 34%, 182 KB/s], Decompressed: 2873
Downloaded: 2924 file(s) [attempted 2924/8459 = 34%, 227 KB/s], Decompressed: 2921
Downloaded: 2965 file(s) [attempted 2965/8459 = 35%, 142 KB/s], Decompressed: 2958
Downloaded: 3000 file(s) [attempted 3000/8459 = 35%, 316 KB/s], Decompressed: 2996
Downloaded: 3041 file(s) [attempted 3041/8459 = 35%, 223 KB/s], Decompressed: 3037
Downloaded: 3085 file(s) [attempted 3085/8459 = 36%, 518 KB/s], Decompressed: 3078
Downloaded: 3125 file(s) [attempted 3125/8459 = 36%, 878 KB/s], Decompressed: 3119
Downloaded: 3164 file(s) [attempted 3164/8459 = 37%, 327 KB/s], Decompressed: 3157
Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 25 KB/s], Decompressed: 3191
Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 282 KB/s], Decompressed: 3232
Downloaded: 3277 file(s) [attempted 3277/8459 = 38%, 242 KB/s], Decompressed: 3273
Downloaded: 3320 file(s) [attempted 3320/8459 = 39%, 40 KB/s], Decompressed: 3311
Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 51 KB/s], Decompressed: 3349
Downloaded: 3397 file(s) [attempted 3397/8459 = 40%, 74 KB/s], Decompressed: 3390
Downloaded: 3434 file(s) [attempted 3434/8459 = 40%, 107 KB/s], Decompressed: 3427
Downloaded: 3469 file(s) [attempted 3469/8459 = 41%, 398 KB/s], Decompressed: 3465
Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 65 KB/s], Decompressed: 3506
Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 139 KB/s], Decompressed: 3550
Downloaded: 3592 file(s) [attempted 3592/8459 = 42%, 75 KB/s], Decompressed: 3588
Downloaded: 3626 file(s) [attempted 3626/8459 = 42%, 223 KB/s], Decompressed: 3619
Downloaded: 3667 file(s) [attempted 3667/8459 = 43%, 104 KB/s], Decompressed: 3663
Downloaded: 3706 file(s) [attempted 3706/8459 = 43%, 180 KB/s], Decompressed: 3701
Downloaded: 3746 file(s) [attempted 3746/8459 = 44%, 232 KB/s], Decompressed: 3735
Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 352 KB/s], Decompressed: 3780
Downloaded: 3817 file(s) [attempted 3817/8459 = 45%, 1010 KB/s], Decompressed: 3811
Downloaded: 3862 file(s) [attempted 3862/8459 = 45%, 816 KB/s], Decompressed: 3859
Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 159 KB/s], Decompressed: 3900
Downloaded: 3948 file(s) [attempted 3948/8459 = 46%, 429 KB/s], Decompressed: 3944
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 275 KB/s], Decompressed: 3975
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 243 KB/s], Decompressed: 4013
Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 4122 KB/s], Decompressed: 4054
Downloaded: 4105 file(s) [attempted 4105/8459 = 48%, 442 KB/s], Decompressed: 4102
Downloaded: 4148 file(s) [attempted 4148/8459 = 49%, 104 KB/s], Decompressed: 4145
Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 449 KB/s], Decompressed: 4177
Downloaded: 4218 file(s) [attempted 4218/8459 = 49%, 403 KB/s], Decompressed: 4214
Downloaded: 4259 file(s) [attempted 4259/8459 = 50%, 303 KB/s], Decompressed: 4256
Downloaded: 4301 file(s) [attempted 4301/8459 = 50%, 215 KB/s], Decompressed: 4297
Downloaded: 4338 file(s) [attempted 4338/8459 = 51%, 144 KB/s], Decompressed: 4334
Downloaded: 4375 file(s) [attempted 4375/8459 = 51%, 173 KB/s], Decompressed: 4372
Downloaded: 4413 file(s) [attempted 4413/8459 = 52%, 102 KB/s], Decompressed: 4410
Downloaded: 4455 file(s) [attempted 4455/8459 = 52%, 864 KB/s], Decompressed: 4451
Downloaded: 4498 file(s) [attempted 4498/8459 = 53%, 942 KB/s], Decompressed: 4488
Downloaded: 4536 file(s) [attempted 4536/8459 = 53%, 190 KB/s], Decompressed: 4522
Downloaded: 4570 file(s) [attempted 4570/8459 = 54%, 120 KB/s], Decompressed: 4567
Downloaded: 4611 file(s) [attempted 4611/8459 = 54%, 2296 KB/s], Decompressed: 4605
Downloaded: 4653 file(s) [attempted 4653/8459 = 55%, 170 KB/s], Decompressed: 4649
Downloaded: 4694 file(s) [attempted 4694/8459 = 55%, 126 KB/s], Decompressed: 4690
Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 94 KB/s], Decompressed: 4735
Downloaded: 4776 file(s) [attempted 4776/8459 = 56%, 562 KB/s], Decompressed: 4765
Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 206 KB/s], Decompressed: 4807
Downloaded: 4858 file(s) [attempted 4858/8459 = 57%, 313 KB/s], Decompressed: 4851
Downloaded: 4895 file(s) [attempted 4895/8459 = 57%, 399 KB/s], Decompressed: 4889
Downloaded: 4940 file(s) [attempted 4940/8459 = 58%, 616 KB/s], Decompressed: 4933
Downloaded: 4981 file(s) [attempted 4981/8459 = 58%, 187 KB/s], Decompressed: 4978
Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 412 KB/s], Decompressed: 5015
Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 56 KB/s], Decompressed: 5053
Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 319 KB/s], Decompressed: 5091
Downloaded: 5142 file(s) [attempted 5142/8459 = 60%, 100 KB/s], Decompressed: 5139
Downloaded: 5183 file(s) [attempted 5183/8459 = 61%, 97 KB/s], Decompressed: 5176
Downloaded: 5221 file(s) [attempted 5221/8459 = 61%, 56 KB/s], Decompressed: 5214
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 128 KB/s], Decompressed: 5255
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 55 KB/s], Decompressed: 5296
Downloaded: 5340 file(s) [attempted 5340/8459 = 63%, 157 KB/s], Decompressed: 5337
Downloaded: 5381 file(s) [attempted 5381/8459 = 63%, 874 KB/s], Decompressed: 5375
Downloaded: 5416 file(s) [attempted 5416/8459 = 64%, 28 KB/s], Decompressed: 5405
Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 337 KB/s], Decompressed: 5450
Downloaded: 5498 file(s) [attempted 5498/8459 = 64%, 66 KB/s], Decompressed: 5494
Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 279 KB/s], Decompressed: 5536
Downloaded: 5583 file(s) [attempted 5583/8459 = 66%, 334 KB/s], Decompressed: 5580
Downloaded: 5625 file(s) [attempted 5625/8459 = 66%, 332 KB/s], Decompressed: 5618
Downloaded: 5661 file(s) [attempted 5661/8459 = 66%, 2594 KB/s], Decompressed: 5648
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 122 KB/s], Decompressed: 5693
Downloaded: 5741 file(s) [attempted 5741/8459 = 67%, 41 KB/s], Decompressed: 5737
Downloaded: 5776 file(s) [attempted 5776/8459 = 68%, 720 KB/s], Decompressed: 5768
Downloaded: 5810 file(s) [attempted 5810/8459 = 68%, 484 KB/s], Decompressed: 5802
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 116 KB/s], Decompressed: 5844
Downloaded: 5898 file(s) [attempted 5898/8459 = 69%, 807 KB/s], Decompressed: 5891
Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 647 KB/s], Decompressed: 5943
Downloaded: 5987 file(s) [attempted 5987/8459 = 70%, 558 KB/s], Decompressed: 5980
Downloaded: 6023 file(s) [attempted 6023/8459 = 71%, 271 KB/s], Decompressed: 6018
Downloaded: 6063 file(s) [attempted 6063/8459 = 71%, 164 KB/s], Decompressed: 6056
Downloaded: 6100 file(s) [attempted 6100/8459 = 72%, 613 KB/s], Decompressed: 6097
Downloaded: 6145 file(s) [attempted 6145/8459 = 72%, 67 KB/s], Decompressed: 6138
Downloaded: 6186 file(s) [attempted 6186/8459 = 73%, 184 KB/s], Decompressed: 6182
Downloaded: 6224 file(s) [attempted 6224/8459 = 73%, 286 KB/s], Decompressed: 6220
Downloaded: 6262 file(s) [attempted 6262/8459 = 74%, 190 KB/s], Decompressed: 6258
Downloaded: 6300 file(s) [attempted 6300/8459 = 74%, 681 KB/s], Decompressed: 6297
Downloaded: 6338 file(s) [attempted 6338/8459 = 74%, 2983 KB/s], Decompressed: 6329
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 180 KB/s], Decompressed: 6371
Downloaded: 6418 file(s) [attempted 6418/8459 = 75%, 25 KB/s], Decompressed: 6398
Downloaded: 6460 file(s) [attempted 6460/8459 = 76%, 301 KB/s], Decompressed: 6456
Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 570 KB/s], Decompressed: 6490
Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 527 KB/s], Decompressed: 6531
Downloaded: 6576 file(s) [attempted 6576/8459 = 77%, 99 KB/s], Decompressed: 6572
Downloaded: 6614 file(s) [attempted 6614/8459 = 78%, 589 KB/s], Decompressed: 6610
Downloaded: 6658 file(s) [attempted 6658/8459 = 78%, 996 KB/s], Decompressed: 6655
Downloaded: 6696 file(s) [attempted 6696/8459 = 79%, 1428 KB/s], Decompressed: 6692
Downloaded: 6740 file(s) [attempted 6740/8459 = 79%, 760 KB/s], Decompressed: 6733
Downloaded: 6781 file(s) [attempted 6781/8459 = 80%, 84 KB/s], Decompressed: 6778
Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 237 KB/s], Decompressed: 6815
Downloaded: 6857 file(s) [attempted 6857/8459 = 81%, 277 KB/s], Decompressed: 6846
Downloaded: 6894 file(s) [attempted 6894/8459 = 81%, 198 KB/s], Decompressed: 6887
Downloaded: 6939 file(s) [attempted 6939/8459 = 82%, 260 KB/s], Decompressed: 6935
Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 633 KB/s], Decompressed: 6966
Downloaded: 7014 file(s) [attempted 7014/8459 = 82%, 281 KB/s], Decompressed: 7007
Downloaded: 7054 file(s) [attempted 7054/8459 = 83%, 235 KB/s], Decompressed: 7048
Downloaded: 7096 file(s) [attempted 7096/8459 = 83%, 79 KB/s], Decompressed: 7093
Downloaded: 7137 file(s) [attempted 7137/8459 = 84%, 77 KB/s], Decompressed: 7134
Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 39 KB/s], Decompressed: 7168
Downloaded: 7212 file(s) [attempted 7212/8459 = 85%, 665 KB/s], Decompressed: 7206
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 35 KB/s], Decompressed: 7243
Downloaded: 7291 file(s) [attempted 7291/8459 = 86%, 401 KB/s], Decompressed: 7284
Downloaded: 7329 file(s) [attempted 7329/8459 = 86%, 404 KB/s], Decompressed: 7322
Downloaded: 7370 file(s) [attempted 7370/8459 = 87%, 257 KB/s], Decompressed: 7363
Downloaded: 7401 file(s) [attempted 7401/8459 = 87%, 42 KB/s], Decompressed: 7390
Downloaded: 7442 file(s) [attempted 7442/8459 = 87%, 121 KB/s], Decompressed: 7438
Downloaded: 7486 file(s) [attempted 7486/8459 = 88%, 140 KB/s], Decompressed: 7479
Downloaded: 7528 file(s) [attempted 7528/8459 = 88%, 183 KB/s], Decompressed: 7517
Downloaded: 7569 file(s) [attempted 7569/8459 = 89%, 221 KB/s], Decompressed: 7558
Downloaded: 7603 file(s) [attempted 7603/8459 = 89%, 287 KB/s], Decompressed: 7599
Downloaded: 7646 file(s) [attempted 7646/8459 = 90%, 298 KB/s], Decompressed: 7640
Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 49 KB/s], Decompressed: 7682
Downloaded: 7726 file(s) [attempted 7726/8459 = 91%, 3758 KB/s], Decompressed: 7719
Downloaded: 7764 file(s) [attempted 7764/8459 = 91%, 294 KB/s], Decompressed: 7753
Downloaded: 7801 file(s) [attempted 7801/8459 = 92%, 582 KB/s], Decompressed: 7798
Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 1040 KB/s], Decompressed: 7839
Downloaded: 7882 file(s) [attempted 7882/8459 = 93%, 415 KB/s], Decompressed: 7873
Downloaded: 7918 file(s) [attempted 7918/8459 = 93%, 171 KB/s], Decompressed: 7914
Downloaded: 7959 file(s) [attempted 7959/8459 = 94%, 809 KB/s], Decompressed: 7952
Downloaded: 7996 file(s) [attempted 7996/8459 = 94%, 275 KB/s], Decompressed: 7966
Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 101 KB/s], Decompressed: 8034
Downloaded: 8075 file(s) [attempted 8075/8459 = 95%, 643 KB/s], Decompressed: 8068
Downloaded: 8116 file(s) [attempted 8116/8459 = 95%, 366 KB/s], Decompressed: 8109
Downloaded: 8157 file(s) [attempted 8157/8459 = 96%, 113 KB/s], Decompressed: 8154
Downloaded: 8195 file(s) [attempted 8195/8459 = 96%, 339 KB/s], Decompressed: 8191
Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 498 KB/s], Decompressed: 8229
Downloaded: 8276 file(s) [attempted 8276/8459 = 97%, 266 KB/s], Decompressed: 8260
Downloaded: 8315 file(s) [attempted 8315/8459 = 98%, 51 KB/s], Decompressed: 8291
Downloaded: 8349 file(s) [attempted 8349/8459 = 98%, 141 KB/s], Decompressed: 8339
Downloaded: 8386 file(s) [attempted 8386/8459 = 99%, 52 KB/s], Decompressed: 8380
Downloaded: 8431 file(s) [attempted 8431/8459 = 99%, 204 KB/s], Decompressed: 8428
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 113 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 113 KB/s], Decompressed: 8455
$ lake build
exit_code=Some(1) duration_ms=451022
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (24s)
✔ [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.4s)
✔ [763/775] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.5s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.5s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (36s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.0s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3394/3425] Built Iut.Stage1.IUTStage1Data (3.2s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (83s)
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 (21s)
⚠ [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.6s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.1s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.2s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.2s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (24s)
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 (169s)
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=1077
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-1373-source
Cloning into '/var/lib/apodeixis/repos/job-1373-source'...
git_checkout exit 0
git checkout 825e75ac440b2d03baa53fbe21b4d14ef6b7f33c
Note: switching to '825e75ac440b2d03baa53fbe21b4d14ef6b7f33c'. 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 825e75a Construct packet localized CTheta source
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%, 10 KB/s], Decompressed: 0 Downloaded: 15 file(s) [attempted 15/8459 = 0%, 2 KB/s], Decompressed: 12 Downloaded: 38 file(s) [attempted 38/8459 = 0%, 16 KB/s], Decompressed: 33 Downloaded: 64 file(s) [attempted 64/8459 = 0%, 47 KB/s], Decompressed: 57 Downloaded: 86 file(s) [attempted 86/8459 = 1%, 407 KB/s], Decompressed: 83 Downloaded: 117 file(s) [attempted 117/8459 = 1%, 140 KB/s], Decompressed: 114 Downloaded: 153 file(s) [attempted 153/8459 = 1%, 179 KB/s], Decompressed: 148 Downloaded: 182 file(s) [attempted 182/8459 = 2%, 530 KB/s], Decompressed: 175 Downloaded: 220 file(s) [attempted 220/8459 = 2%, 339 KB/s], Decompressed: 216 Downloaded: 254 file(s) [attempted 254/8459 = 3%, 439 KB/s], Decompressed: 247 Downloaded: 288 file(s) [attempted 288/8459 = 3%, 83 KB/s], Decompressed: 282 Downloaded: 324 file(s) [attempted 324/8459 = 3%, 345 KB/s], Decompressed: 319 Downloaded: 365 file(s) [attempted 365/8459 = 4%, 1210 KB/s], Decompressed: 360 Downloaded: 398 file(s) [attempted 398/8459 = 4%, 67 KB/s], Decompressed: 395 Downloaded: 433 file(s) [attempted 433/8459 = 5%, 264 KB/s], Decompressed: 429 Downloaded: 469 file(s) [attempted 469/8459 = 5%, 715 KB/s], Decompressed: 463 Downloaded: 508 file(s) [attempted 508/8459 = 6%, 772 KB/s], Decompressed: 504 Downloaded: 546 file(s) [attempted 546/8459 = 6%, 28 KB/s], Decompressed: 542 Downloaded: 586 file(s) [attempted 586/8459 = 6%, 65 KB/s], Decompressed: 583 Downloaded: 626 file(s) [attempted 626/8459 = 7%, 438 KB/s], Decompressed: 617 Downloaded: 665 file(s) [attempted 665/8459 = 7%, 500 KB/s], Decompressed: 662 Downloaded: 703 file(s) [attempted 703/8459 = 8%, 28 KB/s], Decompressed: 693 Downloaded: 741 file(s) [attempted 741/8459 = 8%, 174 KB/s], Decompressed: 737 Downloaded: 782 file(s) [attempted 782/8459 = 9%, 147 KB/s], Decompressed: 775 Downloaded: 819 file(s) [attempted 819/8459 = 9%, 1844 KB/s], Decompressed: 816 Downloaded: 864 file(s) [attempted 864/8459 = 10%, 423 KB/s], Decompressed: 860 Downloaded: 902 file(s) [attempted 902/8459 = 10%, 29 KB/s], Decompressed: 898 Downloaded: 939 file(s) [attempted 939/8459 = 11%, 178 KB/s], Decompressed: 932 Downloaded: 975 file(s) [attempted 975/8459 = 11%, 451 KB/s], Decompressed: 970 Downloaded: 1018 file(s) [attempted 1018/8459 = 12%, 233 KB/s], Decompressed: 1015 Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 41 KB/s], Decompressed: 1059 Downloaded: 1100 file(s) [attempted 1100/8459 = 13%, 237 KB/s], Decompressed: 1083 Downloaded: 1134 file(s) [attempted 1134/8459 = 13%, 283 KB/s], Decompressed: 1127 Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 100 KB/s], Decompressed: 1172 Downloaded: 1213 file(s) [attempted 1213/8459 = 14%, 635 KB/s], Decompressed: 1210 Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 43 KB/s], Decompressed: 1254 Downloaded: 1292 file(s) [attempted 1292/8459 = 15%, 102 KB/s], Decompressed: 1285 Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 155 KB/s], Decompressed: 1326 Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 1243 KB/s], Decompressed: 1367 Downloaded: 1406 file(s) [attempted 1406/8459 = 16%, 346 KB/s], Decompressed: 1401 Downloaded: 1446 file(s) [attempted 1446/8459 = 17%, 175 KB/s], Decompressed: 1439 Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 129 KB/s], Decompressed: 1480 Downloaded: 1529 file(s) [attempted 1529/8459 = 18%, 26 KB/s], Decompressed: 1524 Downloaded: 1566 file(s) [attempted 1566/8459 = 18%, 1023 KB/s], Decompressed: 1562 Downloaded: 1603 file(s) [attempted 1603/8459 = 18%, 1052 KB/s], Decompressed: 1600 Downloaded: 1641 file(s) [attempted 1641/8459 = 19%, 654 KB/s], Decompressed: 1637 Downloaded: 1682 file(s) [attempted 1682/8459 = 19%, 346 KB/s], Decompressed: 1675 Downloaded: 1718 file(s) [attempted 1718/8459 = 20%, 296 KB/s], Decompressed: 1713 Downloaded: 1757 file(s) [attempted 1757/8459 = 20%, 441 KB/s], Decompressed: 1754 Downloaded: 1795 file(s) [attempted 1795/8459 = 21%, 34 KB/s], Decompressed: 1791 Downloaded: 1838 file(s) [attempted 1838/8459 = 21%, 481 KB/s], Decompressed: 1832 Downloaded: 1874 file(s) [attempted 1874/8459 = 22%, 435 KB/s], Decompressed: 1870 Downloaded: 1915 file(s) [attempted 1915/8459 = 22%, 498 KB/s], Decompressed: 1911 Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 746 KB/s], Decompressed: 1945 Downloaded: 1990 file(s) [attempted 1990/8459 = 23%, 677 KB/s], Decompressed: 1986 Downloaded: 2034 file(s) [attempted 2034/8459 = 24%, 180 KB/s], Decompressed: 2031 Downloaded: 2082 file(s) [attempted 2082/8459 = 24%, 227 KB/s], Decompressed: 2075 Downloaded: 2127 file(s) [attempted 2127/8459 = 25%, 89 KB/s], Decompressed: 2120 Downloaded: 2163 file(s) [attempted 2163/8459 = 25%, 100 KB/s], Decompressed: 2154 Downloaded: 2195 file(s) [attempted 2195/8459 = 25%, 453 KB/s], Decompressed: 2192 Downloaded: 2236 file(s) [attempted 2236/8459 = 26%, 194 KB/s], Decompressed: 2233 Downloaded: 2277 file(s) [attempted 2277/8459 = 26%, 345 KB/s], Decompressed: 2274 Downloaded: 2318 file(s) [attempted 2318/8459 = 27%, 392 KB/s], Decompressed: 2315 Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 283 KB/s], Decompressed: 2353 Downloaded: 2393 file(s) [attempted 2393/8459 = 28%, 88 KB/s], Decompressed: 2387 Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 577 KB/s], Decompressed: 2425 Downloaded: 2472 file(s) [attempted 2472/8459 = 29%, 213 KB/s], Decompressed: 2469 Downloaded: 2520 file(s) [attempted 2520/8459 = 29%, 80 KB/s], Decompressed: 2517 Downloaded: 2568 file(s) [attempted 2568/8459 = 30%, 728 KB/s], Decompressed: 2565 Downloaded: 2609 file(s) [attempted 2609/8459 = 30%, 119 KB/s], Decompressed: 2585 Downloaded: 2649 file(s) [attempted 2649/8459 = 31%, 147 KB/s], Decompressed: 2640 Downloaded: 2685 file(s) [attempted 2685/8459 = 31%, 359 KB/s], Decompressed: 2674 Downloaded: 2724 file(s) [attempted 2724/8459 = 32%, 409 KB/s], Decompressed: 2715 Downloaded: 2764 file(s) [attempted 2764/8459 = 32%, 445 KB/s], Decompressed: 2760 Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 673 KB/s], Decompressed: 2801 Downloaded: 2846 file(s) [attempted 2846/8459 = 33%, 75 KB/s], Decompressed: 2835 Downloaded: 2884 file(s) [attempted 2884/8459 = 34%, 182 KB/s], Decompressed: 2873 Downloaded: 2924 file(s) [attempted 2924/8459 = 34%, 227 KB/s], Decompressed: 2921 Downloaded: 2965 file(s) [attempted 2965/8459 = 35%, 142 KB/s], Decompressed: 2958 Downloaded: 3000 file(s) [attempted 3000/8459 = 35%, 316 KB/s], Decompressed: 2996 Downloaded: 3041 file(s) [attempted 3041/8459 = 35%, 223 KB/s], Decompressed: 3037 Downloaded: 3085 file(s) [attempted 3085/8459 = 36%, 518 KB/s], Decompressed: 3078 Downloaded: 3125 file(s) [attempted 3125/8459 = 36%, 878 KB/s], Decompressed: 3119 Downloaded: 3164 file(s) [attempted 3164/8459 = 37%, 327 KB/s], Decompressed: 3157 Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 25 KB/s], Decompressed: 3191 Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 282 KB/s], Decompressed: 3232 Downloaded: 3277 file(s) [attempted 3277/8459 = 38%, 242 KB/s], Decompressed: 3273 Downloaded: 3320 file(s) [attempted 3320/8459 = 39%, 40 KB/s], Decompressed: 3311 Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 51 KB/s], Decompressed: 3349 Downloaded: 3397 file(s) [attempted 3397/8459 = 40%, 74 KB/s], Decompressed: 3390 Downloaded: 3434 file(s) [attempted 3434/8459 = 40%, 107 KB/s], Decompressed: 3427 Downloaded: 3469 file(s) [attempted 3469/8459 = 41%, 398 KB/s], Decompressed: 3465 Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 65 KB/s], Decompressed: 3506 Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 139 KB/s], Decompressed: 3550 Downloaded: 3592 file(s) [attempted 3592/8459 = 42%, 75 KB/s], Decompressed: 3588 Downloaded: 3626 file(s) [attempted 3626/8459 = 42%, 223 KB/s], Decompressed: 3619 Downloaded: 3667 file(s) [attempted 3667/8459 = 43%, 104 KB/s], Decompressed: 3663 Downloaded: 3706 file(s) [attempted 3706/8459 = 43%, 180 KB/s], Decompressed: 3701 Downloaded: 3746 file(s) [attempted 3746/8459 = 44%, 232 KB/s], Decompressed: 3735 Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 352 KB/s], Decompressed: 3780 Downloaded: 3817 file(s) [attempted 3817/8459 = 45%, 1010 KB/s], Decompressed: 3811 Downloaded: 3862 file(s) [attempted 3862/8459 = 45%, 816 KB/s], Decompressed: 3859 Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 159 KB/s], Decompressed: 3900 Downloaded: 3948 file(s) [attempted 3948/8459 = 46%, 429 KB/s], Decompressed: 3944 Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 275 KB/s], Decompressed: 3975 Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 243 KB/s], Decompressed: 4013 Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 4122 KB/s], Decompressed: 4054 Downloaded: 4105 file(s) [attempted 4105/8459 = 48%, 442 KB/s], Decompressed: 4102 Downloaded: 4148 file(s) [attempted 4148/8459 = 49%, 104 KB/s], Decompressed: 4145 Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 449 KB/s], Decompressed: 4177 Downloaded: 4218 file(s) [attempted 4218/8459 = 49%, 403 KB/s], Decompressed: 4214 Downloaded: 4259 file(s) [attempted 4259/8459 = 50%, 303 KB/s], Decompressed: 4256 Downloaded: 4301 file(s) [attempted 4301/8459 = 50%, 215 KB/s], Decompressed: 4297 Downloaded: 4338 file(s) [attempted 4338/8459 = 51%, 144 KB/s], Decompressed: 4334 Downloaded: 4375 file(s) [attempted 4375/8459 = 51%, 173 KB/s], Decompressed: 4372 Downloaded: 4413 file(s) [attempted 4413/8459 = 52%, 102 KB/s], Decompressed: 4410 Downloaded: 4455 file(s) [attempted 4455/8459 = 52%, 864 KB/s], Decompressed: 4451 Downloaded: 4498 file(s) [attempted 4498/8459 = 53%, 942 KB/s], Decompressed: 4488 Downloaded: 4536 file(s) [attempted 4536/8459 = 53%, 190 KB/s], Decompressed: 4522 Downloaded: 4570 file(s) [attempted 4570/8459 = 54%, 120 KB/s], Decompressed: 4567 Downloaded: 4611 file(s) [attempted 4611/8459 = 54%, 2296 KB/s], Decompressed: 4605 Downloaded: 4653 file(s) [attempted 4653/8459 = 55%, 170 KB/s], Decompressed: 4649 Downloaded: 4694 file(s) [attempted 4694/8459 = 55%, 126 KB/s], Decompressed: 4690 Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 94 KB/s], Decompressed: 4735 Downloaded: 4776 file(s) [attempted 4776/8459 = 56%, 562 KB/s], Decompressed: 4765 Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 206 KB/s], Decompressed: 4807 Downloaded: 4858 file(s) [attempted 4858/8459 = 57%, 313 KB/s], Decompressed: 4851 Downloaded: 4895 file(s) [attempted 4895/8459 = 57%, 399 KB/s], Decompressed: 4889 Downloaded: 4940 file(s) [attempted 4940/8459 = 58%, 616 KB/s], Decompressed: 4933 Downloaded: 4981 file(s) [attempted 4981/8459 = 58%, 187 KB/s], Decompressed: 4978 Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 412 KB/s], Decompressed: 5015 Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 56 KB/s], Decompressed: 5053 Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 319 KB/s], Decompressed: 5091 Downloaded: 5142 file(s) [attempted 5142/8459 = 60%, 100 KB/s], Decompressed: 5139 Downloaded: 5183 file(s) [attempted 5183/8459 = 61%, 97 KB/s], Decompressed: 5176 Downloaded: 5221 file(s) [attempted 5221/8459 = 61%, 56 KB/s], Decompressed: 5214 Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 128 KB/s], Decompressed: 5255 Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 55 KB/s], Decompressed: 5296 Downloaded: 5340 file(s) [attempted 5340/8459 = 63%, 157 KB/s], Decompressed: 5337 Downloaded: 5381 file(s) [attempted 5381/8459 = 63%, 874 KB/s], Decompressed: 5375 Downloaded: 5416 file(s) [attempted 5416/8459 = 64%, 28 KB/s], Decompressed: 5405 Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 337 KB/s], Decompressed: 5450 Downloaded: 5498 file(s) [attempted 5498/8459 = 64%, 66 KB/s], Decompressed: 5494 Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 279 KB/s], Decompressed: 5536 Downloaded: 5583 file(s) [attempted 5583/8459 = 66%, 334 KB/s], Decompressed: 5580 Downloaded: 5625 file(s) [attempted 5625/8459 = 66%, 332 KB/s], Decompressed: 5618 Downloaded: 5661 file(s) [attempted 5661/8459 = 66%, 2594 KB/s], Decompressed: 5648 Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 122 KB/s], Decompressed: 5693 Downloaded: 5741 file(s) [attempted 5741/8459 = 67%, 41 KB/s], Decompressed: 5737 Downloaded: 5776 file(s) [attempted 5776/8459 = 68%, 720 KB/s], Decompressed: 5768 Downloaded: 5810 file(s) [attempted 5810/8459 = 68%, 484 KB/s], Decompressed: 5802 Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 116 KB/s], Decompressed: 5844 Downloaded: 5898 file(s) [attempted 5898/8459 = 69%, 807 KB/s], Decompressed: 5891 Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 647 KB/s], Decompressed: 5943 Downloaded: 5987 file(s) [attempted 5987/8459 = 70%, 558 KB/s], Decompressed: 5980 Downloaded: 6023 file(s) [attempted 6023/8459 = 71%, 271 KB/s], Decompressed: 6018 Downloaded: 6063 file(s) [attempted 6063/8459 = 71%, 164 KB/s], Decompressed: 6056 Downloaded: 6100 file(s) [attempted 6100/8459 = 72%, 613 KB/s], Decompressed: 6097 Downloaded: 6145 file(s) [attempted 6145/8459 = 72%, 67 KB/s], Decompressed: 6138 Downloaded: 6186 file(s) [attempted 6186/8459 = 73%, 184 KB/s], Decompressed: 6182 Downloaded: 6224 file(s) [attempted 6224/8459 = 73%, 286 KB/s], Decompressed: 6220 Downloaded: 6262 file(s) [attempted 6262/8459 = 74%, 190 KB/s], Decompressed: 6258 Downloaded: 6300 file(s) [attempted 6300/8459 = 74%, 681 KB/s], Decompressed: 6297 Downloaded: 6338 file(s) [attempted 6338/8459 = 74%, 2983 KB/s], Decompressed: 6329 Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 180 KB/s], Decompressed: 6371 Downloaded: 6418 file(s) [attempted 6418/8459 = 75%, 25 KB/s], Decompressed: 6398 Downloaded: 6460 file(s) [attempted 6460/8459 = 76%, 301 KB/s], Decompressed: 6456 Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 570 KB/s], Decompressed: 6490 Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 527 KB/s], Decompressed: 6531 Downloaded: 6576 file(s) [attempted 6576/8459 = 77%, 99 KB/s], Decompressed: 6572 Downloaded: 6614 file(s) [attempted 6614/8459 = 78%, 589 KB/s], Decompressed: 6610 Downloaded: 6658 file(s) [attempted 6658/8459 = 78%, 996 KB/s], Decompressed: 6655 Downloaded: 6696 file(s) [attempted 6696/8459 = 79%, 1428 KB/s], Decompressed: 6692 Downloaded: 6740 file(s) [attempted 6740/8459 = 79%, 760 KB/s], Decompressed: 6733 Downloaded: 6781 file(s) [attempted 6781/8459 = 80%, 84 KB/s], Decompressed: 6778 Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 237 KB/s], Decompressed: 6815 Downloaded: 6857 file(s) [attempted 6857/8459 = 81%, 277 KB/s], Decompressed: 6846 Downloaded: 6894 file(s) [attempted 6894/8459 = 81%, 198 KB/s], Decompressed: 6887 Downloaded: 6939 file(s) [attempted 6939/8459 = 82%, 260 KB/s], Decompressed: 6935 Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 633 KB/s], Decompressed: 6966 Downloaded: 7014 file(s) [attempted 7014/8459 = 82%, 281 KB/s], Decompressed: 7007 Downloaded: 7054 file(s) [attempted 7054/8459 = 83%, 235 KB/s], Decompressed: 7048 Downloaded: 7096 file(s) [attempted 7096/8459 = 83%, 79 KB/s], Decompressed: 7093 Downloaded: 7137 file(s) [attempted 7137/8459 = 84%, 77 KB/s], Decompressed: 7134 Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 39 KB/s], Decompressed: 7168 Downloaded: 7212 file(s) [attempted 7212/8459 = 85%, 665 KB/s], Decompressed: 7206 Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 35 KB/s], Decompressed: 7243 Downloaded: 7291 file(s) [attempted 7291/8459 = 86%, 401 KB/s], Decompressed: 7284 Downloaded: 7329 file(s) [attempted 7329/8459 = 86%, 404 KB/s], Decompressed: 7322 Downloaded: 7370 file(s) [attempted 7370/8459 = 87%, 257 KB/s], Decompressed: 7363 Downloaded: 7401 file(s) [attempted 7401/8459 = 87%, 42 KB/s], Decompressed: 7390 Downloaded: 7442 file(s) [attempted 7442/8459 = 87%, 121 KB/s], Decompressed: 7438 Downloaded: 7486 file(s) [attempted 7486/8459 = 88%, 140 KB/s], Decompressed: 7479 Downloaded: 7528 file(s) [attempted 7528/8459 = 88%, 183 KB/s], Decompressed: 7517 Downloaded: 7569 file(s) [attempted 7569/8459 = 89%, 221 KB/s], Decompressed: 7558 Downloaded: 7603 file(s) [attempted 7603/8459 = 89%, 287 KB/s], Decompressed: 7599 Downloaded: 7646 file(s) [attempted 7646/8459 = 90%, 298 KB/s], Decompressed: 7640 Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 49 KB/s], Decompressed: 7682 Downloaded: 7726 file(s) [attempted 7726/8459 = 91%, 3758 KB/s], Decompressed: 7719 Downloaded: 7764 file(s) [attempted 7764/8459 = 91%, 294 KB/s], Decompressed: 7753 Downloaded: 7801 file(s) [attempted 7801/8459 = 92%, 582 KB/s], Decompressed: 7798 Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 1040 KB/s], Decompressed: 7839 Downloaded: 7882 file(s) [attempted 7882/8459 = 93%, 415 KB/s], Decompressed: 7873 Downloaded: 7918 file(s) [attempted 7918/8459 = 93%, 171 KB/s], Decompressed: 7914 Downloaded: 7959 file(s) [attempted 7959/8459 = 94%, 809 KB/s], Decompressed: 7952 Downloaded: 7996 file(s) [attempted 7996/8459 = 94%, 275 KB/s], Decompressed: 7966 Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 101 KB/s], Decompressed: 8034 Downloaded: 8075 file(s) [attempted 8075/8459 = 95%, 643 KB/s], Decompressed: 8068 Downloaded: 8116 file(s) [attempted 8116/8459 = 95%, 366 KB/s], Decompressed: 8109 Downloaded: 8157 file(s) [attempted 8157/8459 = 96%, 113 KB/s], Decompressed: 8154 Downloaded: 8195 file(s) [attempted 8195/8459 = 96%, 339 KB/s], Decompressed: 8191 Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 498 KB/s], Decompressed: 8229 Downloaded: 8276 file(s) [attempted 8276/8459 = 97%, 266 KB/s], Decompressed: 8260 Downloaded: 8315 file(s) [attempted 8315/8459 = 98%, 51 KB/s], Decompressed: 8291 Downloaded: 8349 file(s) [attempted 8349/8459 = 98%, 141 KB/s], Decompressed: 8339 Downloaded: 8386 file(s) [attempted 8386/8459 = 99%, 52 KB/s], Decompressed: 8380 Downloaded: 8431 file(s) [attempted 8431/8459 = 99%, 204 KB/s], Decompressed: 8428 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 113 KB/s], Decompressed: 8455 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 113 KB/s], Decompressed: 8455
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (24s)
✔ [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.4s)
✔ [763/775] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.5s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.5s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (36s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.0s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3394/3425] Built Iut.Stage1.IUTStage1Data (3.2s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (83s)
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 (21s)
⚠ [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.6s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.1s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.2s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.2s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (24s)
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 (169s)
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`