Verification run
Run 1034
failed commit
9ad3d67e022d toolchain lean-v4-30-0 prover lean took 25m 31s · 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-1330-source
exit_code=Some(0) duration_ms=3499
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1330-source'...
$ git checkout 9ad3d67e022dee2d7ef4f1b2f33a9f08b2dfa2ca
exit_code=Some(0) duration_ms=145
stderr:
Note: switching to '9ad3d67e022dee2d7ef4f1b2f33a9f08b2dfa2ca'.
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 9ad3d67 Thread inverse-base valuation CTheta route
Resolved source revision: 9ad3d67e022dee2d7ef4f1b2f33a9f08b2dfa2ca
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=9ad3d67e022dee2d7ef4f1b2f33a9f08b2dfa2ca provenance={"branch":"master","checked_out_revision":"9ad3d67e022dee2d7ef4f1b2f33a9f08b2dfa2ca","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"9ad3d67e022dee2d7ef4f1b2f33a9f08b2dfa2ca","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=130726
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: 15 file(s) [attempted 15/8459 = 0%, 2 KB/s], Decompressed: 14
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 17 KB/s], Decompressed: 26
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 28 KB/s], Decompressed: 26
Downloaded: 97 file(s) [attempted 97/8459 = 1%, 100 KB/s], Decompressed: 93
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 425 KB/s], Decompressed: 131
Downloaded: 168 file(s) [attempted 168/8459 = 1%, 116 KB/s], Decompressed: 165
Downloaded: 207 file(s) [attempted 207/8459 = 2%, 291 KB/s], Decompressed: 203
Downloaded: 247 file(s) [attempted 247/8459 = 2%, 314 KB/s], Decompressed: 237
Downloaded: 288 file(s) [attempted 288/8459 = 3%, 187 KB/s], Decompressed: 278
Downloaded: 323 file(s) [attempted 323/8459 = 3%, 681 KB/s], Decompressed: 319
Downloaded: 367 file(s) [attempted 367/8459 = 4%, 1177 KB/s], Decompressed: 364
Downloaded: 415 file(s) [attempted 415/8459 = 4%, 28 KB/s], Decompressed: 412
Downloaded: 463 file(s) [attempted 463/8459 = 5%, 929 KB/s], Decompressed: 460
Downloaded: 514 file(s) [attempted 514/8459 = 6%, 677 KB/s], Decompressed: 504
Downloaded: 562 file(s) [attempted 562/8459 = 6%, 323 KB/s], Decompressed: 559
Downloaded: 607 file(s) [attempted 607/8459 = 7%, 623 KB/s], Decompressed: 603
Downloaded: 651 file(s) [attempted 651/8459 = 7%, 1550 KB/s], Decompressed: 648
Downloaded: 691 file(s) [attempted 691/8459 = 8%, 701 KB/s], Decompressed: 682
Downloaded: 734 file(s) [attempted 734/8459 = 8%, 123 KB/s], Decompressed: 727
Downloaded: 778 file(s) [attempted 778/8459 = 9%, 439 KB/s], Decompressed: 775
Downloaded: 823 file(s) [attempted 823/8459 = 9%, 532 KB/s], Decompressed: 816
Downloaded: 866 file(s) [attempted 866/8459 = 10%, 283 KB/s], Decompressed: 857
Downloaded: 908 file(s) [attempted 908/8459 = 10%, 682 KB/s], Decompressed: 881
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 447 KB/s], Decompressed: 886
Downloaded: 994 file(s) [attempted 994/8459 = 11%, 162 KB/s], Decompressed: 886
Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 359 KB/s], Decompressed: 912
Downloaded: 1080 file(s) [attempted 1080/8459 = 12%, 297 KB/s], Decompressed: 912
Downloaded: 1124 file(s) [attempted 1124/8459 = 13%, 398 KB/s], Decompressed: 1008
Downloaded: 1165 file(s) [attempted 1165/8459 = 13%, 355 KB/s], Decompressed: 1008
Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 276 KB/s], Decompressed: 1008
Downloaded: 1251 file(s) [attempted 1251/8459 = 14%, 595 KB/s], Decompressed: 1107
Downloaded: 1292 file(s) [attempted 1292/8459 = 15%, 873 KB/s], Decompressed: 1107
Downloaded: 1333 file(s) [attempted 1333/8459 = 15%, 69 KB/s], Decompressed: 1207
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 29 KB/s], Decompressed: 1207
Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 107 KB/s], Decompressed: 1305
Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 49 KB/s], Decompressed: 1305
Downloaded: 1504 file(s) [attempted 1504/8459 = 17%, 96 KB/s], Decompressed: 1305
Downloaded: 1545 file(s) [attempted 1545/8459 = 18%, 1075 KB/s], Decompressed: 1408
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 37 KB/s], Decompressed: 1408
Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 729 KB/s], Decompressed: 1514
Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 584 KB/s], Decompressed: 1514
Downloaded: 1715 file(s) [attempted 1715/8459 = 20%, 225 KB/s], Decompressed: 1613
Downloaded: 1754 file(s) [attempted 1754/8459 = 20%, 283 KB/s], Decompressed: 1613
Downloaded: 1802 file(s) [attempted 1802/8459 = 21%, 1109 KB/s], Decompressed: 1613
Downloaded: 1846 file(s) [attempted 1846/8459 = 21%, 571 KB/s], Decompressed: 1815
Downloaded: 1884 file(s) [attempted 1884/8459 = 22%, 726 KB/s], Decompressed: 1856
Downloaded: 1921 file(s) [attempted 1921/8459 = 22%, 789 KB/s], Decompressed: 1856
Downloaded: 1966 file(s) [attempted 1966/8459 = 23%, 967 KB/s], Decompressed: 1870
Downloaded: 2008 file(s) [attempted 2008/8459 = 23%, 138 KB/s], Decompressed: 2004
Downloaded: 2055 file(s) [attempted 2055/8459 = 24%, 47 KB/s], Decompressed: 2024
Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 1104 KB/s], Decompressed: 2024
Downloaded: 2140 file(s) [attempted 2140/8459 = 25%, 963 KB/s], Decompressed: 2034
Downloaded: 2182 file(s) [attempted 2182/8459 = 25%, 57 KB/s], Decompressed: 2116
Downloaded: 2223 file(s) [attempted 2223/8459 = 26%, 120 KB/s], Decompressed: 2116
Downloaded: 2266 file(s) [attempted 2266/8459 = 26%, 516 KB/s], Decompressed: 2260
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 105 KB/s], Decompressed: 2298
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 173 KB/s], Decompressed: 2339
Downloaded: 2387 file(s) [attempted 2387/8459 = 28%, 268 KB/s], Decompressed: 2346
Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 518 KB/s], Decompressed: 2346
Downloaded: 2472 file(s) [attempted 2472/8459 = 29%, 456 KB/s], Decompressed: 2353
Downloaded: 2513 file(s) [attempted 2513/8459 = 29%, 598 KB/s], Decompressed: 2353
Downloaded: 2555 file(s) [attempted 2555/8459 = 30%, 456 KB/s], Decompressed: 2438
Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 392 KB/s], Decompressed: 2537
Downloaded: 2637 file(s) [attempted 2637/8459 = 31%, 100 KB/s], Decompressed: 2537
Downloaded: 2681 file(s) [attempted 2681/8459 = 31%, 197 KB/s], Decompressed: 2565
Downloaded: 2722 file(s) [attempted 2722/8459 = 32%, 194 KB/s], Decompressed: 2565
Downloaded: 2767 file(s) [attempted 2767/8459 = 32%, 376 KB/s], Decompressed: 2756
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 523 KB/s], Decompressed: 2794
Downloaded: 2852 file(s) [attempted 2852/8459 = 33%, 187 KB/s], Decompressed: 2845
Downloaded: 2900 file(s) [attempted 2900/8459 = 34%, 721 KB/s], Decompressed: 2897
Downloaded: 2939 file(s) [attempted 2939/8459 = 34%, 1081 KB/s], Decompressed: 2934
Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 24 KB/s], Decompressed: 2979
Downloaded: 3023 file(s) [attempted 3023/8459 = 35%, 126 KB/s], Decompressed: 2999
Downloaded: 3064 file(s) [attempted 3064/8459 = 36%, 196 KB/s], Decompressed: 3054
Downloaded: 3102 file(s) [attempted 3102/8459 = 36%, 102 KB/s], Decompressed: 3095
Downloaded: 3147 file(s) [attempted 3147/8459 = 37%, 53 KB/s], Decompressed: 3143
Downloaded: 3194 file(s) [attempted 3194/8459 = 37%, 313 KB/s], Decompressed: 3191
Downloaded: 3242 file(s) [attempted 3242/8459 = 38%, 294 KB/s], Decompressed: 3222
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 107 KB/s], Decompressed: 3222
Downloaded: 3331 file(s) [attempted 3331/8459 = 39%, 182 KB/s], Decompressed: 3232
Downloaded: 3372 file(s) [attempted 3372/8459 = 39%, 44 KB/s], Decompressed: 3232
Downloaded: 3414 file(s) [attempted 3414/8459 = 40%, 212 KB/s], Decompressed: 3232
Downloaded: 3455 file(s) [attempted 3455/8459 = 40%, 500 KB/s], Decompressed: 3314
Downloaded: 3502 file(s) [attempted 3502/8459 = 41%, 864 KB/s], Decompressed: 3314
Downloaded: 3547 file(s) [attempted 3547/8459 = 41%, 203 KB/s], Decompressed: 3424
Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 82 KB/s], Decompressed: 3581
Downloaded: 3629 file(s) [attempted 3629/8459 = 42%, 670 KB/s], Decompressed: 3619
Downloaded: 3670 file(s) [attempted 3670/8459 = 43%, 560 KB/s], Decompressed: 3639
Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 66 KB/s], Decompressed: 3639
Downloaded: 3758 file(s) [attempted 3758/8459 = 44%, 898 KB/s], Decompressed: 3739
Downloaded: 3800 file(s) [attempted 3800/8459 = 44%, 317 KB/s], Decompressed: 3797
Downloaded: 3845 file(s) [attempted 3845/8459 = 45%, 470 KB/s], Decompressed: 3834
Downloaded: 3886 file(s) [attempted 3886/8459 = 45%, 149 KB/s], Decompressed: 3838
Downloaded: 3927 file(s) [attempted 3927/8459 = 46%, 163 KB/s], Decompressed: 3838
Downloaded: 3968 file(s) [attempted 3968/8459 = 46%, 107 KB/s], Decompressed: 3961
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 337 KB/s], Decompressed: 4002
Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 688 KB/s], Decompressed: 4043
Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 154 KB/s], Decompressed: 4043
Downloaded: 4142 file(s) [attempted 4142/8459 = 48%, 201 KB/s], Decompressed: 4047
Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 197 KB/s], Decompressed: 4047
Downloaded: 4225 file(s) [attempted 4225/8459 = 49%, 294 KB/s], Decompressed: 4047
Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 247 KB/s], Decompressed: 4231
Downloaded: 4310 file(s) [attempted 4310/8459 = 50%, 246 KB/s], Decompressed: 4231
Downloaded: 4355 file(s) [attempted 4355/8459 = 51%, 1224 KB/s], Decompressed: 4259
Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 37 KB/s], Decompressed: 4392
Downloaded: 4433 file(s) [attempted 4433/8459 = 52%, 112 KB/s], Decompressed: 4427
Downloaded: 4474 file(s) [attempted 4474/8459 = 52%, 452 KB/s], Decompressed: 4471
Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 120 KB/s], Decompressed: 4471
Downloaded: 4563 file(s) [attempted 4563/8459 = 53%, 76 KB/s], Decompressed: 4474
Downloaded: 4608 file(s) [attempted 4608/8459 = 54%, 405 KB/s], Decompressed: 4584
Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 552 KB/s], Decompressed: 4584
Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 105 KB/s], Decompressed: 4591
Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 212 KB/s], Decompressed: 4591
Downloaded: 4772 file(s) [attempted 4772/8459 = 56%, 129 KB/s], Decompressed: 4673
Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 303 KB/s], Decompressed: 4806
Downloaded: 4861 file(s) [attempted 4861/8459 = 57%, 865 KB/s], Decompressed: 4858
Downloaded: 4907 file(s) [attempted 4907/8459 = 58%, 409 KB/s], Decompressed: 4902
Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 128 KB/s], Decompressed: 4943
Downloaded: 4986 file(s) [attempted 4986/8459 = 58%, 338 KB/s], Decompressed: 4954
Downloaded: 5029 file(s) [attempted 5029/8459 = 59%, 257 KB/s], Decompressed: 4984
Downloaded: 5077 file(s) [attempted 5077/8459 = 60%, 160 KB/s], Decompressed: 4984
Downloaded: 5118 file(s) [attempted 5118/8459 = 60%, 100 KB/s], Decompressed: 5108
Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 451 KB/s], Decompressed: 5108
Downloaded: 5210 file(s) [attempted 5210/8459 = 61%, 193 KB/s], Decompressed: 5114
Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 98 KB/s], Decompressed: 5114
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 64 KB/s], Decompressed: 5114
Downloaded: 5340 file(s) [attempted 5340/8459 = 63%, 417 KB/s], Decompressed: 5327
Downloaded: 5385 file(s) [attempted 5385/8459 = 63%, 136 KB/s], Decompressed: 5381
Downloaded: 5426 file(s) [attempted 5426/8459 = 64%, 392 KB/s], Decompressed: 5422
Downloaded: 5470 file(s) [attempted 5470/8459 = 64%, 25 KB/s], Decompressed: 5422
Downloaded: 5511 file(s) [attempted 5511/8459 = 65%, 366 KB/s], Decompressed: 5426
Downloaded: 5556 file(s) [attempted 5556/8459 = 65%, 364 KB/s], Decompressed: 5552
Downloaded: 5600 file(s) [attempted 5600/8459 = 66%, 23 KB/s], Decompressed: 5594
Downloaded: 5641 file(s) [attempted 5641/8459 = 66%, 51 KB/s], Decompressed: 5635
Downloaded: 5684 file(s) [attempted 5684/8459 = 67%, 74 KB/s], Decompressed: 5676
Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 509 KB/s], Decompressed: 5713
Downloaded: 5771 file(s) [attempted 5771/8459 = 68%, 465 KB/s], Decompressed: 5713
Downloaded: 5811 file(s) [attempted 5811/8459 = 68%, 65 KB/s], Decompressed: 5720
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 1061 KB/s], Decompressed: 5843
Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 351 KB/s], Decompressed: 5891
Downloaded: 5943 file(s) [attempted 5943/8459 = 70%, 708 KB/s], Decompressed: 5936
Downloaded: 5985 file(s) [attempted 5985/8459 = 70%, 1670 KB/s], Decompressed: 5980
Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 30 KB/s], Decompressed: 6014
Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 257 KB/s], Decompressed: 6066
Downloaded: 6110 file(s) [attempted 6110/8459 = 72%, 1047 KB/s], Decompressed: 6069
Downloaded: 6155 file(s) [attempted 6155/8459 = 72%, 47 KB/s], Decompressed: 6069
Downloaded: 6196 file(s) [attempted 6196/8459 = 73%, 83 KB/s], Decompressed: 6076
Downloaded: 6240 file(s) [attempted 6240/8459 = 73%, 693 KB/s], Decompressed: 6076
Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 181 KB/s], Decompressed: 6264
Downloaded: 6326 file(s) [attempted 6326/8459 = 74%, 397 KB/s], Decompressed: 6319
Downloaded: 6367 file(s) [attempted 6367/8459 = 75%, 754 KB/s], Decompressed: 6343
Downloaded: 6411 file(s) [attempted 6411/8459 = 75%, 227 KB/s], Decompressed: 6343
Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 324 KB/s], Decompressed: 6350
Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 1291 KB/s], Decompressed: 6350
Downloaded: 6541 file(s) [attempted 6541/8459 = 77%, 209 KB/s], Decompressed: 6442
Downloaded: 6584 file(s) [attempted 6584/8459 = 77%, 81 KB/s], Decompressed: 6442
Downloaded: 6620 file(s) [attempted 6620/8459 = 78%, 309 KB/s], Decompressed: 6442
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 89 KB/s], Decompressed: 6637
Downloaded: 6709 file(s) [attempted 6709/8459 = 79%, 464 KB/s], Decompressed: 6637
Downloaded: 6754 file(s) [attempted 6754/8459 = 79%, 511 KB/s], Decompressed: 6654
Downloaded: 6792 file(s) [attempted 6792/8459 = 80%, 388 KB/s], Decompressed: 6654
Downloaded: 6836 file(s) [attempted 6836/8459 = 80%, 302 KB/s], Decompressed: 6654
Downloaded: 6880 file(s) [attempted 6880/8459 = 81%, 238 KB/s], Decompressed: 6747
Downloaded: 6921 file(s) [attempted 6921/8459 = 81%, 344 KB/s], Decompressed: 6747
Downloaded: 6962 file(s) [attempted 6962/8459 = 82%, 97 KB/s], Decompressed: 6949
Downloaded: 7006 file(s) [attempted 7006/8459 = 82%, 504 KB/s], Decompressed: 7000
Downloaded: 7051 file(s) [attempted 7051/8459 = 83%, 1944 KB/s], Decompressed: 7048
Downloaded: 7099 file(s) [attempted 7099/8459 = 83%, 140 KB/s], Decompressed: 7075
Downloaded: 7140 file(s) [attempted 7140/8459 = 84%, 112 KB/s], Decompressed: 7075
Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 153 KB/s], Decompressed: 7082
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 340 KB/s], Decompressed: 7219
Downloaded: 7265 file(s) [attempted 7265/8459 = 85%, 757 KB/s], Decompressed: 7260
Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 45 KB/s], Decompressed: 7301
Downloaded: 7349 file(s) [attempted 7349/8459 = 86%, 50 KB/s], Decompressed: 7346
Downloaded: 7392 file(s) [attempted 7392/8459 = 87%, 478 KB/s], Decompressed: 7383
Downloaded: 7431 file(s) [attempted 7431/8459 = 87%, 167 KB/s], Decompressed: 7428
Downloaded: 7471 file(s) [attempted 7471/8459 = 88%, 305 KB/s], Decompressed: 7466
Downloaded: 7513 file(s) [attempted 7513/8459 = 88%, 214 KB/s], Decompressed: 7510
Downloaded: 7558 file(s) [attempted 7558/8459 = 89%, 246 KB/s], Decompressed: 7554
Downloaded: 7599 file(s) [attempted 7599/8459 = 89%, 1097 KB/s], Decompressed: 7578
Downloaded: 7643 file(s) [attempted 7643/8459 = 90%, 280 KB/s], Decompressed: 7578
Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 25 KB/s], Decompressed: 7585
Downloaded: 7726 file(s) [attempted 7726/8459 = 91%, 198 KB/s], Decompressed: 7585
Downloaded: 7763 file(s) [attempted 7763/8459 = 91%, 554 KB/s], Decompressed: 7667
Downloaded: 7811 file(s) [attempted 7811/8459 = 92%, 153 KB/s], Decompressed: 7667
Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 36 KB/s], Decompressed: 7763
Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 657 KB/s], Decompressed: 7763
Downloaded: 7955 file(s) [attempted 7955/8459 = 94%, 107 KB/s], Decompressed: 7763
Downloaded: 7999 file(s) [attempted 7999/8459 = 94%, 174 KB/s], Decompressed: 7859
Downloaded: 8047 file(s) [attempted 8047/8459 = 95%, 155 KB/s], Decompressed: 7859
Downloaded: 8095 file(s) [attempted 8095/8459 = 95%, 555 KB/s], Decompressed: 7962
Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 525 KB/s], Decompressed: 7962
Downloaded: 8177 file(s) [attempted 8177/8459 = 96%, 56 KB/s], Decompressed: 8153
Downloaded: 8222 file(s) [attempted 8222/8459 = 97%, 82 KB/s], Decompressed: 8194
Downloaded: 8266 file(s) [attempted 8266/8459 = 97%, 47 KB/s], Decompressed: 8194
Downloaded: 8307 file(s) [attempted 8307/8459 = 98%, 655 KB/s], Decompressed: 8297
Downloaded: 8348 file(s) [attempted 8348/8459 = 98%, 217 KB/s], Decompressed: 8345
Downloaded: 8395 file(s) [attempted 8395/8459 = 99%, 91 KB/s], Decompressed: 8389
Downloaded: 8437 file(s) [attempted 8437/8459 = 99%, 120 KB/s], Decompressed: 8431
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 120 KB/s], Decompressed: 8456
$ lake build
exit_code=Some(1) duration_ms=729813
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (84s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.8s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.6s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.7s)
✔ [763/772] Built Iut.Foundations.QualitativeData (2.1s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.9s)
✔ [3388/3393] Built Iut.Stage1.CorollarySchema (104s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.2s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.8s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.5s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (98s)
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 (47s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (24s)
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 (15s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.8s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (10s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (9.3s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (30s)
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 (182s)
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=7544
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-1330-source
Cloning into '/var/lib/apodeixis/repos/job-1330-source'...
git_checkout exit 0
git checkout 9ad3d67e022dee2d7ef4f1b2f33a9f08b2dfa2ca
Note: switching to '9ad3d67e022dee2d7ef4f1b2f33a9f08b2dfa2ca'. 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 9ad3d67 Thread inverse-base valuation CTheta route
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: 15 file(s) [attempted 15/8459 = 0%, 2 KB/s], Decompressed: 14 Downloaded: 39 file(s) [attempted 39/8459 = 0%, 17 KB/s], Decompressed: 26 Downloaded: 68 file(s) [attempted 68/8459 = 0%, 28 KB/s], Decompressed: 26 Downloaded: 97 file(s) [attempted 97/8459 = 1%, 100 KB/s], Decompressed: 93 Downloaded: 134 file(s) [attempted 134/8459 = 1%, 425 KB/s], Decompressed: 131 Downloaded: 168 file(s) [attempted 168/8459 = 1%, 116 KB/s], Decompressed: 165 Downloaded: 207 file(s) [attempted 207/8459 = 2%, 291 KB/s], Decompressed: 203 Downloaded: 247 file(s) [attempted 247/8459 = 2%, 314 KB/s], Decompressed: 237 Downloaded: 288 file(s) [attempted 288/8459 = 3%, 187 KB/s], Decompressed: 278 Downloaded: 323 file(s) [attempted 323/8459 = 3%, 681 KB/s], Decompressed: 319 Downloaded: 367 file(s) [attempted 367/8459 = 4%, 1177 KB/s], Decompressed: 364 Downloaded: 415 file(s) [attempted 415/8459 = 4%, 28 KB/s], Decompressed: 412 Downloaded: 463 file(s) [attempted 463/8459 = 5%, 929 KB/s], Decompressed: 460 Downloaded: 514 file(s) [attempted 514/8459 = 6%, 677 KB/s], Decompressed: 504 Downloaded: 562 file(s) [attempted 562/8459 = 6%, 323 KB/s], Decompressed: 559 Downloaded: 607 file(s) [attempted 607/8459 = 7%, 623 KB/s], Decompressed: 603 Downloaded: 651 file(s) [attempted 651/8459 = 7%, 1550 KB/s], Decompressed: 648 Downloaded: 691 file(s) [attempted 691/8459 = 8%, 701 KB/s], Decompressed: 682 Downloaded: 734 file(s) [attempted 734/8459 = 8%, 123 KB/s], Decompressed: 727 Downloaded: 778 file(s) [attempted 778/8459 = 9%, 439 KB/s], Decompressed: 775 Downloaded: 823 file(s) [attempted 823/8459 = 9%, 532 KB/s], Decompressed: 816 Downloaded: 866 file(s) [attempted 866/8459 = 10%, 283 KB/s], Decompressed: 857 Downloaded: 908 file(s) [attempted 908/8459 = 10%, 682 KB/s], Decompressed: 881 Downloaded: 949 file(s) [attempted 949/8459 = 11%, 447 KB/s], Decompressed: 886 Downloaded: 994 file(s) [attempted 994/8459 = 11%, 162 KB/s], Decompressed: 886 Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 359 KB/s], Decompressed: 912 Downloaded: 1080 file(s) [attempted 1080/8459 = 12%, 297 KB/s], Decompressed: 912 Downloaded: 1124 file(s) [attempted 1124/8459 = 13%, 398 KB/s], Decompressed: 1008 Downloaded: 1165 file(s) [attempted 1165/8459 = 13%, 355 KB/s], Decompressed: 1008 Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 276 KB/s], Decompressed: 1008 Downloaded: 1251 file(s) [attempted 1251/8459 = 14%, 595 KB/s], Decompressed: 1107 Downloaded: 1292 file(s) [attempted 1292/8459 = 15%, 873 KB/s], Decompressed: 1107 Downloaded: 1333 file(s) [attempted 1333/8459 = 15%, 69 KB/s], Decompressed: 1207 Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 29 KB/s], Decompressed: 1207 Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 107 KB/s], Decompressed: 1305 Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 49 KB/s], Decompressed: 1305 Downloaded: 1504 file(s) [attempted 1504/8459 = 17%, 96 KB/s], Decompressed: 1305 Downloaded: 1545 file(s) [attempted 1545/8459 = 18%, 1075 KB/s], Decompressed: 1408 Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 37 KB/s], Decompressed: 1408 Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 729 KB/s], Decompressed: 1514 Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 584 KB/s], Decompressed: 1514 Downloaded: 1715 file(s) [attempted 1715/8459 = 20%, 225 KB/s], Decompressed: 1613 Downloaded: 1754 file(s) [attempted 1754/8459 = 20%, 283 KB/s], Decompressed: 1613 Downloaded: 1802 file(s) [attempted 1802/8459 = 21%, 1109 KB/s], Decompressed: 1613 Downloaded: 1846 file(s) [attempted 1846/8459 = 21%, 571 KB/s], Decompressed: 1815 Downloaded: 1884 file(s) [attempted 1884/8459 = 22%, 726 KB/s], Decompressed: 1856 Downloaded: 1921 file(s) [attempted 1921/8459 = 22%, 789 KB/s], Decompressed: 1856 Downloaded: 1966 file(s) [attempted 1966/8459 = 23%, 967 KB/s], Decompressed: 1870 Downloaded: 2008 file(s) [attempted 2008/8459 = 23%, 138 KB/s], Decompressed: 2004 Downloaded: 2055 file(s) [attempted 2055/8459 = 24%, 47 KB/s], Decompressed: 2024 Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 1104 KB/s], Decompressed: 2024 Downloaded: 2140 file(s) [attempted 2140/8459 = 25%, 963 KB/s], Decompressed: 2034 Downloaded: 2182 file(s) [attempted 2182/8459 = 25%, 57 KB/s], Decompressed: 2116 Downloaded: 2223 file(s) [attempted 2223/8459 = 26%, 120 KB/s], Decompressed: 2116 Downloaded: 2266 file(s) [attempted 2266/8459 = 26%, 516 KB/s], Decompressed: 2260 Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 105 KB/s], Decompressed: 2298 Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 173 KB/s], Decompressed: 2339 Downloaded: 2387 file(s) [attempted 2387/8459 = 28%, 268 KB/s], Decompressed: 2346 Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 518 KB/s], Decompressed: 2346 Downloaded: 2472 file(s) [attempted 2472/8459 = 29%, 456 KB/s], Decompressed: 2353 Downloaded: 2513 file(s) [attempted 2513/8459 = 29%, 598 KB/s], Decompressed: 2353 Downloaded: 2555 file(s) [attempted 2555/8459 = 30%, 456 KB/s], Decompressed: 2438 Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 392 KB/s], Decompressed: 2537 Downloaded: 2637 file(s) [attempted 2637/8459 = 31%, 100 KB/s], Decompressed: 2537 Downloaded: 2681 file(s) [attempted 2681/8459 = 31%, 197 KB/s], Decompressed: 2565 Downloaded: 2722 file(s) [attempted 2722/8459 = 32%, 194 KB/s], Decompressed: 2565 Downloaded: 2767 file(s) [attempted 2767/8459 = 32%, 376 KB/s], Decompressed: 2756 Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 523 KB/s], Decompressed: 2794 Downloaded: 2852 file(s) [attempted 2852/8459 = 33%, 187 KB/s], Decompressed: 2845 Downloaded: 2900 file(s) [attempted 2900/8459 = 34%, 721 KB/s], Decompressed: 2897 Downloaded: 2939 file(s) [attempted 2939/8459 = 34%, 1081 KB/s], Decompressed: 2934 Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 24 KB/s], Decompressed: 2979 Downloaded: 3023 file(s) [attempted 3023/8459 = 35%, 126 KB/s], Decompressed: 2999 Downloaded: 3064 file(s) [attempted 3064/8459 = 36%, 196 KB/s], Decompressed: 3054 Downloaded: 3102 file(s) [attempted 3102/8459 = 36%, 102 KB/s], Decompressed: 3095 Downloaded: 3147 file(s) [attempted 3147/8459 = 37%, 53 KB/s], Decompressed: 3143 Downloaded: 3194 file(s) [attempted 3194/8459 = 37%, 313 KB/s], Decompressed: 3191 Downloaded: 3242 file(s) [attempted 3242/8459 = 38%, 294 KB/s], Decompressed: 3222 Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 107 KB/s], Decompressed: 3222 Downloaded: 3331 file(s) [attempted 3331/8459 = 39%, 182 KB/s], Decompressed: 3232 Downloaded: 3372 file(s) [attempted 3372/8459 = 39%, 44 KB/s], Decompressed: 3232 Downloaded: 3414 file(s) [attempted 3414/8459 = 40%, 212 KB/s], Decompressed: 3232 Downloaded: 3455 file(s) [attempted 3455/8459 = 40%, 500 KB/s], Decompressed: 3314 Downloaded: 3502 file(s) [attempted 3502/8459 = 41%, 864 KB/s], Decompressed: 3314 Downloaded: 3547 file(s) [attempted 3547/8459 = 41%, 203 KB/s], Decompressed: 3424 Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 82 KB/s], Decompressed: 3581 Downloaded: 3629 file(s) [attempted 3629/8459 = 42%, 670 KB/s], Decompressed: 3619 Downloaded: 3670 file(s) [attempted 3670/8459 = 43%, 560 KB/s], Decompressed: 3639 Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 66 KB/s], Decompressed: 3639 Downloaded: 3758 file(s) [attempted 3758/8459 = 44%, 898 KB/s], Decompressed: 3739 Downloaded: 3800 file(s) [attempted 3800/8459 = 44%, 317 KB/s], Decompressed: 3797 Downloaded: 3845 file(s) [attempted 3845/8459 = 45%, 470 KB/s], Decompressed: 3834 Downloaded: 3886 file(s) [attempted 3886/8459 = 45%, 149 KB/s], Decompressed: 3838 Downloaded: 3927 file(s) [attempted 3927/8459 = 46%, 163 KB/s], Decompressed: 3838 Downloaded: 3968 file(s) [attempted 3968/8459 = 46%, 107 KB/s], Decompressed: 3961 Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 337 KB/s], Decompressed: 4002 Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 688 KB/s], Decompressed: 4043 Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 154 KB/s], Decompressed: 4043 Downloaded: 4142 file(s) [attempted 4142/8459 = 48%, 201 KB/s], Decompressed: 4047 Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 197 KB/s], Decompressed: 4047 Downloaded: 4225 file(s) [attempted 4225/8459 = 49%, 294 KB/s], Decompressed: 4047 Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 247 KB/s], Decompressed: 4231 Downloaded: 4310 file(s) [attempted 4310/8459 = 50%, 246 KB/s], Decompressed: 4231 Downloaded: 4355 file(s) [attempted 4355/8459 = 51%, 1224 KB/s], Decompressed: 4259 Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 37 KB/s], Decompressed: 4392 Downloaded: 4433 file(s) [attempted 4433/8459 = 52%, 112 KB/s], Decompressed: 4427 Downloaded: 4474 file(s) [attempted 4474/8459 = 52%, 452 KB/s], Decompressed: 4471 Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 120 KB/s], Decompressed: 4471 Downloaded: 4563 file(s) [attempted 4563/8459 = 53%, 76 KB/s], Decompressed: 4474 Downloaded: 4608 file(s) [attempted 4608/8459 = 54%, 405 KB/s], Decompressed: 4584 Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 552 KB/s], Decompressed: 4584 Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 105 KB/s], Decompressed: 4591 Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 212 KB/s], Decompressed: 4591 Downloaded: 4772 file(s) [attempted 4772/8459 = 56%, 129 KB/s], Decompressed: 4673 Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 303 KB/s], Decompressed: 4806 Downloaded: 4861 file(s) [attempted 4861/8459 = 57%, 865 KB/s], Decompressed: 4858 Downloaded: 4907 file(s) [attempted 4907/8459 = 58%, 409 KB/s], Decompressed: 4902 Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 128 KB/s], Decompressed: 4943 Downloaded: 4986 file(s) [attempted 4986/8459 = 58%, 338 KB/s], Decompressed: 4954 Downloaded: 5029 file(s) [attempted 5029/8459 = 59%, 257 KB/s], Decompressed: 4984 Downloaded: 5077 file(s) [attempted 5077/8459 = 60%, 160 KB/s], Decompressed: 4984 Downloaded: 5118 file(s) [attempted 5118/8459 = 60%, 100 KB/s], Decompressed: 5108 Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 451 KB/s], Decompressed: 5108 Downloaded: 5210 file(s) [attempted 5210/8459 = 61%, 193 KB/s], Decompressed: 5114 Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 98 KB/s], Decompressed: 5114 Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 64 KB/s], Decompressed: 5114 Downloaded: 5340 file(s) [attempted 5340/8459 = 63%, 417 KB/s], Decompressed: 5327 Downloaded: 5385 file(s) [attempted 5385/8459 = 63%, 136 KB/s], Decompressed: 5381 Downloaded: 5426 file(s) [attempted 5426/8459 = 64%, 392 KB/s], Decompressed: 5422 Downloaded: 5470 file(s) [attempted 5470/8459 = 64%, 25 KB/s], Decompressed: 5422 Downloaded: 5511 file(s) [attempted 5511/8459 = 65%, 366 KB/s], Decompressed: 5426 Downloaded: 5556 file(s) [attempted 5556/8459 = 65%, 364 KB/s], Decompressed: 5552 Downloaded: 5600 file(s) [attempted 5600/8459 = 66%, 23 KB/s], Decompressed: 5594 Downloaded: 5641 file(s) [attempted 5641/8459 = 66%, 51 KB/s], Decompressed: 5635 Downloaded: 5684 file(s) [attempted 5684/8459 = 67%, 74 KB/s], Decompressed: 5676 Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 509 KB/s], Decompressed: 5713 Downloaded: 5771 file(s) [attempted 5771/8459 = 68%, 465 KB/s], Decompressed: 5713 Downloaded: 5811 file(s) [attempted 5811/8459 = 68%, 65 KB/s], Decompressed: 5720 Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 1061 KB/s], Decompressed: 5843 Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 351 KB/s], Decompressed: 5891 Downloaded: 5943 file(s) [attempted 5943/8459 = 70%, 708 KB/s], Decompressed: 5936 Downloaded: 5985 file(s) [attempted 5985/8459 = 70%, 1670 KB/s], Decompressed: 5980 Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 30 KB/s], Decompressed: 6014 Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 257 KB/s], Decompressed: 6066 Downloaded: 6110 file(s) [attempted 6110/8459 = 72%, 1047 KB/s], Decompressed: 6069 Downloaded: 6155 file(s) [attempted 6155/8459 = 72%, 47 KB/s], Decompressed: 6069 Downloaded: 6196 file(s) [attempted 6196/8459 = 73%, 83 KB/s], Decompressed: 6076 Downloaded: 6240 file(s) [attempted 6240/8459 = 73%, 693 KB/s], Decompressed: 6076 Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 181 KB/s], Decompressed: 6264 Downloaded: 6326 file(s) [attempted 6326/8459 = 74%, 397 KB/s], Decompressed: 6319 Downloaded: 6367 file(s) [attempted 6367/8459 = 75%, 754 KB/s], Decompressed: 6343 Downloaded: 6411 file(s) [attempted 6411/8459 = 75%, 227 KB/s], Decompressed: 6343 Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 324 KB/s], Decompressed: 6350 Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 1291 KB/s], Decompressed: 6350 Downloaded: 6541 file(s) [attempted 6541/8459 = 77%, 209 KB/s], Decompressed: 6442 Downloaded: 6584 file(s) [attempted 6584/8459 = 77%, 81 KB/s], Decompressed: 6442 Downloaded: 6620 file(s) [attempted 6620/8459 = 78%, 309 KB/s], Decompressed: 6442 Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 89 KB/s], Decompressed: 6637 Downloaded: 6709 file(s) [attempted 6709/8459 = 79%, 464 KB/s], Decompressed: 6637 Downloaded: 6754 file(s) [attempted 6754/8459 = 79%, 511 KB/s], Decompressed: 6654 Downloaded: 6792 file(s) [attempted 6792/8459 = 80%, 388 KB/s], Decompressed: 6654 Downloaded: 6836 file(s) [attempted 6836/8459 = 80%, 302 KB/s], Decompressed: 6654 Downloaded: 6880 file(s) [attempted 6880/8459 = 81%, 238 KB/s], Decompressed: 6747 Downloaded: 6921 file(s) [attempted 6921/8459 = 81%, 344 KB/s], Decompressed: 6747 Downloaded: 6962 file(s) [attempted 6962/8459 = 82%, 97 KB/s], Decompressed: 6949 Downloaded: 7006 file(s) [attempted 7006/8459 = 82%, 504 KB/s], Decompressed: 7000 Downloaded: 7051 file(s) [attempted 7051/8459 = 83%, 1944 KB/s], Decompressed: 7048 Downloaded: 7099 file(s) [attempted 7099/8459 = 83%, 140 KB/s], Decompressed: 7075 Downloaded: 7140 file(s) [attempted 7140/8459 = 84%, 112 KB/s], Decompressed: 7075 Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 153 KB/s], Decompressed: 7082 Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 340 KB/s], Decompressed: 7219 Downloaded: 7265 file(s) [attempted 7265/8459 = 85%, 757 KB/s], Decompressed: 7260 Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 45 KB/s], Decompressed: 7301 Downloaded: 7349 file(s) [attempted 7349/8459 = 86%, 50 KB/s], Decompressed: 7346 Downloaded: 7392 file(s) [attempted 7392/8459 = 87%, 478 KB/s], Decompressed: 7383 Downloaded: 7431 file(s) [attempted 7431/8459 = 87%, 167 KB/s], Decompressed: 7428 Downloaded: 7471 file(s) [attempted 7471/8459 = 88%, 305 KB/s], Decompressed: 7466 Downloaded: 7513 file(s) [attempted 7513/8459 = 88%, 214 KB/s], Decompressed: 7510 Downloaded: 7558 file(s) [attempted 7558/8459 = 89%, 246 KB/s], Decompressed: 7554 Downloaded: 7599 file(s) [attempted 7599/8459 = 89%, 1097 KB/s], Decompressed: 7578 Downloaded: 7643 file(s) [attempted 7643/8459 = 90%, 280 KB/s], Decompressed: 7578 Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 25 KB/s], Decompressed: 7585 Downloaded: 7726 file(s) [attempted 7726/8459 = 91%, 198 KB/s], Decompressed: 7585 Downloaded: 7763 file(s) [attempted 7763/8459 = 91%, 554 KB/s], Decompressed: 7667 Downloaded: 7811 file(s) [attempted 7811/8459 = 92%, 153 KB/s], Decompressed: 7667 Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 36 KB/s], Decompressed: 7763 Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 657 KB/s], Decompressed: 7763 Downloaded: 7955 file(s) [attempted 7955/8459 = 94%, 107 KB/s], Decompressed: 7763 Downloaded: 7999 file(s) [attempted 7999/8459 = 94%, 174 KB/s], Decompressed: 7859 Downloaded: 8047 file(s) [attempted 8047/8459 = 95%, 155 KB/s], Decompressed: 7859 Downloaded: 8095 file(s) [attempted 8095/8459 = 95%, 555 KB/s], Decompressed: 7962 Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 525 KB/s], Decompressed: 7962 Downloaded: 8177 file(s) [attempted 8177/8459 = 96%, 56 KB/s], Decompressed: 8153 Downloaded: 8222 file(s) [attempted 8222/8459 = 97%, 82 KB/s], Decompressed: 8194 Downloaded: 8266 file(s) [attempted 8266/8459 = 97%, 47 KB/s], Decompressed: 8194 Downloaded: 8307 file(s) [attempted 8307/8459 = 98%, 655 KB/s], Decompressed: 8297 Downloaded: 8348 file(s) [attempted 8348/8459 = 98%, 217 KB/s], Decompressed: 8345 Downloaded: 8395 file(s) [attempted 8395/8459 = 99%, 91 KB/s], Decompressed: 8389 Downloaded: 8437 file(s) [attempted 8437/8459 = 99%, 120 KB/s], Decompressed: 8431 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 120 KB/s], Decompressed: 8456
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (84s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.8s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.6s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.7s)
✔ [763/772] Built Iut.Foundations.QualitativeData (2.1s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.9s)
✔ [3388/3393] Built Iut.Stage1.CorollarySchema (104s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.2s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.8s)
✔ [3393/3401] Built Iut.Stage1.IUTStage1Data (3.5s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (98s)
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 (47s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (24s)
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 (15s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.8s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (10s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (9.3s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (30s)
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 (182s)
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`