Verification run
Run 1037
failed commit
debe0878e45d toolchain lean-v4-30-0 prover lean took 10m 48s · 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-1334-source
exit_code=Some(0) duration_ms=3278
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1334-source'...
$ git checkout debe0878e45d9c0b482c66aa4b555b57237dcbf5
exit_code=Some(0) duration_ms=146
stderr:
Note: switching to 'debe0878e45d9c0b482c66aa4b555b57237dcbf5'.
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 debe087 Lower norm square CTheta route
Resolved source revision: debe0878e45d9c0b482c66aa4b555b57237dcbf5
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=debe0878e45d9c0b482c66aa4b555b57237dcbf5 provenance={"branch":"master","checked_out_revision":"debe0878e45d9c0b482c66aa4b555b57237dcbf5","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"debe0878e45d9c0b482c66aa4b555b57237dcbf5","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=42169
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: 16 file(s) [attempted 16/8459 = 0%, 11 KB/s], Decompressed: 13
Downloaded: 42 file(s) [attempted 42/8459 = 0%, 80 KB/s], Decompressed: 35
Downloaded: 72 file(s) [attempted 72/8459 = 0%, 45 KB/s], Decompressed: 68
Downloaded: 98 file(s) [attempted 98/8459 = 1%, 94 KB/s], Decompressed: 93
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 60 KB/s], Decompressed: 127
Downloaded: 172 file(s) [attempted 172/8459 = 2%, 111 KB/s], Decompressed: 158
Downloaded: 203 file(s) [attempted 203/8459 = 2%, 316 KB/s], Decompressed: 199
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 568 KB/s], Decompressed: 230
Downloaded: 271 file(s) [attempted 271/8459 = 3%, 679 KB/s], Decompressed: 268
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 527 KB/s], Decompressed: 309
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 83 KB/s], Decompressed: 347
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 127 KB/s], Decompressed: 388
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 281 KB/s], Decompressed: 425
Downloaded: 470 file(s) [attempted 470/8459 = 5%, 269 KB/s], Decompressed: 463
Downloaded: 508 file(s) [attempted 508/8459 = 6%, 648 KB/s], Decompressed: 477
Downloaded: 549 file(s) [attempted 549/8459 = 6%, 315 KB/s], Decompressed: 545
Downloaded: 593 file(s) [attempted 593/8459 = 7%, 271 KB/s], Decompressed: 583
Downloaded: 640 file(s) [attempted 640/8459 = 7%, 260 KB/s], Decompressed: 631
Downloaded: 679 file(s) [attempted 679/8459 = 8%, 105 KB/s], Decompressed: 675
Downloaded: 723 file(s) [attempted 723/8459 = 8%, 241 KB/s], Decompressed: 713
Downloaded: 758 file(s) [attempted 758/8459 = 8%, 55 KB/s], Decompressed: 754
Downloaded: 799 file(s) [attempted 799/8459 = 9%, 770 KB/s], Decompressed: 792
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 222 KB/s], Decompressed: 826
Downloaded: 882 file(s) [attempted 882/8459 = 10%, 300 KB/s], Decompressed: 874
Downloaded: 919 file(s) [attempted 919/8459 = 10%, 583 KB/s], Decompressed: 915
Downloaded: 956 file(s) [attempted 956/8459 = 11%, 884 KB/s], Decompressed: 949
Downloaded: 999 file(s) [attempted 999/8459 = 11%, 313 KB/s], Decompressed: 991
Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 772 KB/s], Decompressed: 1032
Downloaded: 1086 file(s) [attempted 1086/8459 = 12%, 88 KB/s], Decompressed: 1085
Downloaded: 1127 file(s) [attempted 1127/8459 = 13%, 294 KB/s], Decompressed: 1124
Downloaded: 1165 file(s) [attempted 1165/8459 = 13%, 1780 KB/s], Decompressed: 1151
Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 1046 KB/s], Decompressed: 1203
Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 1138 KB/s], Decompressed: 1240
Downloaded: 1290 file(s) [attempted 1290/8459 = 15%, 179 KB/s], Decompressed: 1281
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 302 KB/s], Decompressed: 1323
Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 238 KB/s], Decompressed: 1364
Downloaded: 1412 file(s) [attempted 1412/8459 = 16%, 236 KB/s], Decompressed: 1398
Downloaded: 1449 file(s) [attempted 1449/8459 = 17%, 743 KB/s], Decompressed: 1442
Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 2154 KB/s], Decompressed: 1487
Downloaded: 1538 file(s) [attempted 1538/8459 = 18%, 495 KB/s], Decompressed: 1535
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 343 KB/s], Decompressed: 1572
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 868 KB/s], Decompressed: 1603
Downloaded: 1664 file(s) [attempted 1664/8459 = 19%, 153 KB/s], Decompressed: 1658
Downloaded: 1702 file(s) [attempted 1702/8459 = 20%, 131 KB/s], Decompressed: 1696
Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 92 KB/s], Decompressed: 1740
Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 75 KB/s], Decompressed: 1778
Downloaded: 1826 file(s) [attempted 1826/8459 = 21%, 267 KB/s], Decompressed: 1822
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 1505 KB/s], Decompressed: 1860
Downloaded: 1908 file(s) [attempted 1908/8459 = 22%, 343 KB/s], Decompressed: 1904
Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 836 KB/s], Decompressed: 1945
Downloaded: 1984 file(s) [attempted 1984/8459 = 23%, 80 KB/s], Decompressed: 1976
Downloaded: 2028 file(s) [attempted 2028/8459 = 23%, 520 KB/s], Decompressed: 2024
Downloaded: 2072 file(s) [attempted 2072/8459 = 24%, 40 KB/s], Decompressed: 2069
Downloaded: 2112 file(s) [attempted 2112/8459 = 24%, 371 KB/s], Decompressed: 2106
Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 175 KB/s], Decompressed: 2147
Downloaded: 2189 file(s) [attempted 2189/8459 = 25%, 438 KB/s], Decompressed: 2185
Downloaded: 2233 file(s) [attempted 2233/8459 = 26%, 114 KB/s], Decompressed: 2229
Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 369 KB/s], Decompressed: 2277
Downloaded: 2322 file(s) [attempted 2322/8459 = 27%, 84 KB/s], Decompressed: 2320
Downloaded: 2363 file(s) [attempted 2363/8459 = 27%, 149 KB/s], Decompressed: 2353
Downloaded: 2404 file(s) [attempted 2404/8459 = 28%, 472 KB/s], Decompressed: 2401
Downloaded: 2442 file(s) [attempted 2442/8459 = 28%, 268 KB/s], Decompressed: 2438
Downloaded: 2480 file(s) [attempted 2480/8459 = 29%, 31 KB/s], Decompressed: 2476
Downloaded: 2524 file(s) [attempted 2524/8459 = 29%, 260 KB/s], Decompressed: 2520
Downloaded: 2570 file(s) [attempted 2570/8459 = 30%, 454 KB/s], Decompressed: 2558
Downloaded: 2603 file(s) [attempted 2603/8459 = 30%, 626 KB/s], Decompressed: 2599
Downloaded: 2640 file(s) [attempted 2640/8459 = 31%, 765 KB/s], Decompressed: 2635
Downloaded: 2688 file(s) [attempted 2688/8459 = 31%, 181 KB/s], Decompressed: 2681
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 168 KB/s], Decompressed: 2722
Downloaded: 2770 file(s) [attempted 2770/8459 = 32%, 256 KB/s], Decompressed: 2760
Downloaded: 2808 file(s) [attempted 2808/8459 = 33%, 107 KB/s], Decompressed: 2804
Downloaded: 2852 file(s) [attempted 2852/8459 = 33%, 133 KB/s], Decompressed: 2845
Downloaded: 2897 file(s) [attempted 2897/8459 = 34%, 82 KB/s], Decompressed: 2890
Downloaded: 2938 file(s) [attempted 2938/8459 = 34%, 273 KB/s], Decompressed: 2907
Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 24 KB/s], Decompressed: 2976
Downloaded: 3022 file(s) [attempted 3022/8459 = 35%, 144 KB/s], Decompressed: 3013
Downloaded: 3054 file(s) [attempted 3054/8459 = 36%, 408 KB/s], Decompressed: 3051
Downloaded: 3099 file(s) [attempted 3099/8459 = 36%, 503 KB/s], Decompressed: 3096
Downloaded: 3147 file(s) [attempted 3147/8459 = 37%, 100 KB/s], Decompressed: 3143
Downloaded: 3193 file(s) [attempted 3193/8459 = 37%, 443 KB/s], Decompressed: 3190
Downloaded: 3233 file(s) [attempted 3233/8459 = 38%, 116 KB/s], Decompressed: 3225
Downloaded: 3270 file(s) [attempted 3270/8459 = 38%, 186 KB/s], Decompressed: 3249
Downloaded: 3311 file(s) [attempted 3311/8459 = 39%, 700 KB/s], Decompressed: 3280
Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 52 KB/s], Decompressed: 3352
Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 1164 KB/s], Decompressed: 3390
Downloaded: 3438 file(s) [attempted 3438/8459 = 40%, 894 KB/s], Decompressed: 3427
Downloaded: 3474 file(s) [attempted 3474/8459 = 41%, 852 KB/s], Decompressed: 3465
Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 587 KB/s], Decompressed: 3503
Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 201 KB/s], Decompressed: 3550
Downloaded: 3598 file(s) [attempted 3598/8459 = 42%, 190 KB/s], Decompressed: 3595
Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 124 KB/s], Decompressed: 3630
Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 78 KB/s], Decompressed: 3667
Downloaded: 3718 file(s) [attempted 3718/8459 = 43%, 88 KB/s], Decompressed: 3708
Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 675 KB/s], Decompressed: 3756
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 450 KB/s], Decompressed: 3804
Downloaded: 3852 file(s) [attempted 3852/8459 = 45%, 106 KB/s], Decompressed: 3848
Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 592 KB/s], Decompressed: 3869
Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 96 KB/s], Decompressed: 3927
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 312 KB/s], Decompressed: 3958
Downloaded: 4016 file(s) [attempted 4016/8459 = 47%, 47 KB/s], Decompressed: 4009
Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 2073 KB/s], Decompressed: 4054
Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 748 KB/s], Decompressed: 4057
Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 178 KB/s], Decompressed: 4057
Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 112 KB/s], Decompressed: 4149
Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 393 KB/s], Decompressed: 4214
Downloaded: 4262 file(s) [attempted 4262/8459 = 50%, 254 KB/s], Decompressed: 4252
Downloaded: 4299 file(s) [attempted 4299/8459 = 50%, 115 KB/s], Decompressed: 4293
Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 209 KB/s], Decompressed: 4334
Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 194 KB/s], Decompressed: 4379
Downloaded: 4427 file(s) [attempted 4427/8459 = 52%, 549 KB/s], Decompressed: 4416
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 621 KB/s], Decompressed: 4461
Downloaded: 4506 file(s) [attempted 4506/8459 = 53%, 440 KB/s], Decompressed: 4502
Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 1291 KB/s], Decompressed: 4543
Downloaded: 4587 file(s) [attempted 4587/8459 = 54%, 608 KB/s], Decompressed: 4584
Downloaded: 4626 file(s) [attempted 4626/8459 = 54%, 1112 KB/s], Decompressed: 4618
Downloaded: 4670 file(s) [attempted 4670/8459 = 55%, 410 KB/s], Decompressed: 4666
Downloaded: 4711 file(s) [attempted 4711/8459 = 55%, 159 KB/s], Decompressed: 4707
Downloaded: 4753 file(s) [attempted 4753/8459 = 56%, 171 KB/s], Decompressed: 4748
Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 369 KB/s], Decompressed: 4789
Downloaded: 4831 file(s) [attempted 4831/8459 = 57%, 53 KB/s], Decompressed: 4827
Downloaded: 4871 file(s) [attempted 4871/8459 = 57%, 89 KB/s], Decompressed: 4868
Downloaded: 4913 file(s) [attempted 4913/8459 = 58%, 277 KB/s], Decompressed: 4909
Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 199 KB/s], Decompressed: 4954
Downloaded: 4998 file(s) [attempted 4998/8459 = 59%, 267 KB/s], Decompressed: 4995
Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 275 KB/s], Decompressed: 5036
Downloaded: 5087 file(s) [attempted 5087/8459 = 60%, 99 KB/s], Decompressed: 5080
Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 46 KB/s], Decompressed: 5121
Downloaded: 5166 file(s) [attempted 5166/8459 = 61%, 502 KB/s], Decompressed: 5162
Downloaded: 5210 file(s) [attempted 5210/8459 = 61%, 49 KB/s], Decompressed: 5207
Downloaded: 5248 file(s) [attempted 5248/8459 = 62%, 441 KB/s], Decompressed: 5241
Downloaded: 5289 file(s) [attempted 5289/8459 = 62%, 151 KB/s], Decompressed: 5286
Downloaded: 5334 file(s) [attempted 5334/8459 = 63%, 417 KB/s], Decompressed: 5323
Downloaded: 5371 file(s) [attempted 5371/8459 = 63%, 1126 KB/s], Decompressed: 5347
Downloaded: 5416 file(s) [attempted 5416/8459 = 64%, 324 KB/s], Decompressed: 5409
Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 172 KB/s], Decompressed: 5450
Downloaded: 5499 file(s) [attempted 5499/8459 = 65%, 70 KB/s], Decompressed: 5491
Downloaded: 5537 file(s) [attempted 5537/8459 = 65%, 170 KB/s], Decompressed: 5529
Downloaded: 5576 file(s) [attempted 5576/8459 = 65%, 1464 KB/s], Decompressed: 5573
Downloaded: 5624 file(s) [attempted 5624/8459 = 66%, 539 KB/s], Decompressed: 5618
Downloaded: 5665 file(s) [attempted 5665/8459 = 66%, 147 KB/s], Decompressed: 5659
Downloaded: 5707 file(s) [attempted 5707/8459 = 67%, 184 KB/s], Decompressed: 5696
Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 254 KB/s], Decompressed: 5737
Downloaded: 5782 file(s) [attempted 5782/8459 = 68%, 117 KB/s], Decompressed: 5778
Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 390 KB/s], Decompressed: 5819
Downloaded: 5874 file(s) [attempted 5874/8459 = 69%, 157 KB/s], Decompressed: 5867
Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 334 KB/s], Decompressed: 5915
Downloaded: 5963 file(s) [attempted 5963/8459 = 70%, 965 KB/s], Decompressed: 5956
Downloaded: 6001 file(s) [attempted 6001/8459 = 70%, 1120 KB/s], Decompressed: 5991
Downloaded: 6039 file(s) [attempted 6039/8459 = 71%, 496 KB/s], Decompressed: 6032
Downloaded: 6082 file(s) [attempted 6082/8459 = 71%, 230 KB/s], Decompressed: 6073
Downloaded: 6121 file(s) [attempted 6121/8459 = 72%, 191 KB/s], Decompressed: 6114
Downloaded: 6165 file(s) [attempted 6165/8459 = 72%, 206 KB/s], Decompressed: 6158
Downloaded: 6206 file(s) [attempted 6206/8459 = 73%, 43 KB/s], Decompressed: 6199
Downloaded: 6247 file(s) [attempted 6247/8459 = 73%, 32 KB/s], Decompressed: 6240
Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 54 KB/s], Decompressed: 6275
Downloaded: 6329 file(s) [attempted 6329/8459 = 74%, 114 KB/s], Decompressed: 6326
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 495 KB/s], Decompressed: 6370
Downloaded: 6416 file(s) [attempted 6416/8459 = 75%, 51 KB/s], Decompressed: 6412
Downloaded: 6459 file(s) [attempted 6459/8459 = 76%, 648 KB/s], Decompressed: 6456
Downloaded: 6504 file(s) [attempted 6504/8459 = 76%, 434 KB/s], Decompressed: 6497
Downloaded: 6539 file(s) [attempted 6539/8459 = 77%, 211 KB/s], Decompressed: 6531
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 364 KB/s], Decompressed: 6576
Downloaded: 6620 file(s) [attempted 6620/8459 = 78%, 290 KB/s], Decompressed: 6617
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 208 KB/s], Decompressed: 6658
Downloaded: 6706 file(s) [attempted 6706/8459 = 79%, 80 KB/s], Decompressed: 6702
Downloaded: 6747 file(s) [attempted 6747/8459 = 79%, 715 KB/s], Decompressed: 6740
Downloaded: 6785 file(s) [attempted 6785/8459 = 80%, 79 KB/s], Decompressed: 6778
Downloaded: 6829 file(s) [attempted 6829/8459 = 80%, 332 KB/s], Decompressed: 6798
Downloaded: 6870 file(s) [attempted 6870/8459 = 81%, 222 KB/s], Decompressed: 6863
Downloaded: 6918 file(s) [attempted 6918/8459 = 81%, 34 KB/s], Decompressed: 6911
Downloaded: 6966 file(s) [attempted 6966/8459 = 82%, 198 KB/s], Decompressed: 6959
Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 166 KB/s], Decompressed: 7000
Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 23 KB/s], Decompressed: 7028
Downloaded: 7082 file(s) [attempted 7082/8459 = 83%, 43 KB/s], Decompressed: 7075
Downloaded: 7127 file(s) [attempted 7127/8459 = 84%, 32 KB/s], Decompressed: 7123
Downloaded: 7175 file(s) [attempted 7175/8459 = 84%, 317 KB/s], Decompressed: 7171
Downloaded: 7224 file(s) [attempted 7224/8459 = 85%, 460 KB/s], Decompressed: 7216
Downloaded: 7264 file(s) [attempted 7264/8459 = 85%, 129 KB/s], Decompressed: 7260
Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 2135 KB/s], Decompressed: 7291
Downloaded: 7341 file(s) [attempted 7341/8459 = 86%, 599 KB/s], Decompressed: 7332
Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 197 KB/s], Decompressed: 7377
Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 241 KB/s], Decompressed: 7418
Downloaded: 7464 file(s) [attempted 7464/8459 = 88%, 380 KB/s], Decompressed: 7455
Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 451 KB/s], Decompressed: 7486
Downloaded: 7536 file(s) [attempted 7536/8459 = 89%, 172 KB/s], Decompressed: 7527
Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 915 KB/s], Decompressed: 7565
Downloaded: 7616 file(s) [attempted 7616/8459 = 90%, 33 KB/s], Decompressed: 7613
Downloaded: 7664 file(s) [attempted 7664/8459 = 90%, 133 KB/s], Decompressed: 7657
Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 199 KB/s], Decompressed: 7698
Downloaded: 7753 file(s) [attempted 7753/8459 = 91%, 223 KB/s], Decompressed: 7746
Downloaded: 7794 file(s) [attempted 7794/8459 = 92%, 51 KB/s], Decompressed: 7787
Downloaded: 7832 file(s) [attempted 7832/8459 = 92%, 450 KB/s], Decompressed: 7825
Downloaded: 7873 file(s) [attempted 7873/8459 = 93%, 92 KB/s], Decompressed: 7866
Downloaded: 7910 file(s) [attempted 7910/8459 = 93%, 56 KB/s], Decompressed: 7908
Downloaded: 7953 file(s) [attempted 7953/8459 = 94%, 306 KB/s], Decompressed: 7948
Downloaded: 7996 file(s) [attempted 7996/8459 = 94%, 303 KB/s], Decompressed: 7993
Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 108 KB/s], Decompressed: 8027
Downloaded: 8072 file(s) [attempted 8072/8459 = 95%, 306 KB/s], Decompressed: 8068
Downloaded: 8109 file(s) [attempted 8109/8459 = 95%, 94 KB/s], Decompressed: 8106
Downloaded: 8157 file(s) [attempted 8157/8459 = 96%, 121 KB/s], Decompressed: 8153
Downloaded: 8205 file(s) [attempted 8205/8459 = 96%, 421 KB/s], Decompressed: 8198
Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 409 KB/s], Decompressed: 8236
Downloaded: 8283 file(s) [attempted 8283/8459 = 97%, 130 KB/s], Decompressed: 8260
Downloaded: 8321 file(s) [attempted 8321/8459 = 98%, 306 KB/s], Decompressed: 8314
Downloaded: 8362 file(s) [attempted 8362/8459 = 98%, 238 KB/s], Decompressed: 8359
Downloaded: 8403 file(s) [attempted 8403/8459 = 99%, 119 KB/s], Decompressed: 8400
Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 189 KB/s], Decompressed: 8441
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 189 KB/s], Decompressed: 8455
$ lake build
exit_code=Some(1) duration_ms=414859
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (11s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.7s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/779] Built Iut.Foundations.QualitativeData (2.2s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.7s)
✔ [3388/3393] Built Iut.Stage1.CorollarySchema (35s)
✔ [3390/3393] Built Iut.Stage1.SourceObligations (3.5s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.8s)
✔ [3393/3407] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (80s)
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 (13s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (15s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.0s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.3s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.9s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (23s)
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 (153s)
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=1372
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-1334-source
Cloning into '/var/lib/apodeixis/repos/job-1334-source'...
git_checkout exit 0
git checkout debe0878e45d9c0b482c66aa4b555b57237dcbf5
Note: switching to 'debe0878e45d9c0b482c66aa4b555b57237dcbf5'. 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 debe087 Lower norm square 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: 16 file(s) [attempted 16/8459 = 0%, 11 KB/s], Decompressed: 13 Downloaded: 42 file(s) [attempted 42/8459 = 0%, 80 KB/s], Decompressed: 35 Downloaded: 72 file(s) [attempted 72/8459 = 0%, 45 KB/s], Decompressed: 68 Downloaded: 98 file(s) [attempted 98/8459 = 1%, 94 KB/s], Decompressed: 93 Downloaded: 134 file(s) [attempted 134/8459 = 1%, 60 KB/s], Decompressed: 127 Downloaded: 172 file(s) [attempted 172/8459 = 2%, 111 KB/s], Decompressed: 158 Downloaded: 203 file(s) [attempted 203/8459 = 2%, 316 KB/s], Decompressed: 199 Downloaded: 234 file(s) [attempted 234/8459 = 2%, 568 KB/s], Decompressed: 230 Downloaded: 271 file(s) [attempted 271/8459 = 3%, 679 KB/s], Decompressed: 268 Downloaded: 312 file(s) [attempted 312/8459 = 3%, 527 KB/s], Decompressed: 309 Downloaded: 353 file(s) [attempted 353/8459 = 4%, 83 KB/s], Decompressed: 347 Downloaded: 391 file(s) [attempted 391/8459 = 4%, 127 KB/s], Decompressed: 388 Downloaded: 432 file(s) [attempted 432/8459 = 5%, 281 KB/s], Decompressed: 425 Downloaded: 470 file(s) [attempted 470/8459 = 5%, 269 KB/s], Decompressed: 463 Downloaded: 508 file(s) [attempted 508/8459 = 6%, 648 KB/s], Decompressed: 477 Downloaded: 549 file(s) [attempted 549/8459 = 6%, 315 KB/s], Decompressed: 545 Downloaded: 593 file(s) [attempted 593/8459 = 7%, 271 KB/s], Decompressed: 583 Downloaded: 640 file(s) [attempted 640/8459 = 7%, 260 KB/s], Decompressed: 631 Downloaded: 679 file(s) [attempted 679/8459 = 8%, 105 KB/s], Decompressed: 675 Downloaded: 723 file(s) [attempted 723/8459 = 8%, 241 KB/s], Decompressed: 713 Downloaded: 758 file(s) [attempted 758/8459 = 8%, 55 KB/s], Decompressed: 754 Downloaded: 799 file(s) [attempted 799/8459 = 9%, 770 KB/s], Decompressed: 792 Downloaded: 836 file(s) [attempted 836/8459 = 9%, 222 KB/s], Decompressed: 826 Downloaded: 882 file(s) [attempted 882/8459 = 10%, 300 KB/s], Decompressed: 874 Downloaded: 919 file(s) [attempted 919/8459 = 10%, 583 KB/s], Decompressed: 915 Downloaded: 956 file(s) [attempted 956/8459 = 11%, 884 KB/s], Decompressed: 949 Downloaded: 999 file(s) [attempted 999/8459 = 11%, 313 KB/s], Decompressed: 991 Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 772 KB/s], Decompressed: 1032 Downloaded: 1086 file(s) [attempted 1086/8459 = 12%, 88 KB/s], Decompressed: 1085 Downloaded: 1127 file(s) [attempted 1127/8459 = 13%, 294 KB/s], Decompressed: 1124 Downloaded: 1165 file(s) [attempted 1165/8459 = 13%, 1780 KB/s], Decompressed: 1151 Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 1046 KB/s], Decompressed: 1203 Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 1138 KB/s], Decompressed: 1240 Downloaded: 1290 file(s) [attempted 1290/8459 = 15%, 179 KB/s], Decompressed: 1281 Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 302 KB/s], Decompressed: 1323 Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 238 KB/s], Decompressed: 1364 Downloaded: 1412 file(s) [attempted 1412/8459 = 16%, 236 KB/s], Decompressed: 1398 Downloaded: 1449 file(s) [attempted 1449/8459 = 17%, 743 KB/s], Decompressed: 1442 Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 2154 KB/s], Decompressed: 1487 Downloaded: 1538 file(s) [attempted 1538/8459 = 18%, 495 KB/s], Decompressed: 1535 Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 343 KB/s], Decompressed: 1572 Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 868 KB/s], Decompressed: 1603 Downloaded: 1664 file(s) [attempted 1664/8459 = 19%, 153 KB/s], Decompressed: 1658 Downloaded: 1702 file(s) [attempted 1702/8459 = 20%, 131 KB/s], Decompressed: 1696 Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 92 KB/s], Decompressed: 1740 Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 75 KB/s], Decompressed: 1778 Downloaded: 1826 file(s) [attempted 1826/8459 = 21%, 267 KB/s], Decompressed: 1822 Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 1505 KB/s], Decompressed: 1860 Downloaded: 1908 file(s) [attempted 1908/8459 = 22%, 343 KB/s], Decompressed: 1904 Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 836 KB/s], Decompressed: 1945 Downloaded: 1984 file(s) [attempted 1984/8459 = 23%, 80 KB/s], Decompressed: 1976 Downloaded: 2028 file(s) [attempted 2028/8459 = 23%, 520 KB/s], Decompressed: 2024 Downloaded: 2072 file(s) [attempted 2072/8459 = 24%, 40 KB/s], Decompressed: 2069 Downloaded: 2112 file(s) [attempted 2112/8459 = 24%, 371 KB/s], Decompressed: 2106 Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 175 KB/s], Decompressed: 2147 Downloaded: 2189 file(s) [attempted 2189/8459 = 25%, 438 KB/s], Decompressed: 2185 Downloaded: 2233 file(s) [attempted 2233/8459 = 26%, 114 KB/s], Decompressed: 2229 Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 369 KB/s], Decompressed: 2277 Downloaded: 2322 file(s) [attempted 2322/8459 = 27%, 84 KB/s], Decompressed: 2320 Downloaded: 2363 file(s) [attempted 2363/8459 = 27%, 149 KB/s], Decompressed: 2353 Downloaded: 2404 file(s) [attempted 2404/8459 = 28%, 472 KB/s], Decompressed: 2401 Downloaded: 2442 file(s) [attempted 2442/8459 = 28%, 268 KB/s], Decompressed: 2438 Downloaded: 2480 file(s) [attempted 2480/8459 = 29%, 31 KB/s], Decompressed: 2476 Downloaded: 2524 file(s) [attempted 2524/8459 = 29%, 260 KB/s], Decompressed: 2520 Downloaded: 2570 file(s) [attempted 2570/8459 = 30%, 454 KB/s], Decompressed: 2558 Downloaded: 2603 file(s) [attempted 2603/8459 = 30%, 626 KB/s], Decompressed: 2599 Downloaded: 2640 file(s) [attempted 2640/8459 = 31%, 765 KB/s], Decompressed: 2635 Downloaded: 2688 file(s) [attempted 2688/8459 = 31%, 181 KB/s], Decompressed: 2681 Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 168 KB/s], Decompressed: 2722 Downloaded: 2770 file(s) [attempted 2770/8459 = 32%, 256 KB/s], Decompressed: 2760 Downloaded: 2808 file(s) [attempted 2808/8459 = 33%, 107 KB/s], Decompressed: 2804 Downloaded: 2852 file(s) [attempted 2852/8459 = 33%, 133 KB/s], Decompressed: 2845 Downloaded: 2897 file(s) [attempted 2897/8459 = 34%, 82 KB/s], Decompressed: 2890 Downloaded: 2938 file(s) [attempted 2938/8459 = 34%, 273 KB/s], Decompressed: 2907 Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 24 KB/s], Decompressed: 2976 Downloaded: 3022 file(s) [attempted 3022/8459 = 35%, 144 KB/s], Decompressed: 3013 Downloaded: 3054 file(s) [attempted 3054/8459 = 36%, 408 KB/s], Decompressed: 3051 Downloaded: 3099 file(s) [attempted 3099/8459 = 36%, 503 KB/s], Decompressed: 3096 Downloaded: 3147 file(s) [attempted 3147/8459 = 37%, 100 KB/s], Decompressed: 3143 Downloaded: 3193 file(s) [attempted 3193/8459 = 37%, 443 KB/s], Decompressed: 3190 Downloaded: 3233 file(s) [attempted 3233/8459 = 38%, 116 KB/s], Decompressed: 3225 Downloaded: 3270 file(s) [attempted 3270/8459 = 38%, 186 KB/s], Decompressed: 3249 Downloaded: 3311 file(s) [attempted 3311/8459 = 39%, 700 KB/s], Decompressed: 3280 Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 52 KB/s], Decompressed: 3352 Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 1164 KB/s], Decompressed: 3390 Downloaded: 3438 file(s) [attempted 3438/8459 = 40%, 894 KB/s], Decompressed: 3427 Downloaded: 3474 file(s) [attempted 3474/8459 = 41%, 852 KB/s], Decompressed: 3465 Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 587 KB/s], Decompressed: 3503 Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 201 KB/s], Decompressed: 3550 Downloaded: 3598 file(s) [attempted 3598/8459 = 42%, 190 KB/s], Decompressed: 3595 Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 124 KB/s], Decompressed: 3630 Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 78 KB/s], Decompressed: 3667 Downloaded: 3718 file(s) [attempted 3718/8459 = 43%, 88 KB/s], Decompressed: 3708 Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 675 KB/s], Decompressed: 3756 Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 450 KB/s], Decompressed: 3804 Downloaded: 3852 file(s) [attempted 3852/8459 = 45%, 106 KB/s], Decompressed: 3848 Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 592 KB/s], Decompressed: 3869 Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 96 KB/s], Decompressed: 3927 Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 312 KB/s], Decompressed: 3958 Downloaded: 4016 file(s) [attempted 4016/8459 = 47%, 47 KB/s], Decompressed: 4009 Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 2073 KB/s], Decompressed: 4054 Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 748 KB/s], Decompressed: 4057 Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 178 KB/s], Decompressed: 4057 Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 112 KB/s], Decompressed: 4149 Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 393 KB/s], Decompressed: 4214 Downloaded: 4262 file(s) [attempted 4262/8459 = 50%, 254 KB/s], Decompressed: 4252 Downloaded: 4299 file(s) [attempted 4299/8459 = 50%, 115 KB/s], Decompressed: 4293 Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 209 KB/s], Decompressed: 4334 Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 194 KB/s], Decompressed: 4379 Downloaded: 4427 file(s) [attempted 4427/8459 = 52%, 549 KB/s], Decompressed: 4416 Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 621 KB/s], Decompressed: 4461 Downloaded: 4506 file(s) [attempted 4506/8459 = 53%, 440 KB/s], Decompressed: 4502 Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 1291 KB/s], Decompressed: 4543 Downloaded: 4587 file(s) [attempted 4587/8459 = 54%, 608 KB/s], Decompressed: 4584 Downloaded: 4626 file(s) [attempted 4626/8459 = 54%, 1112 KB/s], Decompressed: 4618 Downloaded: 4670 file(s) [attempted 4670/8459 = 55%, 410 KB/s], Decompressed: 4666 Downloaded: 4711 file(s) [attempted 4711/8459 = 55%, 159 KB/s], Decompressed: 4707 Downloaded: 4753 file(s) [attempted 4753/8459 = 56%, 171 KB/s], Decompressed: 4748 Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 369 KB/s], Decompressed: 4789 Downloaded: 4831 file(s) [attempted 4831/8459 = 57%, 53 KB/s], Decompressed: 4827 Downloaded: 4871 file(s) [attempted 4871/8459 = 57%, 89 KB/s], Decompressed: 4868 Downloaded: 4913 file(s) [attempted 4913/8459 = 58%, 277 KB/s], Decompressed: 4909 Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 199 KB/s], Decompressed: 4954 Downloaded: 4998 file(s) [attempted 4998/8459 = 59%, 267 KB/s], Decompressed: 4995 Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 275 KB/s], Decompressed: 5036 Downloaded: 5087 file(s) [attempted 5087/8459 = 60%, 99 KB/s], Decompressed: 5080 Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 46 KB/s], Decompressed: 5121 Downloaded: 5166 file(s) [attempted 5166/8459 = 61%, 502 KB/s], Decompressed: 5162 Downloaded: 5210 file(s) [attempted 5210/8459 = 61%, 49 KB/s], Decompressed: 5207 Downloaded: 5248 file(s) [attempted 5248/8459 = 62%, 441 KB/s], Decompressed: 5241 Downloaded: 5289 file(s) [attempted 5289/8459 = 62%, 151 KB/s], Decompressed: 5286 Downloaded: 5334 file(s) [attempted 5334/8459 = 63%, 417 KB/s], Decompressed: 5323 Downloaded: 5371 file(s) [attempted 5371/8459 = 63%, 1126 KB/s], Decompressed: 5347 Downloaded: 5416 file(s) [attempted 5416/8459 = 64%, 324 KB/s], Decompressed: 5409 Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 172 KB/s], Decompressed: 5450 Downloaded: 5499 file(s) [attempted 5499/8459 = 65%, 70 KB/s], Decompressed: 5491 Downloaded: 5537 file(s) [attempted 5537/8459 = 65%, 170 KB/s], Decompressed: 5529 Downloaded: 5576 file(s) [attempted 5576/8459 = 65%, 1464 KB/s], Decompressed: 5573 Downloaded: 5624 file(s) [attempted 5624/8459 = 66%, 539 KB/s], Decompressed: 5618 Downloaded: 5665 file(s) [attempted 5665/8459 = 66%, 147 KB/s], Decompressed: 5659 Downloaded: 5707 file(s) [attempted 5707/8459 = 67%, 184 KB/s], Decompressed: 5696 Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 254 KB/s], Decompressed: 5737 Downloaded: 5782 file(s) [attempted 5782/8459 = 68%, 117 KB/s], Decompressed: 5778 Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 390 KB/s], Decompressed: 5819 Downloaded: 5874 file(s) [attempted 5874/8459 = 69%, 157 KB/s], Decompressed: 5867 Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 334 KB/s], Decompressed: 5915 Downloaded: 5963 file(s) [attempted 5963/8459 = 70%, 965 KB/s], Decompressed: 5956 Downloaded: 6001 file(s) [attempted 6001/8459 = 70%, 1120 KB/s], Decompressed: 5991 Downloaded: 6039 file(s) [attempted 6039/8459 = 71%, 496 KB/s], Decompressed: 6032 Downloaded: 6082 file(s) [attempted 6082/8459 = 71%, 230 KB/s], Decompressed: 6073 Downloaded: 6121 file(s) [attempted 6121/8459 = 72%, 191 KB/s], Decompressed: 6114 Downloaded: 6165 file(s) [attempted 6165/8459 = 72%, 206 KB/s], Decompressed: 6158 Downloaded: 6206 file(s) [attempted 6206/8459 = 73%, 43 KB/s], Decompressed: 6199 Downloaded: 6247 file(s) [attempted 6247/8459 = 73%, 32 KB/s], Decompressed: 6240 Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 54 KB/s], Decompressed: 6275 Downloaded: 6329 file(s) [attempted 6329/8459 = 74%, 114 KB/s], Decompressed: 6326 Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 495 KB/s], Decompressed: 6370 Downloaded: 6416 file(s) [attempted 6416/8459 = 75%, 51 KB/s], Decompressed: 6412 Downloaded: 6459 file(s) [attempted 6459/8459 = 76%, 648 KB/s], Decompressed: 6456 Downloaded: 6504 file(s) [attempted 6504/8459 = 76%, 434 KB/s], Decompressed: 6497 Downloaded: 6539 file(s) [attempted 6539/8459 = 77%, 211 KB/s], Decompressed: 6531 Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 364 KB/s], Decompressed: 6576 Downloaded: 6620 file(s) [attempted 6620/8459 = 78%, 290 KB/s], Decompressed: 6617 Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 208 KB/s], Decompressed: 6658 Downloaded: 6706 file(s) [attempted 6706/8459 = 79%, 80 KB/s], Decompressed: 6702 Downloaded: 6747 file(s) [attempted 6747/8459 = 79%, 715 KB/s], Decompressed: 6740 Downloaded: 6785 file(s) [attempted 6785/8459 = 80%, 79 KB/s], Decompressed: 6778 Downloaded: 6829 file(s) [attempted 6829/8459 = 80%, 332 KB/s], Decompressed: 6798 Downloaded: 6870 file(s) [attempted 6870/8459 = 81%, 222 KB/s], Decompressed: 6863 Downloaded: 6918 file(s) [attempted 6918/8459 = 81%, 34 KB/s], Decompressed: 6911 Downloaded: 6966 file(s) [attempted 6966/8459 = 82%, 198 KB/s], Decompressed: 6959 Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 166 KB/s], Decompressed: 7000 Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 23 KB/s], Decompressed: 7028 Downloaded: 7082 file(s) [attempted 7082/8459 = 83%, 43 KB/s], Decompressed: 7075 Downloaded: 7127 file(s) [attempted 7127/8459 = 84%, 32 KB/s], Decompressed: 7123 Downloaded: 7175 file(s) [attempted 7175/8459 = 84%, 317 KB/s], Decompressed: 7171 Downloaded: 7224 file(s) [attempted 7224/8459 = 85%, 460 KB/s], Decompressed: 7216 Downloaded: 7264 file(s) [attempted 7264/8459 = 85%, 129 KB/s], Decompressed: 7260 Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 2135 KB/s], Decompressed: 7291 Downloaded: 7341 file(s) [attempted 7341/8459 = 86%, 599 KB/s], Decompressed: 7332 Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 197 KB/s], Decompressed: 7377 Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 241 KB/s], Decompressed: 7418 Downloaded: 7464 file(s) [attempted 7464/8459 = 88%, 380 KB/s], Decompressed: 7455 Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 451 KB/s], Decompressed: 7486 Downloaded: 7536 file(s) [attempted 7536/8459 = 89%, 172 KB/s], Decompressed: 7527 Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 915 KB/s], Decompressed: 7565 Downloaded: 7616 file(s) [attempted 7616/8459 = 90%, 33 KB/s], Decompressed: 7613 Downloaded: 7664 file(s) [attempted 7664/8459 = 90%, 133 KB/s], Decompressed: 7657 Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 199 KB/s], Decompressed: 7698 Downloaded: 7753 file(s) [attempted 7753/8459 = 91%, 223 KB/s], Decompressed: 7746 Downloaded: 7794 file(s) [attempted 7794/8459 = 92%, 51 KB/s], Decompressed: 7787 Downloaded: 7832 file(s) [attempted 7832/8459 = 92%, 450 KB/s], Decompressed: 7825 Downloaded: 7873 file(s) [attempted 7873/8459 = 93%, 92 KB/s], Decompressed: 7866 Downloaded: 7910 file(s) [attempted 7910/8459 = 93%, 56 KB/s], Decompressed: 7908 Downloaded: 7953 file(s) [attempted 7953/8459 = 94%, 306 KB/s], Decompressed: 7948 Downloaded: 7996 file(s) [attempted 7996/8459 = 94%, 303 KB/s], Decompressed: 7993 Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 108 KB/s], Decompressed: 8027 Downloaded: 8072 file(s) [attempted 8072/8459 = 95%, 306 KB/s], Decompressed: 8068 Downloaded: 8109 file(s) [attempted 8109/8459 = 95%, 94 KB/s], Decompressed: 8106 Downloaded: 8157 file(s) [attempted 8157/8459 = 96%, 121 KB/s], Decompressed: 8153 Downloaded: 8205 file(s) [attempted 8205/8459 = 96%, 421 KB/s], Decompressed: 8198 Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 409 KB/s], Decompressed: 8236 Downloaded: 8283 file(s) [attempted 8283/8459 = 97%, 130 KB/s], Decompressed: 8260 Downloaded: 8321 file(s) [attempted 8321/8459 = 98%, 306 KB/s], Decompressed: 8314 Downloaded: 8362 file(s) [attempted 8362/8459 = 98%, 238 KB/s], Decompressed: 8359 Downloaded: 8403 file(s) [attempted 8403/8459 = 99%, 119 KB/s], Decompressed: 8400 Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 189 KB/s], Decompressed: 8441 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 189 KB/s], Decompressed: 8455
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (11s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.7s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/779] Built Iut.Foundations.QualitativeData (2.2s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.7s)
✔ [3388/3393] Built Iut.Stage1.CorollarySchema (35s)
✔ [3390/3393] Built Iut.Stage1.SourceObligations (3.5s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.8s)
✔ [3393/3407] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (80s)
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 (13s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (15s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.0s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.3s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.9s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (23s)
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 (153s)
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`