Verification run
Run 1067
failed commit
7832205a5231 toolchain lean-v4-30-0 prover lean took 11m 48s · 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-1369-source
exit_code=Some(0) duration_ms=3618
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1369-source'...
$ git checkout 7832205a52316331f46f3fbbac89608c9a2737bf
exit_code=Some(0) duration_ms=174
stderr:
Note: switching to '7832205a52316331f46f3fbbac89608c9a2737bf'.
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 7832205 Preserve formula gap route input source
Resolved source revision: 7832205a52316331f46f3fbbac89608c9a2737bf
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=7832205a52316331f46f3fbbac89608c9a2737bf provenance={"branch":"master","checked_out_revision":"7832205a52316331f46f3fbbac89608c9a2737bf","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"7832205a52316331f46f3fbbac89608c9a2737bf","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=49414
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: 17 file(s) [attempted 17/8459 = 0%, 5 KB/s], Decompressed: 16
Downloaded: 40 file(s) [attempted 40/8459 = 0%, 17 KB/s], Decompressed: 35
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 97 KB/s], Decompressed: 65
Downloaded: 100 file(s) [attempted 100/8459 = 1%, 74 KB/s], Decompressed: 93
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 395 KB/s], Decompressed: 127
Downloaded: 165 file(s) [attempted 165/8459 = 1%, 389 KB/s], Decompressed: 151
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 428 KB/s], Decompressed: 196
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 248 KB/s], Decompressed: 223
Downloaded: 264 file(s) [attempted 264/8459 = 3%, 842 KB/s], Decompressed: 261
Downloaded: 302 file(s) [attempted 302/8459 = 3%, 27 KB/s], Decompressed: 295
Downloaded: 340 file(s) [attempted 340/8459 = 4%, 106 KB/s], Decompressed: 336
Downloaded: 379 file(s) [attempted 379/8459 = 4%, 123 KB/s], Decompressed: 374
Downloaded: 415 file(s) [attempted 415/8459 = 4%, 99 KB/s], Decompressed: 408
Downloaded: 449 file(s) [attempted 449/8459 = 5%, 67 KB/s], Decompressed: 443
Downloaded: 492 file(s) [attempted 492/8459 = 5%, 82 KB/s], Decompressed: 480
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 216 KB/s], Decompressed: 521
Downloaded: 566 file(s) [attempted 566/8459 = 6%, 168 KB/s], Decompressed: 562
Downloaded: 607 file(s) [attempted 607/8459 = 7%, 747 KB/s], Decompressed: 597
Downloaded: 648 file(s) [attempted 648/8459 = 7%, 315 KB/s], Decompressed: 641
Downloaded: 689 file(s) [attempted 689/8459 = 8%, 162 KB/s], Decompressed: 682
Downloaded: 730 file(s) [attempted 730/8459 = 8%, 121 KB/s], Decompressed: 713
Downloaded: 771 file(s) [attempted 771/8459 = 9%, 1150 KB/s], Decompressed: 765
Downloaded: 812 file(s) [attempted 812/8459 = 9%, 226 KB/s], Decompressed: 795
Downloaded: 857 file(s) [attempted 857/8459 = 10%, 201 KB/s], Decompressed: 850
Downloaded: 898 file(s) [attempted 898/8459 = 10%, 586 KB/s], Decompressed: 895
Downloaded: 937 file(s) [attempted 937/8459 = 11%, 29 KB/s], Decompressed: 932
Downloaded: 973 file(s) [attempted 973/8459 = 11%, 83 KB/s], Decompressed: 970
Downloaded: 1015 file(s) [attempted 1015/8459 = 11%, 207 KB/s], Decompressed: 1011
Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 238 KB/s], Decompressed: 1052
Downloaded: 1100 file(s) [attempted 1100/8459 = 13%, 76 KB/s], Decompressed: 1097
Downloaded: 1142 file(s) [attempted 1142/8459 = 13%, 884 KB/s], Decompressed: 1134
Downloaded: 1179 file(s) [attempted 1179/8459 = 13%, 136 KB/s], Decompressed: 1175
Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 303 KB/s], Decompressed: 1213
Downloaded: 1261 file(s) [attempted 1261/8459 = 14%, 709 KB/s], Decompressed: 1254
Downloaded: 1295 file(s) [attempted 1295/8459 = 15%, 329 KB/s], Decompressed: 1292
Downloaded: 1336 file(s) [attempted 1336/8459 = 15%, 500 KB/s], Decompressed: 1333
Downloaded: 1384 file(s) [attempted 1384/8459 = 16%, 831 KB/s], Decompressed: 1377
Downloaded: 1429 file(s) [attempted 1429/8459 = 16%, 31 KB/s], Decompressed: 1425
Downloaded: 1473 file(s) [attempted 1473/8459 = 17%, 181 KB/s], Decompressed: 1466
Downloaded: 1511 file(s) [attempted 1511/8459 = 17%, 134 KB/s], Decompressed: 1487
Downloaded: 1545 file(s) [attempted 1545/8459 = 18%, 1057 KB/s], Decompressed: 1542
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 148 KB/s], Decompressed: 1579
Downloaded: 1628 file(s) [attempted 1628/8459 = 19%, 1615 KB/s], Decompressed: 1624
Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 1533 KB/s], Decompressed: 1665
Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 422 KB/s], Decompressed: 1709
Downloaded: 1754 file(s) [attempted 1754/8459 = 20%, 381 KB/s], Decompressed: 1743
Downloaded: 1794 file(s) [attempted 1794/8459 = 21%, 26 KB/s], Decompressed: 1788
Downloaded: 1832 file(s) [attempted 1832/8459 = 21%, 100 KB/s], Decompressed: 1822
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 105 KB/s], Decompressed: 1863
Downloaded: 1908 file(s) [attempted 1908/8459 = 22%, 42 KB/s], Decompressed: 1904
Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 72 KB/s], Decompressed: 1942
Downloaded: 1987 file(s) [attempted 1987/8459 = 23%, 72 KB/s], Decompressed: 1983
Downloaded: 2026 file(s) [attempted 2026/8459 = 23%, 155 KB/s], Decompressed: 2017
Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 228 KB/s], Decompressed: 2058
Downloaded: 2106 file(s) [attempted 2106/8459 = 24%, 133 KB/s], Decompressed: 2103
Downloaded: 2147 file(s) [attempted 2147/8459 = 25%, 80 KB/s], Decompressed: 2130
Downloaded: 2188 file(s) [attempted 2188/8459 = 25%, 460 KB/s], Decompressed: 2182
Downloaded: 2230 file(s) [attempted 2230/8459 = 26%, 285 KB/s], Decompressed: 2226
Downloaded: 2267 file(s) [attempted 2267/8459 = 26%, 478 KB/s], Decompressed: 2264
Downloaded: 2312 file(s) [attempted 2312/8459 = 27%, 442 KB/s], Decompressed: 2308
Downloaded: 2346 file(s) [attempted 2346/8459 = 27%, 421 KB/s], Decompressed: 2342
Downloaded: 2383 file(s) [attempted 2383/8459 = 28%, 483 KB/s], Decompressed: 2373
Downloaded: 2426 file(s) [attempted 2426/8459 = 28%, 133 KB/s], Decompressed: 2421
Downloaded: 2466 file(s) [attempted 2466/8459 = 29%, 230 KB/s], Decompressed: 2462
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 45 KB/s], Decompressed: 2486
Downloaded: 2544 file(s) [attempted 2544/8459 = 30%, 128 KB/s], Decompressed: 2541
Downloaded: 2585 file(s) [attempted 2585/8459 = 30%, 231 KB/s], Decompressed: 2582
Downloaded: 2626 file(s) [attempted 2626/8459 = 31%, 74 KB/s], Decompressed: 2623
Downloaded: 2665 file(s) [attempted 2665/8459 = 31%, 198 KB/s], Decompressed: 2661
Downloaded: 2706 file(s) [attempted 2706/8459 = 31%, 975 KB/s], Decompressed: 2702
Downloaded: 2743 file(s) [attempted 2743/8459 = 32%, 58 KB/s], Decompressed: 2739
Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 638 KB/s], Decompressed: 2774
Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 41 KB/s], Decompressed: 2825
Downloaded: 2869 file(s) [attempted 2869/8459 = 33%, 862 KB/s], Decompressed: 2859
Downloaded: 2907 file(s) [attempted 2907/8459 = 34%, 392 KB/s], Decompressed: 2904
Downloaded: 2948 file(s) [attempted 2948/8459 = 34%, 260 KB/s], Decompressed: 2941
Downloaded: 2986 file(s) [attempted 2986/8459 = 35%, 442 KB/s], Decompressed: 2982
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 114 KB/s], Decompressed: 3030
Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 131 KB/s], Decompressed: 3068
Downloaded: 3113 file(s) [attempted 3113/8459 = 36%, 253 KB/s], Decompressed: 3109
Downloaded: 3149 file(s) [attempted 3149/8459 = 37%, 93 KB/s], Decompressed: 3140
Downloaded: 3184 file(s) [attempted 3184/8459 = 37%, 176 KB/s], Decompressed: 3181
Downloaded: 3226 file(s) [attempted 3226/8459 = 38%, 539 KB/s], Decompressed: 3222
Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 207 KB/s], Decompressed: 3266
Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 864 KB/s], Decompressed: 3314
Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 67 KB/s], Decompressed: 3355
Downloaded: 3402 file(s) [attempted 3402/8459 = 40%, 442 KB/s], Decompressed: 3393
Downloaded: 3438 file(s) [attempted 3438/8459 = 40%, 110 KB/s], Decompressed: 3434
Downloaded: 3475 file(s) [attempted 3475/8459 = 41%, 1015 KB/s], Decompressed: 3472
Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 191 KB/s], Decompressed: 3516
Downloaded: 3561 file(s) [attempted 3561/8459 = 42%, 110 KB/s], Decompressed: 3554
Downloaded: 3598 file(s) [attempted 3598/8459 = 42%, 219 KB/s], Decompressed: 3592
Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 301 KB/s], Decompressed: 3633
Downloaded: 3681 file(s) [attempted 3681/8459 = 43%, 250 KB/s], Decompressed: 3677
Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 157 KB/s], Decompressed: 3718
Downloaded: 3765 file(s) [attempted 3765/8459 = 44%, 462 KB/s], Decompressed: 3756
Downloaded: 3797 file(s) [attempted 3797/8459 = 44%, 714 KB/s], Decompressed: 3793
Downloaded: 3838 file(s) [attempted 3838/8459 = 45%, 350 KB/s], Decompressed: 3835
Downloaded: 3882 file(s) [attempted 3882/8459 = 45%, 247 KB/s], Decompressed: 3876
Downloaded: 3927 file(s) [attempted 3927/8459 = 46%, 452 KB/s], Decompressed: 3920
Downloaded: 3968 file(s) [attempted 3968/8459 = 46%, 100 KB/s], Decompressed: 3961
Downloaded: 4007 file(s) [attempted 4007/8459 = 47%, 34 KB/s], Decompressed: 4002
Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 716 KB/s], Decompressed: 4040
Downloaded: 4082 file(s) [attempted 4082/8459 = 48%, 725 KB/s], Decompressed: 4078
Downloaded: 4124 file(s) [attempted 4124/8459 = 48%, 148 KB/s], Decompressed: 4119
Downloaded: 4163 file(s) [attempted 4163/8459 = 49%, 174 KB/s], Decompressed: 4160
Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 340 KB/s], Decompressed: 4197
Downloaded: 4242 file(s) [attempted 4242/8459 = 50%, 370 KB/s], Decompressed: 4238
Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 384 KB/s], Decompressed: 4273
Downloaded: 4317 file(s) [attempted 4317/8459 = 51%, 209 KB/s], Decompressed: 4314
Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 586 KB/s], Decompressed: 4355
Downloaded: 4403 file(s) [attempted 4403/8459 = 52%, 698 KB/s], Decompressed: 4396
Downloaded: 4442 file(s) [attempted 4442/8459 = 52%, 249 KB/s], Decompressed: 4433
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 889 KB/s], Decompressed: 4475
Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 57 KB/s], Decompressed: 4516
Downloaded: 4560 file(s) [attempted 4560/8459 = 53%, 483 KB/s], Decompressed: 4557
Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 95 KB/s], Decompressed: 4598
Downloaded: 4639 file(s) [attempted 4639/8459 = 54%, 330 KB/s], Decompressed: 4629
Downloaded: 4678 file(s) [attempted 4678/8459 = 55%, 516 KB/s], Decompressed: 4673
Downloaded: 4721 file(s) [attempted 4721/8459 = 55%, 1668 KB/s], Decompressed: 4718
Downloaded: 4762 file(s) [attempted 4762/8459 = 56%, 398 KB/s], Decompressed: 4759
Downloaded: 4800 file(s) [attempted 4800/8459 = 56%, 563 KB/s], Decompressed: 4786
Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 1928 KB/s], Decompressed: 4834
Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 34 KB/s], Decompressed: 4875
Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 912 KB/s], Decompressed: 4916
Downloaded: 4964 file(s) [attempted 4964/8459 = 58%, 86 KB/s], Decompressed: 4957
Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 150 KB/s], Decompressed: 4998
Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 265 KB/s], Decompressed: 5032
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 1155 KB/s], Decompressed: 5073
Downloaded: 5125 file(s) [attempted 5125/8459 = 60%, 303 KB/s], Decompressed: 5121
Downloaded: 5163 file(s) [attempted 5163/8459 = 61%, 989 KB/s], Decompressed: 5159
Downloaded: 5207 file(s) [attempted 5207/8459 = 61%, 113 KB/s], Decompressed: 5200
Downloaded: 5241 file(s) [attempted 5241/8459 = 61%, 103 KB/s], Decompressed: 5234
Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 464 KB/s], Decompressed: 5275
Downloaded: 5322 file(s) [attempted 5322/8459 = 62%, 110 KB/s], Decompressed: 5313
Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 877 KB/s], Decompressed: 5358
Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 62 KB/s], Decompressed: 5395
Downloaded: 5446 file(s) [attempted 5446/8459 = 64%, 694 KB/s], Decompressed: 5436
Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 190 KB/s], Decompressed: 5477
Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 979 KB/s], Decompressed: 5522
Downloaded: 5571 file(s) [attempted 5571/8459 = 65%, 146 KB/s], Decompressed: 5566
Downloaded: 5607 file(s) [attempted 5607/8459 = 66%, 183 KB/s], Decompressed: 5604
Downloaded: 5648 file(s) [attempted 5648/8459 = 66%, 547 KB/s], Decompressed: 5642
Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 236 KB/s], Decompressed: 5686
Downloaded: 5731 file(s) [attempted 5731/8459 = 67%, 577 KB/s], Decompressed: 5717
Downloaded: 5775 file(s) [attempted 5775/8459 = 68%, 237 KB/s], Decompressed: 5772
Downloaded: 5813 file(s) [attempted 5813/8459 = 68%, 64 KB/s], Decompressed: 5806
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 115 KB/s], Decompressed: 5847
Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 101 KB/s], Decompressed: 5891
Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 883 KB/s], Decompressed: 5912
Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 244 KB/s], Decompressed: 5977
Downloaded: 6020 file(s) [attempted 6020/8459 = 71%, 221 KB/s], Decompressed: 6015
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 361 KB/s], Decompressed: 6053
Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 531 KB/s], Decompressed: 6093
Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 1159 KB/s], Decompressed: 6134
Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 194 KB/s], Decompressed: 6175
Downloaded: 6219 file(s) [attempted 6219/8459 = 73%, 139 KB/s], Decompressed: 6213
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 978 KB/s], Decompressed: 6247
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 355 KB/s], Decompressed: 6292
Downloaded: 6340 file(s) [attempted 6340/8459 = 74%, 56 KB/s], Decompressed: 6329
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 296 KB/s], Decompressed: 6374
Downloaded: 6417 file(s) [attempted 6417/8459 = 75%, 186 KB/s], Decompressed: 6408
Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 1275 KB/s], Decompressed: 6449
Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 1023 KB/s], Decompressed: 6483
Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 90 KB/s], Decompressed: 6528
Downloaded: 6576 file(s) [attempted 6576/8459 = 77%, 454 KB/s], Decompressed: 6566
Downloaded: 6613 file(s) [attempted 6613/8459 = 78%, 520 KB/s], Decompressed: 6610
Downloaded: 6658 file(s) [attempted 6658/8459 = 78%, 74 KB/s], Decompressed: 6651
Downloaded: 6699 file(s) [attempted 6699/8459 = 79%, 94 KB/s], Decompressed: 6692
Downloaded: 6737 file(s) [attempted 6737/8459 = 79%, 302 KB/s], Decompressed: 6730
Downloaded: 6778 file(s) [attempted 6778/8459 = 80%, 141 KB/s], Decompressed: 6774
Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 42 KB/s], Decompressed: 6812
Downloaded: 6856 file(s) [attempted 6856/8459 = 81%, 105 KB/s], Decompressed: 6850
Downloaded: 6898 file(s) [attempted 6898/8459 = 81%, 31 KB/s], Decompressed: 6894
Downloaded: 6935 file(s) [attempted 6935/8459 = 81%, 1221 KB/s], Decompressed: 6932
Downloaded: 6976 file(s) [attempted 6976/8459 = 82%, 566 KB/s], Decompressed: 6966
Downloaded: 7017 file(s) [attempted 7017/8459 = 82%, 121 KB/s], Decompressed: 7010
Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 1207 KB/s], Decompressed: 7055
Downloaded: 7099 file(s) [attempted 7099/8459 = 83%, 537 KB/s], Decompressed: 7089
Downloaded: 7141 file(s) [attempted 7141/8459 = 84%, 1279 KB/s], Decompressed: 7130
Downloaded: 7175 file(s) [attempted 7175/8459 = 84%, 318 KB/s], Decompressed: 7171
Downloaded: 7212 file(s) [attempted 7212/8459 = 85%, 90 KB/s], Decompressed: 7202
Downloaded: 7255 file(s) [attempted 7255/8459 = 85%, 61 KB/s], Decompressed: 7250
Downloaded: 7298 file(s) [attempted 7298/8459 = 86%, 193 KB/s], Decompressed: 7284
Downloaded: 7336 file(s) [attempted 7336/8459 = 86%, 117 KB/s], Decompressed: 7329
Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 66 KB/s], Decompressed: 7360
Downloaded: 7414 file(s) [attempted 7414/8459 = 87%, 169 KB/s], Decompressed: 7407
Downloaded: 7455 file(s) [attempted 7455/8459 = 88%, 255 KB/s], Decompressed: 7452
Downloaded: 7496 file(s) [attempted 7496/8459 = 88%, 21 KB/s], Decompressed: 7493
Downloaded: 7534 file(s) [attempted 7534/8459 = 89%, 122 KB/s], Decompressed: 7531
Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 261 KB/s], Decompressed: 7565
Downloaded: 7614 file(s) [attempted 7614/8459 = 90%, 473 KB/s], Decompressed: 7599
Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 447 KB/s], Decompressed: 7644
Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 879 KB/s], Decompressed: 7688
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 142 KB/s], Decompressed: 7729
Downloaded: 7774 file(s) [attempted 7774/8459 = 91%, 161 KB/s], Decompressed: 7770
Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 801 KB/s], Decompressed: 7811
Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 36 KB/s], Decompressed: 7852
Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 653 KB/s], Decompressed: 7897
Downloaded: 7941 file(s) [attempted 7941/8459 = 93%, 86 KB/s], Decompressed: 7917
Downloaded: 7979 file(s) [attempted 7979/8459 = 94%, 957 KB/s], Decompressed: 7972
Downloaded: 8017 file(s) [attempted 8017/8459 = 94%, 262 KB/s], Decompressed: 8006
Downloaded: 8054 file(s) [attempted 8054/8459 = 95%, 181 KB/s], Decompressed: 8051
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 2614 KB/s], Decompressed: 8099
Downloaded: 8150 file(s) [attempted 8150/8459 = 96%, 819 KB/s], Decompressed: 8147
Downloaded: 8195 file(s) [attempted 8195/8459 = 96%, 93 KB/s], Decompressed: 8194
Downloaded: 8232 file(s) [attempted 8232/8459 = 97%, 297 KB/s], Decompressed: 8222
Downloaded: 8266 file(s) [attempted 8266/8459 = 97%, 1045 KB/s], Decompressed: 8263
Downloaded: 8311 file(s) [attempted 8311/8459 = 98%, 180 KB/s], Decompressed: 8308
Downloaded: 8355 file(s) [attempted 8355/8459 = 98%, 540 KB/s], Decompressed: 8349
Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 125 KB/s], Decompressed: 8396
Downloaded: 8435 file(s) [attempted 8435/8459 = 99%, 113 KB/s], Decompressed: 8431
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 112 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 112 KB/s], Decompressed: 8455
$ lake build
exit_code=Some(1) duration_ms=464362
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (24s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.6s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.7s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/775] Built Iut.Foundations.QualitativeData (2.2s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.9s)
✔ [3389/3394] Built Iut.Stage1.CorollarySchema (32s)
✔ [3390/3397] Built Iut.Stage1.SourceObligations (3.6s)
✔ [3392/3398] Built Iut.Stage1.IUTSourceScaffold (2.0s)
✔ [3394/3398] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (86s)
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 (28s)
⚠ [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.7s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.2s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.6s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.4s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (32s)
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 (168s)
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=2460
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-1369-source
Cloning into '/var/lib/apodeixis/repos/job-1369-source'...
git_checkout exit 0
git checkout 7832205a52316331f46f3fbbac89608c9a2737bf
Note: switching to '7832205a52316331f46f3fbbac89608c9a2737bf'. 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 7832205 Preserve formula gap route input 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: 17 file(s) [attempted 17/8459 = 0%, 5 KB/s], Decompressed: 16 Downloaded: 40 file(s) [attempted 40/8459 = 0%, 17 KB/s], Decompressed: 35 Downloaded: 68 file(s) [attempted 68/8459 = 0%, 97 KB/s], Decompressed: 65 Downloaded: 100 file(s) [attempted 100/8459 = 1%, 74 KB/s], Decompressed: 93 Downloaded: 134 file(s) [attempted 134/8459 = 1%, 395 KB/s], Decompressed: 127 Downloaded: 165 file(s) [attempted 165/8459 = 1%, 389 KB/s], Decompressed: 151 Downloaded: 199 file(s) [attempted 199/8459 = 2%, 428 KB/s], Decompressed: 196 Downloaded: 230 file(s) [attempted 230/8459 = 2%, 248 KB/s], Decompressed: 223 Downloaded: 264 file(s) [attempted 264/8459 = 3%, 842 KB/s], Decompressed: 261 Downloaded: 302 file(s) [attempted 302/8459 = 3%, 27 KB/s], Decompressed: 295 Downloaded: 340 file(s) [attempted 340/8459 = 4%, 106 KB/s], Decompressed: 336 Downloaded: 379 file(s) [attempted 379/8459 = 4%, 123 KB/s], Decompressed: 374 Downloaded: 415 file(s) [attempted 415/8459 = 4%, 99 KB/s], Decompressed: 408 Downloaded: 449 file(s) [attempted 449/8459 = 5%, 67 KB/s], Decompressed: 443 Downloaded: 492 file(s) [attempted 492/8459 = 5%, 82 KB/s], Decompressed: 480 Downloaded: 528 file(s) [attempted 528/8459 = 6%, 216 KB/s], Decompressed: 521 Downloaded: 566 file(s) [attempted 566/8459 = 6%, 168 KB/s], Decompressed: 562 Downloaded: 607 file(s) [attempted 607/8459 = 7%, 747 KB/s], Decompressed: 597 Downloaded: 648 file(s) [attempted 648/8459 = 7%, 315 KB/s], Decompressed: 641 Downloaded: 689 file(s) [attempted 689/8459 = 8%, 162 KB/s], Decompressed: 682 Downloaded: 730 file(s) [attempted 730/8459 = 8%, 121 KB/s], Decompressed: 713 Downloaded: 771 file(s) [attempted 771/8459 = 9%, 1150 KB/s], Decompressed: 765 Downloaded: 812 file(s) [attempted 812/8459 = 9%, 226 KB/s], Decompressed: 795 Downloaded: 857 file(s) [attempted 857/8459 = 10%, 201 KB/s], Decompressed: 850 Downloaded: 898 file(s) [attempted 898/8459 = 10%, 586 KB/s], Decompressed: 895 Downloaded: 937 file(s) [attempted 937/8459 = 11%, 29 KB/s], Decompressed: 932 Downloaded: 973 file(s) [attempted 973/8459 = 11%, 83 KB/s], Decompressed: 970 Downloaded: 1015 file(s) [attempted 1015/8459 = 11%, 207 KB/s], Decompressed: 1011 Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 238 KB/s], Decompressed: 1052 Downloaded: 1100 file(s) [attempted 1100/8459 = 13%, 76 KB/s], Decompressed: 1097 Downloaded: 1142 file(s) [attempted 1142/8459 = 13%, 884 KB/s], Decompressed: 1134 Downloaded: 1179 file(s) [attempted 1179/8459 = 13%, 136 KB/s], Decompressed: 1175 Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 303 KB/s], Decompressed: 1213 Downloaded: 1261 file(s) [attempted 1261/8459 = 14%, 709 KB/s], Decompressed: 1254 Downloaded: 1295 file(s) [attempted 1295/8459 = 15%, 329 KB/s], Decompressed: 1292 Downloaded: 1336 file(s) [attempted 1336/8459 = 15%, 500 KB/s], Decompressed: 1333 Downloaded: 1384 file(s) [attempted 1384/8459 = 16%, 831 KB/s], Decompressed: 1377 Downloaded: 1429 file(s) [attempted 1429/8459 = 16%, 31 KB/s], Decompressed: 1425 Downloaded: 1473 file(s) [attempted 1473/8459 = 17%, 181 KB/s], Decompressed: 1466 Downloaded: 1511 file(s) [attempted 1511/8459 = 17%, 134 KB/s], Decompressed: 1487 Downloaded: 1545 file(s) [attempted 1545/8459 = 18%, 1057 KB/s], Decompressed: 1542 Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 148 KB/s], Decompressed: 1579 Downloaded: 1628 file(s) [attempted 1628/8459 = 19%, 1615 KB/s], Decompressed: 1624 Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 1533 KB/s], Decompressed: 1665 Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 422 KB/s], Decompressed: 1709 Downloaded: 1754 file(s) [attempted 1754/8459 = 20%, 381 KB/s], Decompressed: 1743 Downloaded: 1794 file(s) [attempted 1794/8459 = 21%, 26 KB/s], Decompressed: 1788 Downloaded: 1832 file(s) [attempted 1832/8459 = 21%, 100 KB/s], Decompressed: 1822 Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 105 KB/s], Decompressed: 1863 Downloaded: 1908 file(s) [attempted 1908/8459 = 22%, 42 KB/s], Decompressed: 1904 Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 72 KB/s], Decompressed: 1942 Downloaded: 1987 file(s) [attempted 1987/8459 = 23%, 72 KB/s], Decompressed: 1983 Downloaded: 2026 file(s) [attempted 2026/8459 = 23%, 155 KB/s], Decompressed: 2017 Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 228 KB/s], Decompressed: 2058 Downloaded: 2106 file(s) [attempted 2106/8459 = 24%, 133 KB/s], Decompressed: 2103 Downloaded: 2147 file(s) [attempted 2147/8459 = 25%, 80 KB/s], Decompressed: 2130 Downloaded: 2188 file(s) [attempted 2188/8459 = 25%, 460 KB/s], Decompressed: 2182 Downloaded: 2230 file(s) [attempted 2230/8459 = 26%, 285 KB/s], Decompressed: 2226 Downloaded: 2267 file(s) [attempted 2267/8459 = 26%, 478 KB/s], Decompressed: 2264 Downloaded: 2312 file(s) [attempted 2312/8459 = 27%, 442 KB/s], Decompressed: 2308 Downloaded: 2346 file(s) [attempted 2346/8459 = 27%, 421 KB/s], Decompressed: 2342 Downloaded: 2383 file(s) [attempted 2383/8459 = 28%, 483 KB/s], Decompressed: 2373 Downloaded: 2426 file(s) [attempted 2426/8459 = 28%, 133 KB/s], Decompressed: 2421 Downloaded: 2466 file(s) [attempted 2466/8459 = 29%, 230 KB/s], Decompressed: 2462 Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 45 KB/s], Decompressed: 2486 Downloaded: 2544 file(s) [attempted 2544/8459 = 30%, 128 KB/s], Decompressed: 2541 Downloaded: 2585 file(s) [attempted 2585/8459 = 30%, 231 KB/s], Decompressed: 2582 Downloaded: 2626 file(s) [attempted 2626/8459 = 31%, 74 KB/s], Decompressed: 2623 Downloaded: 2665 file(s) [attempted 2665/8459 = 31%, 198 KB/s], Decompressed: 2661 Downloaded: 2706 file(s) [attempted 2706/8459 = 31%, 975 KB/s], Decompressed: 2702 Downloaded: 2743 file(s) [attempted 2743/8459 = 32%, 58 KB/s], Decompressed: 2739 Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 638 KB/s], Decompressed: 2774 Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 41 KB/s], Decompressed: 2825 Downloaded: 2869 file(s) [attempted 2869/8459 = 33%, 862 KB/s], Decompressed: 2859 Downloaded: 2907 file(s) [attempted 2907/8459 = 34%, 392 KB/s], Decompressed: 2904 Downloaded: 2948 file(s) [attempted 2948/8459 = 34%, 260 KB/s], Decompressed: 2941 Downloaded: 2986 file(s) [attempted 2986/8459 = 35%, 442 KB/s], Decompressed: 2982 Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 114 KB/s], Decompressed: 3030 Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 131 KB/s], Decompressed: 3068 Downloaded: 3113 file(s) [attempted 3113/8459 = 36%, 253 KB/s], Decompressed: 3109 Downloaded: 3149 file(s) [attempted 3149/8459 = 37%, 93 KB/s], Decompressed: 3140 Downloaded: 3184 file(s) [attempted 3184/8459 = 37%, 176 KB/s], Decompressed: 3181 Downloaded: 3226 file(s) [attempted 3226/8459 = 38%, 539 KB/s], Decompressed: 3222 Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 207 KB/s], Decompressed: 3266 Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 864 KB/s], Decompressed: 3314 Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 67 KB/s], Decompressed: 3355 Downloaded: 3402 file(s) [attempted 3402/8459 = 40%, 442 KB/s], Decompressed: 3393 Downloaded: 3438 file(s) [attempted 3438/8459 = 40%, 110 KB/s], Decompressed: 3434 Downloaded: 3475 file(s) [attempted 3475/8459 = 41%, 1015 KB/s], Decompressed: 3472 Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 191 KB/s], Decompressed: 3516 Downloaded: 3561 file(s) [attempted 3561/8459 = 42%, 110 KB/s], Decompressed: 3554 Downloaded: 3598 file(s) [attempted 3598/8459 = 42%, 219 KB/s], Decompressed: 3592 Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 301 KB/s], Decompressed: 3633 Downloaded: 3681 file(s) [attempted 3681/8459 = 43%, 250 KB/s], Decompressed: 3677 Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 157 KB/s], Decompressed: 3718 Downloaded: 3765 file(s) [attempted 3765/8459 = 44%, 462 KB/s], Decompressed: 3756 Downloaded: 3797 file(s) [attempted 3797/8459 = 44%, 714 KB/s], Decompressed: 3793 Downloaded: 3838 file(s) [attempted 3838/8459 = 45%, 350 KB/s], Decompressed: 3835 Downloaded: 3882 file(s) [attempted 3882/8459 = 45%, 247 KB/s], Decompressed: 3876 Downloaded: 3927 file(s) [attempted 3927/8459 = 46%, 452 KB/s], Decompressed: 3920 Downloaded: 3968 file(s) [attempted 3968/8459 = 46%, 100 KB/s], Decompressed: 3961 Downloaded: 4007 file(s) [attempted 4007/8459 = 47%, 34 KB/s], Decompressed: 4002 Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 716 KB/s], Decompressed: 4040 Downloaded: 4082 file(s) [attempted 4082/8459 = 48%, 725 KB/s], Decompressed: 4078 Downloaded: 4124 file(s) [attempted 4124/8459 = 48%, 148 KB/s], Decompressed: 4119 Downloaded: 4163 file(s) [attempted 4163/8459 = 49%, 174 KB/s], Decompressed: 4160 Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 340 KB/s], Decompressed: 4197 Downloaded: 4242 file(s) [attempted 4242/8459 = 50%, 370 KB/s], Decompressed: 4238 Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 384 KB/s], Decompressed: 4273 Downloaded: 4317 file(s) [attempted 4317/8459 = 51%, 209 KB/s], Decompressed: 4314 Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 586 KB/s], Decompressed: 4355 Downloaded: 4403 file(s) [attempted 4403/8459 = 52%, 698 KB/s], Decompressed: 4396 Downloaded: 4442 file(s) [attempted 4442/8459 = 52%, 249 KB/s], Decompressed: 4433 Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 889 KB/s], Decompressed: 4475 Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 57 KB/s], Decompressed: 4516 Downloaded: 4560 file(s) [attempted 4560/8459 = 53%, 483 KB/s], Decompressed: 4557 Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 95 KB/s], Decompressed: 4598 Downloaded: 4639 file(s) [attempted 4639/8459 = 54%, 330 KB/s], Decompressed: 4629 Downloaded: 4678 file(s) [attempted 4678/8459 = 55%, 516 KB/s], Decompressed: 4673 Downloaded: 4721 file(s) [attempted 4721/8459 = 55%, 1668 KB/s], Decompressed: 4718 Downloaded: 4762 file(s) [attempted 4762/8459 = 56%, 398 KB/s], Decompressed: 4759 Downloaded: 4800 file(s) [attempted 4800/8459 = 56%, 563 KB/s], Decompressed: 4786 Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 1928 KB/s], Decompressed: 4834 Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 34 KB/s], Decompressed: 4875 Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 912 KB/s], Decompressed: 4916 Downloaded: 4964 file(s) [attempted 4964/8459 = 58%, 86 KB/s], Decompressed: 4957 Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 150 KB/s], Decompressed: 4998 Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 265 KB/s], Decompressed: 5032 Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 1155 KB/s], Decompressed: 5073 Downloaded: 5125 file(s) [attempted 5125/8459 = 60%, 303 KB/s], Decompressed: 5121 Downloaded: 5163 file(s) [attempted 5163/8459 = 61%, 989 KB/s], Decompressed: 5159 Downloaded: 5207 file(s) [attempted 5207/8459 = 61%, 113 KB/s], Decompressed: 5200 Downloaded: 5241 file(s) [attempted 5241/8459 = 61%, 103 KB/s], Decompressed: 5234 Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 464 KB/s], Decompressed: 5275 Downloaded: 5322 file(s) [attempted 5322/8459 = 62%, 110 KB/s], Decompressed: 5313 Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 877 KB/s], Decompressed: 5358 Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 62 KB/s], Decompressed: 5395 Downloaded: 5446 file(s) [attempted 5446/8459 = 64%, 694 KB/s], Decompressed: 5436 Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 190 KB/s], Decompressed: 5477 Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 979 KB/s], Decompressed: 5522 Downloaded: 5571 file(s) [attempted 5571/8459 = 65%, 146 KB/s], Decompressed: 5566 Downloaded: 5607 file(s) [attempted 5607/8459 = 66%, 183 KB/s], Decompressed: 5604 Downloaded: 5648 file(s) [attempted 5648/8459 = 66%, 547 KB/s], Decompressed: 5642 Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 236 KB/s], Decompressed: 5686 Downloaded: 5731 file(s) [attempted 5731/8459 = 67%, 577 KB/s], Decompressed: 5717 Downloaded: 5775 file(s) [attempted 5775/8459 = 68%, 237 KB/s], Decompressed: 5772 Downloaded: 5813 file(s) [attempted 5813/8459 = 68%, 64 KB/s], Decompressed: 5806 Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 115 KB/s], Decompressed: 5847 Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 101 KB/s], Decompressed: 5891 Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 883 KB/s], Decompressed: 5912 Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 244 KB/s], Decompressed: 5977 Downloaded: 6020 file(s) [attempted 6020/8459 = 71%, 221 KB/s], Decompressed: 6015 Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 361 KB/s], Decompressed: 6053 Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 531 KB/s], Decompressed: 6093 Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 1159 KB/s], Decompressed: 6134 Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 194 KB/s], Decompressed: 6175 Downloaded: 6219 file(s) [attempted 6219/8459 = 73%, 139 KB/s], Decompressed: 6213 Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 978 KB/s], Decompressed: 6247 Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 355 KB/s], Decompressed: 6292 Downloaded: 6340 file(s) [attempted 6340/8459 = 74%, 56 KB/s], Decompressed: 6329 Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 296 KB/s], Decompressed: 6374 Downloaded: 6417 file(s) [attempted 6417/8459 = 75%, 186 KB/s], Decompressed: 6408 Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 1275 KB/s], Decompressed: 6449 Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 1023 KB/s], Decompressed: 6483 Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 90 KB/s], Decompressed: 6528 Downloaded: 6576 file(s) [attempted 6576/8459 = 77%, 454 KB/s], Decompressed: 6566 Downloaded: 6613 file(s) [attempted 6613/8459 = 78%, 520 KB/s], Decompressed: 6610 Downloaded: 6658 file(s) [attempted 6658/8459 = 78%, 74 KB/s], Decompressed: 6651 Downloaded: 6699 file(s) [attempted 6699/8459 = 79%, 94 KB/s], Decompressed: 6692 Downloaded: 6737 file(s) [attempted 6737/8459 = 79%, 302 KB/s], Decompressed: 6730 Downloaded: 6778 file(s) [attempted 6778/8459 = 80%, 141 KB/s], Decompressed: 6774 Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 42 KB/s], Decompressed: 6812 Downloaded: 6856 file(s) [attempted 6856/8459 = 81%, 105 KB/s], Decompressed: 6850 Downloaded: 6898 file(s) [attempted 6898/8459 = 81%, 31 KB/s], Decompressed: 6894 Downloaded: 6935 file(s) [attempted 6935/8459 = 81%, 1221 KB/s], Decompressed: 6932 Downloaded: 6976 file(s) [attempted 6976/8459 = 82%, 566 KB/s], Decompressed: 6966 Downloaded: 7017 file(s) [attempted 7017/8459 = 82%, 121 KB/s], Decompressed: 7010 Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 1207 KB/s], Decompressed: 7055 Downloaded: 7099 file(s) [attempted 7099/8459 = 83%, 537 KB/s], Decompressed: 7089 Downloaded: 7141 file(s) [attempted 7141/8459 = 84%, 1279 KB/s], Decompressed: 7130 Downloaded: 7175 file(s) [attempted 7175/8459 = 84%, 318 KB/s], Decompressed: 7171 Downloaded: 7212 file(s) [attempted 7212/8459 = 85%, 90 KB/s], Decompressed: 7202 Downloaded: 7255 file(s) [attempted 7255/8459 = 85%, 61 KB/s], Decompressed: 7250 Downloaded: 7298 file(s) [attempted 7298/8459 = 86%, 193 KB/s], Decompressed: 7284 Downloaded: 7336 file(s) [attempted 7336/8459 = 86%, 117 KB/s], Decompressed: 7329 Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 66 KB/s], Decompressed: 7360 Downloaded: 7414 file(s) [attempted 7414/8459 = 87%, 169 KB/s], Decompressed: 7407 Downloaded: 7455 file(s) [attempted 7455/8459 = 88%, 255 KB/s], Decompressed: 7452 Downloaded: 7496 file(s) [attempted 7496/8459 = 88%, 21 KB/s], Decompressed: 7493 Downloaded: 7534 file(s) [attempted 7534/8459 = 89%, 122 KB/s], Decompressed: 7531 Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 261 KB/s], Decompressed: 7565 Downloaded: 7614 file(s) [attempted 7614/8459 = 90%, 473 KB/s], Decompressed: 7599 Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 447 KB/s], Decompressed: 7644 Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 879 KB/s], Decompressed: 7688 Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 142 KB/s], Decompressed: 7729 Downloaded: 7774 file(s) [attempted 7774/8459 = 91%, 161 KB/s], Decompressed: 7770 Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 801 KB/s], Decompressed: 7811 Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 36 KB/s], Decompressed: 7852 Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 653 KB/s], Decompressed: 7897 Downloaded: 7941 file(s) [attempted 7941/8459 = 93%, 86 KB/s], Decompressed: 7917 Downloaded: 7979 file(s) [attempted 7979/8459 = 94%, 957 KB/s], Decompressed: 7972 Downloaded: 8017 file(s) [attempted 8017/8459 = 94%, 262 KB/s], Decompressed: 8006 Downloaded: 8054 file(s) [attempted 8054/8459 = 95%, 181 KB/s], Decompressed: 8051 Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 2614 KB/s], Decompressed: 8099 Downloaded: 8150 file(s) [attempted 8150/8459 = 96%, 819 KB/s], Decompressed: 8147 Downloaded: 8195 file(s) [attempted 8195/8459 = 96%, 93 KB/s], Decompressed: 8194 Downloaded: 8232 file(s) [attempted 8232/8459 = 97%, 297 KB/s], Decompressed: 8222 Downloaded: 8266 file(s) [attempted 8266/8459 = 97%, 1045 KB/s], Decompressed: 8263 Downloaded: 8311 file(s) [attempted 8311/8459 = 98%, 180 KB/s], Decompressed: 8308 Downloaded: 8355 file(s) [attempted 8355/8459 = 98%, 540 KB/s], Decompressed: 8349 Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 125 KB/s], Decompressed: 8396 Downloaded: 8435 file(s) [attempted 8435/8459 = 99%, 113 KB/s], Decompressed: 8431 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 112 KB/s], Decompressed: 8455 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 112 KB/s], Decompressed: 8455
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (24s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.6s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.7s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/775] Built Iut.Foundations.QualitativeData (2.2s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.9s)
✔ [3389/3394] Built Iut.Stage1.CorollarySchema (32s)
✔ [3390/3397] Built Iut.Stage1.SourceObligations (3.6s)
✔ [3392/3398] Built Iut.Stage1.IUTSourceScaffold (2.0s)
✔ [3394/3398] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (86s)
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 (28s)
⚠ [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.7s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.2s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.6s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.4s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (32s)
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 (168s)
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`