Verification run
Run 1069
failed commit
829a0be0cbe5 toolchain lean-v4-30-0 prover lean took 11m 12s · 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-1371-source
exit_code=Some(0) duration_ms=3496
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1371-source'...
$ git checkout 829a0be0cbe55c128a85e3e7394abdc832dbe126
exit_code=Some(0) duration_ms=146
stderr:
Note: switching to '829a0be0cbe55c128a85e3e7394abdc832dbe126'.
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 829a0be Project final evidence from local arithmetic
Resolved source revision: 829a0be0cbe55c128a85e3e7394abdc832dbe126
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=829a0be0cbe55c128a85e3e7394abdc832dbe126 provenance={"branch":"master","checked_out_revision":"829a0be0cbe55c128a85e3e7394abdc832dbe126","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"829a0be0cbe55c128a85e3e7394abdc832dbe126","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=33964
stdout:
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 2 KB/s], Decompressed: 13
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 17 KB/s], Decompressed: 30
Downloaded: 63 file(s) [attempted 63/8459 = 0%, 47 KB/s], Decompressed: 61
Downloaded: 83 file(s) [attempted 83/8459 = 0%, 158 KB/s], Decompressed: 79
Downloaded: 112 file(s) [attempted 112/8459 = 1%, 73 KB/s], Decompressed: 97
Downloaded: 138 file(s) [attempted 138/8459 = 1%, 347 KB/s], Decompressed: 134
Downloaded: 179 file(s) [attempted 179/8459 = 2%, 357 KB/s], Decompressed: 176
Downloaded: 220 file(s) [attempted 220/8459 = 2%, 98 KB/s], Decompressed: 216
Downloaded: 262 file(s) [attempted 262/8459 = 3%, 44 KB/s], Decompressed: 258
Downloaded: 299 file(s) [attempted 299/8459 = 3%, 172 KB/s], Decompressed: 292
Downloaded: 340 file(s) [attempted 340/8459 = 4%, 90 KB/s], Decompressed: 337
Downloaded: 372 file(s) [attempted 372/8459 = 4%, 110 KB/s], Decompressed: 367
Downloaded: 404 file(s) [attempted 404/8459 = 4%, 80 KB/s], Decompressed: 398
Downloaded: 446 file(s) [attempted 446/8459 = 5%, 233 KB/s], Decompressed: 439
Downloaded: 491 file(s) [attempted 491/8459 = 5%, 261 KB/s], Decompressed: 484
Downloaded: 530 file(s) [attempted 530/8459 = 6%, 448 KB/s], Decompressed: 525
Downloaded: 565 file(s) [attempted 565/8459 = 6%, 77 KB/s], Decompressed: 552
Downloaded: 600 file(s) [attempted 600/8459 = 7%, 814 KB/s], Decompressed: 593
Downloaded: 641 file(s) [attempted 641/8459 = 7%, 246 KB/s], Decompressed: 638
Downloaded: 686 file(s) [attempted 686/8459 = 8%, 255 KB/s], Decompressed: 679
Downloaded: 725 file(s) [attempted 725/8459 = 8%, 86 KB/s], Decompressed: 710
Downloaded: 761 file(s) [attempted 761/8459 = 8%, 167 KB/s], Decompressed: 754
Downloaded: 792 file(s) [attempted 792/8459 = 9%, 113 KB/s], Decompressed: 789
Downloaded: 837 file(s) [attempted 837/8459 = 9%, 75 KB/s], Decompressed: 833
Downloaded: 878 file(s) [attempted 878/8459 = 10%, 261 KB/s], Decompressed: 874
Downloaded: 922 file(s) [attempted 922/8459 = 10%, 462 KB/s], Decompressed: 919
Downloaded: 967 file(s) [attempted 967/8459 = 11%, 205 KB/s], Decompressed: 960
Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 172 KB/s], Decompressed: 994
Downloaded: 1036 file(s) [attempted 1036/8459 = 12%, 137 KB/s], Decompressed: 1028
Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 269 KB/s], Decompressed: 1073
Downloaded: 1124 file(s) [attempted 1124/8459 = 13%, 374 KB/s], Decompressed: 1121
Downloaded: 1172 file(s) [attempted 1172/8459 = 13%, 826 KB/s], Decompressed: 1165
Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 366 KB/s], Decompressed: 1213
Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 639 KB/s], Decompressed: 1254
Downloaded: 1293 file(s) [attempted 1293/8459 = 15%, 327 KB/s], Decompressed: 1289
Downloaded: 1326 file(s) [attempted 1326/8459 = 15%, 154 KB/s], Decompressed: 1319
Downloaded: 1367 file(s) [attempted 1367/8459 = 16%, 131 KB/s], Decompressed: 1364
Downloaded: 1415 file(s) [attempted 1415/8459 = 16%, 224 KB/s], Decompressed: 1408
Downloaded: 1463 file(s) [attempted 1463/8459 = 17%, 105 KB/s], Decompressed: 1456
Downloaded: 1501 file(s) [attempted 1501/8459 = 17%, 236 KB/s], Decompressed: 1494
Downloaded: 1539 file(s) [attempted 1539/8459 = 18%, 155 KB/s], Decompressed: 1535
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 414 KB/s], Decompressed: 1573
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 195 KB/s], Decompressed: 1617
Downloaded: 1662 file(s) [attempted 1662/8459 = 19%, 337 KB/s], Decompressed: 1658
Downloaded: 1699 file(s) [attempted 1699/8459 = 20%, 119 KB/s], Decompressed: 1692
Downloaded: 1738 file(s) [attempted 1738/8459 = 20%, 322 KB/s], Decompressed: 1733
Downloaded: 1772 file(s) [attempted 1772/8459 = 20%, 135 KB/s], Decompressed: 1764
Downloaded: 1814 file(s) [attempted 1814/8459 = 21%, 161 KB/s], Decompressed: 1805
Downloaded: 1857 file(s) [attempted 1857/8459 = 21%, 24 KB/s], Decompressed: 1850
Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 731 KB/s], Decompressed: 1887
Downloaded: 1932 file(s) [attempted 1932/8459 = 22%, 74 KB/s], Decompressed: 1925
Downloaded: 1963 file(s) [attempted 1963/8459 = 23%, 314 KB/s], Decompressed: 1959
Downloaded: 2007 file(s) [attempted 2007/8459 = 23%, 270 KB/s], Decompressed: 2004
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 114 KB/s], Decompressed: 2045
Downloaded: 2086 file(s) [attempted 2086/8459 = 24%, 75 KB/s], Decompressed: 2083
Downloaded: 2124 file(s) [attempted 2124/8459 = 25%, 272 KB/s], Decompressed: 2120
Downloaded: 2158 file(s) [attempted 2158/8459 = 25%, 112 KB/s], Decompressed: 2154
Downloaded: 2202 file(s) [attempted 2202/8459 = 26%, 172 KB/s], Decompressed: 2195
Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 298 KB/s], Decompressed: 2237
Downloaded: 2284 file(s) [attempted 2284/8459 = 27%, 363 KB/s], Decompressed: 2281
Downloaded: 2321 file(s) [attempted 2321/8459 = 27%, 90 KB/s], Decompressed: 2315
Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 289 KB/s], Decompressed: 2349
Downloaded: 2394 file(s) [attempted 2394/8459 = 28%, 37 KB/s], Decompressed: 2387
Downloaded: 2435 file(s) [attempted 2435/8459 = 28%, 147 KB/s], Decompressed: 2432
Downloaded: 2473 file(s) [attempted 2473/8459 = 29%, 330 KB/s], Decompressed: 2469
Downloaded: 2514 file(s) [attempted 2514/8459 = 29%, 126 KB/s], Decompressed: 2510
Downloaded: 2555 file(s) [attempted 2555/8459 = 30%, 159 KB/s], Decompressed: 2551
Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 354 KB/s], Decompressed: 2589
Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 141 KB/s], Decompressed: 2623
Downloaded: 2666 file(s) [attempted 2666/8459 = 31%, 250 KB/s], Decompressed: 2657
Downloaded: 2705 file(s) [attempted 2705/8459 = 31%, 121 KB/s], Decompressed: 2702
Downloaded: 2748 file(s) [attempted 2748/8459 = 32%, 614 KB/s], Decompressed: 2743
Downloaded: 2784 file(s) [attempted 2784/8459 = 32%, 717 KB/s], Decompressed: 2777
Downloaded: 2818 file(s) [attempted 2818/8459 = 33%, 64 KB/s], Decompressed: 2811
Downloaded: 2859 file(s) [attempted 2859/8459 = 33%, 250 KB/s], Decompressed: 2856
Downloaded: 2900 file(s) [attempted 2900/8459 = 34%, 689 KB/s], Decompressed: 2897
Downloaded: 2938 file(s) [attempted 2938/8459 = 34%, 985 KB/s], Decompressed: 2932
Downloaded: 2975 file(s) [attempted 2975/8459 = 35%, 173 KB/s], Decompressed: 2965
Downloaded: 3013 file(s) [attempted 3013/8459 = 35%, 151 KB/s], Decompressed: 3007
Downloaded: 3054 file(s) [attempted 3054/8459 = 36%, 400 KB/s], Decompressed: 3051
Downloaded: 3099 file(s) [attempted 3099/8459 = 36%, 182 KB/s], Decompressed: 3096
Downloaded: 3140 file(s) [attempted 3140/8459 = 37%, 50 KB/s], Decompressed: 3133
Downloaded: 3174 file(s) [attempted 3174/8459 = 37%, 68 KB/s], Decompressed: 3167
Downloaded: 3215 file(s) [attempted 3215/8459 = 38%, 83 KB/s], Decompressed: 3212
Downloaded: 3254 file(s) [attempted 3254/8459 = 38%, 1390 KB/s], Decompressed: 3246
Downloaded: 3297 file(s) [attempted 3297/8459 = 38%, 164 KB/s], Decompressed: 3291
Downloaded: 3332 file(s) [attempted 3332/8459 = 39%, 768 KB/s], Decompressed: 3328
Downloaded: 3370 file(s) [attempted 3370/8459 = 39%, 154 KB/s], Decompressed: 3366
Downloaded: 3414 file(s) [attempted 3414/8459 = 40%, 353 KB/s], Decompressed: 3410
Downloaded: 3458 file(s) [attempted 3458/8459 = 40%, 84 KB/s], Decompressed: 3451
Downloaded: 3496 file(s) [attempted 3496/8459 = 41%, 1863 KB/s], Decompressed: 3486
Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 152 KB/s], Decompressed: 3527
Downloaded: 3571 file(s) [attempted 3571/8459 = 42%, 525 KB/s], Decompressed: 3568
Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 555 KB/s], Decompressed: 3602
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 428 KB/s], Decompressed: 3643
Downloaded: 3684 file(s) [attempted 3684/8459 = 43%, 695 KB/s], Decompressed: 3681
Downloaded: 3729 file(s) [attempted 3729/8459 = 44%, 740 KB/s], Decompressed: 3722
Downloaded: 3773 file(s) [attempted 3773/8459 = 44%, 286 KB/s], Decompressed: 3766
Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 383 KB/s], Decompressed: 3807
Downloaded: 3852 file(s) [attempted 3852/8459 = 45%, 40 KB/s], Decompressed: 3845
Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 535 KB/s], Decompressed: 3886
Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 225 KB/s], Decompressed: 3927
Downloaded: 3975 file(s) [attempted 3975/8459 = 46%, 350 KB/s], Decompressed: 3968
Downloaded: 4016 file(s) [attempted 4016/8459 = 47%, 435 KB/s], Decompressed: 4009
Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 1991 KB/s], Decompressed: 4054
Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 633 KB/s], Decompressed: 4095
Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 54 KB/s], Decompressed: 4136
Downloaded: 4174 file(s) [attempted 4174/8459 = 49%, 24 KB/s], Decompressed: 4168
Downloaded: 4211 file(s) [attempted 4211/8459 = 49%, 937 KB/s], Decompressed: 4208
Downloaded: 4250 file(s) [attempted 4250/8459 = 50%, 193 KB/s], Decompressed: 4245
Downloaded: 4290 file(s) [attempted 4290/8459 = 50%, 53 KB/s], Decompressed: 4283
Downloaded: 4328 file(s) [attempted 4328/8459 = 51%, 182 KB/s], Decompressed: 4317
Downloaded: 4366 file(s) [attempted 4366/8459 = 51%, 127 KB/s], Decompressed: 4362
Downloaded: 4403 file(s) [attempted 4403/8459 = 52%, 374 KB/s], Decompressed: 4399
Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 52 KB/s], Decompressed: 4441
Downloaded: 4482 file(s) [attempted 4482/8459 = 52%, 432 KB/s], Decompressed: 4475
Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 304 KB/s], Decompressed: 4502
Downloaded: 4564 file(s) [attempted 4564/8459 = 53%, 68 KB/s], Decompressed: 4553
Downloaded: 4600 file(s) [attempted 4600/8459 = 54%, 94 KB/s], Decompressed: 4595
Downloaded: 4636 file(s) [attempted 4636/8459 = 54%, 69 KB/s], Decompressed: 4632
Downloaded: 4674 file(s) [attempted 4674/8459 = 55%, 414 KB/s], Decompressed: 4670
Downloaded: 4714 file(s) [attempted 4714/8459 = 55%, 289 KB/s], Decompressed: 4711
Downloaded: 4754 file(s) [attempted 4754/8459 = 56%, 164 KB/s], Decompressed: 4745
Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 47 KB/s], Decompressed: 4790
Downloaded: 4831 file(s) [attempted 4831/8459 = 57%, 102 KB/s], Decompressed: 4824
Downloaded: 4865 file(s) [attempted 4865/8459 = 57%, 188 KB/s], Decompressed: 4861
Downloaded: 4909 file(s) [attempted 4909/8459 = 58%, 58 KB/s], Decompressed: 4906
Downloaded: 4954 file(s) [attempted 4954/8459 = 58%, 193 KB/s], Decompressed: 4947
Downloaded: 4988 file(s) [attempted 4988/8459 = 58%, 109 KB/s], Decompressed: 4981
Downloaded: 5033 file(s) [attempted 5033/8459 = 59%, 245 KB/s], Decompressed: 5029
Downloaded: 5063 file(s) [attempted 5063/8459 = 59%, 2731 KB/s], Decompressed: 5060
Downloaded: 5108 file(s) [attempted 5108/8459 = 60%, 448 KB/s], Decompressed: 5101
Downloaded: 5152 file(s) [attempted 5152/8459 = 60%, 126 KB/s], Decompressed: 5149
Downloaded: 5190 file(s) [attempted 5190/8459 = 61%, 102 KB/s], Decompressed: 5187
Downloaded: 5235 file(s) [attempted 5235/8459 = 61%, 968 KB/s], Decompressed: 5231
Downloaded: 5276 file(s) [attempted 5276/8459 = 62%, 252 KB/s], Decompressed: 5265
Downloaded: 5310 file(s) [attempted 5310/8459 = 62%, 24 KB/s], Decompressed: 5303
Downloaded: 5351 file(s) [attempted 5351/8459 = 63%, 650 KB/s], Decompressed: 5341
Downloaded: 5385 file(s) [attempted 5385/8459 = 63%, 75 KB/s], Decompressed: 5382
Downloaded: 5430 file(s) [attempted 5430/8459 = 64%, 65 KB/s], Decompressed: 5426
Downloaded: 5474 file(s) [attempted 5474/8459 = 64%, 148 KB/s], Decompressed: 5471
Downloaded: 5515 file(s) [attempted 5515/8459 = 65%, 431 KB/s], Decompressed: 5508
Downloaded: 5549 file(s) [attempted 5549/8459 = 65%, 320 KB/s], Decompressed: 5543
Downloaded: 5590 file(s) [attempted 5590/8459 = 66%, 1709 KB/s], Decompressed: 5587
Downloaded: 5635 file(s) [attempted 5635/8459 = 66%, 561 KB/s], Decompressed: 5632
Downloaded: 5676 file(s) [attempted 5676/8459 = 67%, 50 KB/s], Decompressed: 5673
Downloaded: 5721 file(s) [attempted 5721/8459 = 67%, 217 KB/s], Decompressed: 5714
Downloaded: 5751 file(s) [attempted 5751/8459 = 67%, 456 KB/s], Decompressed: 5748
Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 182 KB/s], Decompressed: 5786
Downloaded: 5833 file(s) [attempted 5833/8459 = 68%, 85 KB/s], Decompressed: 5830
Downloaded: 5878 file(s) [attempted 5878/8459 = 69%, 157 KB/s], Decompressed: 5875
Downloaded: 5916 file(s) [attempted 5916/8459 = 69%, 74 KB/s], Decompressed: 5909
Downloaded: 5953 file(s) [attempted 5953/8459 = 70%, 516 KB/s], Decompressed: 5946
Downloaded: 5994 file(s) [attempted 5994/8459 = 70%, 237 KB/s], Decompressed: 5987
Downloaded: 6032 file(s) [attempted 6032/8459 = 71%, 388 KB/s], Decompressed: 6025
Downloaded: 6075 file(s) [attempted 6075/8459 = 71%, 82 KB/s], Decompressed: 6066
Downloaded: 6111 file(s) [attempted 6111/8459 = 72%, 283 KB/s], Decompressed: 6101
Downloaded: 6152 file(s) [attempted 6152/8459 = 72%, 372 KB/s], Decompressed: 6148
Downloaded: 6191 file(s) [attempted 6191/8459 = 73%, 70 KB/s], Decompressed: 6179
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 142 KB/s], Decompressed: 6227
Downloaded: 6275 file(s) [attempted 6275/8459 = 74%, 171 KB/s], Decompressed: 6261
Downloaded: 6309 file(s) [attempted 6309/8459 = 74%, 500 KB/s], Decompressed: 6306
Downloaded: 6354 file(s) [attempted 6354/8459 = 75%, 1011 KB/s], Decompressed: 6347
Downloaded: 6388 file(s) [attempted 6388/8459 = 75%, 432 KB/s], Decompressed: 6384
Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 158 KB/s], Decompressed: 6431
Downloaded: 6470 file(s) [attempted 6470/8459 = 76%, 21 KB/s], Decompressed: 6463
Downloaded: 6511 file(s) [attempted 6511/8459 = 76%, 80 KB/s], Decompressed: 6508
Downloaded: 6552 file(s) [attempted 6552/8459 = 77%, 109 KB/s], Decompressed: 6545
Downloaded: 6590 file(s) [attempted 6590/8459 = 77%, 262 KB/s], Decompressed: 6580
Downloaded: 6631 file(s) [attempted 6631/8459 = 78%, 367 KB/s], Decompressed: 6617
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 78 KB/s], Decompressed: 6662
Downloaded: 6710 file(s) [attempted 6710/8459 = 79%, 153 KB/s], Decompressed: 6703
Downloaded: 6754 file(s) [attempted 6754/8459 = 79%, 298 KB/s], Decompressed: 6751
Downloaded: 6792 file(s) [attempted 6792/8459 = 80%, 363 KB/s], Decompressed: 6788
Downloaded: 6833 file(s) [attempted 6833/8459 = 80%, 321 KB/s], Decompressed: 6826
Downloaded: 6868 file(s) [attempted 6868/8459 = 81%, 138 KB/s], Decompressed: 6864
Downloaded: 6911 file(s) [attempted 6911/8459 = 81%, 561 KB/s], Decompressed: 6905
Downloaded: 6954 file(s) [attempted 6954/8459 = 82%, 46 KB/s], Decompressed: 6949
Downloaded: 6990 file(s) [attempted 6990/8459 = 82%, 93 KB/s], Decompressed: 6980
Downloaded: 7024 file(s) [attempted 7024/8459 = 83%, 692 KB/s], Decompressed: 7018
Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 318 KB/s], Decompressed: 7062
Downloaded: 7107 file(s) [attempted 7107/8459 = 84%, 269 KB/s], Decompressed: 7102
Downloaded: 7145 file(s) [attempted 7145/8459 = 84%, 1362 KB/s], Decompressed: 7141
Downloaded: 7182 file(s) [attempted 7182/8459 = 84%, 123 KB/s], Decompressed: 7178
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 747 KB/s], Decompressed: 7219
Downloaded: 7261 file(s) [attempted 7261/8459 = 85%, 124 KB/s], Decompressed: 7257
Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 138 KB/s], Decompressed: 7302
Downloaded: 7346 file(s) [attempted 7346/8459 = 86%, 316 KB/s], Decompressed: 7343
Downloaded: 7382 file(s) [attempted 7382/8459 = 87%, 60 KB/s], Decompressed: 7374
Downloaded: 7425 file(s) [attempted 7425/8459 = 87%, 23 KB/s], Decompressed: 7415
Downloaded: 7462 file(s) [attempted 7462/8459 = 88%, 940 KB/s], Decompressed: 7456
Downloaded: 7504 file(s) [attempted 7504/8459 = 88%, 432 KB/s], Decompressed: 7500
Downloaded: 7543 file(s) [attempted 7543/8459 = 89%, 162 KB/s], Decompressed: 7534
Downloaded: 7584 file(s) [attempted 7584/8459 = 89%, 43 KB/s], Decompressed: 7575
Downloaded: 7620 file(s) [attempted 7620/8459 = 90%, 154 KB/s], Decompressed: 7610
Downloaded: 7658 file(s) [attempted 7658/8459 = 90%, 113 KB/s], Decompressed: 7651
Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 58 KB/s], Decompressed: 7685
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 177 KB/s], Decompressed: 7733
Downloaded: 7777 file(s) [attempted 7777/8459 = 91%, 1487 KB/s], Decompressed: 7770
Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 44 KB/s], Decompressed: 7812
Downloaded: 7850 file(s) [attempted 7850/8459 = 92%, 79 KB/s], Decompressed: 7842
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 58 KB/s], Decompressed: 7883
Downloaded: 7938 file(s) [attempted 7938/8459 = 93%, 315 KB/s], Decompressed: 7931
Downloaded: 7983 file(s) [attempted 7983/8459 = 94%, 290 KB/s], Decompressed: 7976
Downloaded: 8014 file(s) [attempted 8014/8459 = 94%, 155 KB/s], Decompressed: 8010
Downloaded: 8055 file(s) [attempted 8055/8459 = 95%, 106 KB/s], Decompressed: 8051
Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 106 KB/s], Decompressed: 8089
Downloaded: 8137 file(s) [attempted 8137/8459 = 96%, 65 KB/s], Decompressed: 8133
Downloaded: 8176 file(s) [attempted 8176/8459 = 96%, 49 KB/s], Decompressed: 8154
Downloaded: 8209 file(s) [attempted 8209/8459 = 97%, 761 KB/s], Decompressed: 8205
Downloaded: 8247 file(s) [attempted 8247/8459 = 97%, 188 KB/s], Decompressed: 8243
Downloaded: 8289 file(s) [attempted 8289/8459 = 97%, 486 KB/s], Decompressed: 8280
Downloaded: 8330 file(s) [attempted 8330/8459 = 98%, 531 KB/s], Decompressed: 8325
Downloaded: 8363 file(s) [attempted 8363/8459 = 98%, 317 KB/s], Decompressed: 8356
Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 321 KB/s], Decompressed: 8397
Downloaded: 8442 file(s) [attempted 8442/8459 = 99%, 885 KB/s], Decompressed: 8438
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 885 KB/s], Decompressed: 8455
$ lake build
exit_code=Some(1) duration_ms=453609
stdout:
✔ [753/764] Built Iut.Foundations.RealLineCopy (25s)
✔ [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.5s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.4s)
✔ [763/772] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.6s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.6s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (31s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (2.0s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.8s)
✔ [3393/3398] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (86s)
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 (21s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.7s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.3s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.4s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.6s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (25s)
warning: Iut/Stage1/IUTStage1Theorem311.lean:4518:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4523:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4655:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4687:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4692:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4735:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4789:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4824:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4829:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4961:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4995:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5000:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5138:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5172:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5177:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5320:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5352:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5357:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5470:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:7525:6: try 'simp' instead of 'simpa'
Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15277:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15618:4: try 'simp' instead of 'simpa'
Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:16875:4: try 'simp' instead of 'simpa'
Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:17353:5: unused variable `targetSource`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:18439:5: unused variable `data`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:21472:5: unused variable `obligations`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
✖ [3418/3425] Building Iut.Stage1.IUTStage1StepXI (173s)
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=1476
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-1371-source
Cloning into '/var/lib/apodeixis/repos/job-1371-source'...
git_checkout exit 0
git checkout 829a0be0cbe55c128a85e3e7394abdc832dbe126
Note: switching to '829a0be0cbe55c128a85e3e7394abdc832dbe126'. 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 829a0be Project final evidence from local arithmetic
lake_cache exit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache Decompressed 8459 file(s) Already decompressed 8459 file(s)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0 Downloaded: 14 file(s) [attempted 14/8459 = 0%, 2 KB/s], Decompressed: 13 Downloaded: 37 file(s) [attempted 37/8459 = 0%, 17 KB/s], Decompressed: 30 Downloaded: 63 file(s) [attempted 63/8459 = 0%, 47 KB/s], Decompressed: 61 Downloaded: 83 file(s) [attempted 83/8459 = 0%, 158 KB/s], Decompressed: 79 Downloaded: 112 file(s) [attempted 112/8459 = 1%, 73 KB/s], Decompressed: 97 Downloaded: 138 file(s) [attempted 138/8459 = 1%, 347 KB/s], Decompressed: 134 Downloaded: 179 file(s) [attempted 179/8459 = 2%, 357 KB/s], Decompressed: 176 Downloaded: 220 file(s) [attempted 220/8459 = 2%, 98 KB/s], Decompressed: 216 Downloaded: 262 file(s) [attempted 262/8459 = 3%, 44 KB/s], Decompressed: 258 Downloaded: 299 file(s) [attempted 299/8459 = 3%, 172 KB/s], Decompressed: 292 Downloaded: 340 file(s) [attempted 340/8459 = 4%, 90 KB/s], Decompressed: 337 Downloaded: 372 file(s) [attempted 372/8459 = 4%, 110 KB/s], Decompressed: 367 Downloaded: 404 file(s) [attempted 404/8459 = 4%, 80 KB/s], Decompressed: 398 Downloaded: 446 file(s) [attempted 446/8459 = 5%, 233 KB/s], Decompressed: 439 Downloaded: 491 file(s) [attempted 491/8459 = 5%, 261 KB/s], Decompressed: 484 Downloaded: 530 file(s) [attempted 530/8459 = 6%, 448 KB/s], Decompressed: 525 Downloaded: 565 file(s) [attempted 565/8459 = 6%, 77 KB/s], Decompressed: 552 Downloaded: 600 file(s) [attempted 600/8459 = 7%, 814 KB/s], Decompressed: 593 Downloaded: 641 file(s) [attempted 641/8459 = 7%, 246 KB/s], Decompressed: 638 Downloaded: 686 file(s) [attempted 686/8459 = 8%, 255 KB/s], Decompressed: 679 Downloaded: 725 file(s) [attempted 725/8459 = 8%, 86 KB/s], Decompressed: 710 Downloaded: 761 file(s) [attempted 761/8459 = 8%, 167 KB/s], Decompressed: 754 Downloaded: 792 file(s) [attempted 792/8459 = 9%, 113 KB/s], Decompressed: 789 Downloaded: 837 file(s) [attempted 837/8459 = 9%, 75 KB/s], Decompressed: 833 Downloaded: 878 file(s) [attempted 878/8459 = 10%, 261 KB/s], Decompressed: 874 Downloaded: 922 file(s) [attempted 922/8459 = 10%, 462 KB/s], Decompressed: 919 Downloaded: 967 file(s) [attempted 967/8459 = 11%, 205 KB/s], Decompressed: 960 Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 172 KB/s], Decompressed: 994 Downloaded: 1036 file(s) [attempted 1036/8459 = 12%, 137 KB/s], Decompressed: 1028 Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 269 KB/s], Decompressed: 1073 Downloaded: 1124 file(s) [attempted 1124/8459 = 13%, 374 KB/s], Decompressed: 1121 Downloaded: 1172 file(s) [attempted 1172/8459 = 13%, 826 KB/s], Decompressed: 1165 Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 366 KB/s], Decompressed: 1213 Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 639 KB/s], Decompressed: 1254 Downloaded: 1293 file(s) [attempted 1293/8459 = 15%, 327 KB/s], Decompressed: 1289 Downloaded: 1326 file(s) [attempted 1326/8459 = 15%, 154 KB/s], Decompressed: 1319 Downloaded: 1367 file(s) [attempted 1367/8459 = 16%, 131 KB/s], Decompressed: 1364 Downloaded: 1415 file(s) [attempted 1415/8459 = 16%, 224 KB/s], Decompressed: 1408 Downloaded: 1463 file(s) [attempted 1463/8459 = 17%, 105 KB/s], Decompressed: 1456 Downloaded: 1501 file(s) [attempted 1501/8459 = 17%, 236 KB/s], Decompressed: 1494 Downloaded: 1539 file(s) [attempted 1539/8459 = 18%, 155 KB/s], Decompressed: 1535 Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 414 KB/s], Decompressed: 1573 Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 195 KB/s], Decompressed: 1617 Downloaded: 1662 file(s) [attempted 1662/8459 = 19%, 337 KB/s], Decompressed: 1658 Downloaded: 1699 file(s) [attempted 1699/8459 = 20%, 119 KB/s], Decompressed: 1692 Downloaded: 1738 file(s) [attempted 1738/8459 = 20%, 322 KB/s], Decompressed: 1733 Downloaded: 1772 file(s) [attempted 1772/8459 = 20%, 135 KB/s], Decompressed: 1764 Downloaded: 1814 file(s) [attempted 1814/8459 = 21%, 161 KB/s], Decompressed: 1805 Downloaded: 1857 file(s) [attempted 1857/8459 = 21%, 24 KB/s], Decompressed: 1850 Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 731 KB/s], Decompressed: 1887 Downloaded: 1932 file(s) [attempted 1932/8459 = 22%, 74 KB/s], Decompressed: 1925 Downloaded: 1963 file(s) [attempted 1963/8459 = 23%, 314 KB/s], Decompressed: 1959 Downloaded: 2007 file(s) [attempted 2007/8459 = 23%, 270 KB/s], Decompressed: 2004 Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 114 KB/s], Decompressed: 2045 Downloaded: 2086 file(s) [attempted 2086/8459 = 24%, 75 KB/s], Decompressed: 2083 Downloaded: 2124 file(s) [attempted 2124/8459 = 25%, 272 KB/s], Decompressed: 2120 Downloaded: 2158 file(s) [attempted 2158/8459 = 25%, 112 KB/s], Decompressed: 2154 Downloaded: 2202 file(s) [attempted 2202/8459 = 26%, 172 KB/s], Decompressed: 2195 Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 298 KB/s], Decompressed: 2237 Downloaded: 2284 file(s) [attempted 2284/8459 = 27%, 363 KB/s], Decompressed: 2281 Downloaded: 2321 file(s) [attempted 2321/8459 = 27%, 90 KB/s], Decompressed: 2315 Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 289 KB/s], Decompressed: 2349 Downloaded: 2394 file(s) [attempted 2394/8459 = 28%, 37 KB/s], Decompressed: 2387 Downloaded: 2435 file(s) [attempted 2435/8459 = 28%, 147 KB/s], Decompressed: 2432 Downloaded: 2473 file(s) [attempted 2473/8459 = 29%, 330 KB/s], Decompressed: 2469 Downloaded: 2514 file(s) [attempted 2514/8459 = 29%, 126 KB/s], Decompressed: 2510 Downloaded: 2555 file(s) [attempted 2555/8459 = 30%, 159 KB/s], Decompressed: 2551 Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 354 KB/s], Decompressed: 2589 Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 141 KB/s], Decompressed: 2623 Downloaded: 2666 file(s) [attempted 2666/8459 = 31%, 250 KB/s], Decompressed: 2657 Downloaded: 2705 file(s) [attempted 2705/8459 = 31%, 121 KB/s], Decompressed: 2702 Downloaded: 2748 file(s) [attempted 2748/8459 = 32%, 614 KB/s], Decompressed: 2743 Downloaded: 2784 file(s) [attempted 2784/8459 = 32%, 717 KB/s], Decompressed: 2777 Downloaded: 2818 file(s) [attempted 2818/8459 = 33%, 64 KB/s], Decompressed: 2811 Downloaded: 2859 file(s) [attempted 2859/8459 = 33%, 250 KB/s], Decompressed: 2856 Downloaded: 2900 file(s) [attempted 2900/8459 = 34%, 689 KB/s], Decompressed: 2897 Downloaded: 2938 file(s) [attempted 2938/8459 = 34%, 985 KB/s], Decompressed: 2932 Downloaded: 2975 file(s) [attempted 2975/8459 = 35%, 173 KB/s], Decompressed: 2965 Downloaded: 3013 file(s) [attempted 3013/8459 = 35%, 151 KB/s], Decompressed: 3007 Downloaded: 3054 file(s) [attempted 3054/8459 = 36%, 400 KB/s], Decompressed: 3051 Downloaded: 3099 file(s) [attempted 3099/8459 = 36%, 182 KB/s], Decompressed: 3096 Downloaded: 3140 file(s) [attempted 3140/8459 = 37%, 50 KB/s], Decompressed: 3133 Downloaded: 3174 file(s) [attempted 3174/8459 = 37%, 68 KB/s], Decompressed: 3167 Downloaded: 3215 file(s) [attempted 3215/8459 = 38%, 83 KB/s], Decompressed: 3212 Downloaded: 3254 file(s) [attempted 3254/8459 = 38%, 1390 KB/s], Decompressed: 3246 Downloaded: 3297 file(s) [attempted 3297/8459 = 38%, 164 KB/s], Decompressed: 3291 Downloaded: 3332 file(s) [attempted 3332/8459 = 39%, 768 KB/s], Decompressed: 3328 Downloaded: 3370 file(s) [attempted 3370/8459 = 39%, 154 KB/s], Decompressed: 3366 Downloaded: 3414 file(s) [attempted 3414/8459 = 40%, 353 KB/s], Decompressed: 3410 Downloaded: 3458 file(s) [attempted 3458/8459 = 40%, 84 KB/s], Decompressed: 3451 Downloaded: 3496 file(s) [attempted 3496/8459 = 41%, 1863 KB/s], Decompressed: 3486 Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 152 KB/s], Decompressed: 3527 Downloaded: 3571 file(s) [attempted 3571/8459 = 42%, 525 KB/s], Decompressed: 3568 Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 555 KB/s], Decompressed: 3602 Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 428 KB/s], Decompressed: 3643 Downloaded: 3684 file(s) [attempted 3684/8459 = 43%, 695 KB/s], Decompressed: 3681 Downloaded: 3729 file(s) [attempted 3729/8459 = 44%, 740 KB/s], Decompressed: 3722 Downloaded: 3773 file(s) [attempted 3773/8459 = 44%, 286 KB/s], Decompressed: 3766 Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 383 KB/s], Decompressed: 3807 Downloaded: 3852 file(s) [attempted 3852/8459 = 45%, 40 KB/s], Decompressed: 3845 Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 535 KB/s], Decompressed: 3886 Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 225 KB/s], Decompressed: 3927 Downloaded: 3975 file(s) [attempted 3975/8459 = 46%, 350 KB/s], Decompressed: 3968 Downloaded: 4016 file(s) [attempted 4016/8459 = 47%, 435 KB/s], Decompressed: 4009 Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 1991 KB/s], Decompressed: 4054 Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 633 KB/s], Decompressed: 4095 Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 54 KB/s], Decompressed: 4136 Downloaded: 4174 file(s) [attempted 4174/8459 = 49%, 24 KB/s], Decompressed: 4168 Downloaded: 4211 file(s) [attempted 4211/8459 = 49%, 937 KB/s], Decompressed: 4208 Downloaded: 4250 file(s) [attempted 4250/8459 = 50%, 193 KB/s], Decompressed: 4245 Downloaded: 4290 file(s) [attempted 4290/8459 = 50%, 53 KB/s], Decompressed: 4283 Downloaded: 4328 file(s) [attempted 4328/8459 = 51%, 182 KB/s], Decompressed: 4317 Downloaded: 4366 file(s) [attempted 4366/8459 = 51%, 127 KB/s], Decompressed: 4362 Downloaded: 4403 file(s) [attempted 4403/8459 = 52%, 374 KB/s], Decompressed: 4399 Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 52 KB/s], Decompressed: 4441 Downloaded: 4482 file(s) [attempted 4482/8459 = 52%, 432 KB/s], Decompressed: 4475 Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 304 KB/s], Decompressed: 4502 Downloaded: 4564 file(s) [attempted 4564/8459 = 53%, 68 KB/s], Decompressed: 4553 Downloaded: 4600 file(s) [attempted 4600/8459 = 54%, 94 KB/s], Decompressed: 4595 Downloaded: 4636 file(s) [attempted 4636/8459 = 54%, 69 KB/s], Decompressed: 4632 Downloaded: 4674 file(s) [attempted 4674/8459 = 55%, 414 KB/s], Decompressed: 4670 Downloaded: 4714 file(s) [attempted 4714/8459 = 55%, 289 KB/s], Decompressed: 4711 Downloaded: 4754 file(s) [attempted 4754/8459 = 56%, 164 KB/s], Decompressed: 4745 Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 47 KB/s], Decompressed: 4790 Downloaded: 4831 file(s) [attempted 4831/8459 = 57%, 102 KB/s], Decompressed: 4824 Downloaded: 4865 file(s) [attempted 4865/8459 = 57%, 188 KB/s], Decompressed: 4861 Downloaded: 4909 file(s) [attempted 4909/8459 = 58%, 58 KB/s], Decompressed: 4906 Downloaded: 4954 file(s) [attempted 4954/8459 = 58%, 193 KB/s], Decompressed: 4947 Downloaded: 4988 file(s) [attempted 4988/8459 = 58%, 109 KB/s], Decompressed: 4981 Downloaded: 5033 file(s) [attempted 5033/8459 = 59%, 245 KB/s], Decompressed: 5029 Downloaded: 5063 file(s) [attempted 5063/8459 = 59%, 2731 KB/s], Decompressed: 5060 Downloaded: 5108 file(s) [attempted 5108/8459 = 60%, 448 KB/s], Decompressed: 5101 Downloaded: 5152 file(s) [attempted 5152/8459 = 60%, 126 KB/s], Decompressed: 5149 Downloaded: 5190 file(s) [attempted 5190/8459 = 61%, 102 KB/s], Decompressed: 5187 Downloaded: 5235 file(s) [attempted 5235/8459 = 61%, 968 KB/s], Decompressed: 5231 Downloaded: 5276 file(s) [attempted 5276/8459 = 62%, 252 KB/s], Decompressed: 5265 Downloaded: 5310 file(s) [attempted 5310/8459 = 62%, 24 KB/s], Decompressed: 5303 Downloaded: 5351 file(s) [attempted 5351/8459 = 63%, 650 KB/s], Decompressed: 5341 Downloaded: 5385 file(s) [attempted 5385/8459 = 63%, 75 KB/s], Decompressed: 5382 Downloaded: 5430 file(s) [attempted 5430/8459 = 64%, 65 KB/s], Decompressed: 5426 Downloaded: 5474 file(s) [attempted 5474/8459 = 64%, 148 KB/s], Decompressed: 5471 Downloaded: 5515 file(s) [attempted 5515/8459 = 65%, 431 KB/s], Decompressed: 5508 Downloaded: 5549 file(s) [attempted 5549/8459 = 65%, 320 KB/s], Decompressed: 5543 Downloaded: 5590 file(s) [attempted 5590/8459 = 66%, 1709 KB/s], Decompressed: 5587 Downloaded: 5635 file(s) [attempted 5635/8459 = 66%, 561 KB/s], Decompressed: 5632 Downloaded: 5676 file(s) [attempted 5676/8459 = 67%, 50 KB/s], Decompressed: 5673 Downloaded: 5721 file(s) [attempted 5721/8459 = 67%, 217 KB/s], Decompressed: 5714 Downloaded: 5751 file(s) [attempted 5751/8459 = 67%, 456 KB/s], Decompressed: 5748 Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 182 KB/s], Decompressed: 5786 Downloaded: 5833 file(s) [attempted 5833/8459 = 68%, 85 KB/s], Decompressed: 5830 Downloaded: 5878 file(s) [attempted 5878/8459 = 69%, 157 KB/s], Decompressed: 5875 Downloaded: 5916 file(s) [attempted 5916/8459 = 69%, 74 KB/s], Decompressed: 5909 Downloaded: 5953 file(s) [attempted 5953/8459 = 70%, 516 KB/s], Decompressed: 5946 Downloaded: 5994 file(s) [attempted 5994/8459 = 70%, 237 KB/s], Decompressed: 5987 Downloaded: 6032 file(s) [attempted 6032/8459 = 71%, 388 KB/s], Decompressed: 6025 Downloaded: 6075 file(s) [attempted 6075/8459 = 71%, 82 KB/s], Decompressed: 6066 Downloaded: 6111 file(s) [attempted 6111/8459 = 72%, 283 KB/s], Decompressed: 6101 Downloaded: 6152 file(s) [attempted 6152/8459 = 72%, 372 KB/s], Decompressed: 6148 Downloaded: 6191 file(s) [attempted 6191/8459 = 73%, 70 KB/s], Decompressed: 6179 Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 142 KB/s], Decompressed: 6227 Downloaded: 6275 file(s) [attempted 6275/8459 = 74%, 171 KB/s], Decompressed: 6261 Downloaded: 6309 file(s) [attempted 6309/8459 = 74%, 500 KB/s], Decompressed: 6306 Downloaded: 6354 file(s) [attempted 6354/8459 = 75%, 1011 KB/s], Decompressed: 6347 Downloaded: 6388 file(s) [attempted 6388/8459 = 75%, 432 KB/s], Decompressed: 6384 Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 158 KB/s], Decompressed: 6431 Downloaded: 6470 file(s) [attempted 6470/8459 = 76%, 21 KB/s], Decompressed: 6463 Downloaded: 6511 file(s) [attempted 6511/8459 = 76%, 80 KB/s], Decompressed: 6508 Downloaded: 6552 file(s) [attempted 6552/8459 = 77%, 109 KB/s], Decompressed: 6545 Downloaded: 6590 file(s) [attempted 6590/8459 = 77%, 262 KB/s], Decompressed: 6580 Downloaded: 6631 file(s) [attempted 6631/8459 = 78%, 367 KB/s], Decompressed: 6617 Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 78 KB/s], Decompressed: 6662 Downloaded: 6710 file(s) [attempted 6710/8459 = 79%, 153 KB/s], Decompressed: 6703 Downloaded: 6754 file(s) [attempted 6754/8459 = 79%, 298 KB/s], Decompressed: 6751 Downloaded: 6792 file(s) [attempted 6792/8459 = 80%, 363 KB/s], Decompressed: 6788 Downloaded: 6833 file(s) [attempted 6833/8459 = 80%, 321 KB/s], Decompressed: 6826 Downloaded: 6868 file(s) [attempted 6868/8459 = 81%, 138 KB/s], Decompressed: 6864 Downloaded: 6911 file(s) [attempted 6911/8459 = 81%, 561 KB/s], Decompressed: 6905 Downloaded: 6954 file(s) [attempted 6954/8459 = 82%, 46 KB/s], Decompressed: 6949 Downloaded: 6990 file(s) [attempted 6990/8459 = 82%, 93 KB/s], Decompressed: 6980 Downloaded: 7024 file(s) [attempted 7024/8459 = 83%, 692 KB/s], Decompressed: 7018 Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 318 KB/s], Decompressed: 7062 Downloaded: 7107 file(s) [attempted 7107/8459 = 84%, 269 KB/s], Decompressed: 7102 Downloaded: 7145 file(s) [attempted 7145/8459 = 84%, 1362 KB/s], Decompressed: 7141 Downloaded: 7182 file(s) [attempted 7182/8459 = 84%, 123 KB/s], Decompressed: 7178 Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 747 KB/s], Decompressed: 7219 Downloaded: 7261 file(s) [attempted 7261/8459 = 85%, 124 KB/s], Decompressed: 7257 Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 138 KB/s], Decompressed: 7302 Downloaded: 7346 file(s) [attempted 7346/8459 = 86%, 316 KB/s], Decompressed: 7343 Downloaded: 7382 file(s) [attempted 7382/8459 = 87%, 60 KB/s], Decompressed: 7374 Downloaded: 7425 file(s) [attempted 7425/8459 = 87%, 23 KB/s], Decompressed: 7415 Downloaded: 7462 file(s) [attempted 7462/8459 = 88%, 940 KB/s], Decompressed: 7456 Downloaded: 7504 file(s) [attempted 7504/8459 = 88%, 432 KB/s], Decompressed: 7500 Downloaded: 7543 file(s) [attempted 7543/8459 = 89%, 162 KB/s], Decompressed: 7534 Downloaded: 7584 file(s) [attempted 7584/8459 = 89%, 43 KB/s], Decompressed: 7575 Downloaded: 7620 file(s) [attempted 7620/8459 = 90%, 154 KB/s], Decompressed: 7610 Downloaded: 7658 file(s) [attempted 7658/8459 = 90%, 113 KB/s], Decompressed: 7651 Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 58 KB/s], Decompressed: 7685 Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 177 KB/s], Decompressed: 7733 Downloaded: 7777 file(s) [attempted 7777/8459 = 91%, 1487 KB/s], Decompressed: 7770 Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 44 KB/s], Decompressed: 7812 Downloaded: 7850 file(s) [attempted 7850/8459 = 92%, 79 KB/s], Decompressed: 7842 Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 58 KB/s], Decompressed: 7883 Downloaded: 7938 file(s) [attempted 7938/8459 = 93%, 315 KB/s], Decompressed: 7931 Downloaded: 7983 file(s) [attempted 7983/8459 = 94%, 290 KB/s], Decompressed: 7976 Downloaded: 8014 file(s) [attempted 8014/8459 = 94%, 155 KB/s], Decompressed: 8010 Downloaded: 8055 file(s) [attempted 8055/8459 = 95%, 106 KB/s], Decompressed: 8051 Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 106 KB/s], Decompressed: 8089 Downloaded: 8137 file(s) [attempted 8137/8459 = 96%, 65 KB/s], Decompressed: 8133 Downloaded: 8176 file(s) [attempted 8176/8459 = 96%, 49 KB/s], Decompressed: 8154 Downloaded: 8209 file(s) [attempted 8209/8459 = 97%, 761 KB/s], Decompressed: 8205 Downloaded: 8247 file(s) [attempted 8247/8459 = 97%, 188 KB/s], Decompressed: 8243 Downloaded: 8289 file(s) [attempted 8289/8459 = 97%, 486 KB/s], Decompressed: 8280 Downloaded: 8330 file(s) [attempted 8330/8459 = 98%, 531 KB/s], Decompressed: 8325 Downloaded: 8363 file(s) [attempted 8363/8459 = 98%, 317 KB/s], Decompressed: 8356 Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 321 KB/s], Decompressed: 8397 Downloaded: 8442 file(s) [attempted 8442/8459 = 99%, 885 KB/s], Decompressed: 8438 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 885 KB/s], Decompressed: 8455
lean_checker exit 1
lake build
✔ [753/764] Built Iut.Foundations.RealLineCopy (25s)
✔ [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.5s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.4s)
✔ [763/772] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.6s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.6s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (31s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (2.0s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.8s)
✔ [3393/3398] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (86s)
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 (21s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (16s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.7s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.3s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.4s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.6s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (25s)
warning: Iut/Stage1/IUTStage1Theorem311.lean:4518:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4523:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4655:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4687:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4692:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4735:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4789:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4824:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4829:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4961:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4995:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5000:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5138:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5172:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5177:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5320:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5352:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5357:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5470:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:7525:6: try 'simp' instead of 'simpa'
Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15277:100: This line exceeds the 100 character limit, please shorten it!
Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15618:4: try 'simp' instead of 'simpa'
Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:16875:4: try 'simp' instead of 'simpa'
Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:17353:5: unused variable `targetSource`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:18439:5: unused variable `data`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:21472:5: unused variable `obligations`
Note: This linter can be disabled with `set_option linter.unusedVariables false`
✖ [3418/3425] Building Iut.Stage1.IUTStage1StepXI (173s)
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`