Verification run
Run 1050
failed commit
7e8723799fa4 toolchain lean-v4-30-0 prover lean took 24m 22s · 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-1350-source
exit_code=Some(0) duration_ms=3762
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1350-source'...
$ git checkout 7e8723799fa4cc9fc8310892494d115ef2a885bb
exit_code=Some(0) duration_ms=148
stderr:
Note: switching to '7e8723799fa4cc9fc8310892494d115ef2a885bb'.
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 7e87237 Bundle valuation ball route inputs
Resolved source revision: 7e8723799fa4cc9fc8310892494d115ef2a885bb
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=7e8723799fa4cc9fc8310892494d115ef2a885bb provenance={"branch":"master","checked_out_revision":"7e8723799fa4cc9fc8310892494d115ef2a885bb","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"7e8723799fa4cc9fc8310892494d115ef2a885bb","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=37173
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%, 12 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 10 KB/s], Decompressed: 10
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 29 KB/s], Decompressed: 33
Downloaded: 58 file(s) [attempted 58/8459 = 0%, 33 KB/s], Decompressed: 53
Downloaded: 82 file(s) [attempted 82/8459 = 0%, 187 KB/s], Decompressed: 79
Downloaded: 114 file(s) [attempted 114/8459 = 1%, 77 KB/s], Decompressed: 110
Downloaded: 148 file(s) [attempted 148/8459 = 1%, 359 KB/s], Decompressed: 141
Downloaded: 182 file(s) [attempted 182/8459 = 2%, 239 KB/s], Decompressed: 141
Downloaded: 216 file(s) [attempted 216/8459 = 2%, 102 KB/s], Decompressed: 145
Downloaded: 247 file(s) [attempted 247/8459 = 2%, 659 KB/s], Decompressed: 244
Downloaded: 278 file(s) [attempted 278/8459 = 3%, 376 KB/s], Decompressed: 271
Downloaded: 319 file(s) [attempted 319/8459 = 3%, 172 KB/s], Decompressed: 275
Downloaded: 360 file(s) [attempted 360/8459 = 4%, 216 KB/s], Decompressed: 275
Downloaded: 405 file(s) [attempted 405/8459 = 4%, 60 KB/s], Decompressed: 398
Downloaded: 434 file(s) [attempted 434/8459 = 5%, 90 KB/s], Decompressed: 417
Downloaded: 473 file(s) [attempted 473/8459 = 5%, 364 KB/s], Decompressed: 417
Downloaded: 514 file(s) [attempted 514/8459 = 6%, 67 KB/s], Decompressed: 419
Downloaded: 556 file(s) [attempted 556/8459 = 6%, 935 KB/s], Decompressed: 419
Downloaded: 600 file(s) [attempted 600/8459 = 7%, 177 KB/s], Decompressed: 504
Downloaded: 638 file(s) [attempted 638/8459 = 7%, 882 KB/s], Decompressed: 504
Downloaded: 675 file(s) [attempted 675/8459 = 7%, 64 KB/s], Decompressed: 504
Downloaded: 723 file(s) [attempted 723/8459 = 8%, 333 KB/s], Decompressed: 600
Downloaded: 768 file(s) [attempted 768/8459 = 9%, 1170 KB/s], Decompressed: 600
Downloaded: 809 file(s) [attempted 809/8459 = 9%, 305 KB/s], Decompressed: 600
Downloaded: 854 file(s) [attempted 854/8459 = 10%, 173 KB/s], Decompressed: 696
Downloaded: 898 file(s) [attempted 898/8459 = 10%, 214 KB/s], Decompressed: 696
Downloaded: 943 file(s) [attempted 943/8459 = 11%, 40 KB/s], Decompressed: 696
Downloaded: 982 file(s) [attempted 982/8459 = 11%, 437 KB/s], Decompressed: 977
Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 177 KB/s], Decompressed: 1018
Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 416 KB/s], Decompressed: 1052
Downloaded: 1104 file(s) [attempted 1104/8459 = 13%, 66 KB/s], Decompressed: 1069
Downloaded: 1145 file(s) [attempted 1145/8459 = 13%, 126 KB/s], Decompressed: 1069
Downloaded: 1186 file(s) [attempted 1186/8459 = 14%, 37 KB/s], Decompressed: 1076
Downloaded: 1223 file(s) [attempted 1223/8459 = 14%, 395 KB/s], Decompressed: 1076
Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 144 KB/s], Decompressed: 1076
Downloaded: 1305 file(s) [attempted 1305/8459 = 15%, 675 KB/s], Decompressed: 1165
Downloaded: 1346 file(s) [attempted 1346/8459 = 15%, 144 KB/s], Decompressed: 1165
Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 187 KB/s], Decompressed: 1367
Downloaded: 1425 file(s) [attempted 1425/8459 = 16%, 71 KB/s], Decompressed: 1401
Downloaded: 1466 file(s) [attempted 1466/8459 = 17%, 192 KB/s], Decompressed: 1401
Downloaded: 1507 file(s) [attempted 1507/8459 = 17%, 143 KB/s], Decompressed: 1494
Downloaded: 1548 file(s) [attempted 1548/8459 = 18%, 388 KB/s], Decompressed: 1507
Downloaded: 1589 file(s) [attempted 1589/8459 = 18%, 133 KB/s], Decompressed: 1507
Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 230 KB/s], Decompressed: 1617
Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 455 KB/s], Decompressed: 1661
Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 176 KB/s], Decompressed: 1672
Downloaded: 1750 file(s) [attempted 1750/8459 = 20%, 296 KB/s], Decompressed: 1672
Downloaded: 1791 file(s) [attempted 1791/8459 = 21%, 929 KB/s], Decompressed: 1678
Downloaded: 1836 file(s) [attempted 1836/8459 = 21%, 405 KB/s], Decompressed: 1678
Downloaded: 1877 file(s) [attempted 1877/8459 = 22%, 127 KB/s], Decompressed: 1767
Downloaded: 1915 file(s) [attempted 1915/8459 = 22%, 760 KB/s], Decompressed: 1767
Downloaded: 1956 file(s) [attempted 1956/8459 = 23%, 217 KB/s], Decompressed: 1952
Downloaded: 1997 file(s) [attempted 1997/8459 = 23%, 963 KB/s], Decompressed: 1990
Downloaded: 2038 file(s) [attempted 2038/8459 = 24%, 414 KB/s], Decompressed: 2034
Downloaded: 2082 file(s) [attempted 2082/8459 = 24%, 34 KB/s], Decompressed: 2079
Downloaded: 2127 file(s) [attempted 2127/8459 = 25%, 1406 KB/s], Decompressed: 2120
Downloaded: 2168 file(s) [attempted 2168/8459 = 25%, 287 KB/s], Decompressed: 2161
Downloaded: 2205 file(s) [attempted 2205/8459 = 26%, 430 KB/s], Decompressed: 2192
Downloaded: 2247 file(s) [attempted 2247/8459 = 26%, 918 KB/s], Decompressed: 2233
Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 1031 KB/s], Decompressed: 2233
Downloaded: 2339 file(s) [attempted 2339/8459 = 27%, 393 KB/s], Decompressed: 2240
Downloaded: 2380 file(s) [attempted 2380/8459 = 28%, 114 KB/s], Decompressed: 2373
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 36 KB/s], Decompressed: 2407
Downloaded: 2460 file(s) [attempted 2460/8459 = 29%, 24 KB/s], Decompressed: 2452
Downloaded: 2500 file(s) [attempted 2500/8459 = 29%, 1450 KB/s], Decompressed: 2490
Downloaded: 2537 file(s) [attempted 2537/8459 = 29%, 607 KB/s], Decompressed: 2534
Downloaded: 2582 file(s) [attempted 2582/8459 = 30%, 381 KB/s], Decompressed: 2579
Downloaded: 2617 file(s) [attempted 2617/8459 = 30%, 537 KB/s], Decompressed: 2609
Downloaded: 2661 file(s) [attempted 2661/8459 = 31%, 1750 KB/s], Decompressed: 2609
Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 133 KB/s], Decompressed: 2609
Downloaded: 2743 file(s) [attempted 2743/8459 = 32%, 129 KB/s], Decompressed: 2609
Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 798 KB/s], Decompressed: 2616
Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 587 KB/s], Decompressed: 2825
Downloaded: 2869 file(s) [attempted 2869/8459 = 33%, 868 KB/s], Decompressed: 2863
Downloaded: 2911 file(s) [attempted 2911/8459 = 34%, 776 KB/s], Decompressed: 2900
Downloaded: 2948 file(s) [attempted 2948/8459 = 34%, 261 KB/s], Decompressed: 2934
Downloaded: 2989 file(s) [attempted 2989/8459 = 35%, 223 KB/s], Decompressed: 2934
Downloaded: 3030 file(s) [attempted 3030/8459 = 35%, 847 KB/s], Decompressed: 2938
Downloaded: 3075 file(s) [attempted 3075/8459 = 36%, 234 KB/s], Decompressed: 3041
Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 687 KB/s], Decompressed: 3041
Downloaded: 3153 file(s) [attempted 3153/8459 = 37%, 83 KB/s], Decompressed: 3150
Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 200 KB/s], Decompressed: 3184
Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 626 KB/s], Decompressed: 3212
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 148 KB/s], Decompressed: 3212
Downloaded: 3335 file(s) [attempted 3335/8459 = 39%, 160 KB/s], Decompressed: 3218
Downloaded: 3372 file(s) [attempted 3372/8459 = 39%, 278 KB/s], Decompressed: 3218
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 203 KB/s], Decompressed: 3304
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 407 KB/s], Decompressed: 3304
Downloaded: 3489 file(s) [attempted 3489/8459 = 41%, 75 KB/s], Decompressed: 3304
Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 276 KB/s], Decompressed: 3396
Downloaded: 3585 file(s) [attempted 3585/8459 = 42%, 786 KB/s], Decompressed: 3396
Downloaded: 3626 file(s) [attempted 3626/8459 = 42%, 257 KB/s], Decompressed: 3496
Downloaded: 3660 file(s) [attempted 3660/8459 = 43%, 336 KB/s], Decompressed: 3496
Downloaded: 3694 file(s) [attempted 3694/8459 = 43%, 296 KB/s], Decompressed: 3592
Downloaded: 3735 file(s) [attempted 3735/8459 = 44%, 94 KB/s], Decompressed: 3592
Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 133 KB/s], Decompressed: 3759
Downloaded: 3821 file(s) [attempted 3821/8459 = 45%, 483 KB/s], Decompressed: 3759
Downloaded: 3858 file(s) [attempted 3858/8459 = 45%, 822 KB/s], Decompressed: 3759
Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 65 KB/s], Decompressed: 3759
Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 382 KB/s], Decompressed: 3783
Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 287 KB/s], Decompressed: 3783
Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 120 KB/s], Decompressed: 3934
Downloaded: 4078 file(s) [attempted 4078/8459 = 48%, 781 KB/s], Decompressed: 3934
Downloaded: 4112 file(s) [attempted 4112/8459 = 48%, 148 KB/s], Decompressed: 4023
Downloaded: 4154 file(s) [attempted 4154/8459 = 49%, 632 KB/s], Decompressed: 4149
Downloaded: 4196 file(s) [attempted 4196/8459 = 49%, 743 KB/s], Decompressed: 4160
Downloaded: 4235 file(s) [attempted 4235/8459 = 50%, 699 KB/s], Decompressed: 4160
Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 297 KB/s], Decompressed: 4266
Downloaded: 4324 file(s) [attempted 4324/8459 = 51%, 338 KB/s], Decompressed: 4317
Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 477 KB/s], Decompressed: 4348
Downloaded: 4397 file(s) [attempted 4397/8459 = 51%, 36 KB/s], Decompressed: 4392
Downloaded: 4438 file(s) [attempted 4438/8459 = 52%, 710 KB/s], Decompressed: 4433
Downloaded: 4481 file(s) [attempted 4481/8459 = 52%, 347 KB/s], Decompressed: 4474
Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 533 KB/s], Decompressed: 4516
Downloaded: 4563 file(s) [attempted 4563/8459 = 53%, 112 KB/s], Decompressed: 4560
Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 540 KB/s], Decompressed: 4598
Downloaded: 4646 file(s) [attempted 4646/8459 = 54%, 410 KB/s], Decompressed: 4618
Downloaded: 4680 file(s) [attempted 4680/8459 = 55%, 69 KB/s], Decompressed: 4676
Downloaded: 4721 file(s) [attempted 4721/8459 = 55%, 687 KB/s], Decompressed: 4700
Downloaded: 4759 file(s) [attempted 4759/8459 = 56%, 88 KB/s], Decompressed: 4700
Downloaded: 4800 file(s) [attempted 4800/8459 = 56%, 709 KB/s], Decompressed: 4707
Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 286 KB/s], Decompressed: 4810
Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 850 KB/s], Decompressed: 4810
Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 80 KB/s], Decompressed: 4817
Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 247 KB/s], Decompressed: 4817
Downloaded: 5008 file(s) [attempted 5008/8459 = 59%, 134 KB/s], Decompressed: 4817
Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 280 KB/s], Decompressed: 4817
Downloaded: 5087 file(s) [attempted 5087/8459 = 60%, 131 KB/s], Decompressed: 5070
Downloaded: 5132 file(s) [attempted 5132/8459 = 60%, 42 KB/s], Decompressed: 5125
Downloaded: 5173 file(s) [attempted 5173/8459 = 61%, 175 KB/s], Decompressed: 5159
Downloaded: 5217 file(s) [attempted 5217/8459 = 61%, 872 KB/s], Decompressed: 5159
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 39 KB/s], Decompressed: 5162
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 61 KB/s], Decompressed: 5162
Downloaded: 5340 file(s) [attempted 5340/8459 = 63%, 679 KB/s], Decompressed: 5245
Downloaded: 5378 file(s) [attempted 5378/8459 = 63%, 387 KB/s], Decompressed: 5371
Downloaded: 5419 file(s) [attempted 5419/8459 = 64%, 29 KB/s], Decompressed: 5412
Downloaded: 5461 file(s) [attempted 5461/8459 = 64%, 155 KB/s], Decompressed: 5457
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 308 KB/s], Decompressed: 5498
Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 294 KB/s], Decompressed: 5535
Downloaded: 5578 file(s) [attempted 5578/8459 = 65%, 39 KB/s], Decompressed: 5573
Downloaded: 5623 file(s) [attempted 5623/8459 = 66%, 324 KB/s], Decompressed: 5614
Downloaded: 5656 file(s) [attempted 5656/8459 = 66%, 245 KB/s], Decompressed: 5648
Downloaded: 5693 file(s) [attempted 5693/8459 = 67%, 3011 KB/s], Decompressed: 5686
Downloaded: 5734 file(s) [attempted 5734/8459 = 67%, 71 KB/s], Decompressed: 5730
Downloaded: 5775 file(s) [attempted 5775/8459 = 68%, 137 KB/s], Decompressed: 5734
Downloaded: 5819 file(s) [attempted 5819/8459 = 68%, 108 KB/s], Decompressed: 5734
Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 76 KB/s], Decompressed: 5741
Downloaded: 5905 file(s) [attempted 5905/8459 = 69%, 619 KB/s], Decompressed: 5741
Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 205 KB/s], Decompressed: 5741
Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 74 KB/s], Decompressed: 5741
Downloaded: 6021 file(s) [attempted 6021/8459 = 71%, 888 KB/s], Decompressed: 5997
Downloaded: 6067 file(s) [attempted 6067/8459 = 71%, 372 KB/s], Decompressed: 6062
Downloaded: 6104 file(s) [attempted 6104/8459 = 72%, 27 KB/s], Decompressed: 6097
Downloaded: 6142 file(s) [attempted 6142/8459 = 72%, 1522 KB/s], Decompressed: 6134
Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 456 KB/s], Decompressed: 6176
Downloaded: 6220 file(s) [attempted 6220/8459 = 73%, 511 KB/s], Decompressed: 6193
Downloaded: 6264 file(s) [attempted 6264/8459 = 74%, 387 KB/s], Decompressed: 6193
Downloaded: 6305 file(s) [attempted 6305/8459 = 74%, 81 KB/s], Decompressed: 6299
Downloaded: 6343 file(s) [attempted 6343/8459 = 74%, 207 KB/s], Decompressed: 6316
Downloaded: 6381 file(s) [attempted 6381/8459 = 75%, 246 KB/s], Decompressed: 6316
Downloaded: 6425 file(s) [attempted 6425/8459 = 75%, 785 KB/s], Decompressed: 6323
Downloaded: 6470 file(s) [attempted 6470/8459 = 76%, 465 KB/s], Decompressed: 6466
Downloaded: 6511 file(s) [attempted 6511/8459 = 76%, 75 KB/s], Decompressed: 6483
Downloaded: 6545 file(s) [attempted 6545/8459 = 77%, 1516 KB/s], Decompressed: 6483
Downloaded: 6586 file(s) [attempted 6586/8459 = 77%, 85 KB/s], Decompressed: 6483
Downloaded: 6627 file(s) [attempted 6627/8459 = 78%, 49 KB/s], Decompressed: 6489
Downloaded: 6672 file(s) [attempted 6672/8459 = 78%, 681 KB/s], Decompressed: 6665
Downloaded: 6713 file(s) [attempted 6713/8459 = 79%, 136 KB/s], Decompressed: 6709
Downloaded: 6753 file(s) [attempted 6753/8459 = 79%, 172 KB/s], Decompressed: 6747
Downloaded: 6793 file(s) [attempted 6793/8459 = 80%, 361 KB/s], Decompressed: 6785
Downloaded: 6832 file(s) [attempted 6832/8459 = 80%, 55 KB/s], Decompressed: 6822
Downloaded: 6872 file(s) [attempted 6872/8459 = 81%, 368 KB/s], Decompressed: 6867
Downloaded: 6908 file(s) [attempted 6908/8459 = 81%, 427 KB/s], Decompressed: 6884
Downloaded: 6952 file(s) [attempted 6952/8459 = 82%, 1049 KB/s], Decompressed: 6884
Downloaded: 6993 file(s) [attempted 6993/8459 = 82%, 249 KB/s], Decompressed: 6983
Downloaded: 7034 file(s) [attempted 7034/8459 = 83%, 41 KB/s], Decompressed: 6993
Downloaded: 7079 file(s) [attempted 7079/8459 = 83%, 776 KB/s], Decompressed: 6993
Downloaded: 7120 file(s) [attempted 7120/8459 = 84%, 75 KB/s], Decompressed: 7000
Downloaded: 7158 file(s) [attempted 7158/8459 = 84%, 96 KB/s], Decompressed: 7000
Downloaded: 7199 file(s) [attempted 7199/8459 = 85%, 954 KB/s], Decompressed: 7086
Downloaded: 7236 file(s) [attempted 7236/8459 = 85%, 96 KB/s], Decompressed: 7086
Downloaded: 7281 file(s) [attempted 7281/8459 = 86%, 175 KB/s], Decompressed: 7086
Downloaded: 7322 file(s) [attempted 7322/8459 = 86%, 137 KB/s], Decompressed: 7086
Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 122 KB/s], Decompressed: 7182
Downloaded: 7404 file(s) [attempted 7404/8459 = 87%, 112 KB/s], Decompressed: 7182
Downloaded: 7445 file(s) [attempted 7445/8459 = 88%, 165 KB/s], Decompressed: 7182
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 289 KB/s], Decompressed: 7486
Downloaded: 7527 file(s) [attempted 7527/8459 = 88%, 183 KB/s], Decompressed: 7520
Downloaded: 7568 file(s) [attempted 7568/8459 = 89%, 142 KB/s], Decompressed: 7561
Downloaded: 7609 file(s) [attempted 7609/8459 = 89%, 211 KB/s], Decompressed: 7603
Downloaded: 7650 file(s) [attempted 7650/8459 = 90%, 288 KB/s], Decompressed: 7647
Downloaded: 7691 file(s) [attempted 7691/8459 = 90%, 48 KB/s], Decompressed: 7685
Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 30 KB/s], Decompressed: 7695
Downloaded: 7774 file(s) [attempted 7774/8459 = 91%, 193 KB/s], Decompressed: 7695
Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 22 KB/s], Decompressed: 7698
Downloaded: 7856 file(s) [attempted 7856/8459 = 92%, 2295 KB/s], Decompressed: 7698
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 888 KB/s], Decompressed: 7698
Downloaded: 7934 file(s) [attempted 7934/8459 = 93%, 318 KB/s], Decompressed: 7698
Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 697 KB/s], Decompressed: 7787
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 149 KB/s], Decompressed: 7787
Downloaded: 8054 file(s) [attempted 8054/8459 = 95%, 113 KB/s], Decompressed: 7787
Downloaded: 8095 file(s) [attempted 8095/8459 = 95%, 517 KB/s], Decompressed: 7787
Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 109 KB/s], Decompressed: 7787
Downloaded: 8181 file(s) [attempted 8181/8459 = 96%, 52 KB/s], Decompressed: 7787
Downloaded: 8219 file(s) [attempted 8219/8459 = 97%, 688 KB/s], Decompressed: 7958
Downloaded: 8259 file(s) [attempted 8259/8459 = 97%, 83 KB/s], Decompressed: 7958
Downloaded: 8297 file(s) [attempted 8297/8459 = 98%, 672 KB/s], Decompressed: 7958
Downloaded: 8338 file(s) [attempted 8338/8459 = 98%, 165 KB/s], Decompressed: 7958
Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 342 KB/s], Decompressed: 8208
Downloaded: 8421 file(s) [attempted 8421/8459 = 99%, 436 KB/s], Decompressed: 8414
Downloaded: 8456 file(s) [attempted 8456/8459 = 99%, 724 KB/s], Decompressed: 8451
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 724 KB/s], Decompressed: 8455
$ lake build
exit_code=Some(1) duration_ms=773227
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (92s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.5s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.6s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/771] Built Iut.Foundations.QualitativeData (1.0s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.6s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (120s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.3s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.6s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (110s)
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 (71s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.7s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.1s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.7s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.3s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (25s)
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 (210s)
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=1894
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-1350-source
Cloning into '/var/lib/apodeixis/repos/job-1350-source'...
git_checkout exit 0
git checkout 7e8723799fa4cc9fc8310892494d115ef2a885bb
Note: switching to '7e8723799fa4cc9fc8310892494d115ef2a885bb'. 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 7e87237 Bundle valuation ball route inputs
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%, 12 KB/s], Decompressed: 0 Downloaded: 13 file(s) [attempted 13/8459 = 0%, 10 KB/s], Decompressed: 10 Downloaded: 37 file(s) [attempted 37/8459 = 0%, 29 KB/s], Decompressed: 33 Downloaded: 58 file(s) [attempted 58/8459 = 0%, 33 KB/s], Decompressed: 53 Downloaded: 82 file(s) [attempted 82/8459 = 0%, 187 KB/s], Decompressed: 79 Downloaded: 114 file(s) [attempted 114/8459 = 1%, 77 KB/s], Decompressed: 110 Downloaded: 148 file(s) [attempted 148/8459 = 1%, 359 KB/s], Decompressed: 141 Downloaded: 182 file(s) [attempted 182/8459 = 2%, 239 KB/s], Decompressed: 141 Downloaded: 216 file(s) [attempted 216/8459 = 2%, 102 KB/s], Decompressed: 145 Downloaded: 247 file(s) [attempted 247/8459 = 2%, 659 KB/s], Decompressed: 244 Downloaded: 278 file(s) [attempted 278/8459 = 3%, 376 KB/s], Decompressed: 271 Downloaded: 319 file(s) [attempted 319/8459 = 3%, 172 KB/s], Decompressed: 275 Downloaded: 360 file(s) [attempted 360/8459 = 4%, 216 KB/s], Decompressed: 275 Downloaded: 405 file(s) [attempted 405/8459 = 4%, 60 KB/s], Decompressed: 398 Downloaded: 434 file(s) [attempted 434/8459 = 5%, 90 KB/s], Decompressed: 417 Downloaded: 473 file(s) [attempted 473/8459 = 5%, 364 KB/s], Decompressed: 417 Downloaded: 514 file(s) [attempted 514/8459 = 6%, 67 KB/s], Decompressed: 419 Downloaded: 556 file(s) [attempted 556/8459 = 6%, 935 KB/s], Decompressed: 419 Downloaded: 600 file(s) [attempted 600/8459 = 7%, 177 KB/s], Decompressed: 504 Downloaded: 638 file(s) [attempted 638/8459 = 7%, 882 KB/s], Decompressed: 504 Downloaded: 675 file(s) [attempted 675/8459 = 7%, 64 KB/s], Decompressed: 504 Downloaded: 723 file(s) [attempted 723/8459 = 8%, 333 KB/s], Decompressed: 600 Downloaded: 768 file(s) [attempted 768/8459 = 9%, 1170 KB/s], Decompressed: 600 Downloaded: 809 file(s) [attempted 809/8459 = 9%, 305 KB/s], Decompressed: 600 Downloaded: 854 file(s) [attempted 854/8459 = 10%, 173 KB/s], Decompressed: 696 Downloaded: 898 file(s) [attempted 898/8459 = 10%, 214 KB/s], Decompressed: 696 Downloaded: 943 file(s) [attempted 943/8459 = 11%, 40 KB/s], Decompressed: 696 Downloaded: 982 file(s) [attempted 982/8459 = 11%, 437 KB/s], Decompressed: 977 Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 177 KB/s], Decompressed: 1018 Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 416 KB/s], Decompressed: 1052 Downloaded: 1104 file(s) [attempted 1104/8459 = 13%, 66 KB/s], Decompressed: 1069 Downloaded: 1145 file(s) [attempted 1145/8459 = 13%, 126 KB/s], Decompressed: 1069 Downloaded: 1186 file(s) [attempted 1186/8459 = 14%, 37 KB/s], Decompressed: 1076 Downloaded: 1223 file(s) [attempted 1223/8459 = 14%, 395 KB/s], Decompressed: 1076 Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 144 KB/s], Decompressed: 1076 Downloaded: 1305 file(s) [attempted 1305/8459 = 15%, 675 KB/s], Decompressed: 1165 Downloaded: 1346 file(s) [attempted 1346/8459 = 15%, 144 KB/s], Decompressed: 1165 Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 187 KB/s], Decompressed: 1367 Downloaded: 1425 file(s) [attempted 1425/8459 = 16%, 71 KB/s], Decompressed: 1401 Downloaded: 1466 file(s) [attempted 1466/8459 = 17%, 192 KB/s], Decompressed: 1401 Downloaded: 1507 file(s) [attempted 1507/8459 = 17%, 143 KB/s], Decompressed: 1494 Downloaded: 1548 file(s) [attempted 1548/8459 = 18%, 388 KB/s], Decompressed: 1507 Downloaded: 1589 file(s) [attempted 1589/8459 = 18%, 133 KB/s], Decompressed: 1507 Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 230 KB/s], Decompressed: 1617 Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 455 KB/s], Decompressed: 1661 Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 176 KB/s], Decompressed: 1672 Downloaded: 1750 file(s) [attempted 1750/8459 = 20%, 296 KB/s], Decompressed: 1672 Downloaded: 1791 file(s) [attempted 1791/8459 = 21%, 929 KB/s], Decompressed: 1678 Downloaded: 1836 file(s) [attempted 1836/8459 = 21%, 405 KB/s], Decompressed: 1678 Downloaded: 1877 file(s) [attempted 1877/8459 = 22%, 127 KB/s], Decompressed: 1767 Downloaded: 1915 file(s) [attempted 1915/8459 = 22%, 760 KB/s], Decompressed: 1767 Downloaded: 1956 file(s) [attempted 1956/8459 = 23%, 217 KB/s], Decompressed: 1952 Downloaded: 1997 file(s) [attempted 1997/8459 = 23%, 963 KB/s], Decompressed: 1990 Downloaded: 2038 file(s) [attempted 2038/8459 = 24%, 414 KB/s], Decompressed: 2034 Downloaded: 2082 file(s) [attempted 2082/8459 = 24%, 34 KB/s], Decompressed: 2079 Downloaded: 2127 file(s) [attempted 2127/8459 = 25%, 1406 KB/s], Decompressed: 2120 Downloaded: 2168 file(s) [attempted 2168/8459 = 25%, 287 KB/s], Decompressed: 2161 Downloaded: 2205 file(s) [attempted 2205/8459 = 26%, 430 KB/s], Decompressed: 2192 Downloaded: 2247 file(s) [attempted 2247/8459 = 26%, 918 KB/s], Decompressed: 2233 Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 1031 KB/s], Decompressed: 2233 Downloaded: 2339 file(s) [attempted 2339/8459 = 27%, 393 KB/s], Decompressed: 2240 Downloaded: 2380 file(s) [attempted 2380/8459 = 28%, 114 KB/s], Decompressed: 2373 Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 36 KB/s], Decompressed: 2407 Downloaded: 2460 file(s) [attempted 2460/8459 = 29%, 24 KB/s], Decompressed: 2452 Downloaded: 2500 file(s) [attempted 2500/8459 = 29%, 1450 KB/s], Decompressed: 2490 Downloaded: 2537 file(s) [attempted 2537/8459 = 29%, 607 KB/s], Decompressed: 2534 Downloaded: 2582 file(s) [attempted 2582/8459 = 30%, 381 KB/s], Decompressed: 2579 Downloaded: 2617 file(s) [attempted 2617/8459 = 30%, 537 KB/s], Decompressed: 2609 Downloaded: 2661 file(s) [attempted 2661/8459 = 31%, 1750 KB/s], Decompressed: 2609 Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 133 KB/s], Decompressed: 2609 Downloaded: 2743 file(s) [attempted 2743/8459 = 32%, 129 KB/s], Decompressed: 2609 Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 798 KB/s], Decompressed: 2616 Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 587 KB/s], Decompressed: 2825 Downloaded: 2869 file(s) [attempted 2869/8459 = 33%, 868 KB/s], Decompressed: 2863 Downloaded: 2911 file(s) [attempted 2911/8459 = 34%, 776 KB/s], Decompressed: 2900 Downloaded: 2948 file(s) [attempted 2948/8459 = 34%, 261 KB/s], Decompressed: 2934 Downloaded: 2989 file(s) [attempted 2989/8459 = 35%, 223 KB/s], Decompressed: 2934 Downloaded: 3030 file(s) [attempted 3030/8459 = 35%, 847 KB/s], Decompressed: 2938 Downloaded: 3075 file(s) [attempted 3075/8459 = 36%, 234 KB/s], Decompressed: 3041 Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 687 KB/s], Decompressed: 3041 Downloaded: 3153 file(s) [attempted 3153/8459 = 37%, 83 KB/s], Decompressed: 3150 Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 200 KB/s], Decompressed: 3184 Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 626 KB/s], Decompressed: 3212 Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 148 KB/s], Decompressed: 3212 Downloaded: 3335 file(s) [attempted 3335/8459 = 39%, 160 KB/s], Decompressed: 3218 Downloaded: 3372 file(s) [attempted 3372/8459 = 39%, 278 KB/s], Decompressed: 3218 Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 203 KB/s], Decompressed: 3304 Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 407 KB/s], Decompressed: 3304 Downloaded: 3489 file(s) [attempted 3489/8459 = 41%, 75 KB/s], Decompressed: 3304 Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 276 KB/s], Decompressed: 3396 Downloaded: 3585 file(s) [attempted 3585/8459 = 42%, 786 KB/s], Decompressed: 3396 Downloaded: 3626 file(s) [attempted 3626/8459 = 42%, 257 KB/s], Decompressed: 3496 Downloaded: 3660 file(s) [attempted 3660/8459 = 43%, 336 KB/s], Decompressed: 3496 Downloaded: 3694 file(s) [attempted 3694/8459 = 43%, 296 KB/s], Decompressed: 3592 Downloaded: 3735 file(s) [attempted 3735/8459 = 44%, 94 KB/s], Decompressed: 3592 Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 133 KB/s], Decompressed: 3759 Downloaded: 3821 file(s) [attempted 3821/8459 = 45%, 483 KB/s], Decompressed: 3759 Downloaded: 3858 file(s) [attempted 3858/8459 = 45%, 822 KB/s], Decompressed: 3759 Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 65 KB/s], Decompressed: 3759 Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 382 KB/s], Decompressed: 3783 Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 287 KB/s], Decompressed: 3783 Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 120 KB/s], Decompressed: 3934 Downloaded: 4078 file(s) [attempted 4078/8459 = 48%, 781 KB/s], Decompressed: 3934 Downloaded: 4112 file(s) [attempted 4112/8459 = 48%, 148 KB/s], Decompressed: 4023 Downloaded: 4154 file(s) [attempted 4154/8459 = 49%, 632 KB/s], Decompressed: 4149 Downloaded: 4196 file(s) [attempted 4196/8459 = 49%, 743 KB/s], Decompressed: 4160 Downloaded: 4235 file(s) [attempted 4235/8459 = 50%, 699 KB/s], Decompressed: 4160 Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 297 KB/s], Decompressed: 4266 Downloaded: 4324 file(s) [attempted 4324/8459 = 51%, 338 KB/s], Decompressed: 4317 Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 477 KB/s], Decompressed: 4348 Downloaded: 4397 file(s) [attempted 4397/8459 = 51%, 36 KB/s], Decompressed: 4392 Downloaded: 4438 file(s) [attempted 4438/8459 = 52%, 710 KB/s], Decompressed: 4433 Downloaded: 4481 file(s) [attempted 4481/8459 = 52%, 347 KB/s], Decompressed: 4474 Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 533 KB/s], Decompressed: 4516 Downloaded: 4563 file(s) [attempted 4563/8459 = 53%, 112 KB/s], Decompressed: 4560 Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 540 KB/s], Decompressed: 4598 Downloaded: 4646 file(s) [attempted 4646/8459 = 54%, 410 KB/s], Decompressed: 4618 Downloaded: 4680 file(s) [attempted 4680/8459 = 55%, 69 KB/s], Decompressed: 4676 Downloaded: 4721 file(s) [attempted 4721/8459 = 55%, 687 KB/s], Decompressed: 4700 Downloaded: 4759 file(s) [attempted 4759/8459 = 56%, 88 KB/s], Decompressed: 4700 Downloaded: 4800 file(s) [attempted 4800/8459 = 56%, 709 KB/s], Decompressed: 4707 Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 286 KB/s], Decompressed: 4810 Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 850 KB/s], Decompressed: 4810 Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 80 KB/s], Decompressed: 4817 Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 247 KB/s], Decompressed: 4817 Downloaded: 5008 file(s) [attempted 5008/8459 = 59%, 134 KB/s], Decompressed: 4817 Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 280 KB/s], Decompressed: 4817 Downloaded: 5087 file(s) [attempted 5087/8459 = 60%, 131 KB/s], Decompressed: 5070 Downloaded: 5132 file(s) [attempted 5132/8459 = 60%, 42 KB/s], Decompressed: 5125 Downloaded: 5173 file(s) [attempted 5173/8459 = 61%, 175 KB/s], Decompressed: 5159 Downloaded: 5217 file(s) [attempted 5217/8459 = 61%, 872 KB/s], Decompressed: 5159 Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 39 KB/s], Decompressed: 5162 Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 61 KB/s], Decompressed: 5162 Downloaded: 5340 file(s) [attempted 5340/8459 = 63%, 679 KB/s], Decompressed: 5245 Downloaded: 5378 file(s) [attempted 5378/8459 = 63%, 387 KB/s], Decompressed: 5371 Downloaded: 5419 file(s) [attempted 5419/8459 = 64%, 29 KB/s], Decompressed: 5412 Downloaded: 5461 file(s) [attempted 5461/8459 = 64%, 155 KB/s], Decompressed: 5457 Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 308 KB/s], Decompressed: 5498 Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 294 KB/s], Decompressed: 5535 Downloaded: 5578 file(s) [attempted 5578/8459 = 65%, 39 KB/s], Decompressed: 5573 Downloaded: 5623 file(s) [attempted 5623/8459 = 66%, 324 KB/s], Decompressed: 5614 Downloaded: 5656 file(s) [attempted 5656/8459 = 66%, 245 KB/s], Decompressed: 5648 Downloaded: 5693 file(s) [attempted 5693/8459 = 67%, 3011 KB/s], Decompressed: 5686 Downloaded: 5734 file(s) [attempted 5734/8459 = 67%, 71 KB/s], Decompressed: 5730 Downloaded: 5775 file(s) [attempted 5775/8459 = 68%, 137 KB/s], Decompressed: 5734 Downloaded: 5819 file(s) [attempted 5819/8459 = 68%, 108 KB/s], Decompressed: 5734 Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 76 KB/s], Decompressed: 5741 Downloaded: 5905 file(s) [attempted 5905/8459 = 69%, 619 KB/s], Decompressed: 5741 Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 205 KB/s], Decompressed: 5741 Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 74 KB/s], Decompressed: 5741 Downloaded: 6021 file(s) [attempted 6021/8459 = 71%, 888 KB/s], Decompressed: 5997 Downloaded: 6067 file(s) [attempted 6067/8459 = 71%, 372 KB/s], Decompressed: 6062 Downloaded: 6104 file(s) [attempted 6104/8459 = 72%, 27 KB/s], Decompressed: 6097 Downloaded: 6142 file(s) [attempted 6142/8459 = 72%, 1522 KB/s], Decompressed: 6134 Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 456 KB/s], Decompressed: 6176 Downloaded: 6220 file(s) [attempted 6220/8459 = 73%, 511 KB/s], Decompressed: 6193 Downloaded: 6264 file(s) [attempted 6264/8459 = 74%, 387 KB/s], Decompressed: 6193 Downloaded: 6305 file(s) [attempted 6305/8459 = 74%, 81 KB/s], Decompressed: 6299 Downloaded: 6343 file(s) [attempted 6343/8459 = 74%, 207 KB/s], Decompressed: 6316 Downloaded: 6381 file(s) [attempted 6381/8459 = 75%, 246 KB/s], Decompressed: 6316 Downloaded: 6425 file(s) [attempted 6425/8459 = 75%, 785 KB/s], Decompressed: 6323 Downloaded: 6470 file(s) [attempted 6470/8459 = 76%, 465 KB/s], Decompressed: 6466 Downloaded: 6511 file(s) [attempted 6511/8459 = 76%, 75 KB/s], Decompressed: 6483 Downloaded: 6545 file(s) [attempted 6545/8459 = 77%, 1516 KB/s], Decompressed: 6483 Downloaded: 6586 file(s) [attempted 6586/8459 = 77%, 85 KB/s], Decompressed: 6483 Downloaded: 6627 file(s) [attempted 6627/8459 = 78%, 49 KB/s], Decompressed: 6489 Downloaded: 6672 file(s) [attempted 6672/8459 = 78%, 681 KB/s], Decompressed: 6665 Downloaded: 6713 file(s) [attempted 6713/8459 = 79%, 136 KB/s], Decompressed: 6709 Downloaded: 6753 file(s) [attempted 6753/8459 = 79%, 172 KB/s], Decompressed: 6747 Downloaded: 6793 file(s) [attempted 6793/8459 = 80%, 361 KB/s], Decompressed: 6785 Downloaded: 6832 file(s) [attempted 6832/8459 = 80%, 55 KB/s], Decompressed: 6822 Downloaded: 6872 file(s) [attempted 6872/8459 = 81%, 368 KB/s], Decompressed: 6867 Downloaded: 6908 file(s) [attempted 6908/8459 = 81%, 427 KB/s], Decompressed: 6884 Downloaded: 6952 file(s) [attempted 6952/8459 = 82%, 1049 KB/s], Decompressed: 6884 Downloaded: 6993 file(s) [attempted 6993/8459 = 82%, 249 KB/s], Decompressed: 6983 Downloaded: 7034 file(s) [attempted 7034/8459 = 83%, 41 KB/s], Decompressed: 6993 Downloaded: 7079 file(s) [attempted 7079/8459 = 83%, 776 KB/s], Decompressed: 6993 Downloaded: 7120 file(s) [attempted 7120/8459 = 84%, 75 KB/s], Decompressed: 7000 Downloaded: 7158 file(s) [attempted 7158/8459 = 84%, 96 KB/s], Decompressed: 7000 Downloaded: 7199 file(s) [attempted 7199/8459 = 85%, 954 KB/s], Decompressed: 7086 Downloaded: 7236 file(s) [attempted 7236/8459 = 85%, 96 KB/s], Decompressed: 7086 Downloaded: 7281 file(s) [attempted 7281/8459 = 86%, 175 KB/s], Decompressed: 7086 Downloaded: 7322 file(s) [attempted 7322/8459 = 86%, 137 KB/s], Decompressed: 7086 Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 122 KB/s], Decompressed: 7182 Downloaded: 7404 file(s) [attempted 7404/8459 = 87%, 112 KB/s], Decompressed: 7182 Downloaded: 7445 file(s) [attempted 7445/8459 = 88%, 165 KB/s], Decompressed: 7182 Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 289 KB/s], Decompressed: 7486 Downloaded: 7527 file(s) [attempted 7527/8459 = 88%, 183 KB/s], Decompressed: 7520 Downloaded: 7568 file(s) [attempted 7568/8459 = 89%, 142 KB/s], Decompressed: 7561 Downloaded: 7609 file(s) [attempted 7609/8459 = 89%, 211 KB/s], Decompressed: 7603 Downloaded: 7650 file(s) [attempted 7650/8459 = 90%, 288 KB/s], Decompressed: 7647 Downloaded: 7691 file(s) [attempted 7691/8459 = 90%, 48 KB/s], Decompressed: 7685 Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 30 KB/s], Decompressed: 7695 Downloaded: 7774 file(s) [attempted 7774/8459 = 91%, 193 KB/s], Decompressed: 7695 Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 22 KB/s], Decompressed: 7698 Downloaded: 7856 file(s) [attempted 7856/8459 = 92%, 2295 KB/s], Decompressed: 7698 Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 888 KB/s], Decompressed: 7698 Downloaded: 7934 file(s) [attempted 7934/8459 = 93%, 318 KB/s], Decompressed: 7698 Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 697 KB/s], Decompressed: 7787 Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 149 KB/s], Decompressed: 7787 Downloaded: 8054 file(s) [attempted 8054/8459 = 95%, 113 KB/s], Decompressed: 7787 Downloaded: 8095 file(s) [attempted 8095/8459 = 95%, 517 KB/s], Decompressed: 7787 Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 109 KB/s], Decompressed: 7787 Downloaded: 8181 file(s) [attempted 8181/8459 = 96%, 52 KB/s], Decompressed: 7787 Downloaded: 8219 file(s) [attempted 8219/8459 = 97%, 688 KB/s], Decompressed: 7958 Downloaded: 8259 file(s) [attempted 8259/8459 = 97%, 83 KB/s], Decompressed: 7958 Downloaded: 8297 file(s) [attempted 8297/8459 = 98%, 672 KB/s], Decompressed: 7958 Downloaded: 8338 file(s) [attempted 8338/8459 = 98%, 165 KB/s], Decompressed: 7958 Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 342 KB/s], Decompressed: 8208 Downloaded: 8421 file(s) [attempted 8421/8459 = 99%, 436 KB/s], Decompressed: 8414 Downloaded: 8456 file(s) [attempted 8456/8459 = 99%, 724 KB/s], Decompressed: 8451 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 724 KB/s], Decompressed: 8455
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (92s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.5s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.6s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/771] Built Iut.Foundations.QualitativeData (1.0s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.6s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (120s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.3s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.6s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (110s)
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 (71s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.7s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.1s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.7s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.3s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (25s)
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 (210s)
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`