Verification run
Run 1066
failed commit
bf681f8016ff toolchain lean-v4-30-0 prover lean took 21m 5s · 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-1367-source
exit_code=Some(0) duration_ms=4087
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1367-source'...
$ git checkout bf681f8016ffedb0923c61ab7ebb81e2cef08828
exit_code=Some(0) duration_ms=51
stderr:
Note: switching to 'bf681f8016ffedb0923c61ab7ebb81e2cef08828'.
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 bf681f8 Route pointwise handoff through formula gap
Resolved source revision: bf681f8016ffedb0923c61ab7ebb81e2cef08828
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=bf681f8016ffedb0923c61ab7ebb81e2cef08828 provenance={"branch":"master","checked_out_revision":"bf681f8016ffedb0923c61ab7ebb81e2cef08828","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"bf681f8016ffedb0923c61ab7ebb81e2cef08828","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=37495
stdout:
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 5 KB/s], Decompressed: 3
Downloaded: 34 file(s) [attempted 34/8459 = 0%, 17 KB/s], Decompressed: 3
Downloaded: 66 file(s) [attempted 66/8459 = 0%, 48 KB/s], Decompressed: 65
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 190 KB/s], Decompressed: 82
Downloaded: 121 file(s) [attempted 121/8459 = 1%, 404 KB/s], Decompressed: 117
Downloaded: 155 file(s) [attempted 155/8459 = 1%, 213 KB/s], Decompressed: 134
Downloaded: 189 file(s) [attempted 189/8459 = 2%, 537 KB/s], Decompressed: 134
Downloaded: 223 file(s) [attempted 223/8459 = 2%, 330 KB/s], Decompressed: 141
Downloaded: 264 file(s) [attempted 264/8459 = 3%, 775 KB/s], Decompressed: 258
Downloaded: 302 file(s) [attempted 302/8459 = 3%, 26 KB/s], Decompressed: 258
Downloaded: 340 file(s) [attempted 340/8459 = 4%, 37 KB/s], Decompressed: 264
Downloaded: 377 file(s) [attempted 377/8459 = 4%, 395 KB/s], Decompressed: 367
Downloaded: 415 file(s) [attempted 415/8459 = 4%, 168 KB/s], Decompressed: 391
Downloaded: 457 file(s) [attempted 457/8459 = 5%, 208 KB/s], Decompressed: 453
Downloaded: 494 file(s) [attempted 494/8459 = 5%, 244 KB/s], Decompressed: 490
Downloaded: 529 file(s) [attempted 529/8459 = 6%, 209 KB/s], Decompressed: 521
Downloaded: 562 file(s) [attempted 562/8459 = 6%, 554 KB/s], Decompressed: 559
Downloaded: 607 file(s) [attempted 607/8459 = 7%, 147 KB/s], Decompressed: 604
Downloaded: 648 file(s) [attempted 648/8459 = 7%, 131 KB/s], Decompressed: 631
Downloaded: 689 file(s) [attempted 689/8459 = 8%, 132 KB/s], Decompressed: 648
Downloaded: 727 file(s) [attempted 727/8459 = 8%, 73 KB/s], Decompressed: 648
Downloaded: 765 file(s) [attempted 765/8459 = 9%, 212 KB/s], Decompressed: 655
Downloaded: 806 file(s) [attempted 806/8459 = 9%, 30 KB/s], Decompressed: 655
Downloaded: 848 file(s) [attempted 848/8459 = 10%, 118 KB/s], Decompressed: 831
Downloaded: 888 file(s) [attempted 888/8459 = 10%, 48 KB/s], Decompressed: 881
Downloaded: 925 file(s) [attempted 925/8459 = 10%, 332 KB/s], Decompressed: 919
Downloaded: 967 file(s) [attempted 967/8459 = 11%, 210 KB/s], Decompressed: 963
Downloaded: 1011 file(s) [attempted 1011/8459 = 11%, 464 KB/s], Decompressed: 1004
Downloaded: 1053 file(s) [attempted 1053/8459 = 12%, 85 KB/s], Decompressed: 1049
Downloaded: 1090 file(s) [attempted 1090/8459 = 12%, 72 KB/s], Decompressed: 1083
Downloaded: 1125 file(s) [attempted 1125/8459 = 13%, 138 KB/s], Decompressed: 1121
Downloaded: 1165 file(s) [attempted 1165/8459 = 13%, 1210 KB/s], Decompressed: 1162
Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 255 KB/s], Decompressed: 1199
Downloaded: 1247 file(s) [attempted 1247/8459 = 14%, 97 KB/s], Decompressed: 1240
Downloaded: 1288 file(s) [attempted 1288/8459 = 15%, 229 KB/s], Decompressed: 1281
Downloaded: 1333 file(s) [attempted 1333/8459 = 15%, 65 KB/s], Decompressed: 1326
Downloaded: 1378 file(s) [attempted 1378/8459 = 16%, 28 KB/s], Decompressed: 1370
Downloaded: 1413 file(s) [attempted 1413/8459 = 16%, 98 KB/s], Decompressed: 1408
Downloaded: 1453 file(s) [attempted 1453/8459 = 17%, 263 KB/s], Decompressed: 1446
Downloaded: 1488 file(s) [attempted 1488/8459 = 17%, 652 KB/s], Decompressed: 1483
Downloaded: 1528 file(s) [attempted 1528/8459 = 18%, 25 KB/s], Decompressed: 1483
Downloaded: 1572 file(s) [attempted 1572/8459 = 18%, 91 KB/s], Decompressed: 1483
Downloaded: 1610 file(s) [attempted 1610/8459 = 19%, 56 KB/s], Decompressed: 1487
Downloaded: 1651 file(s) [attempted 1651/8459 = 19%, 21 KB/s], Decompressed: 1487
Downloaded: 1689 file(s) [attempted 1689/8459 = 19%, 298 KB/s], Decompressed: 1678
Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 247 KB/s], Decompressed: 1699
Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 140 KB/s], Decompressed: 1699
Downloaded: 1806 file(s) [attempted 1806/8459 = 21%, 274 KB/s], Decompressed: 1802
Downloaded: 1850 file(s) [attempted 1850/8459 = 21%, 83 KB/s], Decompressed: 1846
Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 596 KB/s], Decompressed: 1884
Downloaded: 1928 file(s) [attempted 1928/8459 = 22%, 73 KB/s], Decompressed: 1904
Downloaded: 1963 file(s) [attempted 1963/8459 = 23%, 257 KB/s], Decompressed: 1904
Downloaded: 2004 file(s) [attempted 2004/8459 = 23%, 77 KB/s], Decompressed: 1911
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 301 KB/s], Decompressed: 2041
Downloaded: 2089 file(s) [attempted 2089/8459 = 24%, 80 KB/s], Decompressed: 2082
Downloaded: 2130 file(s) [attempted 2130/8459 = 25%, 45 KB/s], Decompressed: 2123
Downloaded: 2171 file(s) [attempted 2171/8459 = 25%, 261 KB/s], Decompressed: 2164
Downloaded: 2209 file(s) [attempted 2209/8459 = 26%, 231 KB/s], Decompressed: 2202
Downloaded: 2253 file(s) [attempted 2253/8459 = 26%, 676 KB/s], Decompressed: 2250
Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 108 KB/s], Decompressed: 2291
Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 88 KB/s], Decompressed: 2325
Downloaded: 2373 file(s) [attempted 2373/8459 = 28%, 613 KB/s], Decompressed: 2370
Downloaded: 2413 file(s) [attempted 2413/8459 = 28%, 271 KB/s], Decompressed: 2404
Downloaded: 2452 file(s) [attempted 2452/8459 = 28%, 86 KB/s], Decompressed: 2445
Downloaded: 2493 file(s) [attempted 2493/8459 = 29%, 52 KB/s], Decompressed: 2490
Downloaded: 2537 file(s) [attempted 2537/8459 = 29%, 28 KB/s], Decompressed: 2531
Downloaded: 2575 file(s) [attempted 2575/8459 = 30%, 640 KB/s], Decompressed: 2561
Downloaded: 2613 file(s) [attempted 2613/8459 = 30%, 2250 KB/s], Decompressed: 2599
Downloaded: 2650 file(s) [attempted 2650/8459 = 31%, 337 KB/s], Decompressed: 2644
Downloaded: 2688 file(s) [attempted 2688/8459 = 31%, 132 KB/s], Decompressed: 2681
Downloaded: 2733 file(s) [attempted 2733/8459 = 32%, 67 KB/s], Decompressed: 2729
Downloaded: 2770 file(s) [attempted 2770/8459 = 32%, 86 KB/s], Decompressed: 2760
Downloaded: 2808 file(s) [attempted 2808/8459 = 33%, 224 KB/s], Decompressed: 2777
Downloaded: 2842 file(s) [attempted 2842/8459 = 33%, 175 KB/s], Decompressed: 2777
Downloaded: 2887 file(s) [attempted 2887/8459 = 34%, 39 KB/s], Decompressed: 2883
Downloaded: 2925 file(s) [attempted 2925/8459 = 34%, 226 KB/s], Decompressed: 2921
Downloaded: 2966 file(s) [attempted 2966/8459 = 35%, 148 KB/s], Decompressed: 2958
Downloaded: 3006 file(s) [attempted 3006/8459 = 35%, 42 KB/s], Decompressed: 3000
Downloaded: 3045 file(s) [attempted 3045/8459 = 35%, 1262 KB/s], Decompressed: 3041
Downloaded: 3085 file(s) [attempted 3085/8459 = 36%, 228 KB/s], Decompressed: 3078
Downloaded: 3123 file(s) [attempted 3123/8459 = 36%, 926 KB/s], Decompressed: 3078
Downloaded: 3167 file(s) [attempted 3167/8459 = 37%, 68 KB/s], Decompressed: 3085
Downloaded: 3212 file(s) [attempted 3212/8459 = 37%, 81 KB/s], Decompressed: 3167
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 237 KB/s], Decompressed: 3167
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 101 KB/s], Decompressed: 3273
Downloaded: 3328 file(s) [attempted 3328/8459 = 39%, 167 KB/s], Decompressed: 3297
Downloaded: 3373 file(s) [attempted 3373/8459 = 39%, 114 KB/s], Decompressed: 3297
Downloaded: 3417 file(s) [attempted 3417/8459 = 40%, 345 KB/s], Decompressed: 3307
Downloaded: 3458 file(s) [attempted 3458/8459 = 40%, 152 KB/s], Decompressed: 3307
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 191 KB/s], Decompressed: 3386
Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 152 KB/s], Decompressed: 3527
Downloaded: 3578 file(s) [attempted 3578/8459 = 42%, 737 KB/s], Decompressed: 3533
Downloaded: 3626 file(s) [attempted 3626/8459 = 42%, 405 KB/s], Decompressed: 3533
Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 78 KB/s], Decompressed: 3670
Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 37 KB/s], Decompressed: 3708
Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 475 KB/s], Decompressed: 3742
Downloaded: 3787 file(s) [attempted 3787/8459 = 44%, 51 KB/s], Decompressed: 3783
Downloaded: 3828 file(s) [attempted 3828/8459 = 45%, 114 KB/s], Decompressed: 3804
Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 244 KB/s], Decompressed: 3804
Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 132 KB/s], Decompressed: 3807
Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 203 KB/s], Decompressed: 3807
Downloaded: 3995 file(s) [attempted 3995/8459 = 47%, 201 KB/s], Decompressed: 3889
Downloaded: 4035 file(s) [attempted 4035/8459 = 47%, 271 KB/s], Decompressed: 4026
Downloaded: 4071 file(s) [attempted 4071/8459 = 48%, 287 KB/s], Decompressed: 4067
Downloaded: 4108 file(s) [attempted 4108/8459 = 48%, 147 KB/s], Decompressed: 4088
Downloaded: 4153 file(s) [attempted 4153/8459 = 49%, 128 KB/s], Decompressed: 4088
Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 387 KB/s], Decompressed: 4173
Downloaded: 4232 file(s) [attempted 4232/8459 = 50%, 85 KB/s], Decompressed: 4221
Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 99 KB/s], Decompressed: 4259
Downloaded: 4307 file(s) [attempted 4307/8459 = 50%, 290 KB/s], Decompressed: 4300
Downloaded: 4348 file(s) [attempted 4348/8459 = 51%, 830 KB/s], Decompressed: 4344
Downloaded: 4392 file(s) [attempted 4392/8459 = 51%, 188 KB/s], Decompressed: 4386
Downloaded: 4432 file(s) [attempted 4432/8459 = 52%, 125 KB/s], Decompressed: 4423
Downloaded: 4471 file(s) [attempted 4471/8459 = 52%, 53 KB/s], Decompressed: 4423
Downloaded: 4512 file(s) [attempted 4512/8459 = 53%, 73 KB/s], Decompressed: 4423
Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 40 KB/s], Decompressed: 4550
Downloaded: 4594 file(s) [attempted 4594/8459 = 54%, 37 KB/s], Decompressed: 4557
Downloaded: 4635 file(s) [attempted 4635/8459 = 54%, 351 KB/s], Decompressed: 4557
Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 24 KB/s], Decompressed: 4564
Downloaded: 4718 file(s) [attempted 4718/8459 = 55%, 289 KB/s], Decompressed: 4564
Downloaded: 4759 file(s) [attempted 4759/8459 = 56%, 1328 KB/s], Decompressed: 4564
Downloaded: 4796 file(s) [attempted 4796/8459 = 56%, 49 KB/s], Decompressed: 4564
Downloaded: 4834 file(s) [attempted 4834/8459 = 57%, 100 KB/s], Decompressed: 4564
Downloaded: 4875 file(s) [attempted 4875/8459 = 57%, 183 KB/s], Decompressed: 4564
Downloaded: 4916 file(s) [attempted 4916/8459 = 58%, 1673 KB/s], Decompressed: 4646
Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 178 KB/s], Decompressed: 4646
Downloaded: 4998 file(s) [attempted 4998/8459 = 59%, 263 KB/s], Decompressed: 4646
Downloaded: 5036 file(s) [attempted 5036/8459 = 59%, 113 KB/s], Decompressed: 5019
Downloaded: 5077 file(s) [attempted 5077/8459 = 60%, 315 KB/s], Decompressed: 5039
Downloaded: 5118 file(s) [attempted 5118/8459 = 60%, 91 KB/s], Decompressed: 5039
Downloaded: 5157 file(s) [attempted 5157/8459 = 60%, 143 KB/s], Decompressed: 5149
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 171 KB/s], Decompressed: 5193
Downloaded: 5234 file(s) [attempted 5234/8459 = 61%, 96 KB/s], Decompressed: 5217
Downloaded: 5275 file(s) [attempted 5275/8459 = 62%, 411 KB/s], Decompressed: 5217
Downloaded: 5316 file(s) [attempted 5316/8459 = 62%, 481 KB/s], Decompressed: 5224
Downloaded: 5358 file(s) [attempted 5358/8459 = 63%, 244 KB/s], Decompressed: 5347
Downloaded: 5399 file(s) [attempted 5399/8459 = 63%, 86 KB/s], Decompressed: 5395
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 786 KB/s], Decompressed: 5436
Downloaded: 5481 file(s) [attempted 5481/8459 = 64%, 536 KB/s], Decompressed: 5467
Downloaded: 5518 file(s) [attempted 5518/8459 = 65%, 183 KB/s], Decompressed: 5467
Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 77 KB/s], Decompressed: 5470
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 22 KB/s], Decompressed: 5594
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 28 KB/s], Decompressed: 5638
Downloaded: 5679 file(s) [attempted 5679/8459 = 67%, 181 KB/s], Decompressed: 5662
Downloaded: 5720 file(s) [attempted 5720/8459 = 67%, 289 KB/s], Decompressed: 5713
Downloaded: 5765 file(s) [attempted 5765/8459 = 68%, 197 KB/s], Decompressed: 5713
Downloaded: 5803 file(s) [attempted 5803/8459 = 68%, 324 KB/s], Decompressed: 5713
Downloaded: 5840 file(s) [attempted 5840/8459 = 69%, 226 KB/s], Decompressed: 5833
Downloaded: 5881 file(s) [attempted 5881/8459 = 69%, 600 KB/s], Decompressed: 5878
Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 734 KB/s], Decompressed: 5919
Downloaded: 5960 file(s) [attempted 5960/8459 = 70%, 434 KB/s], Decompressed: 5956
Downloaded: 6004 file(s) [attempted 6004/8459 = 70%, 92 KB/s], Decompressed: 5994
Downloaded: 6045 file(s) [attempted 6045/8459 = 71%, 64 KB/s], Decompressed: 6021
Downloaded: 6090 file(s) [attempted 6090/8459 = 71%, 305 KB/s], Decompressed: 6021
Downloaded: 6131 file(s) [attempted 6131/8459 = 72%, 64 KB/s], Decompressed: 6021
Downloaded: 6169 file(s) [attempted 6169/8459 = 72%, 54 KB/s], Decompressed: 6021
Downloaded: 6206 file(s) [attempted 6206/8459 = 73%, 129 KB/s], Decompressed: 6028
Downloaded: 6247 file(s) [attempted 6247/8459 = 73%, 672 KB/s], Decompressed: 6193
Downloaded: 6288 file(s) [attempted 6288/8459 = 74%, 183 KB/s], Decompressed: 6193
Downloaded: 6329 file(s) [attempted 6329/8459 = 74%, 598 KB/s], Decompressed: 6326
Downloaded: 6371 file(s) [attempted 6371/8459 = 75%, 230 KB/s], Decompressed: 6360
Downloaded: 6408 file(s) [attempted 6408/8459 = 75%, 219 KB/s], Decompressed: 6401
Downloaded: 6446 file(s) [attempted 6446/8459 = 76%, 321 KB/s], Decompressed: 6436
Downloaded: 6484 file(s) [attempted 6484/8459 = 76%, 159 KB/s], Decompressed: 6480
Downloaded: 6525 file(s) [attempted 6525/8459 = 77%, 419 KB/s], Decompressed: 6480
Downloaded: 6562 file(s) [attempted 6562/8459 = 77%, 791 KB/s], Decompressed: 6480
Downloaded: 6607 file(s) [attempted 6607/8459 = 78%, 169 KB/s], Decompressed: 6603
Downloaded: 6648 file(s) [attempted 6648/8459 = 78%, 231 KB/s], Decompressed: 6637
Downloaded: 6689 file(s) [attempted 6689/8459 = 79%, 141 KB/s], Decompressed: 6682
Downloaded: 6725 file(s) [attempted 6725/8459 = 79%, 159 KB/s], Decompressed: 6716
Downloaded: 6764 file(s) [attempted 6764/8459 = 79%, 76 KB/s], Decompressed: 6757
Downloaded: 6805 file(s) [attempted 6805/8459 = 80%, 550 KB/s], Decompressed: 6798
Downloaded: 6845 file(s) [attempted 6845/8459 = 80%, 385 KB/s], Decompressed: 6822
Downloaded: 6884 file(s) [attempted 6884/8459 = 81%, 2072 KB/s], Decompressed: 6822
Downloaded: 6926 file(s) [attempted 6926/8459 = 81%, 341 KB/s], Decompressed: 6829
Downloaded: 6964 file(s) [attempted 6964/8459 = 82%, 120 KB/s], Decompressed: 6956
Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 176 KB/s], Decompressed: 6990
Downloaded: 7034 file(s) [attempted 7034/8459 = 83%, 1713 KB/s], Decompressed: 7028
Downloaded: 7076 file(s) [attempted 7076/8459 = 83%, 1168 KB/s], Decompressed: 7072
Downloaded: 7123 file(s) [attempted 7123/8459 = 84%, 489 KB/s], Decompressed: 7117
Downloaded: 7165 file(s) [attempted 7165/8459 = 84%, 82 KB/s], Decompressed: 7161
Downloaded: 7202 file(s) [attempted 7202/8459 = 85%, 140 KB/s], Decompressed: 7195
Downloaded: 7236 file(s) [attempted 7236/8459 = 85%, 97 KB/s], Decompressed: 7230
Downloaded: 7277 file(s) [attempted 7277/8459 = 86%, 59 KB/s], Decompressed: 7274
Downloaded: 7322 file(s) [attempted 7322/8459 = 86%, 72 KB/s], Decompressed: 7319
Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 229 KB/s], Decompressed: 7332
Downloaded: 7404 file(s) [attempted 7404/8459 = 87%, 104 KB/s], Decompressed: 7332
Downloaded: 7445 file(s) [attempted 7445/8459 = 88%, 82 KB/s], Decompressed: 7438
Downloaded: 7483 file(s) [attempted 7483/8459 = 88%, 149 KB/s], Decompressed: 7469
Downloaded: 7524 file(s) [attempted 7524/8459 = 88%, 123 KB/s], Decompressed: 7469
Downloaded: 7565 file(s) [attempted 7565/8459 = 89%, 231 KB/s], Decompressed: 7473
Downloaded: 7599 file(s) [attempted 7599/8459 = 89%, 407 KB/s], Decompressed: 7558
Downloaded: 7640 file(s) [attempted 7640/8459 = 90%, 300 KB/s], Decompressed: 7558
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 23 KB/s], Decompressed: 7572
Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 72 KB/s], Decompressed: 7572
Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 471 KB/s], Decompressed: 7767
Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 437 KB/s], Decompressed: 7767
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 321 KB/s], Decompressed: 7767
Downloaded: 7887 file(s) [attempted 7887/8459 = 93%, 804 KB/s], Decompressed: 7880
Downloaded: 7924 file(s) [attempted 7924/8459 = 93%, 1000 KB/s], Decompressed: 7921
Downloaded: 7965 file(s) [attempted 7965/8459 = 94%, 104 KB/s], Decompressed: 7958
Downloaded: 8006 file(s) [attempted 8006/8459 = 94%, 307 KB/s], Decompressed: 8003
Downloaded: 8046 file(s) [attempted 8046/8459 = 95%, 178 KB/s], Decompressed: 8037
Downloaded: 8078 file(s) [attempted 8078/8459 = 95%, 1162 KB/s], Decompressed: 8075
Downloaded: 8120 file(s) [attempted 8120/8459 = 95%, 620 KB/s], Decompressed: 8112
Downloaded: 8164 file(s) [attempted 8164/8459 = 96%, 94 KB/s], Decompressed: 8130
Downloaded: 8201 file(s) [attempted 8201/8459 = 96%, 147 KB/s], Decompressed: 8130
Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 107 KB/s], Decompressed: 8140
Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 192 KB/s], Decompressed: 8140
Downloaded: 8321 file(s) [attempted 8321/8459 = 98%, 296 KB/s], Decompressed: 8308
Downloaded: 8362 file(s) [attempted 8362/8459 = 98%, 224 KB/s], Decompressed: 8359
Downloaded: 8407 file(s) [attempted 8407/8459 = 99%, 799 KB/s], Decompressed: 8400
Downloaded: 8444 file(s) [attempted 8444/8459 = 99%, 147 KB/s], Decompressed: 8441
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 268 KB/s], Decompressed: 8451
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 268 KB/s], Decompressed: 8451
$ lake build
exit_code=Some(1) duration_ms=642304
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (58s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.6s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.5s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/764] Built Iut.Foundations.QualitativeData (1.0s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.5s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.6s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (99s)
✔ [3390/3393] Built Iut.Stage1.SourceObligations (3.1s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (100s)
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 (62s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.3s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.4s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.7s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (31s)
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 (171s)
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=1212
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-1367-source
Cloning into '/var/lib/apodeixis/repos/job-1367-source'...
git_checkout exit 0
git checkout bf681f8016ffedb0923c61ab7ebb81e2cef08828
Note: switching to 'bf681f8016ffedb0923c61ab7ebb81e2cef08828'. 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 bf681f8 Route pointwise handoff through formula gap
lake_cache exit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache Decompressed 8459 file(s) Already decompressed 8459 file(s)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0 Downloaded: 14 file(s) [attempted 14/8459 = 0%, 5 KB/s], Decompressed: 3 Downloaded: 34 file(s) [attempted 34/8459 = 0%, 17 KB/s], Decompressed: 3 Downloaded: 66 file(s) [attempted 66/8459 = 0%, 48 KB/s], Decompressed: 65 Downloaded: 89 file(s) [attempted 89/8459 = 1%, 190 KB/s], Decompressed: 82 Downloaded: 121 file(s) [attempted 121/8459 = 1%, 404 KB/s], Decompressed: 117 Downloaded: 155 file(s) [attempted 155/8459 = 1%, 213 KB/s], Decompressed: 134 Downloaded: 189 file(s) [attempted 189/8459 = 2%, 537 KB/s], Decompressed: 134 Downloaded: 223 file(s) [attempted 223/8459 = 2%, 330 KB/s], Decompressed: 141 Downloaded: 264 file(s) [attempted 264/8459 = 3%, 775 KB/s], Decompressed: 258 Downloaded: 302 file(s) [attempted 302/8459 = 3%, 26 KB/s], Decompressed: 258 Downloaded: 340 file(s) [attempted 340/8459 = 4%, 37 KB/s], Decompressed: 264 Downloaded: 377 file(s) [attempted 377/8459 = 4%, 395 KB/s], Decompressed: 367 Downloaded: 415 file(s) [attempted 415/8459 = 4%, 168 KB/s], Decompressed: 391 Downloaded: 457 file(s) [attempted 457/8459 = 5%, 208 KB/s], Decompressed: 453 Downloaded: 494 file(s) [attempted 494/8459 = 5%, 244 KB/s], Decompressed: 490 Downloaded: 529 file(s) [attempted 529/8459 = 6%, 209 KB/s], Decompressed: 521 Downloaded: 562 file(s) [attempted 562/8459 = 6%, 554 KB/s], Decompressed: 559 Downloaded: 607 file(s) [attempted 607/8459 = 7%, 147 KB/s], Decompressed: 604 Downloaded: 648 file(s) [attempted 648/8459 = 7%, 131 KB/s], Decompressed: 631 Downloaded: 689 file(s) [attempted 689/8459 = 8%, 132 KB/s], Decompressed: 648 Downloaded: 727 file(s) [attempted 727/8459 = 8%, 73 KB/s], Decompressed: 648 Downloaded: 765 file(s) [attempted 765/8459 = 9%, 212 KB/s], Decompressed: 655 Downloaded: 806 file(s) [attempted 806/8459 = 9%, 30 KB/s], Decompressed: 655 Downloaded: 848 file(s) [attempted 848/8459 = 10%, 118 KB/s], Decompressed: 831 Downloaded: 888 file(s) [attempted 888/8459 = 10%, 48 KB/s], Decompressed: 881 Downloaded: 925 file(s) [attempted 925/8459 = 10%, 332 KB/s], Decompressed: 919 Downloaded: 967 file(s) [attempted 967/8459 = 11%, 210 KB/s], Decompressed: 963 Downloaded: 1011 file(s) [attempted 1011/8459 = 11%, 464 KB/s], Decompressed: 1004 Downloaded: 1053 file(s) [attempted 1053/8459 = 12%, 85 KB/s], Decompressed: 1049 Downloaded: 1090 file(s) [attempted 1090/8459 = 12%, 72 KB/s], Decompressed: 1083 Downloaded: 1125 file(s) [attempted 1125/8459 = 13%, 138 KB/s], Decompressed: 1121 Downloaded: 1165 file(s) [attempted 1165/8459 = 13%, 1210 KB/s], Decompressed: 1162 Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 255 KB/s], Decompressed: 1199 Downloaded: 1247 file(s) [attempted 1247/8459 = 14%, 97 KB/s], Decompressed: 1240 Downloaded: 1288 file(s) [attempted 1288/8459 = 15%, 229 KB/s], Decompressed: 1281 Downloaded: 1333 file(s) [attempted 1333/8459 = 15%, 65 KB/s], Decompressed: 1326 Downloaded: 1378 file(s) [attempted 1378/8459 = 16%, 28 KB/s], Decompressed: 1370 Downloaded: 1413 file(s) [attempted 1413/8459 = 16%, 98 KB/s], Decompressed: 1408 Downloaded: 1453 file(s) [attempted 1453/8459 = 17%, 263 KB/s], Decompressed: 1446 Downloaded: 1488 file(s) [attempted 1488/8459 = 17%, 652 KB/s], Decompressed: 1483 Downloaded: 1528 file(s) [attempted 1528/8459 = 18%, 25 KB/s], Decompressed: 1483 Downloaded: 1572 file(s) [attempted 1572/8459 = 18%, 91 KB/s], Decompressed: 1483 Downloaded: 1610 file(s) [attempted 1610/8459 = 19%, 56 KB/s], Decompressed: 1487 Downloaded: 1651 file(s) [attempted 1651/8459 = 19%, 21 KB/s], Decompressed: 1487 Downloaded: 1689 file(s) [attempted 1689/8459 = 19%, 298 KB/s], Decompressed: 1678 Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 247 KB/s], Decompressed: 1699 Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 140 KB/s], Decompressed: 1699 Downloaded: 1806 file(s) [attempted 1806/8459 = 21%, 274 KB/s], Decompressed: 1802 Downloaded: 1850 file(s) [attempted 1850/8459 = 21%, 83 KB/s], Decompressed: 1846 Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 596 KB/s], Decompressed: 1884 Downloaded: 1928 file(s) [attempted 1928/8459 = 22%, 73 KB/s], Decompressed: 1904 Downloaded: 1963 file(s) [attempted 1963/8459 = 23%, 257 KB/s], Decompressed: 1904 Downloaded: 2004 file(s) [attempted 2004/8459 = 23%, 77 KB/s], Decompressed: 1911 Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 301 KB/s], Decompressed: 2041 Downloaded: 2089 file(s) [attempted 2089/8459 = 24%, 80 KB/s], Decompressed: 2082 Downloaded: 2130 file(s) [attempted 2130/8459 = 25%, 45 KB/s], Decompressed: 2123 Downloaded: 2171 file(s) [attempted 2171/8459 = 25%, 261 KB/s], Decompressed: 2164 Downloaded: 2209 file(s) [attempted 2209/8459 = 26%, 231 KB/s], Decompressed: 2202 Downloaded: 2253 file(s) [attempted 2253/8459 = 26%, 676 KB/s], Decompressed: 2250 Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 108 KB/s], Decompressed: 2291 Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 88 KB/s], Decompressed: 2325 Downloaded: 2373 file(s) [attempted 2373/8459 = 28%, 613 KB/s], Decompressed: 2370 Downloaded: 2413 file(s) [attempted 2413/8459 = 28%, 271 KB/s], Decompressed: 2404 Downloaded: 2452 file(s) [attempted 2452/8459 = 28%, 86 KB/s], Decompressed: 2445 Downloaded: 2493 file(s) [attempted 2493/8459 = 29%, 52 KB/s], Decompressed: 2490 Downloaded: 2537 file(s) [attempted 2537/8459 = 29%, 28 KB/s], Decompressed: 2531 Downloaded: 2575 file(s) [attempted 2575/8459 = 30%, 640 KB/s], Decompressed: 2561 Downloaded: 2613 file(s) [attempted 2613/8459 = 30%, 2250 KB/s], Decompressed: 2599 Downloaded: 2650 file(s) [attempted 2650/8459 = 31%, 337 KB/s], Decompressed: 2644 Downloaded: 2688 file(s) [attempted 2688/8459 = 31%, 132 KB/s], Decompressed: 2681 Downloaded: 2733 file(s) [attempted 2733/8459 = 32%, 67 KB/s], Decompressed: 2729 Downloaded: 2770 file(s) [attempted 2770/8459 = 32%, 86 KB/s], Decompressed: 2760 Downloaded: 2808 file(s) [attempted 2808/8459 = 33%, 224 KB/s], Decompressed: 2777 Downloaded: 2842 file(s) [attempted 2842/8459 = 33%, 175 KB/s], Decompressed: 2777 Downloaded: 2887 file(s) [attempted 2887/8459 = 34%, 39 KB/s], Decompressed: 2883 Downloaded: 2925 file(s) [attempted 2925/8459 = 34%, 226 KB/s], Decompressed: 2921 Downloaded: 2966 file(s) [attempted 2966/8459 = 35%, 148 KB/s], Decompressed: 2958 Downloaded: 3006 file(s) [attempted 3006/8459 = 35%, 42 KB/s], Decompressed: 3000 Downloaded: 3045 file(s) [attempted 3045/8459 = 35%, 1262 KB/s], Decompressed: 3041 Downloaded: 3085 file(s) [attempted 3085/8459 = 36%, 228 KB/s], Decompressed: 3078 Downloaded: 3123 file(s) [attempted 3123/8459 = 36%, 926 KB/s], Decompressed: 3078 Downloaded: 3167 file(s) [attempted 3167/8459 = 37%, 68 KB/s], Decompressed: 3085 Downloaded: 3212 file(s) [attempted 3212/8459 = 37%, 81 KB/s], Decompressed: 3167 Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 237 KB/s], Decompressed: 3167 Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 101 KB/s], Decompressed: 3273 Downloaded: 3328 file(s) [attempted 3328/8459 = 39%, 167 KB/s], Decompressed: 3297 Downloaded: 3373 file(s) [attempted 3373/8459 = 39%, 114 KB/s], Decompressed: 3297 Downloaded: 3417 file(s) [attempted 3417/8459 = 40%, 345 KB/s], Decompressed: 3307 Downloaded: 3458 file(s) [attempted 3458/8459 = 40%, 152 KB/s], Decompressed: 3307 Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 191 KB/s], Decompressed: 3386 Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 152 KB/s], Decompressed: 3527 Downloaded: 3578 file(s) [attempted 3578/8459 = 42%, 737 KB/s], Decompressed: 3533 Downloaded: 3626 file(s) [attempted 3626/8459 = 42%, 405 KB/s], Decompressed: 3533 Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 78 KB/s], Decompressed: 3670 Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 37 KB/s], Decompressed: 3708 Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 475 KB/s], Decompressed: 3742 Downloaded: 3787 file(s) [attempted 3787/8459 = 44%, 51 KB/s], Decompressed: 3783 Downloaded: 3828 file(s) [attempted 3828/8459 = 45%, 114 KB/s], Decompressed: 3804 Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 244 KB/s], Decompressed: 3804 Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 132 KB/s], Decompressed: 3807 Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 203 KB/s], Decompressed: 3807 Downloaded: 3995 file(s) [attempted 3995/8459 = 47%, 201 KB/s], Decompressed: 3889 Downloaded: 4035 file(s) [attempted 4035/8459 = 47%, 271 KB/s], Decompressed: 4026 Downloaded: 4071 file(s) [attempted 4071/8459 = 48%, 287 KB/s], Decompressed: 4067 Downloaded: 4108 file(s) [attempted 4108/8459 = 48%, 147 KB/s], Decompressed: 4088 Downloaded: 4153 file(s) [attempted 4153/8459 = 49%, 128 KB/s], Decompressed: 4088 Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 387 KB/s], Decompressed: 4173 Downloaded: 4232 file(s) [attempted 4232/8459 = 50%, 85 KB/s], Decompressed: 4221 Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 99 KB/s], Decompressed: 4259 Downloaded: 4307 file(s) [attempted 4307/8459 = 50%, 290 KB/s], Decompressed: 4300 Downloaded: 4348 file(s) [attempted 4348/8459 = 51%, 830 KB/s], Decompressed: 4344 Downloaded: 4392 file(s) [attempted 4392/8459 = 51%, 188 KB/s], Decompressed: 4386 Downloaded: 4432 file(s) [attempted 4432/8459 = 52%, 125 KB/s], Decompressed: 4423 Downloaded: 4471 file(s) [attempted 4471/8459 = 52%, 53 KB/s], Decompressed: 4423 Downloaded: 4512 file(s) [attempted 4512/8459 = 53%, 73 KB/s], Decompressed: 4423 Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 40 KB/s], Decompressed: 4550 Downloaded: 4594 file(s) [attempted 4594/8459 = 54%, 37 KB/s], Decompressed: 4557 Downloaded: 4635 file(s) [attempted 4635/8459 = 54%, 351 KB/s], Decompressed: 4557 Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 24 KB/s], Decompressed: 4564 Downloaded: 4718 file(s) [attempted 4718/8459 = 55%, 289 KB/s], Decompressed: 4564 Downloaded: 4759 file(s) [attempted 4759/8459 = 56%, 1328 KB/s], Decompressed: 4564 Downloaded: 4796 file(s) [attempted 4796/8459 = 56%, 49 KB/s], Decompressed: 4564 Downloaded: 4834 file(s) [attempted 4834/8459 = 57%, 100 KB/s], Decompressed: 4564 Downloaded: 4875 file(s) [attempted 4875/8459 = 57%, 183 KB/s], Decompressed: 4564 Downloaded: 4916 file(s) [attempted 4916/8459 = 58%, 1673 KB/s], Decompressed: 4646 Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 178 KB/s], Decompressed: 4646 Downloaded: 4998 file(s) [attempted 4998/8459 = 59%, 263 KB/s], Decompressed: 4646 Downloaded: 5036 file(s) [attempted 5036/8459 = 59%, 113 KB/s], Decompressed: 5019 Downloaded: 5077 file(s) [attempted 5077/8459 = 60%, 315 KB/s], Decompressed: 5039 Downloaded: 5118 file(s) [attempted 5118/8459 = 60%, 91 KB/s], Decompressed: 5039 Downloaded: 5157 file(s) [attempted 5157/8459 = 60%, 143 KB/s], Decompressed: 5149 Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 171 KB/s], Decompressed: 5193 Downloaded: 5234 file(s) [attempted 5234/8459 = 61%, 96 KB/s], Decompressed: 5217 Downloaded: 5275 file(s) [attempted 5275/8459 = 62%, 411 KB/s], Decompressed: 5217 Downloaded: 5316 file(s) [attempted 5316/8459 = 62%, 481 KB/s], Decompressed: 5224 Downloaded: 5358 file(s) [attempted 5358/8459 = 63%, 244 KB/s], Decompressed: 5347 Downloaded: 5399 file(s) [attempted 5399/8459 = 63%, 86 KB/s], Decompressed: 5395 Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 786 KB/s], Decompressed: 5436 Downloaded: 5481 file(s) [attempted 5481/8459 = 64%, 536 KB/s], Decompressed: 5467 Downloaded: 5518 file(s) [attempted 5518/8459 = 65%, 183 KB/s], Decompressed: 5467 Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 77 KB/s], Decompressed: 5470 Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 22 KB/s], Decompressed: 5594 Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 28 KB/s], Decompressed: 5638 Downloaded: 5679 file(s) [attempted 5679/8459 = 67%, 181 KB/s], Decompressed: 5662 Downloaded: 5720 file(s) [attempted 5720/8459 = 67%, 289 KB/s], Decompressed: 5713 Downloaded: 5765 file(s) [attempted 5765/8459 = 68%, 197 KB/s], Decompressed: 5713 Downloaded: 5803 file(s) [attempted 5803/8459 = 68%, 324 KB/s], Decompressed: 5713 Downloaded: 5840 file(s) [attempted 5840/8459 = 69%, 226 KB/s], Decompressed: 5833 Downloaded: 5881 file(s) [attempted 5881/8459 = 69%, 600 KB/s], Decompressed: 5878 Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 734 KB/s], Decompressed: 5919 Downloaded: 5960 file(s) [attempted 5960/8459 = 70%, 434 KB/s], Decompressed: 5956 Downloaded: 6004 file(s) [attempted 6004/8459 = 70%, 92 KB/s], Decompressed: 5994 Downloaded: 6045 file(s) [attempted 6045/8459 = 71%, 64 KB/s], Decompressed: 6021 Downloaded: 6090 file(s) [attempted 6090/8459 = 71%, 305 KB/s], Decompressed: 6021 Downloaded: 6131 file(s) [attempted 6131/8459 = 72%, 64 KB/s], Decompressed: 6021 Downloaded: 6169 file(s) [attempted 6169/8459 = 72%, 54 KB/s], Decompressed: 6021 Downloaded: 6206 file(s) [attempted 6206/8459 = 73%, 129 KB/s], Decompressed: 6028 Downloaded: 6247 file(s) [attempted 6247/8459 = 73%, 672 KB/s], Decompressed: 6193 Downloaded: 6288 file(s) [attempted 6288/8459 = 74%, 183 KB/s], Decompressed: 6193 Downloaded: 6329 file(s) [attempted 6329/8459 = 74%, 598 KB/s], Decompressed: 6326 Downloaded: 6371 file(s) [attempted 6371/8459 = 75%, 230 KB/s], Decompressed: 6360 Downloaded: 6408 file(s) [attempted 6408/8459 = 75%, 219 KB/s], Decompressed: 6401 Downloaded: 6446 file(s) [attempted 6446/8459 = 76%, 321 KB/s], Decompressed: 6436 Downloaded: 6484 file(s) [attempted 6484/8459 = 76%, 159 KB/s], Decompressed: 6480 Downloaded: 6525 file(s) [attempted 6525/8459 = 77%, 419 KB/s], Decompressed: 6480 Downloaded: 6562 file(s) [attempted 6562/8459 = 77%, 791 KB/s], Decompressed: 6480 Downloaded: 6607 file(s) [attempted 6607/8459 = 78%, 169 KB/s], Decompressed: 6603 Downloaded: 6648 file(s) [attempted 6648/8459 = 78%, 231 KB/s], Decompressed: 6637 Downloaded: 6689 file(s) [attempted 6689/8459 = 79%, 141 KB/s], Decompressed: 6682 Downloaded: 6725 file(s) [attempted 6725/8459 = 79%, 159 KB/s], Decompressed: 6716 Downloaded: 6764 file(s) [attempted 6764/8459 = 79%, 76 KB/s], Decompressed: 6757 Downloaded: 6805 file(s) [attempted 6805/8459 = 80%, 550 KB/s], Decompressed: 6798 Downloaded: 6845 file(s) [attempted 6845/8459 = 80%, 385 KB/s], Decompressed: 6822 Downloaded: 6884 file(s) [attempted 6884/8459 = 81%, 2072 KB/s], Decompressed: 6822 Downloaded: 6926 file(s) [attempted 6926/8459 = 81%, 341 KB/s], Decompressed: 6829 Downloaded: 6964 file(s) [attempted 6964/8459 = 82%, 120 KB/s], Decompressed: 6956 Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 176 KB/s], Decompressed: 6990 Downloaded: 7034 file(s) [attempted 7034/8459 = 83%, 1713 KB/s], Decompressed: 7028 Downloaded: 7076 file(s) [attempted 7076/8459 = 83%, 1168 KB/s], Decompressed: 7072 Downloaded: 7123 file(s) [attempted 7123/8459 = 84%, 489 KB/s], Decompressed: 7117 Downloaded: 7165 file(s) [attempted 7165/8459 = 84%, 82 KB/s], Decompressed: 7161 Downloaded: 7202 file(s) [attempted 7202/8459 = 85%, 140 KB/s], Decompressed: 7195 Downloaded: 7236 file(s) [attempted 7236/8459 = 85%, 97 KB/s], Decompressed: 7230 Downloaded: 7277 file(s) [attempted 7277/8459 = 86%, 59 KB/s], Decompressed: 7274 Downloaded: 7322 file(s) [attempted 7322/8459 = 86%, 72 KB/s], Decompressed: 7319 Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 229 KB/s], Decompressed: 7332 Downloaded: 7404 file(s) [attempted 7404/8459 = 87%, 104 KB/s], Decompressed: 7332 Downloaded: 7445 file(s) [attempted 7445/8459 = 88%, 82 KB/s], Decompressed: 7438 Downloaded: 7483 file(s) [attempted 7483/8459 = 88%, 149 KB/s], Decompressed: 7469 Downloaded: 7524 file(s) [attempted 7524/8459 = 88%, 123 KB/s], Decompressed: 7469 Downloaded: 7565 file(s) [attempted 7565/8459 = 89%, 231 KB/s], Decompressed: 7473 Downloaded: 7599 file(s) [attempted 7599/8459 = 89%, 407 KB/s], Decompressed: 7558 Downloaded: 7640 file(s) [attempted 7640/8459 = 90%, 300 KB/s], Decompressed: 7558 Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 23 KB/s], Decompressed: 7572 Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 72 KB/s], Decompressed: 7572 Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 471 KB/s], Decompressed: 7767 Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 437 KB/s], Decompressed: 7767 Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 321 KB/s], Decompressed: 7767 Downloaded: 7887 file(s) [attempted 7887/8459 = 93%, 804 KB/s], Decompressed: 7880 Downloaded: 7924 file(s) [attempted 7924/8459 = 93%, 1000 KB/s], Decompressed: 7921 Downloaded: 7965 file(s) [attempted 7965/8459 = 94%, 104 KB/s], Decompressed: 7958 Downloaded: 8006 file(s) [attempted 8006/8459 = 94%, 307 KB/s], Decompressed: 8003 Downloaded: 8046 file(s) [attempted 8046/8459 = 95%, 178 KB/s], Decompressed: 8037 Downloaded: 8078 file(s) [attempted 8078/8459 = 95%, 1162 KB/s], Decompressed: 8075 Downloaded: 8120 file(s) [attempted 8120/8459 = 95%, 620 KB/s], Decompressed: 8112 Downloaded: 8164 file(s) [attempted 8164/8459 = 96%, 94 KB/s], Decompressed: 8130 Downloaded: 8201 file(s) [attempted 8201/8459 = 96%, 147 KB/s], Decompressed: 8130 Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 107 KB/s], Decompressed: 8140 Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 192 KB/s], Decompressed: 8140 Downloaded: 8321 file(s) [attempted 8321/8459 = 98%, 296 KB/s], Decompressed: 8308 Downloaded: 8362 file(s) [attempted 8362/8459 = 98%, 224 KB/s], Decompressed: 8359 Downloaded: 8407 file(s) [attempted 8407/8459 = 99%, 799 KB/s], Decompressed: 8400 Downloaded: 8444 file(s) [attempted 8444/8459 = 99%, 147 KB/s], Decompressed: 8441 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 268 KB/s], Decompressed: 8451 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 268 KB/s], Decompressed: 8451
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (58s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.6s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.5s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/764] Built Iut.Foundations.QualitativeData (1.0s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.5s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.6s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (99s)
✔ [3390/3393] Built Iut.Stage1.SourceObligations (3.1s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (100s)
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 (62s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.3s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.4s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.7s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (31s)
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 (171s)
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`