Verification run
Run 1058
failed commit
6beb21db0f1b toolchain lean-v4-30-0 prover lean took 11m 39s · 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-1358-source
exit_code=Some(0) duration_ms=3590
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1358-source'...
$ git checkout 6beb21db0f1b60ae3dafd8020c481efbe396d1fd
exit_code=Some(0) duration_ms=175
stderr:
Note: switching to '6beb21db0f1b60ae3dafd8020c481efbe396d1fd'.
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 6beb21d Derive synchronized route inputs
Resolved source revision: 6beb21db0f1b60ae3dafd8020c481efbe396d1fd
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=6beb21db0f1b60ae3dafd8020c481efbe396d1fd provenance={"branch":"master","checked_out_revision":"6beb21db0f1b60ae3dafd8020c481efbe396d1fd","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"6beb21db0f1b60ae3dafd8020c481efbe396d1fd","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=54316
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%, 24 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 4 KB/s], Decompressed: 15
Downloaded: 40 file(s) [attempted 40/8459 = 0%, 22 KB/s], Decompressed: 36
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 26 KB/s], Decompressed: 63
Downloaded: 87 file(s) [attempted 87/8459 = 1%, 448 KB/s], Decompressed: 80
Downloaded: 114 file(s) [attempted 114/8459 = 1%, 44 KB/s], Decompressed: 110
Downloaded: 151 file(s) [attempted 151/8459 = 1%, 208 KB/s], Decompressed: 148
Downloaded: 192 file(s) [attempted 192/8459 = 2%, 511 KB/s], Decompressed: 189
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 578 KB/s], Decompressed: 223
Downloaded: 268 file(s) [attempted 268/8459 = 3%, 507 KB/s], Decompressed: 261
Downloaded: 303 file(s) [attempted 303/8459 = 3%, 25 KB/s], Decompressed: 292
Downloaded: 336 file(s) [attempted 336/8459 = 3%, 119 KB/s], Decompressed: 329
Downloaded: 374 file(s) [attempted 374/8459 = 4%, 283 KB/s], Decompressed: 371
Downloaded: 415 file(s) [attempted 415/8459 = 4%, 116 KB/s], Decompressed: 412
Downloaded: 455 file(s) [attempted 455/8459 = 5%, 549 KB/s], Decompressed: 449
Downloaded: 490 file(s) [attempted 490/8459 = 5%, 1394 KB/s], Decompressed: 487
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 173 KB/s], Decompressed: 521
Downloaded: 569 file(s) [attempted 569/8459 = 6%, 161 KB/s], Decompressed: 562
Downloaded: 610 file(s) [attempted 610/8459 = 7%, 449 KB/s], Decompressed: 604
Downloaded: 651 file(s) [attempted 651/8459 = 7%, 327 KB/s], Decompressed: 645
Downloaded: 690 file(s) [attempted 690/8459 = 8%, 75 KB/s], Decompressed: 686
Downloaded: 730 file(s) [attempted 730/8459 = 8%, 492 KB/s], Decompressed: 727
Downloaded: 768 file(s) [attempted 768/8459 = 9%, 830 KB/s], Decompressed: 761
Downloaded: 802 file(s) [attempted 802/8459 = 9%, 124 KB/s], Decompressed: 799
Downloaded: 843 file(s) [attempted 843/8459 = 9%, 205 KB/s], Decompressed: 840
Downloaded: 884 file(s) [attempted 884/8459 = 10%, 43 KB/s], Decompressed: 878
Downloaded: 925 file(s) [attempted 925/8459 = 10%, 1194 KB/s], Decompressed: 922
Downloaded: 963 file(s) [attempted 963/8459 = 11%, 339 KB/s], Decompressed: 956
Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 494 KB/s], Decompressed: 997
Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 200 KB/s], Decompressed: 1035
Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 289 KB/s], Decompressed: 1073
Downloaded: 1117 file(s) [attempted 1117/8459 = 13%, 1481 KB/s], Decompressed: 1114
Downloaded: 1158 file(s) [attempted 1158/8459 = 13%, 1317 KB/s], Decompressed: 1155
Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 921 KB/s], Decompressed: 1186
Downloaded: 1228 file(s) [attempted 1228/8459 = 14%, 1284 KB/s], Decompressed: 1223
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 266 KB/s], Decompressed: 1268
Downloaded: 1312 file(s) [attempted 1312/8459 = 15%, 178 KB/s], Decompressed: 1305
Downloaded: 1353 file(s) [attempted 1353/8459 = 15%, 696 KB/s], Decompressed: 1350
Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 458 KB/s], Decompressed: 1381
Downloaded: 1425 file(s) [attempted 1425/8459 = 16%, 1314 KB/s], Decompressed: 1422
Downloaded: 1473 file(s) [attempted 1473/8459 = 17%, 254 KB/s], Decompressed: 1466
Downloaded: 1514 file(s) [attempted 1514/8459 = 17%, 246 KB/s], Decompressed: 1511
Downloaded: 1556 file(s) [attempted 1556/8459 = 18%, 101 KB/s], Decompressed: 1548
Downloaded: 1596 file(s) [attempted 1596/8459 = 18%, 22 KB/s], Decompressed: 1593
Downloaded: 1635 file(s) [attempted 1635/8459 = 19%, 241 KB/s], Decompressed: 1627
Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 63 KB/s], Decompressed: 1668
Downloaded: 1709 file(s) [attempted 1709/8459 = 20%, 195 KB/s], Decompressed: 1706
Downloaded: 1754 file(s) [attempted 1754/8459 = 20%, 75 KB/s], Decompressed: 1743
Downloaded: 1795 file(s) [attempted 1795/8459 = 21%, 24 KB/s], Decompressed: 1788
Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 69 KB/s], Decompressed: 1826
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 266 KB/s], Decompressed: 1860
Downloaded: 1908 file(s) [attempted 1908/8459 = 22%, 247 KB/s], Decompressed: 1904
Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 745 KB/s], Decompressed: 1942
Downloaded: 1988 file(s) [attempted 1988/8459 = 23%, 683 KB/s], Decompressed: 1983
Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 800 KB/s], Decompressed: 2017
Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 127 KB/s], Decompressed: 2058
Downloaded: 2106 file(s) [attempted 2106/8459 = 24%, 442 KB/s], Decompressed: 2103
Downloaded: 2147 file(s) [attempted 2147/8459 = 25%, 640 KB/s], Decompressed: 2144
Downloaded: 2185 file(s) [attempted 2185/8459 = 25%, 34 KB/s], Decompressed: 2178
Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 126 KB/s], Decompressed: 2216
Downloaded: 2265 file(s) [attempted 2265/8459 = 26%, 342 KB/s], Decompressed: 2257
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 284 KB/s], Decompressed: 2294
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 4995 KB/s], Decompressed: 2339
Downloaded: 2381 file(s) [attempted 2381/8459 = 28%, 479 KB/s], Decompressed: 2373
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 36 KB/s], Decompressed: 2414
Downloaded: 2466 file(s) [attempted 2466/8459 = 29%, 63 KB/s], Decompressed: 2462
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 176 KB/s], Decompressed: 2496
Downloaded: 2542 file(s) [attempted 2542/8459 = 30%, 340 KB/s], Decompressed: 2534
Downloaded: 2581 file(s) [attempted 2581/8459 = 30%, 64 KB/s], Decompressed: 2575
Downloaded: 2623 file(s) [attempted 2623/8459 = 31%, 77 KB/s], Decompressed: 2616
Downloaded: 2668 file(s) [attempted 2668/8459 = 31%, 183 KB/s], Decompressed: 2664
Downloaded: 2705 file(s) [attempted 2705/8459 = 31%, 1043 KB/s], Decompressed: 2698
Downloaded: 2744 file(s) [attempted 2744/8459 = 32%, 35 KB/s], Decompressed: 2736
Downloaded: 2780 file(s) [attempted 2780/8459 = 32%, 54 KB/s], Decompressed: 2777
Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 39 KB/s], Decompressed: 2822
Downloaded: 2867 file(s) [attempted 2867/8459 = 33%, 2367 KB/s], Decompressed: 2863
Downloaded: 2905 file(s) [attempted 2905/8459 = 34%, 935 KB/s], Decompressed: 2900
Downloaded: 2941 file(s) [attempted 2941/8459 = 34%, 249 KB/s], Decompressed: 2934
Downloaded: 2986 file(s) [attempted 2986/8459 = 35%, 452 KB/s], Decompressed: 2982
Downloaded: 3030 file(s) [attempted 3030/8459 = 35%, 23 KB/s], Decompressed: 3023
Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 365 KB/s], Decompressed: 3068
Downloaded: 3109 file(s) [attempted 3109/8459 = 36%, 63 KB/s], Decompressed: 3102
Downloaded: 3150 file(s) [attempted 3150/8459 = 37%, 544 KB/s], Decompressed: 3147
Downloaded: 3191 file(s) [attempted 3191/8459 = 37%, 444 KB/s], Decompressed: 3188
Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 798 KB/s], Decompressed: 3225
Downloaded: 3271 file(s) [attempted 3271/8459 = 38%, 986 KB/s], Decompressed: 3266
Downloaded: 3311 file(s) [attempted 3311/8459 = 39%, 162 KB/s], Decompressed: 3304
Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 247 KB/s], Decompressed: 3345
Downloaded: 3393 file(s) [attempted 3393/8459 = 40%, 98 KB/s], Decompressed: 3386
Downloaded: 3432 file(s) [attempted 3432/8459 = 40%, 113 KB/s], Decompressed: 3427
Downloaded: 3468 file(s) [attempted 3468/8459 = 40%, 383 KB/s], Decompressed: 3465
Downloaded: 3513 file(s) [attempted 3513/8459 = 41%, 291 KB/s], Decompressed: 3509
Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 92 KB/s], Decompressed: 3547
Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 261 KB/s], Decompressed: 3592
Downloaded: 3633 file(s) [attempted 3633/8459 = 42%, 317 KB/s], Decompressed: 3622
Downloaded: 3670 file(s) [attempted 3670/8459 = 43%, 111 KB/s], Decompressed: 3660
Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 254 KB/s], Decompressed: 3708
Downloaded: 3759 file(s) [attempted 3759/8459 = 44%, 42 KB/s], Decompressed: 3756
Downloaded: 3801 file(s) [attempted 3801/8459 = 44%, 299 KB/s], Decompressed: 3797
Downloaded: 3841 file(s) [attempted 3841/8459 = 45%, 161 KB/s], Decompressed: 3838
Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 244 KB/s], Decompressed: 3872
Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 113 KB/s], Decompressed: 3910
Downloaded: 3958 file(s) [attempted 3958/8459 = 46%, 108 KB/s], Decompressed: 3954
Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 81 KB/s], Decompressed: 3985
Downloaded: 4037 file(s) [attempted 4037/8459 = 47%, 118 KB/s], Decompressed: 4033
Downloaded: 4078 file(s) [attempted 4078/8459 = 48%, 357 KB/s], Decompressed: 4074
Downloaded: 4112 file(s) [attempted 4112/8459 = 48%, 356 KB/s], Decompressed: 4101
Downloaded: 4149 file(s) [attempted 4149/8459 = 49%, 102 KB/s], Decompressed: 4146
Downloaded: 4190 file(s) [attempted 4190/8459 = 49%, 319 KB/s], Decompressed: 4184
Downloaded: 4232 file(s) [attempted 4232/8459 = 50%, 522 KB/s], Decompressed: 4228
Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 534 KB/s], Decompressed: 4273
Downloaded: 4314 file(s) [attempted 4314/8459 = 50%, 464 KB/s], Decompressed: 4307
Downloaded: 4348 file(s) [attempted 4348/8459 = 51%, 165 KB/s], Decompressed: 4341
Downloaded: 4389 file(s) [attempted 4389/8459 = 51%, 218 KB/s], Decompressed: 4386
Downloaded: 4425 file(s) [attempted 4425/8459 = 52%, 841 KB/s], Decompressed: 4420
Downloaded: 4468 file(s) [attempted 4468/8459 = 52%, 343 KB/s], Decompressed: 4461
Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 282 KB/s], Decompressed: 4498
Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 315 KB/s], Decompressed: 4540
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 216 KB/s], Decompressed: 4581
Downloaded: 4629 file(s) [attempted 4629/8459 = 54%, 149 KB/s], Decompressed: 4622
Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 534 KB/s], Decompressed: 4673
Downloaded: 4721 file(s) [attempted 4721/8459 = 55%, 1321 KB/s], Decompressed: 4714
Downloaded: 4759 file(s) [attempted 4759/8459 = 56%, 89 KB/s], Decompressed: 4752
Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 365 KB/s], Decompressed: 4789
Downloaded: 4830 file(s) [attempted 4830/8459 = 57%, 73 KB/s], Decompressed: 4827
Downloaded: 4875 file(s) [attempted 4875/8459 = 57%, 111 KB/s], Decompressed: 4872
Downloaded: 4916 file(s) [attempted 4916/8459 = 58%, 48 KB/s], Decompressed: 4909
Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 186 KB/s], Decompressed: 4950
Downloaded: 4998 file(s) [attempted 4998/8459 = 59%, 452 KB/s], Decompressed: 4991
Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 187 KB/s], Decompressed: 5039
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 516 KB/s], Decompressed: 5077
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 1983 KB/s], Decompressed: 5115
Downloaded: 5159 file(s) [attempted 5159/8459 = 60%, 638 KB/s], Decompressed: 5152
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 855 KB/s], Decompressed: 5197
Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 239 KB/s], Decompressed: 5238
Downloaded: 5286 file(s) [attempted 5286/8459 = 62%, 481 KB/s], Decompressed: 5282
Downloaded: 5323 file(s) [attempted 5323/8459 = 62%, 51 KB/s], Decompressed: 5316
Downloaded: 5361 file(s) [attempted 5361/8459 = 63%, 440 KB/s], Decompressed: 5358
Downloaded: 5399 file(s) [attempted 5399/8459 = 63%, 89 KB/s], Decompressed: 5395
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 502 KB/s], Decompressed: 5440
Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 1081 KB/s], Decompressed: 5477
Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 80 KB/s], Decompressed: 5525
Downloaded: 5571 file(s) [attempted 5571/8459 = 65%, 123 KB/s], Decompressed: 5563
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 21 KB/s], Decompressed: 5597
Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 208 KB/s], Decompressed: 5642
Downloaded: 5686 file(s) [attempted 5686/8459 = 67%, 615 KB/s], Decompressed: 5679
Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 682 KB/s], Decompressed: 5724
Downloaded: 5772 file(s) [attempted 5772/8459 = 68%, 614 KB/s], Decompressed: 5768
Downloaded: 5809 file(s) [attempted 5809/8459 = 68%, 280 KB/s], Decompressed: 5802
Downloaded: 5845 file(s) [attempted 5845/8459 = 69%, 488 KB/s], Decompressed: 5840
Downloaded: 5888 file(s) [attempted 5888/8459 = 69%, 52 KB/s], Decompressed: 5881
Downloaded: 5929 file(s) [attempted 5929/8459 = 70%, 1073 KB/s], Decompressed: 5922
Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 45 KB/s], Decompressed: 5967
Downloaded: 6008 file(s) [attempted 6008/8459 = 71%, 93 KB/s], Decompressed: 5994
Downloaded: 6045 file(s) [attempted 6045/8459 = 71%, 2283 KB/s], Decompressed: 6042
Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 1258 KB/s], Decompressed: 6090
Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 147 KB/s], Decompressed: 6134
Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 478 KB/s], Decompressed: 6169
Downloaded: 6212 file(s) [attempted 6212/8459 = 73%, 113 KB/s], Decompressed: 6206
Downloaded: 6251 file(s) [attempted 6251/8459 = 73%, 94 KB/s], Decompressed: 6247
Downloaded: 6289 file(s) [attempted 6289/8459 = 74%, 2862 KB/s], Decompressed: 6285
Downloaded: 6333 file(s) [attempted 6333/8459 = 74%, 338 KB/s], Decompressed: 6329
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 707 KB/s], Decompressed: 6373
Downloaded: 6416 file(s) [attempted 6416/8459 = 75%, 51 KB/s], Decompressed: 6405
Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 263 KB/s], Decompressed: 6449
Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 707 KB/s], Decompressed: 6490
Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 430 KB/s], Decompressed: 6521
Downloaded: 6573 file(s) [attempted 6573/8459 = 77%, 452 KB/s], Decompressed: 6566
Downloaded: 6614 file(s) [attempted 6614/8459 = 78%, 266 KB/s], Decompressed: 6610
Downloaded: 6655 file(s) [attempted 6655/8459 = 78%, 126 KB/s], Decompressed: 6651
Downloaded: 6692 file(s) [attempted 6692/8459 = 79%, 384 KB/s], Decompressed: 6682
Downloaded: 6728 file(s) [attempted 6728/8459 = 79%, 33 KB/s], Decompressed: 6723
Downloaded: 6771 file(s) [attempted 6771/8459 = 80%, 110 KB/s], Decompressed: 6768
Downloaded: 6815 file(s) [attempted 6815/8459 = 80%, 46 KB/s], Decompressed: 6812
Downloaded: 6852 file(s) [attempted 6852/8459 = 81%, 115 KB/s], Decompressed: 6846
Downloaded: 6880 file(s) [attempted 6880/8459 = 81%, 38 KB/s], Decompressed: 6877
Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 347 KB/s], Decompressed: 6922
Downloaded: 6966 file(s) [attempted 6966/8459 = 82%, 180 KB/s], Decompressed: 6963
Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 111 KB/s], Decompressed: 7004
Downloaded: 7045 file(s) [attempted 7045/8459 = 83%, 21 KB/s], Decompressed: 7041
Downloaded: 7082 file(s) [attempted 7082/8459 = 83%, 595 KB/s], Decompressed: 7076
Downloaded: 7127 file(s) [attempted 7127/8459 = 84%, 223 KB/s], Decompressed: 7123
Downloaded: 7167 file(s) [attempted 7167/8459 = 84%, 78 KB/s], Decompressed: 7161
Downloaded: 7203 file(s) [attempted 7203/8459 = 85%, 43 KB/s], Decompressed: 7199
Downloaded: 7240 file(s) [attempted 7240/8459 = 85%, 1098 KB/s], Decompressed: 7236
Downloaded: 7281 file(s) [attempted 7281/8459 = 86%, 127 KB/s], Decompressed: 7271
Downloaded: 7323 file(s) [attempted 7323/8459 = 86%, 306 KB/s], Decompressed: 7319
Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 43 KB/s], Decompressed: 7363
Downloaded: 7408 file(s) [attempted 7408/8459 = 87%, 87 KB/s], Decompressed: 7394
Downloaded: 7442 file(s) [attempted 7442/8459 = 87%, 66 KB/s], Decompressed: 7431
Downloaded: 7479 file(s) [attempted 7479/8459 = 88%, 104 KB/s], Decompressed: 7476
Downloaded: 7520 file(s) [attempted 7520/8459 = 88%, 243 KB/s], Decompressed: 7517
Downloaded: 7562 file(s) [attempted 7562/8459 = 89%, 125 KB/s], Decompressed: 7558
Downloaded: 7608 file(s) [attempted 7608/8459 = 89%, 46 KB/s], Decompressed: 7599
Downloaded: 7640 file(s) [attempted 7640/8459 = 90%, 214 KB/s], Decompressed: 7637
Downloaded: 7681 file(s) [attempted 7681/8459 = 90%, 468 KB/s], Decompressed: 7679
Downloaded: 7716 file(s) [attempted 7716/8459 = 91%, 67 KB/s], Decompressed: 7712
Downloaded: 7761 file(s) [attempted 7761/8459 = 91%, 271 KB/s], Decompressed: 7757
Downloaded: 7804 file(s) [attempted 7804/8459 = 92%, 617 KB/s], Decompressed: 7801
Downloaded: 7846 file(s) [attempted 7846/8459 = 92%, 218 KB/s], Decompressed: 7839
Downloaded: 7876 file(s) [attempted 7876/8459 = 93%, 98 KB/s], Decompressed: 7870
Downloaded: 7914 file(s) [attempted 7914/8459 = 93%, 829 KB/s], Decompressed: 7911
Downloaded: 7955 file(s) [attempted 7955/8459 = 94%, 53 KB/s], Decompressed: 7952
Downloaded: 7996 file(s) [attempted 7996/8459 = 94%, 279 KB/s], Decompressed: 7993
Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 2066 KB/s], Decompressed: 8030
Downloaded: 8072 file(s) [attempted 8072/8459 = 95%, 98 KB/s], Decompressed: 8061
Downloaded: 8111 file(s) [attempted 8111/8459 = 95%, 115 KB/s], Decompressed: 8106
Downloaded: 8154 file(s) [attempted 8154/8459 = 96%, 196 KB/s], Decompressed: 8150
Downloaded: 8191 file(s) [attempted 8191/8459 = 96%, 250 KB/s], Decompressed: 8184
Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 518 KB/s], Decompressed: 8232
Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 1072 KB/s], Decompressed: 8273
Downloaded: 8318 file(s) [attempted 8318/8459 = 98%, 69 KB/s], Decompressed: 8311
Downloaded: 8356 file(s) [attempted 8356/8459 = 98%, 145 KB/s], Decompressed: 8352
Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 265 KB/s], Decompressed: 8390
Downloaded: 8434 file(s) [attempted 8434/8459 = 99%, 192 KB/s], Decompressed: 8427
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 264 KB/s], Decompressed: 8451
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 264 KB/s], Decompressed: 8451
$ lake build
exit_code=Some(1) duration_ms=451043
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (24s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.6s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/779] Built Iut.Foundations.QualitativeData (2.1s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.8s)
✔ [3389/3394] Built Iut.Stage1.CorollarySchema (32s)
✔ [3390/3397] Built Iut.Stage1.SourceObligations (3.8s)
✔ [3392/3398] Built Iut.Stage1.IUTSourceScaffold (3.0s)
✔ [3394/3401] Built Iut.Stage1.IUTStage1Data (3.5s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (85s)
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 (27s)
⚠ [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.3s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.6s)
⚠ [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 (162s)
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=2827
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-1358-source
Cloning into '/var/lib/apodeixis/repos/job-1358-source'...
git_checkout exit 0
git checkout 6beb21db0f1b60ae3dafd8020c481efbe396d1fd
Note: switching to '6beb21db0f1b60ae3dafd8020c481efbe396d1fd'. 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 6beb21d Derive synchronized route inputs
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%, 24 KB/s], Decompressed: 0 Downloaded: 16 file(s) [attempted 16/8459 = 0%, 4 KB/s], Decompressed: 15 Downloaded: 40 file(s) [attempted 40/8459 = 0%, 22 KB/s], Decompressed: 36 Downloaded: 65 file(s) [attempted 65/8459 = 0%, 26 KB/s], Decompressed: 63 Downloaded: 87 file(s) [attempted 87/8459 = 1%, 448 KB/s], Decompressed: 80 Downloaded: 114 file(s) [attempted 114/8459 = 1%, 44 KB/s], Decompressed: 110 Downloaded: 151 file(s) [attempted 151/8459 = 1%, 208 KB/s], Decompressed: 148 Downloaded: 192 file(s) [attempted 192/8459 = 2%, 511 KB/s], Decompressed: 189 Downloaded: 230 file(s) [attempted 230/8459 = 2%, 578 KB/s], Decompressed: 223 Downloaded: 268 file(s) [attempted 268/8459 = 3%, 507 KB/s], Decompressed: 261 Downloaded: 303 file(s) [attempted 303/8459 = 3%, 25 KB/s], Decompressed: 292 Downloaded: 336 file(s) [attempted 336/8459 = 3%, 119 KB/s], Decompressed: 329 Downloaded: 374 file(s) [attempted 374/8459 = 4%, 283 KB/s], Decompressed: 371 Downloaded: 415 file(s) [attempted 415/8459 = 4%, 116 KB/s], Decompressed: 412 Downloaded: 455 file(s) [attempted 455/8459 = 5%, 549 KB/s], Decompressed: 449 Downloaded: 490 file(s) [attempted 490/8459 = 5%, 1394 KB/s], Decompressed: 487 Downloaded: 528 file(s) [attempted 528/8459 = 6%, 173 KB/s], Decompressed: 521 Downloaded: 569 file(s) [attempted 569/8459 = 6%, 161 KB/s], Decompressed: 562 Downloaded: 610 file(s) [attempted 610/8459 = 7%, 449 KB/s], Decompressed: 604 Downloaded: 651 file(s) [attempted 651/8459 = 7%, 327 KB/s], Decompressed: 645 Downloaded: 690 file(s) [attempted 690/8459 = 8%, 75 KB/s], Decompressed: 686 Downloaded: 730 file(s) [attempted 730/8459 = 8%, 492 KB/s], Decompressed: 727 Downloaded: 768 file(s) [attempted 768/8459 = 9%, 830 KB/s], Decompressed: 761 Downloaded: 802 file(s) [attempted 802/8459 = 9%, 124 KB/s], Decompressed: 799 Downloaded: 843 file(s) [attempted 843/8459 = 9%, 205 KB/s], Decompressed: 840 Downloaded: 884 file(s) [attempted 884/8459 = 10%, 43 KB/s], Decompressed: 878 Downloaded: 925 file(s) [attempted 925/8459 = 10%, 1194 KB/s], Decompressed: 922 Downloaded: 963 file(s) [attempted 963/8459 = 11%, 339 KB/s], Decompressed: 956 Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 494 KB/s], Decompressed: 997 Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 200 KB/s], Decompressed: 1035 Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 289 KB/s], Decompressed: 1073 Downloaded: 1117 file(s) [attempted 1117/8459 = 13%, 1481 KB/s], Decompressed: 1114 Downloaded: 1158 file(s) [attempted 1158/8459 = 13%, 1317 KB/s], Decompressed: 1155 Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 921 KB/s], Decompressed: 1186 Downloaded: 1228 file(s) [attempted 1228/8459 = 14%, 1284 KB/s], Decompressed: 1223 Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 266 KB/s], Decompressed: 1268 Downloaded: 1312 file(s) [attempted 1312/8459 = 15%, 178 KB/s], Decompressed: 1305 Downloaded: 1353 file(s) [attempted 1353/8459 = 15%, 696 KB/s], Decompressed: 1350 Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 458 KB/s], Decompressed: 1381 Downloaded: 1425 file(s) [attempted 1425/8459 = 16%, 1314 KB/s], Decompressed: 1422 Downloaded: 1473 file(s) [attempted 1473/8459 = 17%, 254 KB/s], Decompressed: 1466 Downloaded: 1514 file(s) [attempted 1514/8459 = 17%, 246 KB/s], Decompressed: 1511 Downloaded: 1556 file(s) [attempted 1556/8459 = 18%, 101 KB/s], Decompressed: 1548 Downloaded: 1596 file(s) [attempted 1596/8459 = 18%, 22 KB/s], Decompressed: 1593 Downloaded: 1635 file(s) [attempted 1635/8459 = 19%, 241 KB/s], Decompressed: 1627 Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 63 KB/s], Decompressed: 1668 Downloaded: 1709 file(s) [attempted 1709/8459 = 20%, 195 KB/s], Decompressed: 1706 Downloaded: 1754 file(s) [attempted 1754/8459 = 20%, 75 KB/s], Decompressed: 1743 Downloaded: 1795 file(s) [attempted 1795/8459 = 21%, 24 KB/s], Decompressed: 1788 Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 69 KB/s], Decompressed: 1826 Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 266 KB/s], Decompressed: 1860 Downloaded: 1908 file(s) [attempted 1908/8459 = 22%, 247 KB/s], Decompressed: 1904 Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 745 KB/s], Decompressed: 1942 Downloaded: 1988 file(s) [attempted 1988/8459 = 23%, 683 KB/s], Decompressed: 1983 Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 800 KB/s], Decompressed: 2017 Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 127 KB/s], Decompressed: 2058 Downloaded: 2106 file(s) [attempted 2106/8459 = 24%, 442 KB/s], Decompressed: 2103 Downloaded: 2147 file(s) [attempted 2147/8459 = 25%, 640 KB/s], Decompressed: 2144 Downloaded: 2185 file(s) [attempted 2185/8459 = 25%, 34 KB/s], Decompressed: 2178 Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 126 KB/s], Decompressed: 2216 Downloaded: 2265 file(s) [attempted 2265/8459 = 26%, 342 KB/s], Decompressed: 2257 Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 284 KB/s], Decompressed: 2294 Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 4995 KB/s], Decompressed: 2339 Downloaded: 2381 file(s) [attempted 2381/8459 = 28%, 479 KB/s], Decompressed: 2373 Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 36 KB/s], Decompressed: 2414 Downloaded: 2466 file(s) [attempted 2466/8459 = 29%, 63 KB/s], Decompressed: 2462 Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 176 KB/s], Decompressed: 2496 Downloaded: 2542 file(s) [attempted 2542/8459 = 30%, 340 KB/s], Decompressed: 2534 Downloaded: 2581 file(s) [attempted 2581/8459 = 30%, 64 KB/s], Decompressed: 2575 Downloaded: 2623 file(s) [attempted 2623/8459 = 31%, 77 KB/s], Decompressed: 2616 Downloaded: 2668 file(s) [attempted 2668/8459 = 31%, 183 KB/s], Decompressed: 2664 Downloaded: 2705 file(s) [attempted 2705/8459 = 31%, 1043 KB/s], Decompressed: 2698 Downloaded: 2744 file(s) [attempted 2744/8459 = 32%, 35 KB/s], Decompressed: 2736 Downloaded: 2780 file(s) [attempted 2780/8459 = 32%, 54 KB/s], Decompressed: 2777 Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 39 KB/s], Decompressed: 2822 Downloaded: 2867 file(s) [attempted 2867/8459 = 33%, 2367 KB/s], Decompressed: 2863 Downloaded: 2905 file(s) [attempted 2905/8459 = 34%, 935 KB/s], Decompressed: 2900 Downloaded: 2941 file(s) [attempted 2941/8459 = 34%, 249 KB/s], Decompressed: 2934 Downloaded: 2986 file(s) [attempted 2986/8459 = 35%, 452 KB/s], Decompressed: 2982 Downloaded: 3030 file(s) [attempted 3030/8459 = 35%, 23 KB/s], Decompressed: 3023 Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 365 KB/s], Decompressed: 3068 Downloaded: 3109 file(s) [attempted 3109/8459 = 36%, 63 KB/s], Decompressed: 3102 Downloaded: 3150 file(s) [attempted 3150/8459 = 37%, 544 KB/s], Decompressed: 3147 Downloaded: 3191 file(s) [attempted 3191/8459 = 37%, 444 KB/s], Decompressed: 3188 Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 798 KB/s], Decompressed: 3225 Downloaded: 3271 file(s) [attempted 3271/8459 = 38%, 986 KB/s], Decompressed: 3266 Downloaded: 3311 file(s) [attempted 3311/8459 = 39%, 162 KB/s], Decompressed: 3304 Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 247 KB/s], Decompressed: 3345 Downloaded: 3393 file(s) [attempted 3393/8459 = 40%, 98 KB/s], Decompressed: 3386 Downloaded: 3432 file(s) [attempted 3432/8459 = 40%, 113 KB/s], Decompressed: 3427 Downloaded: 3468 file(s) [attempted 3468/8459 = 40%, 383 KB/s], Decompressed: 3465 Downloaded: 3513 file(s) [attempted 3513/8459 = 41%, 291 KB/s], Decompressed: 3509 Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 92 KB/s], Decompressed: 3547 Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 261 KB/s], Decompressed: 3592 Downloaded: 3633 file(s) [attempted 3633/8459 = 42%, 317 KB/s], Decompressed: 3622 Downloaded: 3670 file(s) [attempted 3670/8459 = 43%, 111 KB/s], Decompressed: 3660 Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 254 KB/s], Decompressed: 3708 Downloaded: 3759 file(s) [attempted 3759/8459 = 44%, 42 KB/s], Decompressed: 3756 Downloaded: 3801 file(s) [attempted 3801/8459 = 44%, 299 KB/s], Decompressed: 3797 Downloaded: 3841 file(s) [attempted 3841/8459 = 45%, 161 KB/s], Decompressed: 3838 Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 244 KB/s], Decompressed: 3872 Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 113 KB/s], Decompressed: 3910 Downloaded: 3958 file(s) [attempted 3958/8459 = 46%, 108 KB/s], Decompressed: 3954 Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 81 KB/s], Decompressed: 3985 Downloaded: 4037 file(s) [attempted 4037/8459 = 47%, 118 KB/s], Decompressed: 4033 Downloaded: 4078 file(s) [attempted 4078/8459 = 48%, 357 KB/s], Decompressed: 4074 Downloaded: 4112 file(s) [attempted 4112/8459 = 48%, 356 KB/s], Decompressed: 4101 Downloaded: 4149 file(s) [attempted 4149/8459 = 49%, 102 KB/s], Decompressed: 4146 Downloaded: 4190 file(s) [attempted 4190/8459 = 49%, 319 KB/s], Decompressed: 4184 Downloaded: 4232 file(s) [attempted 4232/8459 = 50%, 522 KB/s], Decompressed: 4228 Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 534 KB/s], Decompressed: 4273 Downloaded: 4314 file(s) [attempted 4314/8459 = 50%, 464 KB/s], Decompressed: 4307 Downloaded: 4348 file(s) [attempted 4348/8459 = 51%, 165 KB/s], Decompressed: 4341 Downloaded: 4389 file(s) [attempted 4389/8459 = 51%, 218 KB/s], Decompressed: 4386 Downloaded: 4425 file(s) [attempted 4425/8459 = 52%, 841 KB/s], Decompressed: 4420 Downloaded: 4468 file(s) [attempted 4468/8459 = 52%, 343 KB/s], Decompressed: 4461 Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 282 KB/s], Decompressed: 4498 Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 315 KB/s], Decompressed: 4540 Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 216 KB/s], Decompressed: 4581 Downloaded: 4629 file(s) [attempted 4629/8459 = 54%, 149 KB/s], Decompressed: 4622 Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 534 KB/s], Decompressed: 4673 Downloaded: 4721 file(s) [attempted 4721/8459 = 55%, 1321 KB/s], Decompressed: 4714 Downloaded: 4759 file(s) [attempted 4759/8459 = 56%, 89 KB/s], Decompressed: 4752 Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 365 KB/s], Decompressed: 4789 Downloaded: 4830 file(s) [attempted 4830/8459 = 57%, 73 KB/s], Decompressed: 4827 Downloaded: 4875 file(s) [attempted 4875/8459 = 57%, 111 KB/s], Decompressed: 4872 Downloaded: 4916 file(s) [attempted 4916/8459 = 58%, 48 KB/s], Decompressed: 4909 Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 186 KB/s], Decompressed: 4950 Downloaded: 4998 file(s) [attempted 4998/8459 = 59%, 452 KB/s], Decompressed: 4991 Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 187 KB/s], Decompressed: 5039 Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 516 KB/s], Decompressed: 5077 Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 1983 KB/s], Decompressed: 5115 Downloaded: 5159 file(s) [attempted 5159/8459 = 60%, 638 KB/s], Decompressed: 5152 Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 855 KB/s], Decompressed: 5197 Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 239 KB/s], Decompressed: 5238 Downloaded: 5286 file(s) [attempted 5286/8459 = 62%, 481 KB/s], Decompressed: 5282 Downloaded: 5323 file(s) [attempted 5323/8459 = 62%, 51 KB/s], Decompressed: 5316 Downloaded: 5361 file(s) [attempted 5361/8459 = 63%, 440 KB/s], Decompressed: 5358 Downloaded: 5399 file(s) [attempted 5399/8459 = 63%, 89 KB/s], Decompressed: 5395 Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 502 KB/s], Decompressed: 5440 Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 1081 KB/s], Decompressed: 5477 Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 80 KB/s], Decompressed: 5525 Downloaded: 5571 file(s) [attempted 5571/8459 = 65%, 123 KB/s], Decompressed: 5563 Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 21 KB/s], Decompressed: 5597 Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 208 KB/s], Decompressed: 5642 Downloaded: 5686 file(s) [attempted 5686/8459 = 67%, 615 KB/s], Decompressed: 5679 Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 682 KB/s], Decompressed: 5724 Downloaded: 5772 file(s) [attempted 5772/8459 = 68%, 614 KB/s], Decompressed: 5768 Downloaded: 5809 file(s) [attempted 5809/8459 = 68%, 280 KB/s], Decompressed: 5802 Downloaded: 5845 file(s) [attempted 5845/8459 = 69%, 488 KB/s], Decompressed: 5840 Downloaded: 5888 file(s) [attempted 5888/8459 = 69%, 52 KB/s], Decompressed: 5881 Downloaded: 5929 file(s) [attempted 5929/8459 = 70%, 1073 KB/s], Decompressed: 5922 Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 45 KB/s], Decompressed: 5967 Downloaded: 6008 file(s) [attempted 6008/8459 = 71%, 93 KB/s], Decompressed: 5994 Downloaded: 6045 file(s) [attempted 6045/8459 = 71%, 2283 KB/s], Decompressed: 6042 Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 1258 KB/s], Decompressed: 6090 Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 147 KB/s], Decompressed: 6134 Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 478 KB/s], Decompressed: 6169 Downloaded: 6212 file(s) [attempted 6212/8459 = 73%, 113 KB/s], Decompressed: 6206 Downloaded: 6251 file(s) [attempted 6251/8459 = 73%, 94 KB/s], Decompressed: 6247 Downloaded: 6289 file(s) [attempted 6289/8459 = 74%, 2862 KB/s], Decompressed: 6285 Downloaded: 6333 file(s) [attempted 6333/8459 = 74%, 338 KB/s], Decompressed: 6329 Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 707 KB/s], Decompressed: 6373 Downloaded: 6416 file(s) [attempted 6416/8459 = 75%, 51 KB/s], Decompressed: 6405 Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 263 KB/s], Decompressed: 6449 Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 707 KB/s], Decompressed: 6490 Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 430 KB/s], Decompressed: 6521 Downloaded: 6573 file(s) [attempted 6573/8459 = 77%, 452 KB/s], Decompressed: 6566 Downloaded: 6614 file(s) [attempted 6614/8459 = 78%, 266 KB/s], Decompressed: 6610 Downloaded: 6655 file(s) [attempted 6655/8459 = 78%, 126 KB/s], Decompressed: 6651 Downloaded: 6692 file(s) [attempted 6692/8459 = 79%, 384 KB/s], Decompressed: 6682 Downloaded: 6728 file(s) [attempted 6728/8459 = 79%, 33 KB/s], Decompressed: 6723 Downloaded: 6771 file(s) [attempted 6771/8459 = 80%, 110 KB/s], Decompressed: 6768 Downloaded: 6815 file(s) [attempted 6815/8459 = 80%, 46 KB/s], Decompressed: 6812 Downloaded: 6852 file(s) [attempted 6852/8459 = 81%, 115 KB/s], Decompressed: 6846 Downloaded: 6880 file(s) [attempted 6880/8459 = 81%, 38 KB/s], Decompressed: 6877 Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 347 KB/s], Decompressed: 6922 Downloaded: 6966 file(s) [attempted 6966/8459 = 82%, 180 KB/s], Decompressed: 6963 Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 111 KB/s], Decompressed: 7004 Downloaded: 7045 file(s) [attempted 7045/8459 = 83%, 21 KB/s], Decompressed: 7041 Downloaded: 7082 file(s) [attempted 7082/8459 = 83%, 595 KB/s], Decompressed: 7076 Downloaded: 7127 file(s) [attempted 7127/8459 = 84%, 223 KB/s], Decompressed: 7123 Downloaded: 7167 file(s) [attempted 7167/8459 = 84%, 78 KB/s], Decompressed: 7161 Downloaded: 7203 file(s) [attempted 7203/8459 = 85%, 43 KB/s], Decompressed: 7199 Downloaded: 7240 file(s) [attempted 7240/8459 = 85%, 1098 KB/s], Decompressed: 7236 Downloaded: 7281 file(s) [attempted 7281/8459 = 86%, 127 KB/s], Decompressed: 7271 Downloaded: 7323 file(s) [attempted 7323/8459 = 86%, 306 KB/s], Decompressed: 7319 Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 43 KB/s], Decompressed: 7363 Downloaded: 7408 file(s) [attempted 7408/8459 = 87%, 87 KB/s], Decompressed: 7394 Downloaded: 7442 file(s) [attempted 7442/8459 = 87%, 66 KB/s], Decompressed: 7431 Downloaded: 7479 file(s) [attempted 7479/8459 = 88%, 104 KB/s], Decompressed: 7476 Downloaded: 7520 file(s) [attempted 7520/8459 = 88%, 243 KB/s], Decompressed: 7517 Downloaded: 7562 file(s) [attempted 7562/8459 = 89%, 125 KB/s], Decompressed: 7558 Downloaded: 7608 file(s) [attempted 7608/8459 = 89%, 46 KB/s], Decompressed: 7599 Downloaded: 7640 file(s) [attempted 7640/8459 = 90%, 214 KB/s], Decompressed: 7637 Downloaded: 7681 file(s) [attempted 7681/8459 = 90%, 468 KB/s], Decompressed: 7679 Downloaded: 7716 file(s) [attempted 7716/8459 = 91%, 67 KB/s], Decompressed: 7712 Downloaded: 7761 file(s) [attempted 7761/8459 = 91%, 271 KB/s], Decompressed: 7757 Downloaded: 7804 file(s) [attempted 7804/8459 = 92%, 617 KB/s], Decompressed: 7801 Downloaded: 7846 file(s) [attempted 7846/8459 = 92%, 218 KB/s], Decompressed: 7839 Downloaded: 7876 file(s) [attempted 7876/8459 = 93%, 98 KB/s], Decompressed: 7870 Downloaded: 7914 file(s) [attempted 7914/8459 = 93%, 829 KB/s], Decompressed: 7911 Downloaded: 7955 file(s) [attempted 7955/8459 = 94%, 53 KB/s], Decompressed: 7952 Downloaded: 7996 file(s) [attempted 7996/8459 = 94%, 279 KB/s], Decompressed: 7993 Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 2066 KB/s], Decompressed: 8030 Downloaded: 8072 file(s) [attempted 8072/8459 = 95%, 98 KB/s], Decompressed: 8061 Downloaded: 8111 file(s) [attempted 8111/8459 = 95%, 115 KB/s], Decompressed: 8106 Downloaded: 8154 file(s) [attempted 8154/8459 = 96%, 196 KB/s], Decompressed: 8150 Downloaded: 8191 file(s) [attempted 8191/8459 = 96%, 250 KB/s], Decompressed: 8184 Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 518 KB/s], Decompressed: 8232 Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 1072 KB/s], Decompressed: 8273 Downloaded: 8318 file(s) [attempted 8318/8459 = 98%, 69 KB/s], Decompressed: 8311 Downloaded: 8356 file(s) [attempted 8356/8459 = 98%, 145 KB/s], Decompressed: 8352 Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 265 KB/s], Decompressed: 8390 Downloaded: 8434 file(s) [attempted 8434/8459 = 99%, 192 KB/s], Decompressed: 8427 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 264 KB/s], Decompressed: 8451 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 264 KB/s], Decompressed: 8451
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (24s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.6s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/779] Built Iut.Foundations.QualitativeData (2.1s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.8s)
✔ [3389/3394] Built Iut.Stage1.CorollarySchema (32s)
✔ [3390/3397] Built Iut.Stage1.SourceObligations (3.8s)
✔ [3392/3398] Built Iut.Stage1.IUTSourceScaffold (3.0s)
✔ [3394/3401] Built Iut.Stage1.IUTStage1Data (3.5s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (85s)
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 (27s)
⚠ [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.3s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.6s)
⚠ [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 (162s)
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`