Verification run
Run 1049
failed commit
069488bb49af toolchain lean-v4-30-0 prover lean took 23m 51s · 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-1348-source
exit_code=Some(0) duration_ms=3785
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1348-source'...
$ git checkout 069488bb49afaf5f1a1702af6e884a9949845dc4
exit_code=Some(0) duration_ms=144
stderr:
Note: switching to '069488bb49afaf5f1a1702af6e884a9949845dc4'.
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 069488b Bundle valuation ball named HDD boundary
Resolved source revision: 069488bb49afaf5f1a1702af6e884a9949845dc4
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=069488bb49afaf5f1a1702af6e884a9949845dc4 provenance={"branch":"master","checked_out_revision":"069488bb49afaf5f1a1702af6e884a9949845dc4","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"069488bb49afaf5f1a1702af6e884a9949845dc4","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=115201
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: 13 file(s) [attempted 13/8459 = 0%, 5 KB/s], Decompressed: 3
Downloaded: 35 file(s) [attempted 35/8459 = 0%, 15 KB/s], Decompressed: 3
Downloaded: 57 file(s) [attempted 57/8459 = 0%, 185 KB/s], Decompressed: 50
Downloaded: 82 file(s) [attempted 82/8459 = 0%, 500 KB/s], Decompressed: 79
Downloaded: 117 file(s) [attempted 117/8459 = 1%, 287 KB/s], Decompressed: 112
Downloaded: 151 file(s) [attempted 151/8459 = 1%, 284 KB/s], Decompressed: 148
Downloaded: 186 file(s) [attempted 186/8459 = 2%, 516 KB/s], Decompressed: 179
Downloaded: 220 file(s) [attempted 220/8459 = 2%, 608 KB/s], Decompressed: 179
Downloaded: 256 file(s) [attempted 256/8459 = 3%, 593 KB/s], Decompressed: 182
Downloaded: 289 file(s) [attempted 289/8459 = 3%, 131 KB/s], Decompressed: 282
Downloaded: 327 file(s) [attempted 327/8459 = 3%, 313 KB/s], Decompressed: 319
Downloaded: 371 file(s) [attempted 371/8459 = 4%, 150 KB/s], Decompressed: 343
Downloaded: 405 file(s) [attempted 405/8459 = 4%, 473 KB/s], Decompressed: 343
Downloaded: 443 file(s) [attempted 443/8459 = 5%, 245 KB/s], Decompressed: 353
Downloaded: 489 file(s) [attempted 489/8459 = 5%, 271 KB/s], Decompressed: 484
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 735 KB/s], Decompressed: 525
Downloaded: 562 file(s) [attempted 562/8459 = 6%, 482 KB/s], Decompressed: 560
Downloaded: 600 file(s) [attempted 600/8459 = 7%, 229 KB/s], Decompressed: 593
Downloaded: 642 file(s) [attempted 642/8459 = 7%, 247 KB/s], Decompressed: 638
Downloaded: 686 file(s) [attempted 686/8459 = 8%, 135 KB/s], Decompressed: 682
Downloaded: 730 file(s) [attempted 730/8459 = 8%, 69 KB/s], Decompressed: 689
Downloaded: 771 file(s) [attempted 771/8459 = 9%, 830 KB/s], Decompressed: 689
Downloaded: 809 file(s) [attempted 809/8459 = 9%, 130 KB/s], Decompressed: 802
Downloaded: 852 file(s) [attempted 852/8459 = 10%, 183 KB/s], Decompressed: 812
Downloaded: 891 file(s) [attempted 891/8459 = 10%, 142 KB/s], Decompressed: 812
Downloaded: 930 file(s) [attempted 930/8459 = 10%, 1014 KB/s], Decompressed: 925
Downloaded: 970 file(s) [attempted 970/8459 = 11%, 283 KB/s], Decompressed: 963
Downloaded: 1011 file(s) [attempted 1011/8459 = 11%, 351 KB/s], Decompressed: 1004
Downloaded: 1056 file(s) [attempted 1056/8459 = 12%, 345 KB/s], Decompressed: 1004
Downloaded: 1100 file(s) [attempted 1100/8459 = 13%, 60 KB/s], Decompressed: 1004
Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 181 KB/s], Decompressed: 1104
Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 136 KB/s], Decompressed: 1104
Downloaded: 1216 file(s) [attempted 1216/8459 = 14%, 230 KB/s], Decompressed: 1121
Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 205 KB/s], Decompressed: 1251
Downloaded: 1295 file(s) [attempted 1295/8459 = 15%, 704 KB/s], Decompressed: 1281
Downloaded: 1333 file(s) [attempted 1333/8459 = 15%, 51 KB/s], Decompressed: 1329
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 29 KB/s], Decompressed: 1374
Downloaded: 1422 file(s) [attempted 1422/8459 = 16%, 871 KB/s], Decompressed: 1377
Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 338 KB/s], Decompressed: 1377
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 192 KB/s], Decompressed: 1494
Downloaded: 1537 file(s) [attempted 1537/8459 = 18%, 153 KB/s], Decompressed: 1531
Downloaded: 1579 file(s) [attempted 1579/8459 = 18%, 545 KB/s], Decompressed: 1576
Downloaded: 1624 file(s) [attempted 1624/8459 = 19%, 568 KB/s], Decompressed: 1620
Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 573 KB/s], Decompressed: 1655
Downloaded: 1706 file(s) [attempted 1706/8459 = 20%, 500 KB/s], Decompressed: 1702
Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 94 KB/s], Decompressed: 1733
Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 371 KB/s], Decompressed: 1781
Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 706 KB/s], Decompressed: 1826
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 1862 KB/s], Decompressed: 1863
Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 91 KB/s], Decompressed: 1901
Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 165 KB/s], Decompressed: 1939
Downloaded: 1980 file(s) [attempted 1980/8459 = 23%, 141 KB/s], Decompressed: 1976
Downloaded: 2018 file(s) [attempted 2018/8459 = 23%, 59 KB/s], Decompressed: 2010
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 40 KB/s], Decompressed: 2051
Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 298 KB/s], Decompressed: 2062
Downloaded: 2144 file(s) [attempted 2144/8459 = 25%, 1747 KB/s], Decompressed: 2062
Downloaded: 2182 file(s) [attempted 2182/8459 = 25%, 433 KB/s], Decompressed: 2178
Downloaded: 2223 file(s) [attempted 2223/8459 = 26%, 88 KB/s], Decompressed: 2219
Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 102 KB/s], Decompressed: 2260
Downloaded: 2308 file(s) [attempted 2308/8459 = 27%, 123 KB/s], Decompressed: 2298
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 116 KB/s], Decompressed: 2298
Downloaded: 2383 file(s) [attempted 2383/8459 = 28%, 278 KB/s], Decompressed: 2298
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 37 KB/s], Decompressed: 2308
Downloaded: 2469 file(s) [attempted 2469/8459 = 29%, 870 KB/s], Decompressed: 2308
Downloaded: 2510 file(s) [attempted 2510/8459 = 29%, 264 KB/s], Decompressed: 2390
Downloaded: 2551 file(s) [attempted 2551/8459 = 30%, 229 KB/s], Decompressed: 2390
Downloaded: 2596 file(s) [attempted 2596/8459 = 30%, 156 KB/s], Decompressed: 2490
Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 418 KB/s], Decompressed: 2490
Downloaded: 2671 file(s) [attempted 2671/8459 = 31%, 368 KB/s], Decompressed: 2490
Downloaded: 2712 file(s) [attempted 2712/8459 = 32%, 667 KB/s], Decompressed: 2709
Downloaded: 2757 file(s) [attempted 2757/8459 = 32%, 103 KB/s], Decompressed: 2750
Downloaded: 2794 file(s) [attempted 2794/8459 = 33%, 647 KB/s], Decompressed: 2787
Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 2221 KB/s], Decompressed: 2832
Downloaded: 2877 file(s) [attempted 2877/8459 = 34%, 1006 KB/s], Decompressed: 2869
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 275 KB/s], Decompressed: 2911
Downloaded: 2958 file(s) [attempted 2958/8459 = 34%, 480 KB/s], Decompressed: 2952
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 186 KB/s], Decompressed: 2965
Downloaded: 3037 file(s) [attempted 3037/8459 = 35%, 108 KB/s], Decompressed: 2965
Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 784 KB/s], Decompressed: 3068
Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 36 KB/s], Decompressed: 3106
Downloaded: 3160 file(s) [attempted 3160/8459 = 37%, 143 KB/s], Decompressed: 3112
Downloaded: 3208 file(s) [attempted 3208/8459 = 37%, 1363 KB/s], Decompressed: 3123
Downloaded: 3253 file(s) [attempted 3253/8459 = 38%, 211 KB/s], Decompressed: 3123
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 131 KB/s], Decompressed: 3263
Downloaded: 3328 file(s) [attempted 3328/8459 = 39%, 215 KB/s], Decompressed: 3325
Downloaded: 3372 file(s) [attempted 3372/8459 = 39%, 115 KB/s], Decompressed: 3359
Downloaded: 3414 file(s) [attempted 3414/8459 = 40%, 172 KB/s], Decompressed: 3410
Downloaded: 3455 file(s) [attempted 3455/8459 = 40%, 48 KB/s], Decompressed: 3448
Downloaded: 3496 file(s) [attempted 3496/8459 = 41%, 112 KB/s], Decompressed: 3489
Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 143 KB/s], Decompressed: 3526
Downloaded: 3578 file(s) [attempted 3578/8459 = 42%, 744 KB/s], Decompressed: 3574
Downloaded: 3622 file(s) [attempted 3622/8459 = 42%, 1030 KB/s], Decompressed: 3615
Downloaded: 3663 file(s) [attempted 3663/8459 = 43%, 263 KB/s], Decompressed: 3650
Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 327 KB/s], Decompressed: 3650
Downloaded: 3742 file(s) [attempted 3742/8459 = 44%, 380 KB/s], Decompressed: 3657
Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 102 KB/s], Decompressed: 3759
Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 25 KB/s], Decompressed: 3759
Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 223 KB/s], Decompressed: 3869
Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 114 KB/s], Decompressed: 3882
Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 372 KB/s], Decompressed: 3882
Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 727 KB/s], Decompressed: 3886
Downloaded: 4030 file(s) [attempted 4030/8459 = 47%, 106 KB/s], Decompressed: 3978
Downloaded: 4074 file(s) [attempted 4074/8459 = 48%, 369 KB/s], Decompressed: 3978
Downloaded: 4115 file(s) [attempted 4115/8459 = 48%, 169 KB/s], Decompressed: 3995
Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 45 KB/s], Decompressed: 3995
Downloaded: 4190 file(s) [attempted 4190/8459 = 49%, 2087 KB/s], Decompressed: 4081
Downloaded: 4235 file(s) [attempted 4235/8459 = 50%, 707 KB/s], Decompressed: 4081
Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 338 KB/s], Decompressed: 4262
Downloaded: 4322 file(s) [attempted 4322/8459 = 51%, 360 KB/s], Decompressed: 4314
Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 579 KB/s], Decompressed: 4355
Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 217 KB/s], Decompressed: 4368
Downloaded: 4437 file(s) [attempted 4437/8459 = 52%, 286 KB/s], Decompressed: 4368
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 189 KB/s], Decompressed: 4375
Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 25 KB/s], Decompressed: 4481
Downloaded: 4557 file(s) [attempted 4557/8459 = 53%, 289 KB/s], Decompressed: 4481
Downloaded: 4598 file(s) [attempted 4598/8459 = 54%, 558 KB/s], Decompressed: 4591
Downloaded: 4635 file(s) [attempted 4635/8459 = 54%, 545 KB/s], Decompressed: 4615
Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 141 KB/s], Decompressed: 4615
Downloaded: 4717 file(s) [attempted 4717/8459 = 55%, 192 KB/s], Decompressed: 4704
Downloaded: 4762 file(s) [attempted 4762/8459 = 56%, 769 KB/s], Decompressed: 4755
Downloaded: 4805 file(s) [attempted 4805/8459 = 56%, 397 KB/s], Decompressed: 4779
Downloaded: 4841 file(s) [attempted 4841/8459 = 57%, 233 KB/s], Decompressed: 4779
Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 271 KB/s], Decompressed: 4786
Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 269 KB/s], Decompressed: 4902
Downloaded: 4960 file(s) [attempted 4960/8459 = 58%, 481 KB/s], Decompressed: 4902
Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 186 KB/s], Decompressed: 4906
Downloaded: 5046 file(s) [attempted 5046/8459 = 59%, 418 KB/s], Decompressed: 4906
Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 108 KB/s], Decompressed: 4906
Downloaded: 5122 file(s) [attempted 5122/8459 = 60%, 88 KB/s], Decompressed: 5118
Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 46 KB/s], Decompressed: 5152
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 26 KB/s], Decompressed: 5159
Downloaded: 5241 file(s) [attempted 5241/8459 = 61%, 46 KB/s], Decompressed: 5166
Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 719 KB/s], Decompressed: 5166
Downloaded: 5321 file(s) [attempted 5321/8459 = 62%, 1124 KB/s], Decompressed: 5224
Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 747 KB/s], Decompressed: 5354
Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 260 KB/s], Decompressed: 5395
Downloaded: 5441 file(s) [attempted 5441/8459 = 64%, 536 KB/s], Decompressed: 5436
Downloaded: 5481 file(s) [attempted 5481/8459 = 64%, 67 KB/s], Decompressed: 5477
Downloaded: 5522 file(s) [attempted 5522/8459 = 65%, 189 KB/s], Decompressed: 5518
Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 80 KB/s], Decompressed: 5542
Downloaded: 5607 file(s) [attempted 5607/8459 = 66%, 188 KB/s], Decompressed: 5542
Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 1156 KB/s], Decompressed: 5631
Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 450 KB/s], Decompressed: 5686
Downloaded: 5729 file(s) [attempted 5729/8459 = 67%, 683 KB/s], Decompressed: 5724
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 295 KB/s], Decompressed: 5761
Downloaded: 5809 file(s) [attempted 5809/8459 = 68%, 428 KB/s], Decompressed: 5806
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 989 KB/s], Decompressed: 5843
Downloaded: 5891 file(s) [attempted 5891/8459 = 69%, 316 KB/s], Decompressed: 5885
Downloaded: 5936 file(s) [attempted 5936/8459 = 70%, 140 KB/s], Decompressed: 5885
Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 93 KB/s], Decompressed: 5888
Downloaded: 6015 file(s) [attempted 6015/8459 = 71%, 1085 KB/s], Decompressed: 5888
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 2217 KB/s], Decompressed: 5888
Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 41 KB/s], Decompressed: 6083
Downloaded: 6134 file(s) [attempted 6134/8459 = 72%, 115 KB/s], Decompressed: 6083
Downloaded: 6172 file(s) [attempted 6172/8459 = 72%, 291 KB/s], Decompressed: 6090
Downloaded: 6213 file(s) [attempted 6213/8459 = 73%, 309 KB/s], Decompressed: 6090
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 88 KB/s], Decompressed: 6090
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 810 KB/s], Decompressed: 6288
Downloaded: 6338 file(s) [attempted 6338/8459 = 74%, 351 KB/s], Decompressed: 6329
Downloaded: 6370 file(s) [attempted 6370/8459 = 75%, 528 KB/s], Decompressed: 6367
Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 87 KB/s], Decompressed: 6408
Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 126 KB/s], Decompressed: 6446
Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 720 KB/s], Decompressed: 6490
Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 426 KB/s], Decompressed: 6521
Downloaded: 6579 file(s) [attempted 6579/8459 = 77%, 365 KB/s], Decompressed: 6521
Downloaded: 6613 file(s) [attempted 6613/8459 = 78%, 600 KB/s], Decompressed: 6524
Downloaded: 6655 file(s) [attempted 6655/8459 = 78%, 132 KB/s], Decompressed: 6524
Downloaded: 6696 file(s) [attempted 6696/8459 = 79%, 146 KB/s], Decompressed: 6610
Downloaded: 6737 file(s) [attempted 6737/8459 = 79%, 73 KB/s], Decompressed: 6610
Downloaded: 6781 file(s) [attempted 6781/8459 = 80%, 574 KB/s], Decompressed: 6696
Downloaded: 6826 file(s) [attempted 6826/8459 = 80%, 44 KB/s], Decompressed: 6696
Downloaded: 6867 file(s) [attempted 6867/8459 = 81%, 143 KB/s], Decompressed: 6696
Downloaded: 6908 file(s) [attempted 6908/8459 = 81%, 939 KB/s], Decompressed: 6880
Downloaded: 6945 file(s) [attempted 6945/8459 = 82%, 74 KB/s], Decompressed: 6904
Downloaded: 6987 file(s) [attempted 6987/8459 = 82%, 105 KB/s], Decompressed: 6904
Downloaded: 7028 file(s) [attempted 7028/8459 = 83%, 461 KB/s], Decompressed: 6911
Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 150 KB/s], Decompressed: 6911
Downloaded: 7106 file(s) [attempted 7106/8459 = 84%, 358 KB/s], Decompressed: 7017
Downloaded: 7147 file(s) [attempted 7147/8459 = 84%, 1420 KB/s], Decompressed: 7017
Downloaded: 7188 file(s) [attempted 7188/8459 = 84%, 66 KB/s], Decompressed: 7017
Downloaded: 7229 file(s) [attempted 7229/8459 = 85%, 425 KB/s], Decompressed: 7206
Downloaded: 7271 file(s) [attempted 7271/8459 = 85%, 79 KB/s], Decompressed: 7267
Downloaded: 7314 file(s) [attempted 7314/8459 = 86%, 192 KB/s], Decompressed: 7308
Downloaded: 7350 file(s) [attempted 7350/8459 = 86%, 107 KB/s], Decompressed: 7346
Downloaded: 7390 file(s) [attempted 7390/8459 = 87%, 178 KB/s], Decompressed: 7387
Downloaded: 7431 file(s) [attempted 7431/8459 = 87%, 569 KB/s], Decompressed: 7421
Downloaded: 7472 file(s) [attempted 7472/8459 = 88%, 308 KB/s], Decompressed: 7421
Downloaded: 7514 file(s) [attempted 7514/8459 = 88%, 850 KB/s], Decompressed: 7421
Downloaded: 7551 file(s) [attempted 7551/8459 = 89%, 344 KB/s], Decompressed: 7548
Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 95 KB/s], Decompressed: 7585
Downloaded: 7633 file(s) [attempted 7633/8459 = 90%, 163 KB/s], Decompressed: 7630
Downloaded: 7678 file(s) [attempted 7678/8459 = 90%, 646 KB/s], Decompressed: 7674
Downloaded: 7722 file(s) [attempted 7722/8459 = 91%, 44 KB/s], Decompressed: 7715
Downloaded: 7763 file(s) [attempted 7763/8459 = 91%, 302 KB/s], Decompressed: 7750
Downloaded: 7801 file(s) [attempted 7801/8459 = 92%, 162 KB/s], Decompressed: 7787
Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 1131 KB/s], Decompressed: 7787
Downloaded: 7883 file(s) [attempted 7883/8459 = 93%, 96 KB/s], Decompressed: 7794
Downloaded: 7924 file(s) [attempted 7924/8459 = 93%, 35 KB/s], Decompressed: 7794
Downloaded: 7965 file(s) [attempted 7965/8459 = 94%, 179 KB/s], Decompressed: 7794
Downloaded: 8001 file(s) [attempted 8001/8459 = 94%, 211 KB/s], Decompressed: 7993
Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 443 KB/s], Decompressed: 8037
Downloaded: 8088 file(s) [attempted 8088/8459 = 95%, 177 KB/s], Decompressed: 8061
Downloaded: 8130 file(s) [attempted 8130/8459 = 96%, 112 KB/s], Decompressed: 8061
Downloaded: 8174 file(s) [attempted 8174/8459 = 96%, 438 KB/s], Decompressed: 8167
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 95 KB/s], Decompressed: 8208
Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 492 KB/s], Decompressed: 8253
Downloaded: 8295 file(s) [attempted 8295/8459 = 98%, 419 KB/s], Decompressed: 8290
Downloaded: 8338 file(s) [attempted 8338/8459 = 98%, 211 KB/s], Decompressed: 8331
Downloaded: 8379 file(s) [attempted 8379/8459 = 99%, 562 KB/s], Decompressed: 8369
Downloaded: 8420 file(s) [attempted 8420/8459 = 99%, 715 KB/s], Decompressed: 8369
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 111 KB/s], Decompressed: 8373
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 111 KB/s], Decompressed: 8373
$ lake build
exit_code=Some(1) duration_ms=815193
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (95s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [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.2s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.6s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.7s)
✔ [3389/3394] Built Iut.Stage1.CorollarySchema (81s)
✔ [3390/3397] Built Iut.Stage1.SourceObligations (3.3s)
✔ [3392/3398] Built Iut.Stage1.IUTSourceScaffold (2.8s)
✔ [3394/3401] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (111s)
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 (74s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (18s)
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 (11s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.2s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.6s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.3s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (26s)
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 (276s)
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=4505
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-1348-source
Cloning into '/var/lib/apodeixis/repos/job-1348-source'...
git_checkout exit 0
git checkout 069488bb49afaf5f1a1702af6e884a9949845dc4
Note: switching to '069488bb49afaf5f1a1702af6e884a9949845dc4'. 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 069488b Bundle valuation ball named HDD boundary
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: 13 file(s) [attempted 13/8459 = 0%, 5 KB/s], Decompressed: 3 Downloaded: 35 file(s) [attempted 35/8459 = 0%, 15 KB/s], Decompressed: 3 Downloaded: 57 file(s) [attempted 57/8459 = 0%, 185 KB/s], Decompressed: 50 Downloaded: 82 file(s) [attempted 82/8459 = 0%, 500 KB/s], Decompressed: 79 Downloaded: 117 file(s) [attempted 117/8459 = 1%, 287 KB/s], Decompressed: 112 Downloaded: 151 file(s) [attempted 151/8459 = 1%, 284 KB/s], Decompressed: 148 Downloaded: 186 file(s) [attempted 186/8459 = 2%, 516 KB/s], Decompressed: 179 Downloaded: 220 file(s) [attempted 220/8459 = 2%, 608 KB/s], Decompressed: 179 Downloaded: 256 file(s) [attempted 256/8459 = 3%, 593 KB/s], Decompressed: 182 Downloaded: 289 file(s) [attempted 289/8459 = 3%, 131 KB/s], Decompressed: 282 Downloaded: 327 file(s) [attempted 327/8459 = 3%, 313 KB/s], Decompressed: 319 Downloaded: 371 file(s) [attempted 371/8459 = 4%, 150 KB/s], Decompressed: 343 Downloaded: 405 file(s) [attempted 405/8459 = 4%, 473 KB/s], Decompressed: 343 Downloaded: 443 file(s) [attempted 443/8459 = 5%, 245 KB/s], Decompressed: 353 Downloaded: 489 file(s) [attempted 489/8459 = 5%, 271 KB/s], Decompressed: 484 Downloaded: 528 file(s) [attempted 528/8459 = 6%, 735 KB/s], Decompressed: 525 Downloaded: 562 file(s) [attempted 562/8459 = 6%, 482 KB/s], Decompressed: 560 Downloaded: 600 file(s) [attempted 600/8459 = 7%, 229 KB/s], Decompressed: 593 Downloaded: 642 file(s) [attempted 642/8459 = 7%, 247 KB/s], Decompressed: 638 Downloaded: 686 file(s) [attempted 686/8459 = 8%, 135 KB/s], Decompressed: 682 Downloaded: 730 file(s) [attempted 730/8459 = 8%, 69 KB/s], Decompressed: 689 Downloaded: 771 file(s) [attempted 771/8459 = 9%, 830 KB/s], Decompressed: 689 Downloaded: 809 file(s) [attempted 809/8459 = 9%, 130 KB/s], Decompressed: 802 Downloaded: 852 file(s) [attempted 852/8459 = 10%, 183 KB/s], Decompressed: 812 Downloaded: 891 file(s) [attempted 891/8459 = 10%, 142 KB/s], Decompressed: 812 Downloaded: 930 file(s) [attempted 930/8459 = 10%, 1014 KB/s], Decompressed: 925 Downloaded: 970 file(s) [attempted 970/8459 = 11%, 283 KB/s], Decompressed: 963 Downloaded: 1011 file(s) [attempted 1011/8459 = 11%, 351 KB/s], Decompressed: 1004 Downloaded: 1056 file(s) [attempted 1056/8459 = 12%, 345 KB/s], Decompressed: 1004 Downloaded: 1100 file(s) [attempted 1100/8459 = 13%, 60 KB/s], Decompressed: 1004 Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 181 KB/s], Decompressed: 1104 Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 136 KB/s], Decompressed: 1104 Downloaded: 1216 file(s) [attempted 1216/8459 = 14%, 230 KB/s], Decompressed: 1121 Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 205 KB/s], Decompressed: 1251 Downloaded: 1295 file(s) [attempted 1295/8459 = 15%, 704 KB/s], Decompressed: 1281 Downloaded: 1333 file(s) [attempted 1333/8459 = 15%, 51 KB/s], Decompressed: 1329 Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 29 KB/s], Decompressed: 1374 Downloaded: 1422 file(s) [attempted 1422/8459 = 16%, 871 KB/s], Decompressed: 1377 Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 338 KB/s], Decompressed: 1377 Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 192 KB/s], Decompressed: 1494 Downloaded: 1537 file(s) [attempted 1537/8459 = 18%, 153 KB/s], Decompressed: 1531 Downloaded: 1579 file(s) [attempted 1579/8459 = 18%, 545 KB/s], Decompressed: 1576 Downloaded: 1624 file(s) [attempted 1624/8459 = 19%, 568 KB/s], Decompressed: 1620 Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 573 KB/s], Decompressed: 1655 Downloaded: 1706 file(s) [attempted 1706/8459 = 20%, 500 KB/s], Decompressed: 1702 Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 94 KB/s], Decompressed: 1733 Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 371 KB/s], Decompressed: 1781 Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 706 KB/s], Decompressed: 1826 Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 1862 KB/s], Decompressed: 1863 Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 91 KB/s], Decompressed: 1901 Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 165 KB/s], Decompressed: 1939 Downloaded: 1980 file(s) [attempted 1980/8459 = 23%, 141 KB/s], Decompressed: 1976 Downloaded: 2018 file(s) [attempted 2018/8459 = 23%, 59 KB/s], Decompressed: 2010 Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 40 KB/s], Decompressed: 2051 Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 298 KB/s], Decompressed: 2062 Downloaded: 2144 file(s) [attempted 2144/8459 = 25%, 1747 KB/s], Decompressed: 2062 Downloaded: 2182 file(s) [attempted 2182/8459 = 25%, 433 KB/s], Decompressed: 2178 Downloaded: 2223 file(s) [attempted 2223/8459 = 26%, 88 KB/s], Decompressed: 2219 Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 102 KB/s], Decompressed: 2260 Downloaded: 2308 file(s) [attempted 2308/8459 = 27%, 123 KB/s], Decompressed: 2298 Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 116 KB/s], Decompressed: 2298 Downloaded: 2383 file(s) [attempted 2383/8459 = 28%, 278 KB/s], Decompressed: 2298 Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 37 KB/s], Decompressed: 2308 Downloaded: 2469 file(s) [attempted 2469/8459 = 29%, 870 KB/s], Decompressed: 2308 Downloaded: 2510 file(s) [attempted 2510/8459 = 29%, 264 KB/s], Decompressed: 2390 Downloaded: 2551 file(s) [attempted 2551/8459 = 30%, 229 KB/s], Decompressed: 2390 Downloaded: 2596 file(s) [attempted 2596/8459 = 30%, 156 KB/s], Decompressed: 2490 Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 418 KB/s], Decompressed: 2490 Downloaded: 2671 file(s) [attempted 2671/8459 = 31%, 368 KB/s], Decompressed: 2490 Downloaded: 2712 file(s) [attempted 2712/8459 = 32%, 667 KB/s], Decompressed: 2709 Downloaded: 2757 file(s) [attempted 2757/8459 = 32%, 103 KB/s], Decompressed: 2750 Downloaded: 2794 file(s) [attempted 2794/8459 = 33%, 647 KB/s], Decompressed: 2787 Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 2221 KB/s], Decompressed: 2832 Downloaded: 2877 file(s) [attempted 2877/8459 = 34%, 1006 KB/s], Decompressed: 2869 Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 275 KB/s], Decompressed: 2911 Downloaded: 2958 file(s) [attempted 2958/8459 = 34%, 480 KB/s], Decompressed: 2952 Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 186 KB/s], Decompressed: 2965 Downloaded: 3037 file(s) [attempted 3037/8459 = 35%, 108 KB/s], Decompressed: 2965 Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 784 KB/s], Decompressed: 3068 Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 36 KB/s], Decompressed: 3106 Downloaded: 3160 file(s) [attempted 3160/8459 = 37%, 143 KB/s], Decompressed: 3112 Downloaded: 3208 file(s) [attempted 3208/8459 = 37%, 1363 KB/s], Decompressed: 3123 Downloaded: 3253 file(s) [attempted 3253/8459 = 38%, 211 KB/s], Decompressed: 3123 Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 131 KB/s], Decompressed: 3263 Downloaded: 3328 file(s) [attempted 3328/8459 = 39%, 215 KB/s], Decompressed: 3325 Downloaded: 3372 file(s) [attempted 3372/8459 = 39%, 115 KB/s], Decompressed: 3359 Downloaded: 3414 file(s) [attempted 3414/8459 = 40%, 172 KB/s], Decompressed: 3410 Downloaded: 3455 file(s) [attempted 3455/8459 = 40%, 48 KB/s], Decompressed: 3448 Downloaded: 3496 file(s) [attempted 3496/8459 = 41%, 112 KB/s], Decompressed: 3489 Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 143 KB/s], Decompressed: 3526 Downloaded: 3578 file(s) [attempted 3578/8459 = 42%, 744 KB/s], Decompressed: 3574 Downloaded: 3622 file(s) [attempted 3622/8459 = 42%, 1030 KB/s], Decompressed: 3615 Downloaded: 3663 file(s) [attempted 3663/8459 = 43%, 263 KB/s], Decompressed: 3650 Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 327 KB/s], Decompressed: 3650 Downloaded: 3742 file(s) [attempted 3742/8459 = 44%, 380 KB/s], Decompressed: 3657 Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 102 KB/s], Decompressed: 3759 Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 25 KB/s], Decompressed: 3759 Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 223 KB/s], Decompressed: 3869 Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 114 KB/s], Decompressed: 3882 Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 372 KB/s], Decompressed: 3882 Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 727 KB/s], Decompressed: 3886 Downloaded: 4030 file(s) [attempted 4030/8459 = 47%, 106 KB/s], Decompressed: 3978 Downloaded: 4074 file(s) [attempted 4074/8459 = 48%, 369 KB/s], Decompressed: 3978 Downloaded: 4115 file(s) [attempted 4115/8459 = 48%, 169 KB/s], Decompressed: 3995 Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 45 KB/s], Decompressed: 3995 Downloaded: 4190 file(s) [attempted 4190/8459 = 49%, 2087 KB/s], Decompressed: 4081 Downloaded: 4235 file(s) [attempted 4235/8459 = 50%, 707 KB/s], Decompressed: 4081 Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 338 KB/s], Decompressed: 4262 Downloaded: 4322 file(s) [attempted 4322/8459 = 51%, 360 KB/s], Decompressed: 4314 Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 579 KB/s], Decompressed: 4355 Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 217 KB/s], Decompressed: 4368 Downloaded: 4437 file(s) [attempted 4437/8459 = 52%, 286 KB/s], Decompressed: 4368 Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 189 KB/s], Decompressed: 4375 Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 25 KB/s], Decompressed: 4481 Downloaded: 4557 file(s) [attempted 4557/8459 = 53%, 289 KB/s], Decompressed: 4481 Downloaded: 4598 file(s) [attempted 4598/8459 = 54%, 558 KB/s], Decompressed: 4591 Downloaded: 4635 file(s) [attempted 4635/8459 = 54%, 545 KB/s], Decompressed: 4615 Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 141 KB/s], Decompressed: 4615 Downloaded: 4717 file(s) [attempted 4717/8459 = 55%, 192 KB/s], Decompressed: 4704 Downloaded: 4762 file(s) [attempted 4762/8459 = 56%, 769 KB/s], Decompressed: 4755 Downloaded: 4805 file(s) [attempted 4805/8459 = 56%, 397 KB/s], Decompressed: 4779 Downloaded: 4841 file(s) [attempted 4841/8459 = 57%, 233 KB/s], Decompressed: 4779 Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 271 KB/s], Decompressed: 4786 Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 269 KB/s], Decompressed: 4902 Downloaded: 4960 file(s) [attempted 4960/8459 = 58%, 481 KB/s], Decompressed: 4902 Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 186 KB/s], Decompressed: 4906 Downloaded: 5046 file(s) [attempted 5046/8459 = 59%, 418 KB/s], Decompressed: 4906 Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 108 KB/s], Decompressed: 4906 Downloaded: 5122 file(s) [attempted 5122/8459 = 60%, 88 KB/s], Decompressed: 5118 Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 46 KB/s], Decompressed: 5152 Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 26 KB/s], Decompressed: 5159 Downloaded: 5241 file(s) [attempted 5241/8459 = 61%, 46 KB/s], Decompressed: 5166 Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 719 KB/s], Decompressed: 5166 Downloaded: 5321 file(s) [attempted 5321/8459 = 62%, 1124 KB/s], Decompressed: 5224 Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 747 KB/s], Decompressed: 5354 Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 260 KB/s], Decompressed: 5395 Downloaded: 5441 file(s) [attempted 5441/8459 = 64%, 536 KB/s], Decompressed: 5436 Downloaded: 5481 file(s) [attempted 5481/8459 = 64%, 67 KB/s], Decompressed: 5477 Downloaded: 5522 file(s) [attempted 5522/8459 = 65%, 189 KB/s], Decompressed: 5518 Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 80 KB/s], Decompressed: 5542 Downloaded: 5607 file(s) [attempted 5607/8459 = 66%, 188 KB/s], Decompressed: 5542 Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 1156 KB/s], Decompressed: 5631 Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 450 KB/s], Decompressed: 5686 Downloaded: 5729 file(s) [attempted 5729/8459 = 67%, 683 KB/s], Decompressed: 5724 Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 295 KB/s], Decompressed: 5761 Downloaded: 5809 file(s) [attempted 5809/8459 = 68%, 428 KB/s], Decompressed: 5806 Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 989 KB/s], Decompressed: 5843 Downloaded: 5891 file(s) [attempted 5891/8459 = 69%, 316 KB/s], Decompressed: 5885 Downloaded: 5936 file(s) [attempted 5936/8459 = 70%, 140 KB/s], Decompressed: 5885 Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 93 KB/s], Decompressed: 5888 Downloaded: 6015 file(s) [attempted 6015/8459 = 71%, 1085 KB/s], Decompressed: 5888 Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 2217 KB/s], Decompressed: 5888 Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 41 KB/s], Decompressed: 6083 Downloaded: 6134 file(s) [attempted 6134/8459 = 72%, 115 KB/s], Decompressed: 6083 Downloaded: 6172 file(s) [attempted 6172/8459 = 72%, 291 KB/s], Decompressed: 6090 Downloaded: 6213 file(s) [attempted 6213/8459 = 73%, 309 KB/s], Decompressed: 6090 Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 88 KB/s], Decompressed: 6090 Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 810 KB/s], Decompressed: 6288 Downloaded: 6338 file(s) [attempted 6338/8459 = 74%, 351 KB/s], Decompressed: 6329 Downloaded: 6370 file(s) [attempted 6370/8459 = 75%, 528 KB/s], Decompressed: 6367 Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 87 KB/s], Decompressed: 6408 Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 126 KB/s], Decompressed: 6446 Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 720 KB/s], Decompressed: 6490 Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 426 KB/s], Decompressed: 6521 Downloaded: 6579 file(s) [attempted 6579/8459 = 77%, 365 KB/s], Decompressed: 6521 Downloaded: 6613 file(s) [attempted 6613/8459 = 78%, 600 KB/s], Decompressed: 6524 Downloaded: 6655 file(s) [attempted 6655/8459 = 78%, 132 KB/s], Decompressed: 6524 Downloaded: 6696 file(s) [attempted 6696/8459 = 79%, 146 KB/s], Decompressed: 6610 Downloaded: 6737 file(s) [attempted 6737/8459 = 79%, 73 KB/s], Decompressed: 6610 Downloaded: 6781 file(s) [attempted 6781/8459 = 80%, 574 KB/s], Decompressed: 6696 Downloaded: 6826 file(s) [attempted 6826/8459 = 80%, 44 KB/s], Decompressed: 6696 Downloaded: 6867 file(s) [attempted 6867/8459 = 81%, 143 KB/s], Decompressed: 6696 Downloaded: 6908 file(s) [attempted 6908/8459 = 81%, 939 KB/s], Decompressed: 6880 Downloaded: 6945 file(s) [attempted 6945/8459 = 82%, 74 KB/s], Decompressed: 6904 Downloaded: 6987 file(s) [attempted 6987/8459 = 82%, 105 KB/s], Decompressed: 6904 Downloaded: 7028 file(s) [attempted 7028/8459 = 83%, 461 KB/s], Decompressed: 6911 Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 150 KB/s], Decompressed: 6911 Downloaded: 7106 file(s) [attempted 7106/8459 = 84%, 358 KB/s], Decompressed: 7017 Downloaded: 7147 file(s) [attempted 7147/8459 = 84%, 1420 KB/s], Decompressed: 7017 Downloaded: 7188 file(s) [attempted 7188/8459 = 84%, 66 KB/s], Decompressed: 7017 Downloaded: 7229 file(s) [attempted 7229/8459 = 85%, 425 KB/s], Decompressed: 7206 Downloaded: 7271 file(s) [attempted 7271/8459 = 85%, 79 KB/s], Decompressed: 7267 Downloaded: 7314 file(s) [attempted 7314/8459 = 86%, 192 KB/s], Decompressed: 7308 Downloaded: 7350 file(s) [attempted 7350/8459 = 86%, 107 KB/s], Decompressed: 7346 Downloaded: 7390 file(s) [attempted 7390/8459 = 87%, 178 KB/s], Decompressed: 7387 Downloaded: 7431 file(s) [attempted 7431/8459 = 87%, 569 KB/s], Decompressed: 7421 Downloaded: 7472 file(s) [attempted 7472/8459 = 88%, 308 KB/s], Decompressed: 7421 Downloaded: 7514 file(s) [attempted 7514/8459 = 88%, 850 KB/s], Decompressed: 7421 Downloaded: 7551 file(s) [attempted 7551/8459 = 89%, 344 KB/s], Decompressed: 7548 Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 95 KB/s], Decompressed: 7585 Downloaded: 7633 file(s) [attempted 7633/8459 = 90%, 163 KB/s], Decompressed: 7630 Downloaded: 7678 file(s) [attempted 7678/8459 = 90%, 646 KB/s], Decompressed: 7674 Downloaded: 7722 file(s) [attempted 7722/8459 = 91%, 44 KB/s], Decompressed: 7715 Downloaded: 7763 file(s) [attempted 7763/8459 = 91%, 302 KB/s], Decompressed: 7750 Downloaded: 7801 file(s) [attempted 7801/8459 = 92%, 162 KB/s], Decompressed: 7787 Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 1131 KB/s], Decompressed: 7787 Downloaded: 7883 file(s) [attempted 7883/8459 = 93%, 96 KB/s], Decompressed: 7794 Downloaded: 7924 file(s) [attempted 7924/8459 = 93%, 35 KB/s], Decompressed: 7794 Downloaded: 7965 file(s) [attempted 7965/8459 = 94%, 179 KB/s], Decompressed: 7794 Downloaded: 8001 file(s) [attempted 8001/8459 = 94%, 211 KB/s], Decompressed: 7993 Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 443 KB/s], Decompressed: 8037 Downloaded: 8088 file(s) [attempted 8088/8459 = 95%, 177 KB/s], Decompressed: 8061 Downloaded: 8130 file(s) [attempted 8130/8459 = 96%, 112 KB/s], Decompressed: 8061 Downloaded: 8174 file(s) [attempted 8174/8459 = 96%, 438 KB/s], Decompressed: 8167 Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 95 KB/s], Decompressed: 8208 Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 492 KB/s], Decompressed: 8253 Downloaded: 8295 file(s) [attempted 8295/8459 = 98%, 419 KB/s], Decompressed: 8290 Downloaded: 8338 file(s) [attempted 8338/8459 = 98%, 211 KB/s], Decompressed: 8331 Downloaded: 8379 file(s) [attempted 8379/8459 = 99%, 562 KB/s], Decompressed: 8369 Downloaded: 8420 file(s) [attempted 8420/8459 = 99%, 715 KB/s], Decompressed: 8369 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 111 KB/s], Decompressed: 8373 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 111 KB/s], Decompressed: 8373
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (95s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [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.2s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.6s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.7s)
✔ [3389/3394] Built Iut.Stage1.CorollarySchema (81s)
✔ [3390/3397] Built Iut.Stage1.SourceObligations (3.3s)
✔ [3392/3398] Built Iut.Stage1.IUTSourceScaffold (2.8s)
✔ [3394/3401] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (111s)
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 (74s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (18s)
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 (11s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.2s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.6s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.3s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (26s)
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 (276s)
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`