Verification run
Run 1043
failed commit
5d6214b7f2b8 toolchain lean-v4-30-0 prover lean took 12m 2s · 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-1341-source
exit_code=Some(0) duration_ms=3404
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1341-source'...
$ git checkout 5d6214b7f2b8a49e644b49505144e6fa2b59b7c5
exit_code=Some(0) duration_ms=164
stderr:
Note: switching to '5d6214b7f2b8a49e644b49505144e6fa2b59b7c5'.
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 5d6214b Thread Record Ob3 Ob5 into concrete Step XI
Resolved source revision: 5d6214b7f2b8a49e644b49505144e6fa2b59b7c5
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=5d6214b7f2b8a49e644b49505144e6fa2b59b7c5 provenance={"branch":"master","checked_out_revision":"5d6214b7f2b8a49e644b49505144e6fa2b59b7c5","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"5d6214b7f2b8a49e644b49505144e6fa2b59b7c5","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=51857
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%, 14 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 4 KB/s], Decompressed: 12
Downloaded: 42 file(s) [attempted 42/8459 = 0%, 132 KB/s], Decompressed: 36
Downloaded: 61 file(s) [attempted 61/8459 = 0%, 46 KB/s], Decompressed: 58
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 541 KB/s], Decompressed: 83
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 217 KB/s], Decompressed: 117
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 703 KB/s], Decompressed: 155
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 171 KB/s], Decompressed: 192
Downloaded: 237 file(s) [attempted 237/8459 = 2%, 257 KB/s], Decompressed: 230
Downloaded: 275 file(s) [attempted 275/8459 = 3%, 51 KB/s], Decompressed: 268
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 696 KB/s], Decompressed: 309
Downloaded: 347 file(s) [attempted 347/8459 = 4%, 739 KB/s], Decompressed: 343
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 204 KB/s], Decompressed: 388
Downloaded: 436 file(s) [attempted 436/8459 = 5%, 92 KB/s], Decompressed: 432
Downloaded: 474 file(s) [attempted 474/8459 = 5%, 681 KB/s], Decompressed: 470
Downloaded: 511 file(s) [attempted 511/8459 = 6%, 351 KB/s], Decompressed: 508
Downloaded: 549 file(s) [attempted 549/8459 = 6%, 1272 KB/s], Decompressed: 545
Downloaded: 594 file(s) [attempted 594/8459 = 7%, 904 KB/s], Decompressed: 586
Downloaded: 634 file(s) [attempted 634/8459 = 7%, 130 KB/s], Decompressed: 627
Downloaded: 672 file(s) [attempted 672/8459 = 7%, 441 KB/s], Decompressed: 658
Downloaded: 703 file(s) [attempted 703/8459 = 8%, 1233 KB/s], Decompressed: 696
Downloaded: 744 file(s) [attempted 744/8459 = 8%, 240 KB/s], Decompressed: 741
Downloaded: 788 file(s) [attempted 788/8459 = 9%, 215 KB/s], Decompressed: 778
Downloaded: 833 file(s) [attempted 833/8459 = 9%, 763 KB/s], Decompressed: 830
Downloaded: 871 file(s) [attempted 871/8459 = 10%, 1039 KB/s], Decompressed: 860
Downloaded: 908 file(s) [attempted 908/8459 = 10%, 661 KB/s], Decompressed: 905
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 341 KB/s], Decompressed: 943
Downloaded: 994 file(s) [attempted 994/8459 = 11%, 228 KB/s], Decompressed: 987
Downloaded: 1035 file(s) [attempted 1035/8459 = 12%, 1915 KB/s], Decompressed: 1032
Downloaded: 1073 file(s) [attempted 1073/8459 = 12%, 76 KB/s], Decompressed: 1069
Downloaded: 1111 file(s) [attempted 1111/8459 = 13%, 226 KB/s], Decompressed: 1104
Downloaded: 1153 file(s) [attempted 1153/8459 = 13%, 60 KB/s], Decompressed: 1148
Downloaded: 1199 file(s) [attempted 1199/8459 = 14%, 1239 KB/s], Decompressed: 1196
Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 1114 KB/s], Decompressed: 1240
Downloaded: 1280 file(s) [attempted 1280/8459 = 15%, 337 KB/s], Decompressed: 1271
Downloaded: 1319 file(s) [attempted 1319/8459 = 15%, 133 KB/s], Decompressed: 1312
Downloaded: 1360 file(s) [attempted 1360/8459 = 16%, 648 KB/s], Decompressed: 1353
Downloaded: 1405 file(s) [attempted 1405/8459 = 16%, 391 KB/s], Decompressed: 1401
Downloaded: 1449 file(s) [attempted 1449/8459 = 17%, 280 KB/s], Decompressed: 1442
Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 402 KB/s], Decompressed: 1487
Downloaded: 1535 file(s) [attempted 1535/8459 = 18%, 129 KB/s], Decompressed: 1528
Downloaded: 1572 file(s) [attempted 1572/8459 = 18%, 216 KB/s], Decompressed: 1566
Downloaded: 1617 file(s) [attempted 1617/8459 = 19%, 524 KB/s], Decompressed: 1610
Downloaded: 1659 file(s) [attempted 1659/8459 = 19%, 130 KB/s], Decompressed: 1654
Downloaded: 1699 file(s) [attempted 1699/8459 = 20%, 1982 KB/s], Decompressed: 1692
Downloaded: 1737 file(s) [attempted 1737/8459 = 20%, 255 KB/s], Decompressed: 1723
Downloaded: 1774 file(s) [attempted 1774/8459 = 20%, 738 KB/s], Decompressed: 1771
Downloaded: 1822 file(s) [attempted 1822/8459 = 21%, 432 KB/s], Decompressed: 1819
Downloaded: 1870 file(s) [attempted 1870/8459 = 22%, 270 KB/s], Decompressed: 1867
Downloaded: 1916 file(s) [attempted 1916/8459 = 22%, 483 KB/s], Decompressed: 1911
Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 611 KB/s], Decompressed: 1952
Downloaded: 2000 file(s) [attempted 2000/8459 = 23%, 51 KB/s], Decompressed: 1997
Downloaded: 2041 file(s) [attempted 2041/8459 = 24%, 36 KB/s], Decompressed: 2035
Downloaded: 2086 file(s) [attempted 2086/8459 = 24%, 105 KB/s], Decompressed: 2079
Downloaded: 2127 file(s) [attempted 2127/8459 = 25%, 94 KB/s], Decompressed: 2120
Downloaded: 2168 file(s) [attempted 2168/8459 = 25%, 223 KB/s], Decompressed: 2161
Downloaded: 2206 file(s) [attempted 2206/8459 = 26%, 250 KB/s], Decompressed: 2199
Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 198 KB/s], Decompressed: 2237
Downloaded: 2291 file(s) [attempted 2291/8459 = 27%, 392 KB/s], Decompressed: 2288
Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 411 KB/s], Decompressed: 2325
Downloaded: 2377 file(s) [attempted 2377/8459 = 28%, 610 KB/s], Decompressed: 2367
Downloaded: 2411 file(s) [attempted 2411/8459 = 28%, 122 KB/s], Decompressed: 2408
Downloaded: 2447 file(s) [attempted 2447/8459 = 28%, 269 KB/s], Decompressed: 2444
Downloaded: 2490 file(s) [attempted 2490/8459 = 29%, 193 KB/s], Decompressed: 2486
Downloaded: 2534 file(s) [attempted 2534/8459 = 29%, 597 KB/s], Decompressed: 2531
Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 111 KB/s], Decompressed: 2575
Downloaded: 2616 file(s) [attempted 2616/8459 = 30%, 24 KB/s], Decompressed: 2610
Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 597 KB/s], Decompressed: 2654
Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 990 KB/s], Decompressed: 2699
Downloaded: 2746 file(s) [attempted 2746/8459 = 32%, 46 KB/s], Decompressed: 2740
Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 563 KB/s], Decompressed: 2777
Downloaded: 2825 file(s) [attempted 2825/8459 = 33%, 132 KB/s], Decompressed: 2818
Downloaded: 2866 file(s) [attempted 2866/8459 = 33%, 476 KB/s], Decompressed: 2863
Downloaded: 2914 file(s) [attempted 2914/8459 = 34%, 717 KB/s], Decompressed: 2911
Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 1098 KB/s], Decompressed: 2948
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 359 KB/s], Decompressed: 2993
Downloaded: 3037 file(s) [attempted 3037/8459 = 35%, 178 KB/s], Decompressed: 3030
Downloaded: 3077 file(s) [attempted 3077/8459 = 36%, 216 KB/s], Decompressed: 3072
Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 37 KB/s], Decompressed: 3116
Downloaded: 3167 file(s) [attempted 3167/8459 = 37%, 691 KB/s], Decompressed: 3160
Downloaded: 3209 file(s) [attempted 3209/8459 = 37%, 529 KB/s], Decompressed: 3198
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 388 KB/s], Decompressed: 3239
Downloaded: 3285 file(s) [attempted 3285/8459 = 38%, 112 KB/s], Decompressed: 3280
Downloaded: 3328 file(s) [attempted 3328/8459 = 39%, 180 KB/s], Decompressed: 3321
Downloaded: 3369 file(s) [attempted 3369/8459 = 39%, 1858 KB/s], Decompressed: 3366
Downloaded: 3414 file(s) [attempted 3414/8459 = 40%, 1354 KB/s], Decompressed: 3410
Downloaded: 3452 file(s) [attempted 3452/8459 = 40%, 49 KB/s], Decompressed: 3448
Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 388 KB/s], Decompressed: 3486
Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 112 KB/s], Decompressed: 3523
Downloaded: 3570 file(s) [attempted 3570/8459 = 42%, 79 KB/s], Decompressed: 3564
Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 1364 KB/s], Decompressed: 3609
Downloaded: 3657 file(s) [attempted 3657/8459 = 43%, 355 KB/s], Decompressed: 3653
Downloaded: 3696 file(s) [attempted 3696/8459 = 43%, 459 KB/s], Decompressed: 3684
Downloaded: 3734 file(s) [attempted 3734/8459 = 44%, 25 KB/s], Decompressed: 3725
Downloaded: 3775 file(s) [attempted 3775/8459 = 44%, 91 KB/s], Decompressed: 3766
Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 108 KB/s], Decompressed: 3811
Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 148 KB/s], Decompressed: 3845
Downloaded: 3896 file(s) [attempted 3896/8459 = 46%, 428 KB/s], Decompressed: 3893
Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 41 KB/s], Decompressed: 3927
Downloaded: 3977 file(s) [attempted 3977/8459 = 47%, 174 KB/s], Decompressed: 3972
Downloaded: 4016 file(s) [attempted 4016/8459 = 47%, 99 KB/s], Decompressed: 4013
Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 1180 KB/s], Decompressed: 4054
Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 702 KB/s], Decompressed: 4095
Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 58 KB/s], Decompressed: 4136
Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 834 KB/s], Decompressed: 4174
Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 317 KB/s], Decompressed: 4215
Downloaded: 4264 file(s) [attempted 4264/8459 = 50%, 260 KB/s], Decompressed: 4252
Downloaded: 4300 file(s) [attempted 4300/8459 = 50%, 122 KB/s], Decompressed: 4293
Downloaded: 4348 file(s) [attempted 4348/8459 = 51%, 180 KB/s], Decompressed: 4345
Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 99 KB/s], Decompressed: 4389
Downloaded: 4434 file(s) [attempted 4434/8459 = 52%, 135 KB/s], Decompressed: 4430
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 948 KB/s], Decompressed: 4475
Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 499 KB/s], Decompressed: 4512
Downloaded: 4564 file(s) [attempted 4564/8459 = 53%, 114 KB/s], Decompressed: 4560
Downloaded: 4605 file(s) [attempted 4605/8459 = 54%, 451 KB/s], Decompressed: 4601
Downloaded: 4646 file(s) [attempted 4646/8459 = 54%, 412 KB/s], Decompressed: 4639
Downloaded: 4690 file(s) [attempted 4690/8459 = 55%, 49 KB/s], Decompressed: 4687
Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 262 KB/s], Decompressed: 4731
Downloaded: 4783 file(s) [attempted 4783/8459 = 56%, 64 KB/s], Decompressed: 4762
Downloaded: 4819 file(s) [attempted 4819/8459 = 56%, 307 KB/s], Decompressed: 4800
Downloaded: 4861 file(s) [attempted 4861/8459 = 57%, 82 KB/s], Decompressed: 4848
Downloaded: 4899 file(s) [attempted 4899/8459 = 57%, 127 KB/s], Decompressed: 4896
Downloaded: 4944 file(s) [attempted 4944/8459 = 58%, 23 KB/s], Decompressed: 4940
Downloaded: 4985 file(s) [attempted 4985/8459 = 58%, 305 KB/s], Decompressed: 4981
Downloaded: 5029 file(s) [attempted 5029/8459 = 59%, 244 KB/s], Decompressed: 5019
Downloaded: 5063 file(s) [attempted 5063/8459 = 59%, 357 KB/s], Decompressed: 5053
Downloaded: 5101 file(s) [attempted 5101/8459 = 60%, 79 KB/s], Decompressed: 5094
Downloaded: 5145 file(s) [attempted 5145/8459 = 60%, 803 KB/s], Decompressed: 5139
Downloaded: 5191 file(s) [attempted 5191/8459 = 61%, 107 KB/s], Decompressed: 5187
Downloaded: 5234 file(s) [attempted 5234/8459 = 61%, 1044 KB/s], Decompressed: 5231
Downloaded: 5276 file(s) [attempted 5276/8459 = 62%, 439 KB/s], Decompressed: 5270
Downloaded: 5320 file(s) [attempted 5320/8459 = 62%, 503 KB/s], Decompressed: 5313
Downloaded: 5361 file(s) [attempted 5361/8459 = 63%, 23 KB/s], Decompressed: 5354
Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 379 KB/s], Decompressed: 5395
Downloaded: 5440 file(s) [attempted 5440/8459 = 64%, 1172 KB/s], Decompressed: 5436
Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 159 KB/s], Decompressed: 5481
Downloaded: 5528 file(s) [attempted 5528/8459 = 65%, 155 KB/s], Decompressed: 5522
Downloaded: 5570 file(s) [attempted 5570/8459 = 65%, 148 KB/s], Decompressed: 5566
Downloaded: 5614 file(s) [attempted 5614/8459 = 66%, 97 KB/s], Decompressed: 5607
Downloaded: 5655 file(s) [attempted 5655/8459 = 66%, 1435 KB/s], Decompressed: 5649
Downloaded: 5695 file(s) [attempted 5695/8459 = 67%, 129 KB/s], Decompressed: 5686
Downloaded: 5731 file(s) [attempted 5731/8459 = 67%, 68 KB/s], Decompressed: 5727
Downloaded: 5775 file(s) [attempted 5775/8459 = 68%, 104 KB/s], Decompressed: 5772
Downloaded: 5823 file(s) [attempted 5823/8459 = 68%, 54 KB/s], Decompressed: 5820
Downloaded: 5868 file(s) [attempted 5868/8459 = 69%, 203 KB/s], Decompressed: 5864
Downloaded: 5909 file(s) [attempted 5909/8459 = 69%, 2913 KB/s], Decompressed: 5898
Downloaded: 5943 file(s) [attempted 5943/8459 = 70%, 737 KB/s], Decompressed: 5939
Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 74 KB/s], Decompressed: 5977
Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 278 KB/s], Decompressed: 6022
Downloaded: 6073 file(s) [attempted 6073/8459 = 71%, 93 KB/s], Decompressed: 6069
Downloaded: 6117 file(s) [attempted 6117/8459 = 72%, 302 KB/s], Decompressed: 6114
Downloaded: 6159 file(s) [attempted 6159/8459 = 72%, 219 KB/s], Decompressed: 6152
Downloaded: 6197 file(s) [attempted 6197/8459 = 73%, 386 KB/s], Decompressed: 6189
Downloaded: 6234 file(s) [attempted 6234/8459 = 73%, 1062 KB/s], Decompressed: 6223
Downloaded: 6271 file(s) [attempted 6271/8459 = 74%, 86 KB/s], Decompressed: 6268
Downloaded: 6313 file(s) [attempted 6313/8459 = 74%, 92 KB/s], Decompressed: 6309
Downloaded: 6358 file(s) [attempted 6358/8459 = 75%, 863 KB/s], Decompressed: 6351
Downloaded: 6396 file(s) [attempted 6396/8459 = 75%, 756 KB/s], Decompressed: 6391
Downloaded: 6443 file(s) [attempted 6443/8459 = 76%, 1277 KB/s], Decompressed: 6432
Downloaded: 6480 file(s) [attempted 6480/8459 = 76%, 237 KB/s], Decompressed: 6477
Downloaded: 6521 file(s) [attempted 6521/8459 = 77%, 240 KB/s], Decompressed: 6514
Downloaded: 6562 file(s) [attempted 6562/8459 = 77%, 520 KB/s], Decompressed: 6559
Downloaded: 6610 file(s) [attempted 6610/8459 = 78%, 239 KB/s], Decompressed: 6603
Downloaded: 6652 file(s) [attempted 6652/8459 = 78%, 486 KB/s], Decompressed: 6644
Downloaded: 6689 file(s) [attempted 6689/8459 = 79%, 151 KB/s], Decompressed: 6679
Downloaded: 6727 file(s) [attempted 6727/8459 = 79%, 129 KB/s], Decompressed: 6720
Downloaded: 6771 file(s) [attempted 6771/8459 = 80%, 127 KB/s], Decompressed: 6768
Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 140 KB/s], Decompressed: 6812
Downloaded: 6864 file(s) [attempted 6864/8459 = 81%, 149 KB/s], Decompressed: 6857
Downloaded: 6899 file(s) [attempted 6899/8459 = 81%, 121 KB/s], Decompressed: 6894
Downloaded: 6939 file(s) [attempted 6939/8459 = 82%, 257 KB/s], Decompressed: 6935
Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 173 KB/s], Decompressed: 6976
Downloaded: 7024 file(s) [attempted 7024/8459 = 83%, 755 KB/s], Decompressed: 7021
Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 630 KB/s], Decompressed: 7059
Downloaded: 7106 file(s) [attempted 7106/8459 = 84%, 562 KB/s], Decompressed: 7100
Downloaded: 7146 file(s) [attempted 7146/8459 = 84%, 118 KB/s], Decompressed: 7141
Downloaded: 7182 file(s) [attempted 7182/8459 = 84%, 304 KB/s], Decompressed: 7178
Downloaded: 7230 file(s) [attempted 7230/8459 = 85%, 1751 KB/s], Decompressed: 7226
Downloaded: 7278 file(s) [attempted 7278/8459 = 86%, 222 KB/s], Decompressed: 7274
Downloaded: 7322 file(s) [attempted 7322/8459 = 86%, 36 KB/s], Decompressed: 7315
Downloaded: 7363 file(s) [attempted 7363/8459 = 87%, 46 KB/s], Decompressed: 7360
Downloaded: 7401 file(s) [attempted 7401/8459 = 87%, 306 KB/s], Decompressed: 7394
Downloaded: 7444 file(s) [attempted 7444/8459 = 88%, 624 KB/s], Decompressed: 7438
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 306 KB/s], Decompressed: 7479
Downloaded: 7529 file(s) [attempted 7529/8459 = 89%, 1216 KB/s], Decompressed: 7521
Downloaded: 7569 file(s) [attempted 7569/8459 = 89%, 135 KB/s], Decompressed: 7565
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 521 KB/s], Decompressed: 7609
Downloaded: 7657 file(s) [attempted 7657/8459 = 90%, 126 KB/s], Decompressed: 7654
Downloaded: 7696 file(s) [attempted 7696/8459 = 90%, 383 KB/s], Decompressed: 7688
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 143 KB/s], Decompressed: 7729
Downloaded: 7781 file(s) [attempted 7781/8459 = 91%, 120 KB/s], Decompressed: 7774
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 896 KB/s], Decompressed: 7815
Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 25 KB/s], Decompressed: 7856
Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 226 KB/s], Decompressed: 7900
Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 179 KB/s], Decompressed: 7945
Downloaded: 7991 file(s) [attempted 7991/8459 = 94%, 712 KB/s], Decompressed: 7986
Downloaded: 8034 file(s) [attempted 8034/8459 = 94%, 524 KB/s], Decompressed: 8024
Downloaded: 8075 file(s) [attempted 8075/8459 = 95%, 400 KB/s], Decompressed: 8068
Downloaded: 8119 file(s) [attempted 8119/8459 = 95%, 428 KB/s], Decompressed: 8113
Downloaded: 8160 file(s) [attempted 8160/8459 = 96%, 764 KB/s], Decompressed: 8154
Downloaded: 8199 file(s) [attempted 8199/8459 = 96%, 32 KB/s], Decompressed: 8191
Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 76 KB/s], Decompressed: 8239
Downloaded: 8287 file(s) [attempted 8287/8459 = 97%, 133 KB/s], Decompressed: 8284
Downloaded: 8333 file(s) [attempted 8333/8459 = 98%, 89 KB/s], Decompressed: 8321
Downloaded: 8369 file(s) [attempted 8369/8459 = 98%, 856 KB/s], Decompressed: 8362
Downloaded: 8410 file(s) [attempted 8410/8459 = 99%, 142 KB/s], Decompressed: 8403
Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 774 KB/s], Decompressed: 8445
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 774 KB/s], Decompressed: 8454
$ lake build
exit_code=Some(1) duration_ms=471451
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (25s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.8s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.7s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/772] Built Iut.Foundations.QualitativeData (2.1s)
✔ [3382/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.8s)
✔ [3388/3393] Built Iut.Stage1.CorollarySchema (34s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.5s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (87s)
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 (6.3s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (4.9s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.3s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.1s)
⚠ [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 (172s)
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=5257
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-1341-source
Cloning into '/var/lib/apodeixis/repos/job-1341-source'...
git_checkout exit 0
git checkout 5d6214b7f2b8a49e644b49505144e6fa2b59b7c5
Note: switching to '5d6214b7f2b8a49e644b49505144e6fa2b59b7c5'. 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 5d6214b Thread Record Ob3 Ob5 into concrete Step XI
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%, 14 KB/s], Decompressed: 0 Downloaded: 14 file(s) [attempted 14/8459 = 0%, 4 KB/s], Decompressed: 12 Downloaded: 42 file(s) [attempted 42/8459 = 0%, 132 KB/s], Decompressed: 36 Downloaded: 61 file(s) [attempted 61/8459 = 0%, 46 KB/s], Decompressed: 58 Downloaded: 86 file(s) [attempted 86/8459 = 1%, 541 KB/s], Decompressed: 83 Downloaded: 124 file(s) [attempted 124/8459 = 1%, 217 KB/s], Decompressed: 117 Downloaded: 158 file(s) [attempted 158/8459 = 1%, 703 KB/s], Decompressed: 155 Downloaded: 196 file(s) [attempted 196/8459 = 2%, 171 KB/s], Decompressed: 192 Downloaded: 237 file(s) [attempted 237/8459 = 2%, 257 KB/s], Decompressed: 230 Downloaded: 275 file(s) [attempted 275/8459 = 3%, 51 KB/s], Decompressed: 268 Downloaded: 312 file(s) [attempted 312/8459 = 3%, 696 KB/s], Decompressed: 309 Downloaded: 347 file(s) [attempted 347/8459 = 4%, 739 KB/s], Decompressed: 343 Downloaded: 391 file(s) [attempted 391/8459 = 4%, 204 KB/s], Decompressed: 388 Downloaded: 436 file(s) [attempted 436/8459 = 5%, 92 KB/s], Decompressed: 432 Downloaded: 474 file(s) [attempted 474/8459 = 5%, 681 KB/s], Decompressed: 470 Downloaded: 511 file(s) [attempted 511/8459 = 6%, 351 KB/s], Decompressed: 508 Downloaded: 549 file(s) [attempted 549/8459 = 6%, 1272 KB/s], Decompressed: 545 Downloaded: 594 file(s) [attempted 594/8459 = 7%, 904 KB/s], Decompressed: 586 Downloaded: 634 file(s) [attempted 634/8459 = 7%, 130 KB/s], Decompressed: 627 Downloaded: 672 file(s) [attempted 672/8459 = 7%, 441 KB/s], Decompressed: 658 Downloaded: 703 file(s) [attempted 703/8459 = 8%, 1233 KB/s], Decompressed: 696 Downloaded: 744 file(s) [attempted 744/8459 = 8%, 240 KB/s], Decompressed: 741 Downloaded: 788 file(s) [attempted 788/8459 = 9%, 215 KB/s], Decompressed: 778 Downloaded: 833 file(s) [attempted 833/8459 = 9%, 763 KB/s], Decompressed: 830 Downloaded: 871 file(s) [attempted 871/8459 = 10%, 1039 KB/s], Decompressed: 860 Downloaded: 908 file(s) [attempted 908/8459 = 10%, 661 KB/s], Decompressed: 905 Downloaded: 949 file(s) [attempted 949/8459 = 11%, 341 KB/s], Decompressed: 943 Downloaded: 994 file(s) [attempted 994/8459 = 11%, 228 KB/s], Decompressed: 987 Downloaded: 1035 file(s) [attempted 1035/8459 = 12%, 1915 KB/s], Decompressed: 1032 Downloaded: 1073 file(s) [attempted 1073/8459 = 12%, 76 KB/s], Decompressed: 1069 Downloaded: 1111 file(s) [attempted 1111/8459 = 13%, 226 KB/s], Decompressed: 1104 Downloaded: 1153 file(s) [attempted 1153/8459 = 13%, 60 KB/s], Decompressed: 1148 Downloaded: 1199 file(s) [attempted 1199/8459 = 14%, 1239 KB/s], Decompressed: 1196 Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 1114 KB/s], Decompressed: 1240 Downloaded: 1280 file(s) [attempted 1280/8459 = 15%, 337 KB/s], Decompressed: 1271 Downloaded: 1319 file(s) [attempted 1319/8459 = 15%, 133 KB/s], Decompressed: 1312 Downloaded: 1360 file(s) [attempted 1360/8459 = 16%, 648 KB/s], Decompressed: 1353 Downloaded: 1405 file(s) [attempted 1405/8459 = 16%, 391 KB/s], Decompressed: 1401 Downloaded: 1449 file(s) [attempted 1449/8459 = 17%, 280 KB/s], Decompressed: 1442 Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 402 KB/s], Decompressed: 1487 Downloaded: 1535 file(s) [attempted 1535/8459 = 18%, 129 KB/s], Decompressed: 1528 Downloaded: 1572 file(s) [attempted 1572/8459 = 18%, 216 KB/s], Decompressed: 1566 Downloaded: 1617 file(s) [attempted 1617/8459 = 19%, 524 KB/s], Decompressed: 1610 Downloaded: 1659 file(s) [attempted 1659/8459 = 19%, 130 KB/s], Decompressed: 1654 Downloaded: 1699 file(s) [attempted 1699/8459 = 20%, 1982 KB/s], Decompressed: 1692 Downloaded: 1737 file(s) [attempted 1737/8459 = 20%, 255 KB/s], Decompressed: 1723 Downloaded: 1774 file(s) [attempted 1774/8459 = 20%, 738 KB/s], Decompressed: 1771 Downloaded: 1822 file(s) [attempted 1822/8459 = 21%, 432 KB/s], Decompressed: 1819 Downloaded: 1870 file(s) [attempted 1870/8459 = 22%, 270 KB/s], Decompressed: 1867 Downloaded: 1916 file(s) [attempted 1916/8459 = 22%, 483 KB/s], Decompressed: 1911 Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 611 KB/s], Decompressed: 1952 Downloaded: 2000 file(s) [attempted 2000/8459 = 23%, 51 KB/s], Decompressed: 1997 Downloaded: 2041 file(s) [attempted 2041/8459 = 24%, 36 KB/s], Decompressed: 2035 Downloaded: 2086 file(s) [attempted 2086/8459 = 24%, 105 KB/s], Decompressed: 2079 Downloaded: 2127 file(s) [attempted 2127/8459 = 25%, 94 KB/s], Decompressed: 2120 Downloaded: 2168 file(s) [attempted 2168/8459 = 25%, 223 KB/s], Decompressed: 2161 Downloaded: 2206 file(s) [attempted 2206/8459 = 26%, 250 KB/s], Decompressed: 2199 Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 198 KB/s], Decompressed: 2237 Downloaded: 2291 file(s) [attempted 2291/8459 = 27%, 392 KB/s], Decompressed: 2288 Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 411 KB/s], Decompressed: 2325 Downloaded: 2377 file(s) [attempted 2377/8459 = 28%, 610 KB/s], Decompressed: 2367 Downloaded: 2411 file(s) [attempted 2411/8459 = 28%, 122 KB/s], Decompressed: 2408 Downloaded: 2447 file(s) [attempted 2447/8459 = 28%, 269 KB/s], Decompressed: 2444 Downloaded: 2490 file(s) [attempted 2490/8459 = 29%, 193 KB/s], Decompressed: 2486 Downloaded: 2534 file(s) [attempted 2534/8459 = 29%, 597 KB/s], Decompressed: 2531 Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 111 KB/s], Decompressed: 2575 Downloaded: 2616 file(s) [attempted 2616/8459 = 30%, 24 KB/s], Decompressed: 2610 Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 597 KB/s], Decompressed: 2654 Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 990 KB/s], Decompressed: 2699 Downloaded: 2746 file(s) [attempted 2746/8459 = 32%, 46 KB/s], Decompressed: 2740 Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 563 KB/s], Decompressed: 2777 Downloaded: 2825 file(s) [attempted 2825/8459 = 33%, 132 KB/s], Decompressed: 2818 Downloaded: 2866 file(s) [attempted 2866/8459 = 33%, 476 KB/s], Decompressed: 2863 Downloaded: 2914 file(s) [attempted 2914/8459 = 34%, 717 KB/s], Decompressed: 2911 Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 1098 KB/s], Decompressed: 2948 Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 359 KB/s], Decompressed: 2993 Downloaded: 3037 file(s) [attempted 3037/8459 = 35%, 178 KB/s], Decompressed: 3030 Downloaded: 3077 file(s) [attempted 3077/8459 = 36%, 216 KB/s], Decompressed: 3072 Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 37 KB/s], Decompressed: 3116 Downloaded: 3167 file(s) [attempted 3167/8459 = 37%, 691 KB/s], Decompressed: 3160 Downloaded: 3209 file(s) [attempted 3209/8459 = 37%, 529 KB/s], Decompressed: 3198 Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 388 KB/s], Decompressed: 3239 Downloaded: 3285 file(s) [attempted 3285/8459 = 38%, 112 KB/s], Decompressed: 3280 Downloaded: 3328 file(s) [attempted 3328/8459 = 39%, 180 KB/s], Decompressed: 3321 Downloaded: 3369 file(s) [attempted 3369/8459 = 39%, 1858 KB/s], Decompressed: 3366 Downloaded: 3414 file(s) [attempted 3414/8459 = 40%, 1354 KB/s], Decompressed: 3410 Downloaded: 3452 file(s) [attempted 3452/8459 = 40%, 49 KB/s], Decompressed: 3448 Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 388 KB/s], Decompressed: 3486 Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 112 KB/s], Decompressed: 3523 Downloaded: 3570 file(s) [attempted 3570/8459 = 42%, 79 KB/s], Decompressed: 3564 Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 1364 KB/s], Decompressed: 3609 Downloaded: 3657 file(s) [attempted 3657/8459 = 43%, 355 KB/s], Decompressed: 3653 Downloaded: 3696 file(s) [attempted 3696/8459 = 43%, 459 KB/s], Decompressed: 3684 Downloaded: 3734 file(s) [attempted 3734/8459 = 44%, 25 KB/s], Decompressed: 3725 Downloaded: 3775 file(s) [attempted 3775/8459 = 44%, 91 KB/s], Decompressed: 3766 Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 108 KB/s], Decompressed: 3811 Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 148 KB/s], Decompressed: 3845 Downloaded: 3896 file(s) [attempted 3896/8459 = 46%, 428 KB/s], Decompressed: 3893 Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 41 KB/s], Decompressed: 3927 Downloaded: 3977 file(s) [attempted 3977/8459 = 47%, 174 KB/s], Decompressed: 3972 Downloaded: 4016 file(s) [attempted 4016/8459 = 47%, 99 KB/s], Decompressed: 4013 Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 1180 KB/s], Decompressed: 4054 Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 702 KB/s], Decompressed: 4095 Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 58 KB/s], Decompressed: 4136 Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 834 KB/s], Decompressed: 4174 Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 317 KB/s], Decompressed: 4215 Downloaded: 4264 file(s) [attempted 4264/8459 = 50%, 260 KB/s], Decompressed: 4252 Downloaded: 4300 file(s) [attempted 4300/8459 = 50%, 122 KB/s], Decompressed: 4293 Downloaded: 4348 file(s) [attempted 4348/8459 = 51%, 180 KB/s], Decompressed: 4345 Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 99 KB/s], Decompressed: 4389 Downloaded: 4434 file(s) [attempted 4434/8459 = 52%, 135 KB/s], Decompressed: 4430 Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 948 KB/s], Decompressed: 4475 Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 499 KB/s], Decompressed: 4512 Downloaded: 4564 file(s) [attempted 4564/8459 = 53%, 114 KB/s], Decompressed: 4560 Downloaded: 4605 file(s) [attempted 4605/8459 = 54%, 451 KB/s], Decompressed: 4601 Downloaded: 4646 file(s) [attempted 4646/8459 = 54%, 412 KB/s], Decompressed: 4639 Downloaded: 4690 file(s) [attempted 4690/8459 = 55%, 49 KB/s], Decompressed: 4687 Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 262 KB/s], Decompressed: 4731 Downloaded: 4783 file(s) [attempted 4783/8459 = 56%, 64 KB/s], Decompressed: 4762 Downloaded: 4819 file(s) [attempted 4819/8459 = 56%, 307 KB/s], Decompressed: 4800 Downloaded: 4861 file(s) [attempted 4861/8459 = 57%, 82 KB/s], Decompressed: 4848 Downloaded: 4899 file(s) [attempted 4899/8459 = 57%, 127 KB/s], Decompressed: 4896 Downloaded: 4944 file(s) [attempted 4944/8459 = 58%, 23 KB/s], Decompressed: 4940 Downloaded: 4985 file(s) [attempted 4985/8459 = 58%, 305 KB/s], Decompressed: 4981 Downloaded: 5029 file(s) [attempted 5029/8459 = 59%, 244 KB/s], Decompressed: 5019 Downloaded: 5063 file(s) [attempted 5063/8459 = 59%, 357 KB/s], Decompressed: 5053 Downloaded: 5101 file(s) [attempted 5101/8459 = 60%, 79 KB/s], Decompressed: 5094 Downloaded: 5145 file(s) [attempted 5145/8459 = 60%, 803 KB/s], Decompressed: 5139 Downloaded: 5191 file(s) [attempted 5191/8459 = 61%, 107 KB/s], Decompressed: 5187 Downloaded: 5234 file(s) [attempted 5234/8459 = 61%, 1044 KB/s], Decompressed: 5231 Downloaded: 5276 file(s) [attempted 5276/8459 = 62%, 439 KB/s], Decompressed: 5270 Downloaded: 5320 file(s) [attempted 5320/8459 = 62%, 503 KB/s], Decompressed: 5313 Downloaded: 5361 file(s) [attempted 5361/8459 = 63%, 23 KB/s], Decompressed: 5354 Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 379 KB/s], Decompressed: 5395 Downloaded: 5440 file(s) [attempted 5440/8459 = 64%, 1172 KB/s], Decompressed: 5436 Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 159 KB/s], Decompressed: 5481 Downloaded: 5528 file(s) [attempted 5528/8459 = 65%, 155 KB/s], Decompressed: 5522 Downloaded: 5570 file(s) [attempted 5570/8459 = 65%, 148 KB/s], Decompressed: 5566 Downloaded: 5614 file(s) [attempted 5614/8459 = 66%, 97 KB/s], Decompressed: 5607 Downloaded: 5655 file(s) [attempted 5655/8459 = 66%, 1435 KB/s], Decompressed: 5649 Downloaded: 5695 file(s) [attempted 5695/8459 = 67%, 129 KB/s], Decompressed: 5686 Downloaded: 5731 file(s) [attempted 5731/8459 = 67%, 68 KB/s], Decompressed: 5727 Downloaded: 5775 file(s) [attempted 5775/8459 = 68%, 104 KB/s], Decompressed: 5772 Downloaded: 5823 file(s) [attempted 5823/8459 = 68%, 54 KB/s], Decompressed: 5820 Downloaded: 5868 file(s) [attempted 5868/8459 = 69%, 203 KB/s], Decompressed: 5864 Downloaded: 5909 file(s) [attempted 5909/8459 = 69%, 2913 KB/s], Decompressed: 5898 Downloaded: 5943 file(s) [attempted 5943/8459 = 70%, 737 KB/s], Decompressed: 5939 Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 74 KB/s], Decompressed: 5977 Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 278 KB/s], Decompressed: 6022 Downloaded: 6073 file(s) [attempted 6073/8459 = 71%, 93 KB/s], Decompressed: 6069 Downloaded: 6117 file(s) [attempted 6117/8459 = 72%, 302 KB/s], Decompressed: 6114 Downloaded: 6159 file(s) [attempted 6159/8459 = 72%, 219 KB/s], Decompressed: 6152 Downloaded: 6197 file(s) [attempted 6197/8459 = 73%, 386 KB/s], Decompressed: 6189 Downloaded: 6234 file(s) [attempted 6234/8459 = 73%, 1062 KB/s], Decompressed: 6223 Downloaded: 6271 file(s) [attempted 6271/8459 = 74%, 86 KB/s], Decompressed: 6268 Downloaded: 6313 file(s) [attempted 6313/8459 = 74%, 92 KB/s], Decompressed: 6309 Downloaded: 6358 file(s) [attempted 6358/8459 = 75%, 863 KB/s], Decompressed: 6351 Downloaded: 6396 file(s) [attempted 6396/8459 = 75%, 756 KB/s], Decompressed: 6391 Downloaded: 6443 file(s) [attempted 6443/8459 = 76%, 1277 KB/s], Decompressed: 6432 Downloaded: 6480 file(s) [attempted 6480/8459 = 76%, 237 KB/s], Decompressed: 6477 Downloaded: 6521 file(s) [attempted 6521/8459 = 77%, 240 KB/s], Decompressed: 6514 Downloaded: 6562 file(s) [attempted 6562/8459 = 77%, 520 KB/s], Decompressed: 6559 Downloaded: 6610 file(s) [attempted 6610/8459 = 78%, 239 KB/s], Decompressed: 6603 Downloaded: 6652 file(s) [attempted 6652/8459 = 78%, 486 KB/s], Decompressed: 6644 Downloaded: 6689 file(s) [attempted 6689/8459 = 79%, 151 KB/s], Decompressed: 6679 Downloaded: 6727 file(s) [attempted 6727/8459 = 79%, 129 KB/s], Decompressed: 6720 Downloaded: 6771 file(s) [attempted 6771/8459 = 80%, 127 KB/s], Decompressed: 6768 Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 140 KB/s], Decompressed: 6812 Downloaded: 6864 file(s) [attempted 6864/8459 = 81%, 149 KB/s], Decompressed: 6857 Downloaded: 6899 file(s) [attempted 6899/8459 = 81%, 121 KB/s], Decompressed: 6894 Downloaded: 6939 file(s) [attempted 6939/8459 = 82%, 257 KB/s], Decompressed: 6935 Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 173 KB/s], Decompressed: 6976 Downloaded: 7024 file(s) [attempted 7024/8459 = 83%, 755 KB/s], Decompressed: 7021 Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 630 KB/s], Decompressed: 7059 Downloaded: 7106 file(s) [attempted 7106/8459 = 84%, 562 KB/s], Decompressed: 7100 Downloaded: 7146 file(s) [attempted 7146/8459 = 84%, 118 KB/s], Decompressed: 7141 Downloaded: 7182 file(s) [attempted 7182/8459 = 84%, 304 KB/s], Decompressed: 7178 Downloaded: 7230 file(s) [attempted 7230/8459 = 85%, 1751 KB/s], Decompressed: 7226 Downloaded: 7278 file(s) [attempted 7278/8459 = 86%, 222 KB/s], Decompressed: 7274 Downloaded: 7322 file(s) [attempted 7322/8459 = 86%, 36 KB/s], Decompressed: 7315 Downloaded: 7363 file(s) [attempted 7363/8459 = 87%, 46 KB/s], Decompressed: 7360 Downloaded: 7401 file(s) [attempted 7401/8459 = 87%, 306 KB/s], Decompressed: 7394 Downloaded: 7444 file(s) [attempted 7444/8459 = 88%, 624 KB/s], Decompressed: 7438 Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 306 KB/s], Decompressed: 7479 Downloaded: 7529 file(s) [attempted 7529/8459 = 89%, 1216 KB/s], Decompressed: 7521 Downloaded: 7569 file(s) [attempted 7569/8459 = 89%, 135 KB/s], Decompressed: 7565 Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 521 KB/s], Decompressed: 7609 Downloaded: 7657 file(s) [attempted 7657/8459 = 90%, 126 KB/s], Decompressed: 7654 Downloaded: 7696 file(s) [attempted 7696/8459 = 90%, 383 KB/s], Decompressed: 7688 Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 143 KB/s], Decompressed: 7729 Downloaded: 7781 file(s) [attempted 7781/8459 = 91%, 120 KB/s], Decompressed: 7774 Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 896 KB/s], Decompressed: 7815 Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 25 KB/s], Decompressed: 7856 Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 226 KB/s], Decompressed: 7900 Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 179 KB/s], Decompressed: 7945 Downloaded: 7991 file(s) [attempted 7991/8459 = 94%, 712 KB/s], Decompressed: 7986 Downloaded: 8034 file(s) [attempted 8034/8459 = 94%, 524 KB/s], Decompressed: 8024 Downloaded: 8075 file(s) [attempted 8075/8459 = 95%, 400 KB/s], Decompressed: 8068 Downloaded: 8119 file(s) [attempted 8119/8459 = 95%, 428 KB/s], Decompressed: 8113 Downloaded: 8160 file(s) [attempted 8160/8459 = 96%, 764 KB/s], Decompressed: 8154 Downloaded: 8199 file(s) [attempted 8199/8459 = 96%, 32 KB/s], Decompressed: 8191 Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 76 KB/s], Decompressed: 8239 Downloaded: 8287 file(s) [attempted 8287/8459 = 97%, 133 KB/s], Decompressed: 8284 Downloaded: 8333 file(s) [attempted 8333/8459 = 98%, 89 KB/s], Decompressed: 8321 Downloaded: 8369 file(s) [attempted 8369/8459 = 98%, 856 KB/s], Decompressed: 8362 Downloaded: 8410 file(s) [attempted 8410/8459 = 99%, 142 KB/s], Decompressed: 8403 Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 774 KB/s], Decompressed: 8445 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 774 KB/s], Decompressed: 8454
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (25s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.8s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.7s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/772] Built Iut.Foundations.QualitativeData (2.1s)
✔ [3382/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.8s)
✔ [3388/3393] Built Iut.Stage1.CorollarySchema (34s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.5s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (87s)
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 (6.3s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (4.9s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.3s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.1s)
⚠ [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 (172s)
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`