Verification run
Run 1070
failed commit
9c075126c95d toolchain lean-v4-30-0 prover lean took 11m 17s · 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-1372-source
exit_code=Some(0) duration_ms=3510
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1372-source'...
$ git checkout 9c075126c95d000d20987df0663212e2495b5913
exit_code=Some(0) duration_ms=78
stderr:
Note: switching to '9c075126c95d000d20987df0663212e2495b5913'.
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 9c07512 Derive packet CTheta payload internally
Resolved source revision: 9c075126c95d000d20987df0663212e2495b5913
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=9c075126c95d000d20987df0663212e2495b5913 provenance={"branch":"master","checked_out_revision":"9c075126c95d000d20987df0663212e2495b5913","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"9c075126c95d000d20987df0663212e2495b5913","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=33504
stdout:
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
Downloaded: 1 file(s) [attempted 1/8459 = 0%, 11 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 5 KB/s], Decompressed: 11
Downloaded: 35 file(s) [attempted 35/8459 = 0%, 22 KB/s], Decompressed: 32
Downloaded: 63 file(s) [attempted 63/8459 = 0%, 28 KB/s], Decompressed: 58
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 430 KB/s], Decompressed: 82
Downloaded: 117 file(s) [attempted 117/8459 = 1%, 277 KB/s], Decompressed: 113
Downloaded: 148 file(s) [attempted 148/8459 = 1%, 133 KB/s], Decompressed: 145
Downloaded: 186 file(s) [attempted 186/8459 = 2%, 243 KB/s], Decompressed: 182
Downloaded: 218 file(s) [attempted 218/8459 = 2%, 287 KB/s], Decompressed: 213
Downloaded: 254 file(s) [attempted 254/8459 = 3%, 234 KB/s], Decompressed: 251
Downloaded: 289 file(s) [attempted 289/8459 = 3%, 94 KB/s], Decompressed: 285
Downloaded: 326 file(s) [attempted 326/8459 = 3%, 169 KB/s], Decompressed: 319
Downloaded: 364 file(s) [attempted 364/8459 = 4%, 29 KB/s], Decompressed: 357
Downloaded: 399 file(s) [attempted 399/8459 = 4%, 630 KB/s], Decompressed: 395
Downloaded: 433 file(s) [attempted 433/8459 = 5%, 264 KB/s], Decompressed: 429
Downloaded: 469 file(s) [attempted 469/8459 = 5%, 772 KB/s], Decompressed: 463
Downloaded: 508 file(s) [attempted 508/8459 = 6%, 645 KB/s], Decompressed: 501
Downloaded: 549 file(s) [attempted 549/8459 = 6%, 534 KB/s], Decompressed: 545
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 64 KB/s], Decompressed: 580
Downloaded: 622 file(s) [attempted 622/8459 = 7%, 306 KB/s], Decompressed: 617
Downloaded: 665 file(s) [attempted 665/8459 = 7%, 65 KB/s], Decompressed: 662
Downloaded: 705 file(s) [attempted 705/8459 = 8%, 28 KB/s], Decompressed: 693
Downloaded: 738 file(s) [attempted 738/8459 = 8%, 281 KB/s], Decompressed: 735
Downloaded: 778 file(s) [attempted 778/8459 = 9%, 412 KB/s], Decompressed: 771
Downloaded: 819 file(s) [attempted 819/8459 = 9%, 1826 KB/s], Decompressed: 812
Downloaded: 864 file(s) [attempted 864/8459 = 10%, 431 KB/s], Decompressed: 860
Downloaded: 908 file(s) [attempted 908/8459 = 10%, 636 KB/s], Decompressed: 906
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 161 KB/s], Decompressed: 939
Downloaded: 982 file(s) [attempted 982/8459 = 11%, 590 KB/s], Decompressed: 973
Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 427 KB/s], Decompressed: 1018
Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 184 KB/s], Decompressed: 1059
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 378 KB/s], Decompressed: 1100
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 157 KB/s], Decompressed: 1145
Downloaded: 1186 file(s) [attempted 1186/8459 = 14%, 549 KB/s], Decompressed: 1175
Downloaded: 1228 file(s) [attempted 1228/8459 = 14%, 82 KB/s], Decompressed: 1223
Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 96 KB/s], Decompressed: 1264
Downloaded: 1304 file(s) [attempted 1304/8459 = 15%, 805 KB/s], Decompressed: 1299
Downloaded: 1346 file(s) [attempted 1346/8459 = 15%, 213 KB/s], Decompressed: 1343
Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 475 KB/s], Decompressed: 1381
Downloaded: 1429 file(s) [attempted 1429/8459 = 16%, 28 KB/s], Decompressed: 1422
Downloaded: 1468 file(s) [attempted 1468/8459 = 17%, 468 KB/s], Decompressed: 1459
Downloaded: 1500 file(s) [attempted 1500/8459 = 17%, 152 KB/s], Decompressed: 1497
Downloaded: 1545 file(s) [attempted 1545/8459 = 18%, 533 KB/s], Decompressed: 1538
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 33 KB/s], Decompressed: 1579
Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 1414 KB/s], Decompressed: 1620
Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 602 KB/s], Decompressed: 1661
Downloaded: 1709 file(s) [attempted 1709/8459 = 20%, 468 KB/s], Decompressed: 1702
Downloaded: 1747 file(s) [attempted 1747/8459 = 20%, 1000 KB/s], Decompressed: 1743
Downloaded: 1786 file(s) [attempted 1786/8459 = 21%, 104 KB/s], Decompressed: 1781
Downloaded: 1823 file(s) [attempted 1823/8459 = 21%, 474 KB/s], Decompressed: 1819
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 105 KB/s], Decompressed: 1860
Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 270 KB/s], Decompressed: 1901
Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 146 KB/s], Decompressed: 1935
Downloaded: 1983 file(s) [attempted 1983/8459 = 23%, 134 KB/s], Decompressed: 1976
Downloaded: 2021 file(s) [attempted 2021/8459 = 23%, 119 KB/s], Decompressed: 2017
Downloaded: 2063 file(s) [attempted 2063/8459 = 24%, 83 KB/s], Decompressed: 2058
Downloaded: 2101 file(s) [attempted 2101/8459 = 24%, 1400 KB/s], Decompressed: 2093
Downloaded: 2140 file(s) [attempted 2140/8459 = 25%, 880 KB/s], Decompressed: 2137
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 83 KB/s], Decompressed: 2175
Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 113 KB/s], Decompressed: 2212
Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 277 KB/s], Decompressed: 2253
Downloaded: 2295 file(s) [attempted 2295/8459 = 27%, 781 KB/s], Decompressed: 2291
Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 77 KB/s], Decompressed: 2329
Downloaded: 2377 file(s) [attempted 2377/8459 = 28%, 1023 KB/s], Decompressed: 2373
Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 172 KB/s], Decompressed: 2411
Downloaded: 2454 file(s) [attempted 2454/8459 = 29%, 542 KB/s], Decompressed: 2445
Downloaded: 2490 file(s) [attempted 2490/8459 = 29%, 382 KB/s], Decompressed: 2486
Downloaded: 2531 file(s) [attempted 2531/8459 = 29%, 657 KB/s], Decompressed: 2524
Downloaded: 2568 file(s) [attempted 2568/8459 = 30%, 480 KB/s], Decompressed: 2565
Downloaded: 2609 file(s) [attempted 2609/8459 = 30%, 243 KB/s], Decompressed: 2602
Downloaded: 2654 file(s) [attempted 2654/8459 = 31%, 611 KB/s], Decompressed: 2647
Downloaded: 2691 file(s) [attempted 2691/8459 = 31%, 348 KB/s], Decompressed: 2688
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 71 KB/s], Decompressed: 2722
Downloaded: 2767 file(s) [attempted 2767/8459 = 32%, 344 KB/s], Decompressed: 2763
Downloaded: 2811 file(s) [attempted 2811/8459 = 33%, 100 KB/s], Decompressed: 2804
Downloaded: 2852 file(s) [attempted 2852/8459 = 33%, 342 KB/s], Decompressed: 2839
Downloaded: 2890 file(s) [attempted 2890/8459 = 34%, 30 KB/s], Decompressed: 2880
Downloaded: 2931 file(s) [attempted 2931/8459 = 34%, 739 KB/s], Decompressed: 2924
Downloaded: 2974 file(s) [attempted 2974/8459 = 35%, 183 KB/s], Decompressed: 2965
Downloaded: 3011 file(s) [attempted 3011/8459 = 35%, 369 KB/s], Decompressed: 3006
Downloaded: 3051 file(s) [attempted 3051/8459 = 36%, 781 KB/s], Decompressed: 3047
Downloaded: 3089 file(s) [attempted 3089/8459 = 36%, 309 KB/s], Decompressed: 3085
Downloaded: 3133 file(s) [attempted 3133/8459 = 37%, 103 KB/s], Decompressed: 3126
Downloaded: 3171 file(s) [attempted 3171/8459 = 37%, 179 KB/s], Decompressed: 3164
Downloaded: 3208 file(s) [attempted 3208/8459 = 37%, 215 KB/s], Decompressed: 3205
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 24 KB/s], Decompressed: 3242
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 129 KB/s], Decompressed: 3287
Downloaded: 3335 file(s) [attempted 3335/8459 = 39%, 154 KB/s], Decompressed: 3328
Downloaded: 3373 file(s) [attempted 3373/8459 = 39%, 45 KB/s], Decompressed: 3366
Downloaded: 3410 file(s) [attempted 3410/8459 = 40%, 744 KB/s], Decompressed: 3403
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 398 KB/s], Decompressed: 3444
Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 397 KB/s], Decompressed: 3485
Downloaded: 3532 file(s) [attempted 3532/8459 = 41%, 107 KB/s], Decompressed: 3523
Downloaded: 3572 file(s) [attempted 3572/8459 = 42%, 502 KB/s], Decompressed: 3564
Downloaded: 3611 file(s) [attempted 3611/8459 = 42%, 177 KB/s], Decompressed: 3602
Downloaded: 3648 file(s) [attempted 3648/8459 = 43%, 374 KB/s], Decompressed: 3643
Downloaded: 3687 file(s) [attempted 3687/8459 = 43%, 198 KB/s], Decompressed: 3681
Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 135 KB/s], Decompressed: 3711
Downloaded: 3759 file(s) [attempted 3759/8459 = 44%, 120 KB/s], Decompressed: 3752
Downloaded: 3800 file(s) [attempted 3800/8459 = 44%, 290 KB/s], Decompressed: 3797
Downloaded: 3841 file(s) [attempted 3841/8459 = 45%, 590 KB/s], Decompressed: 3838
Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 39 KB/s], Decompressed: 3882
Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 927 KB/s], Decompressed: 3930
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 164 KB/s], Decompressed: 3971
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 39 KB/s], Decompressed: 4009
Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 385 KB/s], Decompressed: 4058
Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 80 KB/s], Decompressed: 4091
Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 79 KB/s], Decompressed: 4132
Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 105 KB/s], Decompressed: 4180
Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 160 KB/s], Decompressed: 4223
Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 69 KB/s], Decompressed: 4262
Downloaded: 4305 file(s) [attempted 4305/8459 = 50%, 48 KB/s], Decompressed: 4297
Downloaded: 4345 file(s) [attempted 4345/8459 = 51%, 177 KB/s], Decompressed: 4341
Downloaded: 4386 file(s) [attempted 4386/8459 = 51%, 224 KB/s], Decompressed: 4382
Downloaded: 4424 file(s) [attempted 4424/8459 = 52%, 453 KB/s], Decompressed: 4416
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 108 KB/s], Decompressed: 4461
Downloaded: 4503 file(s) [attempted 4503/8459 = 53%, 341 KB/s], Decompressed: 4498
Downloaded: 4544 file(s) [attempted 4544/8459 = 53%, 147 KB/s], Decompressed: 4540
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 158 KB/s], Decompressed: 4577
Downloaded: 4617 file(s) [attempted 4617/8459 = 54%, 283 KB/s], Decompressed: 4605
Downloaded: 4652 file(s) [attempted 4652/8459 = 54%, 750 KB/s], Decompressed: 4649
Downloaded: 4700 file(s) [attempted 4700/8459 = 55%, 233 KB/s], Decompressed: 4694
Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 149 KB/s], Decompressed: 4741
Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 213 KB/s], Decompressed: 4786
Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 259 KB/s], Decompressed: 4830
Downloaded: 4884 file(s) [attempted 4884/8459 = 57%, 1074 KB/s], Decompressed: 4872
Downloaded: 4913 file(s) [attempted 4913/8459 = 58%, 215 KB/s], Decompressed: 4909
Downloaded: 4954 file(s) [attempted 4954/8459 = 58%, 134 KB/s], Decompressed: 4950
Downloaded: 4992 file(s) [attempted 4992/8459 = 59%, 133 KB/s], Decompressed: 4985
Downloaded: 5036 file(s) [attempted 5036/8459 = 59%, 120 KB/s], Decompressed: 5026
Downloaded: 5070 file(s) [attempted 5070/8459 = 59%, 61 KB/s], Decompressed: 5063
Downloaded: 5111 file(s) [attempted 5111/8459 = 60%, 152 KB/s], Decompressed: 5108
Downloaded: 5156 file(s) [attempted 5156/8459 = 60%, 146 KB/s], Decompressed: 5152
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 27 KB/s], Decompressed: 5197
Downloaded: 5243 file(s) [attempted 5243/8459 = 61%, 1618 KB/s], Decompressed: 5231
Downloaded: 5273 file(s) [attempted 5273/8459 = 62%, 415 KB/s], Decompressed: 5269
Downloaded: 5313 file(s) [attempted 5313/8459 = 62%, 212 KB/s], Decompressed: 5306
Downloaded: 5354 file(s) [attempted 5354/8459 = 63%, 827 KB/s], Decompressed: 5351
Downloaded: 5399 file(s) [attempted 5399/8459 = 63%, 363 KB/s], Decompressed: 5395
Downloaded: 5447 file(s) [attempted 5447/8459 = 64%, 481 KB/s], Decompressed: 5443
Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 114 KB/s], Decompressed: 5481
Downloaded: 5525 file(s) [attempted 5525/8459 = 65%, 145 KB/s], Decompressed: 5519
Downloaded: 5563 file(s) [attempted 5563/8459 = 65%, 294 KB/s], Decompressed: 5560
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 21 KB/s], Decompressed: 5597
Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 27 KB/s], Decompressed: 5642
Downloaded: 5690 file(s) [attempted 5690/8459 = 67%, 220 KB/s], Decompressed: 5683
Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 668 KB/s], Decompressed: 5724
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 288 KB/s], Decompressed: 5765
Downloaded: 5813 file(s) [attempted 5813/8459 = 68%, 648 KB/s], Decompressed: 5806
Downloaded: 5854 file(s) [attempted 5854/8459 = 69%, 358 KB/s], Decompressed: 5847
Downloaded: 5892 file(s) [attempted 5892/8459 = 69%, 179 KB/s], Decompressed: 5888
Downloaded: 5929 file(s) [attempted 5929/8459 = 70%, 60 KB/s], Decompressed: 5926
Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 225 KB/s], Decompressed: 5967
Downloaded: 6011 file(s) [attempted 6011/8459 = 71%, 121 KB/s], Decompressed: 6008
Downloaded: 6050 file(s) [attempted 6050/8459 = 71%, 362 KB/s], Decompressed: 6042
Downloaded: 6091 file(s) [attempted 6091/8459 = 72%, 1343 KB/s], Decompressed: 6083
Downloaded: 6131 file(s) [attempted 6131/8459 = 72%, 237 KB/s], Decompressed: 6128
Downloaded: 6176 file(s) [attempted 6176/8459 = 73%, 687 KB/s], Decompressed: 6165
Downloaded: 6210 file(s) [attempted 6210/8459 = 73%, 160 KB/s], Decompressed: 6203
Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 99 KB/s], Decompressed: 6237
Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 435 KB/s], Decompressed: 6282
Downloaded: 6330 file(s) [attempted 6330/8459 = 74%, 594 KB/s], Decompressed: 6326
Downloaded: 6374 file(s) [attempted 6374/8459 = 75%, 185 KB/s], Decompressed: 6371
Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 85 KB/s], Decompressed: 6398
Downloaded: 6446 file(s) [attempted 6446/8459 = 76%, 317 KB/s], Decompressed: 6439
Downloaded: 6487 file(s) [attempted 6487/8459 = 76%, 183 KB/s], Decompressed: 6484
Downloaded: 6529 file(s) [attempted 6529/8459 = 77%, 261 KB/s], Decompressed: 6525
Downloaded: 6569 file(s) [attempted 6569/8459 = 77%, 23 KB/s], Decompressed: 6566
Downloaded: 6610 file(s) [attempted 6610/8459 = 78%, 307 KB/s], Decompressed: 6607
Downloaded: 6648 file(s) [attempted 6648/8459 = 78%, 50 KB/s], Decompressed: 6641
Downloaded: 6686 file(s) [attempted 6686/8459 = 79%, 225 KB/s], Decompressed: 6682
Downloaded: 6727 file(s) [attempted 6727/8459 = 79%, 1553 KB/s], Decompressed: 6723
Downloaded: 6771 file(s) [attempted 6771/8459 = 80%, 313 KB/s], Decompressed: 6764
Downloaded: 6809 file(s) [attempted 6809/8459 = 80%, 532 KB/s], Decompressed: 6804
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 124 KB/s], Decompressed: 6836
Downloaded: 6884 file(s) [attempted 6884/8459 = 81%, 674 KB/s], Decompressed: 6881
Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 220 KB/s], Decompressed: 6922
Downloaded: 6970 file(s) [attempted 6970/8459 = 82%, 529 KB/s], Decompressed: 6966
Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 457 KB/s], Decompressed: 7004
Downloaded: 7048 file(s) [attempted 7048/8459 = 83%, 573 KB/s], Decompressed: 7045
Downloaded: 7087 file(s) [attempted 7087/8459 = 83%, 225 KB/s], Decompressed: 7083
Downloaded: 7127 file(s) [attempted 7127/8459 = 84%, 339 KB/s], Decompressed: 7124
Downloaded: 7172 file(s) [attempted 7172/8459 = 84%, 147 KB/s], Decompressed: 7168
Downloaded: 7213 file(s) [attempted 7213/8459 = 85%, 42 KB/s], Decompressed: 7199
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 435 KB/s], Decompressed: 7240
Downloaded: 7288 file(s) [attempted 7288/8459 = 86%, 173 KB/s], Decompressed: 7281
Downloaded: 7326 file(s) [attempted 7326/8459 = 86%, 74 KB/s], Decompressed: 7322
Downloaded: 7370 file(s) [attempted 7370/8459 = 87%, 103 KB/s], Decompressed: 7367
Downloaded: 7411 file(s) [attempted 7411/8459 = 87%, 143 KB/s], Decompressed: 7404
Downloaded: 7452 file(s) [attempted 7452/8459 = 88%, 315 KB/s], Decompressed: 7445
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 134 KB/s], Decompressed: 7486
Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 567 KB/s], Decompressed: 7527
Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 296 KB/s], Decompressed: 7565
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 220 KB/s], Decompressed: 7606
Downloaded: 7647 file(s) [attempted 7647/8459 = 90%, 43 KB/s], Decompressed: 7640
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 289 KB/s], Decompressed: 7685
Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 957 KB/s], Decompressed: 7730
Downloaded: 7771 file(s) [attempted 7771/8459 = 91%, 84 KB/s], Decompressed: 7764
Downloaded: 7808 file(s) [attempted 7808/8459 = 92%, 24 KB/s], Decompressed: 7801
Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 1095 KB/s], Decompressed: 7839
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 258 KB/s], Decompressed: 7883
Downloaded: 7935 file(s) [attempted 7935/8459 = 93%, 274 KB/s], Decompressed: 7931
Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 156 KB/s], Decompressed: 7972
Downloaded: 8011 file(s) [attempted 8011/8459 = 94%, 59 KB/s], Decompressed: 8003
Downloaded: 8051 file(s) [attempted 8051/8459 = 95%, 99 KB/s], Decompressed: 8044
Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 105 KB/s], Decompressed: 8089
Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 498 KB/s], Decompressed: 8137
Downloaded: 8185 file(s) [attempted 8185/8459 = 96%, 116 KB/s], Decompressed: 8181
Downloaded: 8226 file(s) [attempted 8226/8459 = 97%, 868 KB/s], Decompressed: 8215
Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 486 KB/s], Decompressed: 8256
Downloaded: 8301 file(s) [attempted 8301/8459 = 98%, 585 KB/s], Decompressed: 8291
Downloaded: 8337 file(s) [attempted 8337/8459 = 98%, 79 KB/s], Decompressed: 8332
Downloaded: 8380 file(s) [attempted 8380/8459 = 99%, 49 KB/s], Decompressed: 8376
Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 656 KB/s], Decompressed: 8421
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 158 KB/s], Decompressed: 8448
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 158 KB/s], Decompressed: 8448
$ lake build
exit_code=Some(1) duration_ms=451022
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (24s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.5s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.6s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/775] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.6s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.7s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (34s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (2.0s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3393/3398] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (84s)
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 (22s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.0s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.6s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.3s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (28s)
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 (168s)
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=1178
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-1372-source
Cloning into '/var/lib/apodeixis/repos/job-1372-source'...
git_checkout exit 0
git checkout 9c075126c95d000d20987df0663212e2495b5913
Note: switching to '9c075126c95d000d20987df0663212e2495b5913'. 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 9c07512 Derive packet CTheta payload internally
lake_cache exit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache Decompressed 8459 file(s) Already decompressed 8459 file(s)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes Downloaded: 1 file(s) [attempted 1/8459 = 0%, 11 KB/s], Decompressed: 0 Downloaded: 13 file(s) [attempted 13/8459 = 0%, 5 KB/s], Decompressed: 11 Downloaded: 35 file(s) [attempted 35/8459 = 0%, 22 KB/s], Decompressed: 32 Downloaded: 63 file(s) [attempted 63/8459 = 0%, 28 KB/s], Decompressed: 58 Downloaded: 86 file(s) [attempted 86/8459 = 1%, 430 KB/s], Decompressed: 82 Downloaded: 117 file(s) [attempted 117/8459 = 1%, 277 KB/s], Decompressed: 113 Downloaded: 148 file(s) [attempted 148/8459 = 1%, 133 KB/s], Decompressed: 145 Downloaded: 186 file(s) [attempted 186/8459 = 2%, 243 KB/s], Decompressed: 182 Downloaded: 218 file(s) [attempted 218/8459 = 2%, 287 KB/s], Decompressed: 213 Downloaded: 254 file(s) [attempted 254/8459 = 3%, 234 KB/s], Decompressed: 251 Downloaded: 289 file(s) [attempted 289/8459 = 3%, 94 KB/s], Decompressed: 285 Downloaded: 326 file(s) [attempted 326/8459 = 3%, 169 KB/s], Decompressed: 319 Downloaded: 364 file(s) [attempted 364/8459 = 4%, 29 KB/s], Decompressed: 357 Downloaded: 399 file(s) [attempted 399/8459 = 4%, 630 KB/s], Decompressed: 395 Downloaded: 433 file(s) [attempted 433/8459 = 5%, 264 KB/s], Decompressed: 429 Downloaded: 469 file(s) [attempted 469/8459 = 5%, 772 KB/s], Decompressed: 463 Downloaded: 508 file(s) [attempted 508/8459 = 6%, 645 KB/s], Decompressed: 501 Downloaded: 549 file(s) [attempted 549/8459 = 6%, 534 KB/s], Decompressed: 545 Downloaded: 586 file(s) [attempted 586/8459 = 6%, 64 KB/s], Decompressed: 580 Downloaded: 622 file(s) [attempted 622/8459 = 7%, 306 KB/s], Decompressed: 617 Downloaded: 665 file(s) [attempted 665/8459 = 7%, 65 KB/s], Decompressed: 662 Downloaded: 705 file(s) [attempted 705/8459 = 8%, 28 KB/s], Decompressed: 693 Downloaded: 738 file(s) [attempted 738/8459 = 8%, 281 KB/s], Decompressed: 735 Downloaded: 778 file(s) [attempted 778/8459 = 9%, 412 KB/s], Decompressed: 771 Downloaded: 819 file(s) [attempted 819/8459 = 9%, 1826 KB/s], Decompressed: 812 Downloaded: 864 file(s) [attempted 864/8459 = 10%, 431 KB/s], Decompressed: 860 Downloaded: 908 file(s) [attempted 908/8459 = 10%, 636 KB/s], Decompressed: 906 Downloaded: 949 file(s) [attempted 949/8459 = 11%, 161 KB/s], Decompressed: 939 Downloaded: 982 file(s) [attempted 982/8459 = 11%, 590 KB/s], Decompressed: 973 Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 427 KB/s], Decompressed: 1018 Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 184 KB/s], Decompressed: 1059 Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 378 KB/s], Decompressed: 1100 Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 157 KB/s], Decompressed: 1145 Downloaded: 1186 file(s) [attempted 1186/8459 = 14%, 549 KB/s], Decompressed: 1175 Downloaded: 1228 file(s) [attempted 1228/8459 = 14%, 82 KB/s], Decompressed: 1223 Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 96 KB/s], Decompressed: 1264 Downloaded: 1304 file(s) [attempted 1304/8459 = 15%, 805 KB/s], Decompressed: 1299 Downloaded: 1346 file(s) [attempted 1346/8459 = 15%, 213 KB/s], Decompressed: 1343 Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 475 KB/s], Decompressed: 1381 Downloaded: 1429 file(s) [attempted 1429/8459 = 16%, 28 KB/s], Decompressed: 1422 Downloaded: 1468 file(s) [attempted 1468/8459 = 17%, 468 KB/s], Decompressed: 1459 Downloaded: 1500 file(s) [attempted 1500/8459 = 17%, 152 KB/s], Decompressed: 1497 Downloaded: 1545 file(s) [attempted 1545/8459 = 18%, 533 KB/s], Decompressed: 1538 Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 33 KB/s], Decompressed: 1579 Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 1414 KB/s], Decompressed: 1620 Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 602 KB/s], Decompressed: 1661 Downloaded: 1709 file(s) [attempted 1709/8459 = 20%, 468 KB/s], Decompressed: 1702 Downloaded: 1747 file(s) [attempted 1747/8459 = 20%, 1000 KB/s], Decompressed: 1743 Downloaded: 1786 file(s) [attempted 1786/8459 = 21%, 104 KB/s], Decompressed: 1781 Downloaded: 1823 file(s) [attempted 1823/8459 = 21%, 474 KB/s], Decompressed: 1819 Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 105 KB/s], Decompressed: 1860 Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 270 KB/s], Decompressed: 1901 Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 146 KB/s], Decompressed: 1935 Downloaded: 1983 file(s) [attempted 1983/8459 = 23%, 134 KB/s], Decompressed: 1976 Downloaded: 2021 file(s) [attempted 2021/8459 = 23%, 119 KB/s], Decompressed: 2017 Downloaded: 2063 file(s) [attempted 2063/8459 = 24%, 83 KB/s], Decompressed: 2058 Downloaded: 2101 file(s) [attempted 2101/8459 = 24%, 1400 KB/s], Decompressed: 2093 Downloaded: 2140 file(s) [attempted 2140/8459 = 25%, 880 KB/s], Decompressed: 2137 Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 83 KB/s], Decompressed: 2175 Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 113 KB/s], Decompressed: 2212 Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 277 KB/s], Decompressed: 2253 Downloaded: 2295 file(s) [attempted 2295/8459 = 27%, 781 KB/s], Decompressed: 2291 Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 77 KB/s], Decompressed: 2329 Downloaded: 2377 file(s) [attempted 2377/8459 = 28%, 1023 KB/s], Decompressed: 2373 Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 172 KB/s], Decompressed: 2411 Downloaded: 2454 file(s) [attempted 2454/8459 = 29%, 542 KB/s], Decompressed: 2445 Downloaded: 2490 file(s) [attempted 2490/8459 = 29%, 382 KB/s], Decompressed: 2486 Downloaded: 2531 file(s) [attempted 2531/8459 = 29%, 657 KB/s], Decompressed: 2524 Downloaded: 2568 file(s) [attempted 2568/8459 = 30%, 480 KB/s], Decompressed: 2565 Downloaded: 2609 file(s) [attempted 2609/8459 = 30%, 243 KB/s], Decompressed: 2602 Downloaded: 2654 file(s) [attempted 2654/8459 = 31%, 611 KB/s], Decompressed: 2647 Downloaded: 2691 file(s) [attempted 2691/8459 = 31%, 348 KB/s], Decompressed: 2688 Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 71 KB/s], Decompressed: 2722 Downloaded: 2767 file(s) [attempted 2767/8459 = 32%, 344 KB/s], Decompressed: 2763 Downloaded: 2811 file(s) [attempted 2811/8459 = 33%, 100 KB/s], Decompressed: 2804 Downloaded: 2852 file(s) [attempted 2852/8459 = 33%, 342 KB/s], Decompressed: 2839 Downloaded: 2890 file(s) [attempted 2890/8459 = 34%, 30 KB/s], Decompressed: 2880 Downloaded: 2931 file(s) [attempted 2931/8459 = 34%, 739 KB/s], Decompressed: 2924 Downloaded: 2974 file(s) [attempted 2974/8459 = 35%, 183 KB/s], Decompressed: 2965 Downloaded: 3011 file(s) [attempted 3011/8459 = 35%, 369 KB/s], Decompressed: 3006 Downloaded: 3051 file(s) [attempted 3051/8459 = 36%, 781 KB/s], Decompressed: 3047 Downloaded: 3089 file(s) [attempted 3089/8459 = 36%, 309 KB/s], Decompressed: 3085 Downloaded: 3133 file(s) [attempted 3133/8459 = 37%, 103 KB/s], Decompressed: 3126 Downloaded: 3171 file(s) [attempted 3171/8459 = 37%, 179 KB/s], Decompressed: 3164 Downloaded: 3208 file(s) [attempted 3208/8459 = 37%, 215 KB/s], Decompressed: 3205 Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 24 KB/s], Decompressed: 3242 Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 129 KB/s], Decompressed: 3287 Downloaded: 3335 file(s) [attempted 3335/8459 = 39%, 154 KB/s], Decompressed: 3328 Downloaded: 3373 file(s) [attempted 3373/8459 = 39%, 45 KB/s], Decompressed: 3366 Downloaded: 3410 file(s) [attempted 3410/8459 = 40%, 744 KB/s], Decompressed: 3403 Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 398 KB/s], Decompressed: 3444 Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 397 KB/s], Decompressed: 3485 Downloaded: 3532 file(s) [attempted 3532/8459 = 41%, 107 KB/s], Decompressed: 3523 Downloaded: 3572 file(s) [attempted 3572/8459 = 42%, 502 KB/s], Decompressed: 3564 Downloaded: 3611 file(s) [attempted 3611/8459 = 42%, 177 KB/s], Decompressed: 3602 Downloaded: 3648 file(s) [attempted 3648/8459 = 43%, 374 KB/s], Decompressed: 3643 Downloaded: 3687 file(s) [attempted 3687/8459 = 43%, 198 KB/s], Decompressed: 3681 Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 135 KB/s], Decompressed: 3711 Downloaded: 3759 file(s) [attempted 3759/8459 = 44%, 120 KB/s], Decompressed: 3752 Downloaded: 3800 file(s) [attempted 3800/8459 = 44%, 290 KB/s], Decompressed: 3797 Downloaded: 3841 file(s) [attempted 3841/8459 = 45%, 590 KB/s], Decompressed: 3838 Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 39 KB/s], Decompressed: 3882 Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 927 KB/s], Decompressed: 3930 Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 164 KB/s], Decompressed: 3971 Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 39 KB/s], Decompressed: 4009 Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 385 KB/s], Decompressed: 4058 Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 80 KB/s], Decompressed: 4091 Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 79 KB/s], Decompressed: 4132 Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 105 KB/s], Decompressed: 4180 Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 160 KB/s], Decompressed: 4223 Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 69 KB/s], Decompressed: 4262 Downloaded: 4305 file(s) [attempted 4305/8459 = 50%, 48 KB/s], Decompressed: 4297 Downloaded: 4345 file(s) [attempted 4345/8459 = 51%, 177 KB/s], Decompressed: 4341 Downloaded: 4386 file(s) [attempted 4386/8459 = 51%, 224 KB/s], Decompressed: 4382 Downloaded: 4424 file(s) [attempted 4424/8459 = 52%, 453 KB/s], Decompressed: 4416 Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 108 KB/s], Decompressed: 4461 Downloaded: 4503 file(s) [attempted 4503/8459 = 53%, 341 KB/s], Decompressed: 4498 Downloaded: 4544 file(s) [attempted 4544/8459 = 53%, 147 KB/s], Decompressed: 4540 Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 158 KB/s], Decompressed: 4577 Downloaded: 4617 file(s) [attempted 4617/8459 = 54%, 283 KB/s], Decompressed: 4605 Downloaded: 4652 file(s) [attempted 4652/8459 = 54%, 750 KB/s], Decompressed: 4649 Downloaded: 4700 file(s) [attempted 4700/8459 = 55%, 233 KB/s], Decompressed: 4694 Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 149 KB/s], Decompressed: 4741 Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 213 KB/s], Decompressed: 4786 Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 259 KB/s], Decompressed: 4830 Downloaded: 4884 file(s) [attempted 4884/8459 = 57%, 1074 KB/s], Decompressed: 4872 Downloaded: 4913 file(s) [attempted 4913/8459 = 58%, 215 KB/s], Decompressed: 4909 Downloaded: 4954 file(s) [attempted 4954/8459 = 58%, 134 KB/s], Decompressed: 4950 Downloaded: 4992 file(s) [attempted 4992/8459 = 59%, 133 KB/s], Decompressed: 4985 Downloaded: 5036 file(s) [attempted 5036/8459 = 59%, 120 KB/s], Decompressed: 5026 Downloaded: 5070 file(s) [attempted 5070/8459 = 59%, 61 KB/s], Decompressed: 5063 Downloaded: 5111 file(s) [attempted 5111/8459 = 60%, 152 KB/s], Decompressed: 5108 Downloaded: 5156 file(s) [attempted 5156/8459 = 60%, 146 KB/s], Decompressed: 5152 Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 27 KB/s], Decompressed: 5197 Downloaded: 5243 file(s) [attempted 5243/8459 = 61%, 1618 KB/s], Decompressed: 5231 Downloaded: 5273 file(s) [attempted 5273/8459 = 62%, 415 KB/s], Decompressed: 5269 Downloaded: 5313 file(s) [attempted 5313/8459 = 62%, 212 KB/s], Decompressed: 5306 Downloaded: 5354 file(s) [attempted 5354/8459 = 63%, 827 KB/s], Decompressed: 5351 Downloaded: 5399 file(s) [attempted 5399/8459 = 63%, 363 KB/s], Decompressed: 5395 Downloaded: 5447 file(s) [attempted 5447/8459 = 64%, 481 KB/s], Decompressed: 5443 Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 114 KB/s], Decompressed: 5481 Downloaded: 5525 file(s) [attempted 5525/8459 = 65%, 145 KB/s], Decompressed: 5519 Downloaded: 5563 file(s) [attempted 5563/8459 = 65%, 294 KB/s], Decompressed: 5560 Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 21 KB/s], Decompressed: 5597 Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 27 KB/s], Decompressed: 5642 Downloaded: 5690 file(s) [attempted 5690/8459 = 67%, 220 KB/s], Decompressed: 5683 Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 668 KB/s], Decompressed: 5724 Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 288 KB/s], Decompressed: 5765 Downloaded: 5813 file(s) [attempted 5813/8459 = 68%, 648 KB/s], Decompressed: 5806 Downloaded: 5854 file(s) [attempted 5854/8459 = 69%, 358 KB/s], Decompressed: 5847 Downloaded: 5892 file(s) [attempted 5892/8459 = 69%, 179 KB/s], Decompressed: 5888 Downloaded: 5929 file(s) [attempted 5929/8459 = 70%, 60 KB/s], Decompressed: 5926 Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 225 KB/s], Decompressed: 5967 Downloaded: 6011 file(s) [attempted 6011/8459 = 71%, 121 KB/s], Decompressed: 6008 Downloaded: 6050 file(s) [attempted 6050/8459 = 71%, 362 KB/s], Decompressed: 6042 Downloaded: 6091 file(s) [attempted 6091/8459 = 72%, 1343 KB/s], Decompressed: 6083 Downloaded: 6131 file(s) [attempted 6131/8459 = 72%, 237 KB/s], Decompressed: 6128 Downloaded: 6176 file(s) [attempted 6176/8459 = 73%, 687 KB/s], Decompressed: 6165 Downloaded: 6210 file(s) [attempted 6210/8459 = 73%, 160 KB/s], Decompressed: 6203 Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 99 KB/s], Decompressed: 6237 Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 435 KB/s], Decompressed: 6282 Downloaded: 6330 file(s) [attempted 6330/8459 = 74%, 594 KB/s], Decompressed: 6326 Downloaded: 6374 file(s) [attempted 6374/8459 = 75%, 185 KB/s], Decompressed: 6371 Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 85 KB/s], Decompressed: 6398 Downloaded: 6446 file(s) [attempted 6446/8459 = 76%, 317 KB/s], Decompressed: 6439 Downloaded: 6487 file(s) [attempted 6487/8459 = 76%, 183 KB/s], Decompressed: 6484 Downloaded: 6529 file(s) [attempted 6529/8459 = 77%, 261 KB/s], Decompressed: 6525 Downloaded: 6569 file(s) [attempted 6569/8459 = 77%, 23 KB/s], Decompressed: 6566 Downloaded: 6610 file(s) [attempted 6610/8459 = 78%, 307 KB/s], Decompressed: 6607 Downloaded: 6648 file(s) [attempted 6648/8459 = 78%, 50 KB/s], Decompressed: 6641 Downloaded: 6686 file(s) [attempted 6686/8459 = 79%, 225 KB/s], Decompressed: 6682 Downloaded: 6727 file(s) [attempted 6727/8459 = 79%, 1553 KB/s], Decompressed: 6723 Downloaded: 6771 file(s) [attempted 6771/8459 = 80%, 313 KB/s], Decompressed: 6764 Downloaded: 6809 file(s) [attempted 6809/8459 = 80%, 532 KB/s], Decompressed: 6804 Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 124 KB/s], Decompressed: 6836 Downloaded: 6884 file(s) [attempted 6884/8459 = 81%, 674 KB/s], Decompressed: 6881 Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 220 KB/s], Decompressed: 6922 Downloaded: 6970 file(s) [attempted 6970/8459 = 82%, 529 KB/s], Decompressed: 6966 Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 457 KB/s], Decompressed: 7004 Downloaded: 7048 file(s) [attempted 7048/8459 = 83%, 573 KB/s], Decompressed: 7045 Downloaded: 7087 file(s) [attempted 7087/8459 = 83%, 225 KB/s], Decompressed: 7083 Downloaded: 7127 file(s) [attempted 7127/8459 = 84%, 339 KB/s], Decompressed: 7124 Downloaded: 7172 file(s) [attempted 7172/8459 = 84%, 147 KB/s], Decompressed: 7168 Downloaded: 7213 file(s) [attempted 7213/8459 = 85%, 42 KB/s], Decompressed: 7199 Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 435 KB/s], Decompressed: 7240 Downloaded: 7288 file(s) [attempted 7288/8459 = 86%, 173 KB/s], Decompressed: 7281 Downloaded: 7326 file(s) [attempted 7326/8459 = 86%, 74 KB/s], Decompressed: 7322 Downloaded: 7370 file(s) [attempted 7370/8459 = 87%, 103 KB/s], Decompressed: 7367 Downloaded: 7411 file(s) [attempted 7411/8459 = 87%, 143 KB/s], Decompressed: 7404 Downloaded: 7452 file(s) [attempted 7452/8459 = 88%, 315 KB/s], Decompressed: 7445 Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 134 KB/s], Decompressed: 7486 Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 567 KB/s], Decompressed: 7527 Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 296 KB/s], Decompressed: 7565 Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 220 KB/s], Decompressed: 7606 Downloaded: 7647 file(s) [attempted 7647/8459 = 90%, 43 KB/s], Decompressed: 7640 Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 289 KB/s], Decompressed: 7685 Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 957 KB/s], Decompressed: 7730 Downloaded: 7771 file(s) [attempted 7771/8459 = 91%, 84 KB/s], Decompressed: 7764 Downloaded: 7808 file(s) [attempted 7808/8459 = 92%, 24 KB/s], Decompressed: 7801 Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 1095 KB/s], Decompressed: 7839 Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 258 KB/s], Decompressed: 7883 Downloaded: 7935 file(s) [attempted 7935/8459 = 93%, 274 KB/s], Decompressed: 7931 Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 156 KB/s], Decompressed: 7972 Downloaded: 8011 file(s) [attempted 8011/8459 = 94%, 59 KB/s], Decompressed: 8003 Downloaded: 8051 file(s) [attempted 8051/8459 = 95%, 99 KB/s], Decompressed: 8044 Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 105 KB/s], Decompressed: 8089 Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 498 KB/s], Decompressed: 8137 Downloaded: 8185 file(s) [attempted 8185/8459 = 96%, 116 KB/s], Decompressed: 8181 Downloaded: 8226 file(s) [attempted 8226/8459 = 97%, 868 KB/s], Decompressed: 8215 Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 486 KB/s], Decompressed: 8256 Downloaded: 8301 file(s) [attempted 8301/8459 = 98%, 585 KB/s], Decompressed: 8291 Downloaded: 8337 file(s) [attempted 8337/8459 = 98%, 79 KB/s], Decompressed: 8332 Downloaded: 8380 file(s) [attempted 8380/8459 = 99%, 49 KB/s], Decompressed: 8376 Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 656 KB/s], Decompressed: 8421 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 158 KB/s], Decompressed: 8448 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 158 KB/s], Decompressed: 8448
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (24s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.5s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.6s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.6s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/775] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.6s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.7s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (34s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (2.0s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3393/3398] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (84s)
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 (22s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.0s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.6s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.3s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (28s)
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 (168s)
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`