Verification run
Run 1062
failed commit
c1626e83508e toolchain lean-v4-30-0 prover lean took 11m 16s · 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-1363-source
exit_code=Some(0) duration_ms=3511
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1363-source'...
$ git checkout c1626e83508e509c830874d36bec33b0d87fbcb3
exit_code=Some(0) duration_ms=149
stderr:
Note: switching to 'c1626e83508e509c830874d36bec33b0d87fbcb3'.
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 c1626e8 Lower product hull CTheta surface
Resolved source revision: c1626e83508e509c830874d36bec33b0d87fbcb3
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=c1626e83508e509c830874d36bec33b0d87fbcb3 provenance={"branch":"master","checked_out_revision":"c1626e83508e509c830874d36bec33b0d87fbcb3","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"c1626e83508e509c830874d36bec33b0d87fbcb3","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=33229
stdout:
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
Downloaded: 1 file(s) [attempted 1/8459 = 0%, 11 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 2 KB/s], Decompressed: 12
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 16 KB/s], Decompressed: 34
Downloaded: 64 file(s) [attempted 64/8459 = 0%, 221 KB/s], Decompressed: 57
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 301 KB/s], Decompressed: 82
Downloaded: 117 file(s) [attempted 117/8459 = 1%, 25 KB/s], Decompressed: 114
Downloaded: 148 file(s) [attempted 148/8459 = 1%, 431 KB/s], Decompressed: 145
Downloaded: 182 file(s) [attempted 182/8459 = 2%, 250 KB/s], Decompressed: 179
Downloaded: 216 file(s) [attempted 216/8459 = 2%, 327 KB/s], Decompressed: 210
Downloaded: 256 file(s) [attempted 256/8459 = 3%, 325 KB/s], Decompressed: 247
Downloaded: 288 file(s) [attempted 288/8459 = 3%, 186 KB/s], Decompressed: 282
Downloaded: 323 file(s) [attempted 323/8459 = 3%, 481 KB/s], Decompressed: 312
Downloaded: 359 file(s) [attempted 359/8459 = 4%, 879 KB/s], Decompressed: 353
Downloaded: 398 file(s) [attempted 398/8459 = 4%, 155 KB/s], Decompressed: 391
Downloaded: 439 file(s) [attempted 439/8459 = 5%, 120 KB/s], Decompressed: 432
Downloaded: 477 file(s) [attempted 477/8459 = 5%, 92 KB/s], Decompressed: 473
Downloaded: 514 file(s) [attempted 514/8459 = 6%, 589 KB/s], Decompressed: 508
Downloaded: 556 file(s) [attempted 556/8459 = 6%, 252 KB/s], Decompressed: 552
Downloaded: 600 file(s) [attempted 600/8459 = 7%, 893 KB/s], Decompressed: 597
Downloaded: 642 file(s) [attempted 642/8459 = 7%, 217 KB/s], Decompressed: 631
Downloaded: 674 file(s) [attempted 674/8459 = 7%, 62 KB/s], Decompressed: 665
Downloaded: 711 file(s) [attempted 711/8459 = 8%, 1133 KB/s], Decompressed: 706
Downloaded: 754 file(s) [attempted 754/8459 = 8%, 124 KB/s], Decompressed: 747
Downloaded: 799 file(s) [attempted 799/8459 = 9%, 512 KB/s], Decompressed: 795
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 389 KB/s], Decompressed: 833
Downloaded: 872 file(s) [attempted 872/8459 = 10%, 1652 KB/s], Decompressed: 864
Downloaded: 915 file(s) [attempted 915/8459 = 10%, 976 KB/s], Decompressed: 912
Downloaded: 957 file(s) [attempted 957/8459 = 11%, 141 KB/s], Decompressed: 953
Downloaded: 997 file(s) [attempted 997/8459 = 11%, 136 KB/s], Decompressed: 994
Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 527 KB/s], Decompressed: 1032
Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 121 KB/s], Decompressed: 1069
Downloaded: 1117 file(s) [attempted 1117/8459 = 13%, 1256 KB/s], Decompressed: 1114
Downloaded: 1162 file(s) [attempted 1162/8459 = 13%, 426 KB/s], Decompressed: 1155
Downloaded: 1196 file(s) [attempted 1196/8459 = 14%, 27 KB/s], Decompressed: 1189
Downloaded: 1234 file(s) [attempted 1234/8459 = 14%, 101 KB/s], Decompressed: 1230
Downloaded: 1275 file(s) [attempted 1275/8459 = 15%, 1128 KB/s], Decompressed: 1268
Downloaded: 1319 file(s) [attempted 1319/8459 = 15%, 71 KB/s], Decompressed: 1316
Downloaded: 1367 file(s) [attempted 1367/8459 = 16%, 299 KB/s], Decompressed: 1360
Downloaded: 1408 file(s) [attempted 1408/8459 = 16%, 362 KB/s], Decompressed: 1401
Downloaded: 1443 file(s) [attempted 1443/8459 = 17%, 126 KB/s], Decompressed: 1439
Downloaded: 1487 file(s) [attempted 1487/8459 = 17%, 63 KB/s], Decompressed: 1480
Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 136 KB/s], Decompressed: 1518
Downloaded: 1566 file(s) [attempted 1566/8459 = 18%, 229 KB/s], Decompressed: 1555
Downloaded: 1609 file(s) [attempted 1609/8459 = 19%, 58 KB/s], Decompressed: 1600
Downloaded: 1648 file(s) [attempted 1648/8459 = 19%, 155 KB/s], Decompressed: 1644
Downloaded: 1685 file(s) [attempted 1685/8459 = 19%, 139 KB/s], Decompressed: 1678
Downloaded: 1723 file(s) [attempted 1723/8459 = 20%, 84 KB/s], Decompressed: 1716
Downloaded: 1767 file(s) [attempted 1767/8459 = 20%, 480 KB/s], Decompressed: 1764
Downloaded: 1812 file(s) [attempted 1812/8459 = 21%, 95 KB/s], Decompressed: 1802
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 25 KB/s], Decompressed: 1853
Downloaded: 1898 file(s) [attempted 1898/8459 = 22%, 43 KB/s], Decompressed: 1894
Downloaded: 1928 file(s) [attempted 1928/8459 = 22%, 172 KB/s], Decompressed: 1921
Downloaded: 1963 file(s) [attempted 1963/8459 = 23%, 885 KB/s], Decompressed: 1959
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 25 KB/s], Decompressed: 2007
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 38 KB/s], Decompressed: 2055
Downloaded: 2105 file(s) [attempted 2105/8459 = 24%, 438 KB/s], Decompressed: 2099
Downloaded: 2144 file(s) [attempted 2144/8459 = 25%, 345 KB/s], Decompressed: 2140
Downloaded: 2176 file(s) [attempted 2176/8459 = 25%, 83 KB/s], Decompressed: 2168
Downloaded: 2217 file(s) [attempted 2217/8459 = 26%, 421 KB/s], Decompressed: 2212
Downloaded: 2260 file(s) [attempted 2260/8459 = 26%, 564 KB/s], Decompressed: 2257
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 188 KB/s], Decompressed: 2298
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 390 KB/s], Decompressed: 2336
Downloaded: 2383 file(s) [attempted 2383/8459 = 28%, 682 KB/s], Decompressed: 2377
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 36 KB/s], Decompressed: 2414
Downloaded: 2459 file(s) [attempted 2459/8459 = 29%, 444 KB/s], Decompressed: 2452
Downloaded: 2496 file(s) [attempted 2496/8459 = 29%, 47 KB/s], Decompressed: 2493
Downloaded: 2538 file(s) [attempted 2538/8459 = 30%, 333 KB/s], Decompressed: 2534
Downloaded: 2582 file(s) [attempted 2582/8459 = 30%, 1545 KB/s], Decompressed: 2575
Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 22 KB/s], Decompressed: 2616
Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 553 KB/s], Decompressed: 2650
Downloaded: 2698 file(s) [attempted 2698/8459 = 31%, 62 KB/s], Decompressed: 2695
Downloaded: 2746 file(s) [attempted 2746/8459 = 32%, 96 KB/s], Decompressed: 2743
Downloaded: 2794 file(s) [attempted 2794/8459 = 33%, 1713 KB/s], Decompressed: 2787
Downloaded: 2836 file(s) [attempted 2836/8459 = 33%, 95 KB/s], Decompressed: 2828
Downloaded: 2869 file(s) [attempted 2869/8459 = 33%, 444 KB/s], Decompressed: 2866
Downloaded: 2904 file(s) [attempted 2904/8459 = 34%, 117 KB/s], Decompressed: 2900
Downloaded: 2948 file(s) [attempted 2948/8459 = 34%, 231 KB/s], Decompressed: 2945
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 192 KB/s], Decompressed: 2989
Downloaded: 3038 file(s) [attempted 3038/8459 = 35%, 1076 KB/s], Decompressed: 3030
Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 366 KB/s], Decompressed: 3064
Downloaded: 3106 file(s) [attempted 3106/8459 = 36%, 69 KB/s], Decompressed: 3102
Downloaded: 3150 file(s) [attempted 3150/8459 = 37%, 89 KB/s], Decompressed: 3147
Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 207 KB/s], Decompressed: 3195
Downloaded: 3242 file(s) [attempted 3242/8459 = 38%, 1219 KB/s], Decompressed: 3236
Downloaded: 3280 file(s) [attempted 3280/8459 = 38%, 152 KB/s], Decompressed: 3277
Downloaded: 3314 file(s) [attempted 3314/8459 = 39%, 161 KB/s], Decompressed: 3307
Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 389 KB/s], Decompressed: 3352
Downloaded: 3401 file(s) [attempted 3401/8459 = 40%, 112 KB/s], Decompressed: 3396
Downloaded: 3444 file(s) [attempted 3444/8459 = 40%, 262 KB/s], Decompressed: 3438
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 158 KB/s], Decompressed: 3475
Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 441 KB/s], Decompressed: 3513
Downloaded: 3561 file(s) [attempted 3561/8459 = 42%, 234 KB/s], Decompressed: 3557
Downloaded: 3602 file(s) [attempted 3602/8459 = 42%, 401 KB/s], Decompressed: 3595
Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 704 KB/s], Decompressed: 3646
Downloaded: 3688 file(s) [attempted 3688/8459 = 43%, 53 KB/s], Decompressed: 3681
Downloaded: 3724 file(s) [attempted 3724/8459 = 44%, 1095 KB/s], Decompressed: 3718
Downloaded: 3763 file(s) [attempted 3763/8459 = 44%, 109 KB/s], Decompressed: 3759
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 50 KB/s], Decompressed: 3804
Downloaded: 3852 file(s) [attempted 3852/8459 = 45%, 94 KB/s], Decompressed: 3848
Downloaded: 3896 file(s) [attempted 3896/8459 = 46%, 144 KB/s], Decompressed: 3889
Downloaded: 3930 file(s) [attempted 3930/8459 = 46%, 176 KB/s], Decompressed: 3924
Downloaded: 3971 file(s) [attempted 3971/8459 = 46%, 185 KB/s], Decompressed: 3968
Downloaded: 4012 file(s) [attempted 4012/8459 = 47%, 927 KB/s], Decompressed: 4009
Downloaded: 4054 file(s) [attempted 4054/8459 = 47%, 1002 KB/s], Decompressed: 4050
Downloaded: 4101 file(s) [attempted 4101/8459 = 48%, 364 KB/s], Decompressed: 4098
Downloaded: 4149 file(s) [attempted 4149/8459 = 49%, 47 KB/s], Decompressed: 4143
Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 398 KB/s], Decompressed: 4187
Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 75 KB/s], Decompressed: 4225
Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 1286 KB/s], Decompressed: 4266
Downloaded: 4310 file(s) [attempted 4310/8459 = 50%, 89 KB/s], Decompressed: 4303
Downloaded: 4351 file(s) [attempted 4351/8459 = 51%, 505 KB/s], Decompressed: 4348
Downloaded: 4392 file(s) [attempted 4392/8459 = 51%, 220 KB/s], Decompressed: 4382
Downloaded: 4427 file(s) [attempted 4427/8459 = 52%, 111 KB/s], Decompressed: 4420
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 462 KB/s], Decompressed: 4461
Downloaded: 4512 file(s) [attempted 4512/8459 = 53%, 75 KB/s], Decompressed: 4505
Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 304 KB/s], Decompressed: 4546
Downloaded: 4591 file(s) [attempted 4591/8459 = 54%, 391 KB/s], Decompressed: 4587
Downloaded: 4632 file(s) [attempted 4632/8459 = 54%, 1162 KB/s], Decompressed: 4625
Downloaded: 4673 file(s) [attempted 4673/8459 = 55%, 551 KB/s], Decompressed: 4666
Downloaded: 4714 file(s) [attempted 4714/8459 = 55%, 26 KB/s], Decompressed: 4707
Downloaded: 4752 file(s) [attempted 4752/8459 = 56%, 83 KB/s], Decompressed: 4748
Downloaded: 4796 file(s) [attempted 4796/8459 = 56%, 48 KB/s], Decompressed: 4789
Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 408 KB/s], Decompressed: 4834
Downloaded: 4875 file(s) [attempted 4875/8459 = 57%, 188 KB/s], Decompressed: 4868
Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 938 KB/s], Decompressed: 4916
Downloaded: 4965 file(s) [attempted 4965/8459 = 58%, 87 KB/s], Decompressed: 4960
Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 145 KB/s], Decompressed: 4998
Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 186 KB/s], Decompressed: 5039
Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 560 KB/s], Decompressed: 5077
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 50 KB/s], Decompressed: 5115
Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 1236 KB/s], Decompressed: 5159
Downloaded: 5203 file(s) [attempted 5203/8459 = 61%, 89 KB/s], Decompressed: 5197
Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 74 KB/s], Decompressed: 5241
Downloaded: 5290 file(s) [attempted 5290/8459 = 62%, 493 KB/s], Decompressed: 5282
Downloaded: 5325 file(s) [attempted 5325/8459 = 62%, 49 KB/s], Decompressed: 5320
Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 417 KB/s], Decompressed: 5354
Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 396 KB/s], Decompressed: 5399
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 999 KB/s], Decompressed: 5440
Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 1076 KB/s], Decompressed: 5477
Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 82 KB/s], Decompressed: 5522
Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 80 KB/s], Decompressed: 5563
Downloaded: 5607 file(s) [attempted 5607/8459 = 66%, 278 KB/s], Decompressed: 5600
Downloaded: 5648 file(s) [attempted 5648/8459 = 66%, 1165 KB/s], Decompressed: 5645
Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 574 KB/s], Decompressed: 5686
Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 284 KB/s], Decompressed: 5720
Downloaded: 5762 file(s) [attempted 5762/8459 = 68%, 467 KB/s], Decompressed: 5758
Downloaded: 5809 file(s) [attempted 5809/8459 = 68%, 114 KB/s], Decompressed: 5806
Downloaded: 5854 file(s) [attempted 5854/8459 = 69%, 94 KB/s], Decompressed: 5850
Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 175 KB/s], Decompressed: 5891
Downloaded: 5930 file(s) [attempted 5930/8459 = 70%, 153 KB/s], Decompressed: 5919
Downloaded: 5967 file(s) [attempted 5967/8459 = 70%, 537 KB/s], Decompressed: 5963
Downloaded: 6011 file(s) [attempted 6011/8459 = 71%, 129 KB/s], Decompressed: 6008
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 2102 KB/s], Decompressed: 6049
Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 545 KB/s], Decompressed: 6090
Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 145 KB/s], Decompressed: 6131
Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 546 KB/s], Decompressed: 6172
Downloaded: 6216 file(s) [attempted 6216/8459 = 73%, 476 KB/s], Decompressed: 6213
Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 83 KB/s], Decompressed: 6247
Downloaded: 6299 file(s) [attempted 6299/8459 = 74%, 26 KB/s], Decompressed: 6295
Downloaded: 6337 file(s) [attempted 6337/8459 = 74%, 50 KB/s], Decompressed: 6333
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 293 KB/s], Decompressed: 6374
Downloaded: 6416 file(s) [attempted 6416/8459 = 75%, 52 KB/s], Decompressed: 6412
Downloaded: 6459 file(s) [attempted 6459/8459 = 76%, 933 KB/s], Decompressed: 6456
Downloaded: 6498 file(s) [attempted 6498/8459 = 76%, 962 KB/s], Decompressed: 6490
Downloaded: 6536 file(s) [attempted 6536/8459 = 77%, 193 KB/s], Decompressed: 6531
Downloaded: 6572 file(s) [attempted 6572/8459 = 77%, 106 KB/s], Decompressed: 6569
Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 351 KB/s], Decompressed: 6613
Downloaded: 6661 file(s) [attempted 6661/8459 = 78%, 70 KB/s], Decompressed: 6658
Downloaded: 6702 file(s) [attempted 6702/8459 = 79%, 59 KB/s], Decompressed: 6699
Downloaded: 6740 file(s) [attempted 6740/8459 = 79%, 95 KB/s], Decompressed: 6737
Downloaded: 6781 file(s) [attempted 6781/8459 = 80%, 963 KB/s], Decompressed: 6774
Downloaded: 6822 file(s) [attempted 6822/8459 = 80%, 127 KB/s], Decompressed: 6819
Downloaded: 6863 file(s) [attempted 6863/8459 = 81%, 202 KB/s], Decompressed: 6860
Downloaded: 6904 file(s) [attempted 6904/8459 = 81%, 434 KB/s], Decompressed: 6901
Downloaded: 6945 file(s) [attempted 6945/8459 = 82%, 402 KB/s], Decompressed: 6942
Downloaded: 6983 file(s) [attempted 6983/8459 = 82%, 377 KB/s], Decompressed: 6980
Downloaded: 7028 file(s) [attempted 7028/8459 = 83%, 673 KB/s], Decompressed: 7024
Downloaded: 7072 file(s) [attempted 7072/8459 = 83%, 779 KB/s], Decompressed: 7067
Downloaded: 7110 file(s) [attempted 7110/8459 = 84%, 125 KB/s], Decompressed: 7103
Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 72 KB/s], Decompressed: 7141
Downloaded: 7186 file(s) [attempted 7186/8459 = 84%, 1292 KB/s], Decompressed: 7182
Downloaded: 7227 file(s) [attempted 7227/8459 = 85%, 315 KB/s], Decompressed: 7223
Downloaded: 7267 file(s) [attempted 7267/8459 = 85%, 276 KB/s], Decompressed: 7264
Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 2098 KB/s], Decompressed: 7301
Downloaded: 7343 file(s) [attempted 7343/8459 = 86%, 54 KB/s], Decompressed: 7339
Downloaded: 7384 file(s) [attempted 7384/8459 = 87%, 182 KB/s], Decompressed: 7377
Downloaded: 7425 file(s) [attempted 7425/8459 = 87%, 222 KB/s], Decompressed: 7421
Downloaded: 7466 file(s) [attempted 7466/8459 = 88%, 371 KB/s], Decompressed: 7459
Downloaded: 7505 file(s) [attempted 7505/8459 = 88%, 241 KB/s], Decompressed: 7500
Downloaded: 7544 file(s) [attempted 7544/8459 = 89%, 224 KB/s], Decompressed: 7538
Downloaded: 7582 file(s) [attempted 7582/8459 = 89%, 44 KB/s], Decompressed: 7575
Downloaded: 7623 file(s) [attempted 7623/8459 = 90%, 101 KB/s], Decompressed: 7616
Downloaded: 7664 file(s) [attempted 7664/8459 = 90%, 184 KB/s], Decompressed: 7657
Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 89 KB/s], Decompressed: 7702
Downloaded: 7750 file(s) [attempted 7750/8459 = 91%, 223 KB/s], Decompressed: 7743
Downloaded: 7787 file(s) [attempted 7787/8459 = 92%, 130 KB/s], Decompressed: 7780
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 158 KB/s], Decompressed: 7822
Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 247 KB/s], Decompressed: 7856
Downloaded: 7911 file(s) [attempted 7911/8459 = 93%, 591 KB/s], Decompressed: 7900
Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 516 KB/s], Decompressed: 7945
Downloaded: 7991 file(s) [attempted 7991/8459 = 94%, 698 KB/s], Decompressed: 7982
Downloaded: 8024 file(s) [attempted 8024/8459 = 94%, 162 KB/s], Decompressed: 8020
Downloaded: 8068 file(s) [attempted 8068/8459 = 95%, 960 KB/s], Decompressed: 8061
Downloaded: 8116 file(s) [attempted 8116/8459 = 95%, 121 KB/s], Decompressed: 8112
Downloaded: 8160 file(s) [attempted 8160/8459 = 96%, 122 KB/s], Decompressed: 8154
Downloaded: 8200 file(s) [attempted 8200/8459 = 96%, 348 KB/s], Decompressed: 8191
Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 1456 KB/s], Decompressed: 8232
Downloaded: 8270 file(s) [attempted 8270/8459 = 97%, 563 KB/s], Decompressed: 8266
Downloaded: 8312 file(s) [attempted 8312/8459 = 98%, 474 KB/s], Decompressed: 8304
Downloaded: 8355 file(s) [attempted 8355/8459 = 98%, 201 KB/s], Decompressed: 8352
Downloaded: 8396 file(s) [attempted 8396/8459 = 99%, 83 KB/s], Decompressed: 8393
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 306 KB/s], Decompressed: 8434
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 115 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 115 KB/s], Decompressed: 8455
$ lake build
exit_code=Some(1) duration_ms=454394
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (23s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.6s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/772] Built Iut.Foundations.QualitativeData (1.0s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.5s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.5s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (32s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.1s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.6s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (82s)
warning: Iut/Stage1/IUTStage1SourceCore.lean:19880:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotient_card_eq_pow_finrank`:
[FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [FiniteDimensional ℚ_[p] K] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20063:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotientCosetHaarCharacterEndpoint`:
[FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [FiniteDimensional ℚ_[p] K] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20130:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.unitBallHaarCharacterEndpoint`:
[FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [FiniteDimensional ℚ_[p] K] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20532:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20533:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20537:4: `have hinteger_eq : (integer : ℚ_[p]) = (p : ℚ_[p]) * (preimage : ℚ_[p]) := by
simpa [IUTStage1PadicIntegerUnitBallSource.padicIntAddEquivIntegerAddSubgroup, hpreimage_eq] using
hpoint_eq.symm` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20547:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20572:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20573:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20576:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20577:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20578:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
✔ [3411/3425] Built Iut.Stage1.IUTStage1Remark312Absorption (21s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.7s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.2s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.6s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.7s)
⚠ [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 (177s)
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=1189
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-1363-source
Cloning into '/var/lib/apodeixis/repos/job-1363-source'...
git_checkout exit 0
git checkout c1626e83508e509c830874d36bec33b0d87fbcb3
Note: switching to 'c1626e83508e509c830874d36bec33b0d87fbcb3'. 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 c1626e8 Lower product hull CTheta surface
lake_cache exit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache Decompressed 8459 file(s) Already decompressed 8459 file(s)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes Downloaded: 1 file(s) [attempted 1/8459 = 0%, 11 KB/s], Decompressed: 0 Downloaded: 15 file(s) [attempted 15/8459 = 0%, 2 KB/s], Decompressed: 12 Downloaded: 37 file(s) [attempted 37/8459 = 0%, 16 KB/s], Decompressed: 34 Downloaded: 64 file(s) [attempted 64/8459 = 0%, 221 KB/s], Decompressed: 57 Downloaded: 86 file(s) [attempted 86/8459 = 1%, 301 KB/s], Decompressed: 82 Downloaded: 117 file(s) [attempted 117/8459 = 1%, 25 KB/s], Decompressed: 114 Downloaded: 148 file(s) [attempted 148/8459 = 1%, 431 KB/s], Decompressed: 145 Downloaded: 182 file(s) [attempted 182/8459 = 2%, 250 KB/s], Decompressed: 179 Downloaded: 216 file(s) [attempted 216/8459 = 2%, 327 KB/s], Decompressed: 210 Downloaded: 256 file(s) [attempted 256/8459 = 3%, 325 KB/s], Decompressed: 247 Downloaded: 288 file(s) [attempted 288/8459 = 3%, 186 KB/s], Decompressed: 282 Downloaded: 323 file(s) [attempted 323/8459 = 3%, 481 KB/s], Decompressed: 312 Downloaded: 359 file(s) [attempted 359/8459 = 4%, 879 KB/s], Decompressed: 353 Downloaded: 398 file(s) [attempted 398/8459 = 4%, 155 KB/s], Decompressed: 391 Downloaded: 439 file(s) [attempted 439/8459 = 5%, 120 KB/s], Decompressed: 432 Downloaded: 477 file(s) [attempted 477/8459 = 5%, 92 KB/s], Decompressed: 473 Downloaded: 514 file(s) [attempted 514/8459 = 6%, 589 KB/s], Decompressed: 508 Downloaded: 556 file(s) [attempted 556/8459 = 6%, 252 KB/s], Decompressed: 552 Downloaded: 600 file(s) [attempted 600/8459 = 7%, 893 KB/s], Decompressed: 597 Downloaded: 642 file(s) [attempted 642/8459 = 7%, 217 KB/s], Decompressed: 631 Downloaded: 674 file(s) [attempted 674/8459 = 7%, 62 KB/s], Decompressed: 665 Downloaded: 711 file(s) [attempted 711/8459 = 8%, 1133 KB/s], Decompressed: 706 Downloaded: 754 file(s) [attempted 754/8459 = 8%, 124 KB/s], Decompressed: 747 Downloaded: 799 file(s) [attempted 799/8459 = 9%, 512 KB/s], Decompressed: 795 Downloaded: 836 file(s) [attempted 836/8459 = 9%, 389 KB/s], Decompressed: 833 Downloaded: 872 file(s) [attempted 872/8459 = 10%, 1652 KB/s], Decompressed: 864 Downloaded: 915 file(s) [attempted 915/8459 = 10%, 976 KB/s], Decompressed: 912 Downloaded: 957 file(s) [attempted 957/8459 = 11%, 141 KB/s], Decompressed: 953 Downloaded: 997 file(s) [attempted 997/8459 = 11%, 136 KB/s], Decompressed: 994 Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 527 KB/s], Decompressed: 1032 Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 121 KB/s], Decompressed: 1069 Downloaded: 1117 file(s) [attempted 1117/8459 = 13%, 1256 KB/s], Decompressed: 1114 Downloaded: 1162 file(s) [attempted 1162/8459 = 13%, 426 KB/s], Decompressed: 1155 Downloaded: 1196 file(s) [attempted 1196/8459 = 14%, 27 KB/s], Decompressed: 1189 Downloaded: 1234 file(s) [attempted 1234/8459 = 14%, 101 KB/s], Decompressed: 1230 Downloaded: 1275 file(s) [attempted 1275/8459 = 15%, 1128 KB/s], Decompressed: 1268 Downloaded: 1319 file(s) [attempted 1319/8459 = 15%, 71 KB/s], Decompressed: 1316 Downloaded: 1367 file(s) [attempted 1367/8459 = 16%, 299 KB/s], Decompressed: 1360 Downloaded: 1408 file(s) [attempted 1408/8459 = 16%, 362 KB/s], Decompressed: 1401 Downloaded: 1443 file(s) [attempted 1443/8459 = 17%, 126 KB/s], Decompressed: 1439 Downloaded: 1487 file(s) [attempted 1487/8459 = 17%, 63 KB/s], Decompressed: 1480 Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 136 KB/s], Decompressed: 1518 Downloaded: 1566 file(s) [attempted 1566/8459 = 18%, 229 KB/s], Decompressed: 1555 Downloaded: 1609 file(s) [attempted 1609/8459 = 19%, 58 KB/s], Decompressed: 1600 Downloaded: 1648 file(s) [attempted 1648/8459 = 19%, 155 KB/s], Decompressed: 1644 Downloaded: 1685 file(s) [attempted 1685/8459 = 19%, 139 KB/s], Decompressed: 1678 Downloaded: 1723 file(s) [attempted 1723/8459 = 20%, 84 KB/s], Decompressed: 1716 Downloaded: 1767 file(s) [attempted 1767/8459 = 20%, 480 KB/s], Decompressed: 1764 Downloaded: 1812 file(s) [attempted 1812/8459 = 21%, 95 KB/s], Decompressed: 1802 Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 25 KB/s], Decompressed: 1853 Downloaded: 1898 file(s) [attempted 1898/8459 = 22%, 43 KB/s], Decompressed: 1894 Downloaded: 1928 file(s) [attempted 1928/8459 = 22%, 172 KB/s], Decompressed: 1921 Downloaded: 1963 file(s) [attempted 1963/8459 = 23%, 885 KB/s], Decompressed: 1959 Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 25 KB/s], Decompressed: 2007 Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 38 KB/s], Decompressed: 2055 Downloaded: 2105 file(s) [attempted 2105/8459 = 24%, 438 KB/s], Decompressed: 2099 Downloaded: 2144 file(s) [attempted 2144/8459 = 25%, 345 KB/s], Decompressed: 2140 Downloaded: 2176 file(s) [attempted 2176/8459 = 25%, 83 KB/s], Decompressed: 2168 Downloaded: 2217 file(s) [attempted 2217/8459 = 26%, 421 KB/s], Decompressed: 2212 Downloaded: 2260 file(s) [attempted 2260/8459 = 26%, 564 KB/s], Decompressed: 2257 Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 188 KB/s], Decompressed: 2298 Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 390 KB/s], Decompressed: 2336 Downloaded: 2383 file(s) [attempted 2383/8459 = 28%, 682 KB/s], Decompressed: 2377 Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 36 KB/s], Decompressed: 2414 Downloaded: 2459 file(s) [attempted 2459/8459 = 29%, 444 KB/s], Decompressed: 2452 Downloaded: 2496 file(s) [attempted 2496/8459 = 29%, 47 KB/s], Decompressed: 2493 Downloaded: 2538 file(s) [attempted 2538/8459 = 30%, 333 KB/s], Decompressed: 2534 Downloaded: 2582 file(s) [attempted 2582/8459 = 30%, 1545 KB/s], Decompressed: 2575 Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 22 KB/s], Decompressed: 2616 Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 553 KB/s], Decompressed: 2650 Downloaded: 2698 file(s) [attempted 2698/8459 = 31%, 62 KB/s], Decompressed: 2695 Downloaded: 2746 file(s) [attempted 2746/8459 = 32%, 96 KB/s], Decompressed: 2743 Downloaded: 2794 file(s) [attempted 2794/8459 = 33%, 1713 KB/s], Decompressed: 2787 Downloaded: 2836 file(s) [attempted 2836/8459 = 33%, 95 KB/s], Decompressed: 2828 Downloaded: 2869 file(s) [attempted 2869/8459 = 33%, 444 KB/s], Decompressed: 2866 Downloaded: 2904 file(s) [attempted 2904/8459 = 34%, 117 KB/s], Decompressed: 2900 Downloaded: 2948 file(s) [attempted 2948/8459 = 34%, 231 KB/s], Decompressed: 2945 Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 192 KB/s], Decompressed: 2989 Downloaded: 3038 file(s) [attempted 3038/8459 = 35%, 1076 KB/s], Decompressed: 3030 Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 366 KB/s], Decompressed: 3064 Downloaded: 3106 file(s) [attempted 3106/8459 = 36%, 69 KB/s], Decompressed: 3102 Downloaded: 3150 file(s) [attempted 3150/8459 = 37%, 89 KB/s], Decompressed: 3147 Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 207 KB/s], Decompressed: 3195 Downloaded: 3242 file(s) [attempted 3242/8459 = 38%, 1219 KB/s], Decompressed: 3236 Downloaded: 3280 file(s) [attempted 3280/8459 = 38%, 152 KB/s], Decompressed: 3277 Downloaded: 3314 file(s) [attempted 3314/8459 = 39%, 161 KB/s], Decompressed: 3307 Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 389 KB/s], Decompressed: 3352 Downloaded: 3401 file(s) [attempted 3401/8459 = 40%, 112 KB/s], Decompressed: 3396 Downloaded: 3444 file(s) [attempted 3444/8459 = 40%, 262 KB/s], Decompressed: 3438 Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 158 KB/s], Decompressed: 3475 Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 441 KB/s], Decompressed: 3513 Downloaded: 3561 file(s) [attempted 3561/8459 = 42%, 234 KB/s], Decompressed: 3557 Downloaded: 3602 file(s) [attempted 3602/8459 = 42%, 401 KB/s], Decompressed: 3595 Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 704 KB/s], Decompressed: 3646 Downloaded: 3688 file(s) [attempted 3688/8459 = 43%, 53 KB/s], Decompressed: 3681 Downloaded: 3724 file(s) [attempted 3724/8459 = 44%, 1095 KB/s], Decompressed: 3718 Downloaded: 3763 file(s) [attempted 3763/8459 = 44%, 109 KB/s], Decompressed: 3759 Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 50 KB/s], Decompressed: 3804 Downloaded: 3852 file(s) [attempted 3852/8459 = 45%, 94 KB/s], Decompressed: 3848 Downloaded: 3896 file(s) [attempted 3896/8459 = 46%, 144 KB/s], Decompressed: 3889 Downloaded: 3930 file(s) [attempted 3930/8459 = 46%, 176 KB/s], Decompressed: 3924 Downloaded: 3971 file(s) [attempted 3971/8459 = 46%, 185 KB/s], Decompressed: 3968 Downloaded: 4012 file(s) [attempted 4012/8459 = 47%, 927 KB/s], Decompressed: 4009 Downloaded: 4054 file(s) [attempted 4054/8459 = 47%, 1002 KB/s], Decompressed: 4050 Downloaded: 4101 file(s) [attempted 4101/8459 = 48%, 364 KB/s], Decompressed: 4098 Downloaded: 4149 file(s) [attempted 4149/8459 = 49%, 47 KB/s], Decompressed: 4143 Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 398 KB/s], Decompressed: 4187 Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 75 KB/s], Decompressed: 4225 Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 1286 KB/s], Decompressed: 4266 Downloaded: 4310 file(s) [attempted 4310/8459 = 50%, 89 KB/s], Decompressed: 4303 Downloaded: 4351 file(s) [attempted 4351/8459 = 51%, 505 KB/s], Decompressed: 4348 Downloaded: 4392 file(s) [attempted 4392/8459 = 51%, 220 KB/s], Decompressed: 4382 Downloaded: 4427 file(s) [attempted 4427/8459 = 52%, 111 KB/s], Decompressed: 4420 Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 462 KB/s], Decompressed: 4461 Downloaded: 4512 file(s) [attempted 4512/8459 = 53%, 75 KB/s], Decompressed: 4505 Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 304 KB/s], Decompressed: 4546 Downloaded: 4591 file(s) [attempted 4591/8459 = 54%, 391 KB/s], Decompressed: 4587 Downloaded: 4632 file(s) [attempted 4632/8459 = 54%, 1162 KB/s], Decompressed: 4625 Downloaded: 4673 file(s) [attempted 4673/8459 = 55%, 551 KB/s], Decompressed: 4666 Downloaded: 4714 file(s) [attempted 4714/8459 = 55%, 26 KB/s], Decompressed: 4707 Downloaded: 4752 file(s) [attempted 4752/8459 = 56%, 83 KB/s], Decompressed: 4748 Downloaded: 4796 file(s) [attempted 4796/8459 = 56%, 48 KB/s], Decompressed: 4789 Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 408 KB/s], Decompressed: 4834 Downloaded: 4875 file(s) [attempted 4875/8459 = 57%, 188 KB/s], Decompressed: 4868 Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 938 KB/s], Decompressed: 4916 Downloaded: 4965 file(s) [attempted 4965/8459 = 58%, 87 KB/s], Decompressed: 4960 Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 145 KB/s], Decompressed: 4998 Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 186 KB/s], Decompressed: 5039 Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 560 KB/s], Decompressed: 5077 Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 50 KB/s], Decompressed: 5115 Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 1236 KB/s], Decompressed: 5159 Downloaded: 5203 file(s) [attempted 5203/8459 = 61%, 89 KB/s], Decompressed: 5197 Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 74 KB/s], Decompressed: 5241 Downloaded: 5290 file(s) [attempted 5290/8459 = 62%, 493 KB/s], Decompressed: 5282 Downloaded: 5325 file(s) [attempted 5325/8459 = 62%, 49 KB/s], Decompressed: 5320 Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 417 KB/s], Decompressed: 5354 Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 396 KB/s], Decompressed: 5399 Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 999 KB/s], Decompressed: 5440 Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 1076 KB/s], Decompressed: 5477 Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 82 KB/s], Decompressed: 5522 Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 80 KB/s], Decompressed: 5563 Downloaded: 5607 file(s) [attempted 5607/8459 = 66%, 278 KB/s], Decompressed: 5600 Downloaded: 5648 file(s) [attempted 5648/8459 = 66%, 1165 KB/s], Decompressed: 5645 Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 574 KB/s], Decompressed: 5686 Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 284 KB/s], Decompressed: 5720 Downloaded: 5762 file(s) [attempted 5762/8459 = 68%, 467 KB/s], Decompressed: 5758 Downloaded: 5809 file(s) [attempted 5809/8459 = 68%, 114 KB/s], Decompressed: 5806 Downloaded: 5854 file(s) [attempted 5854/8459 = 69%, 94 KB/s], Decompressed: 5850 Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 175 KB/s], Decompressed: 5891 Downloaded: 5930 file(s) [attempted 5930/8459 = 70%, 153 KB/s], Decompressed: 5919 Downloaded: 5967 file(s) [attempted 5967/8459 = 70%, 537 KB/s], Decompressed: 5963 Downloaded: 6011 file(s) [attempted 6011/8459 = 71%, 129 KB/s], Decompressed: 6008 Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 2102 KB/s], Decompressed: 6049 Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 545 KB/s], Decompressed: 6090 Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 145 KB/s], Decompressed: 6131 Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 546 KB/s], Decompressed: 6172 Downloaded: 6216 file(s) [attempted 6216/8459 = 73%, 476 KB/s], Decompressed: 6213 Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 83 KB/s], Decompressed: 6247 Downloaded: 6299 file(s) [attempted 6299/8459 = 74%, 26 KB/s], Decompressed: 6295 Downloaded: 6337 file(s) [attempted 6337/8459 = 74%, 50 KB/s], Decompressed: 6333 Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 293 KB/s], Decompressed: 6374 Downloaded: 6416 file(s) [attempted 6416/8459 = 75%, 52 KB/s], Decompressed: 6412 Downloaded: 6459 file(s) [attempted 6459/8459 = 76%, 933 KB/s], Decompressed: 6456 Downloaded: 6498 file(s) [attempted 6498/8459 = 76%, 962 KB/s], Decompressed: 6490 Downloaded: 6536 file(s) [attempted 6536/8459 = 77%, 193 KB/s], Decompressed: 6531 Downloaded: 6572 file(s) [attempted 6572/8459 = 77%, 106 KB/s], Decompressed: 6569 Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 351 KB/s], Decompressed: 6613 Downloaded: 6661 file(s) [attempted 6661/8459 = 78%, 70 KB/s], Decompressed: 6658 Downloaded: 6702 file(s) [attempted 6702/8459 = 79%, 59 KB/s], Decompressed: 6699 Downloaded: 6740 file(s) [attempted 6740/8459 = 79%, 95 KB/s], Decompressed: 6737 Downloaded: 6781 file(s) [attempted 6781/8459 = 80%, 963 KB/s], Decompressed: 6774 Downloaded: 6822 file(s) [attempted 6822/8459 = 80%, 127 KB/s], Decompressed: 6819 Downloaded: 6863 file(s) [attempted 6863/8459 = 81%, 202 KB/s], Decompressed: 6860 Downloaded: 6904 file(s) [attempted 6904/8459 = 81%, 434 KB/s], Decompressed: 6901 Downloaded: 6945 file(s) [attempted 6945/8459 = 82%, 402 KB/s], Decompressed: 6942 Downloaded: 6983 file(s) [attempted 6983/8459 = 82%, 377 KB/s], Decompressed: 6980 Downloaded: 7028 file(s) [attempted 7028/8459 = 83%, 673 KB/s], Decompressed: 7024 Downloaded: 7072 file(s) [attempted 7072/8459 = 83%, 779 KB/s], Decompressed: 7067 Downloaded: 7110 file(s) [attempted 7110/8459 = 84%, 125 KB/s], Decompressed: 7103 Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 72 KB/s], Decompressed: 7141 Downloaded: 7186 file(s) [attempted 7186/8459 = 84%, 1292 KB/s], Decompressed: 7182 Downloaded: 7227 file(s) [attempted 7227/8459 = 85%, 315 KB/s], Decompressed: 7223 Downloaded: 7267 file(s) [attempted 7267/8459 = 85%, 276 KB/s], Decompressed: 7264 Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 2098 KB/s], Decompressed: 7301 Downloaded: 7343 file(s) [attempted 7343/8459 = 86%, 54 KB/s], Decompressed: 7339 Downloaded: 7384 file(s) [attempted 7384/8459 = 87%, 182 KB/s], Decompressed: 7377 Downloaded: 7425 file(s) [attempted 7425/8459 = 87%, 222 KB/s], Decompressed: 7421 Downloaded: 7466 file(s) [attempted 7466/8459 = 88%, 371 KB/s], Decompressed: 7459 Downloaded: 7505 file(s) [attempted 7505/8459 = 88%, 241 KB/s], Decompressed: 7500 Downloaded: 7544 file(s) [attempted 7544/8459 = 89%, 224 KB/s], Decompressed: 7538 Downloaded: 7582 file(s) [attempted 7582/8459 = 89%, 44 KB/s], Decompressed: 7575 Downloaded: 7623 file(s) [attempted 7623/8459 = 90%, 101 KB/s], Decompressed: 7616 Downloaded: 7664 file(s) [attempted 7664/8459 = 90%, 184 KB/s], Decompressed: 7657 Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 89 KB/s], Decompressed: 7702 Downloaded: 7750 file(s) [attempted 7750/8459 = 91%, 223 KB/s], Decompressed: 7743 Downloaded: 7787 file(s) [attempted 7787/8459 = 92%, 130 KB/s], Decompressed: 7780 Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 158 KB/s], Decompressed: 7822 Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 247 KB/s], Decompressed: 7856 Downloaded: 7911 file(s) [attempted 7911/8459 = 93%, 591 KB/s], Decompressed: 7900 Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 516 KB/s], Decompressed: 7945 Downloaded: 7991 file(s) [attempted 7991/8459 = 94%, 698 KB/s], Decompressed: 7982 Downloaded: 8024 file(s) [attempted 8024/8459 = 94%, 162 KB/s], Decompressed: 8020 Downloaded: 8068 file(s) [attempted 8068/8459 = 95%, 960 KB/s], Decompressed: 8061 Downloaded: 8116 file(s) [attempted 8116/8459 = 95%, 121 KB/s], Decompressed: 8112 Downloaded: 8160 file(s) [attempted 8160/8459 = 96%, 122 KB/s], Decompressed: 8154 Downloaded: 8200 file(s) [attempted 8200/8459 = 96%, 348 KB/s], Decompressed: 8191 Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 1456 KB/s], Decompressed: 8232 Downloaded: 8270 file(s) [attempted 8270/8459 = 97%, 563 KB/s], Decompressed: 8266 Downloaded: 8312 file(s) [attempted 8312/8459 = 98%, 474 KB/s], Decompressed: 8304 Downloaded: 8355 file(s) [attempted 8355/8459 = 98%, 201 KB/s], Decompressed: 8352 Downloaded: 8396 file(s) [attempted 8396/8459 = 99%, 83 KB/s], Decompressed: 8393 Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 306 KB/s], Decompressed: 8434 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 115 KB/s], Decompressed: 8455 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 115 KB/s], Decompressed: 8455
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (23s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.6s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/772] Built Iut.Foundations.QualitativeData (1.0s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.5s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.5s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (32s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.1s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.6s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (82s)
warning: Iut/Stage1/IUTStage1SourceCore.lean:19880:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotient_card_eq_pow_finrank`:
[FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [FiniteDimensional ℚ_[p] K] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20063:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotientCosetHaarCharacterEndpoint`:
[FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [FiniteDimensional ℚ_[p] K] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20130:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.unitBallHaarCharacterEndpoint`:
[FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [FiniteDimensional ℚ_[p] K] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20532:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20533:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20537:4: `have hinteger_eq : (integer : ℚ_[p]) = (p : ℚ_[p]) * (preimage : ℚ_[p]) := by
simpa [IUTStage1PadicIntegerUnitBallSource.padicIntAddEquivIntegerAddSubgroup, hpreimage_eq] using
hpoint_eq.symm` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
[apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20547:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20572:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20573:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20576:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20577:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20578:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
✔ [3411/3425] Built Iut.Stage1.IUTStage1Remark312Absorption (21s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.7s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.2s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.6s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.7s)
⚠ [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 (177s)
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`