Verification run

Run 1063

promachina/iut-leanbranch mastertriggered via poller

failedcommit 2d1393720a87toolchain lean-v4-30-0prover leantook 23m 17s · finished 9w 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)

Open project

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

(no log excerpt)

Command runs

git_cloneexit 0duration 4s · created 7/13/2026, 6:24:38 AM

git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1364-source

Cloning into '/var/lib/apodeixis/repos/job-1364-source'...

git_checkoutexit 0duration 174 ms · created 7/13/2026, 6:24:38 AM

git checkout 2d1393720a875ec8d472de60c2f4b8dd4e75b40e

Note: switching to '2d1393720a875ec8d472de60c2f4b8dd4e75b40e'.

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 2d13937 Lower product hull calibration surface

lake_cacheexit 0duration 41s · created 7/13/2026, 6:24:38 AM

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: 15 file(s) [attempted 15/8459 = 0%, 5 KB/s], Decompressed: 13
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 13 KB/s], Decompressed: 36
Downloaded: 64 file(s) [attempted 64/8459 = 0%, 48 KB/s], Decompressed: 61
Downloaded: 93 file(s) [attempted 93/8459 = 1%, 64 KB/s], Decompressed: 85
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 254 KB/s], Decompressed: 120
Downloaded: 155 file(s) [attempted 155/8459 = 1%, 83 KB/s], Decompressed: 141
Downloaded: 189 file(s) [attempted 189/8459 = 2%, 561 KB/s], Decompressed: 141
Downloaded: 223 file(s) [attempted 223/8459 = 2%, 217 KB/s], Decompressed: 141
Downloaded: 268 file(s) [attempted 268/8459 = 3%, 1320 KB/s], Decompressed: 144
Downloaded: 309 file(s) [attempted 309/8459 = 3%, 24 KB/s], Decompressed: 282
Downloaded: 350 file(s) [attempted 350/8459 = 4%, 296 KB/s], Decompressed: 282
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 82 KB/s], Decompressed: 381
Downloaded: 422 file(s) [attempted 422/8459 = 4%, 329 KB/s], Decompressed: 419
Downloaded: 460 file(s) [attempted 460/8459 = 5%, 688 KB/s], Decompressed: 456
Downloaded: 501 file(s) [attempted 501/8459 = 5%, 836 KB/s], Decompressed: 494
Downloaded: 542 file(s) [attempted 542/8459 = 6%, 71 KB/s], Decompressed: 494
Downloaded: 576 file(s) [attempted 576/8459 = 6%, 286 KB/s], Decompressed: 497
Downloaded: 615 file(s) [attempted 615/8459 = 7%, 79 KB/s], Decompressed: 610
Downloaded: 658 file(s) [attempted 658/8459 = 7%, 86 KB/s], Decompressed: 627
Downloaded: 696 file(s) [attempted 696/8459 = 8%, 100 KB/s], Decompressed: 627
Downloaded: 737 file(s) [attempted 737/8459 = 8%, 452 KB/s], Decompressed: 634
Downloaded: 778 file(s) [attempted 778/8459 = 9%, 68 KB/s], Decompressed: 775
Downloaded: 816 file(s) [attempted 816/8459 = 9%, 512 KB/s], Decompressed: 812
Downloaded: 857 file(s) [attempted 857/8459 = 10%, 204 KB/s], Decompressed: 854
Downloaded: 895 file(s) [attempted 895/8459 = 10%, 1215 KB/s], Decompressed: 891
Downloaded: 931 file(s) [attempted 931/8459 = 11%, 163 KB/s], Decompressed: 925
Downloaded: 973 file(s) [attempted 973/8459 = 11%, 1558 KB/s], Decompressed: 970
Downloaded: 1012 file(s) [attempted 1012/8459 = 11%, 173 KB/s], Decompressed: 1008
Downloaded: 1054 file(s) [attempted 1054/8459 = 12%, 348 KB/s], Decompressed: 1045
Downloaded: 1086 file(s) [attempted 1086/8459 = 12%, 469 KB/s], Decompressed: 1080
Downloaded: 1127 file(s) [attempted 1127/8459 = 13%, 693 KB/s], Decompressed: 1121
Downloaded: 1169 file(s) [attempted 1169/8459 = 13%, 1640 KB/s], Decompressed: 1165
Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 180 KB/s], Decompressed: 1199
Downloaded: 1247 file(s) [attempted 1247/8459 = 14%, 103 KB/s], Decompressed: 1237
Downloaded: 1288 file(s) [attempted 1288/8459 = 15%, 229 KB/s], Decompressed: 1247
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 297 KB/s], Decompressed: 1247
Downloaded: 1371 file(s) [attempted 1371/8459 = 16%, 764 KB/s], Decompressed: 1367
Downloaded: 1414 file(s) [attempted 1414/8459 = 16%, 232 KB/s], Decompressed: 1408
Downloaded: 1449 file(s) [attempted 1449/8459 = 17%, 715 KB/s], Decompressed: 1429
Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 200 KB/s], Decompressed: 1429
Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 24 KB/s], Decompressed: 1518
Downloaded: 1572 file(s) [attempted 1572/8459 = 18%, 85 KB/s], Decompressed: 1562
Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 529 KB/s], Decompressed: 1562
Downloaded: 1651 file(s) [attempted 1651/8459 = 19%, 491 KB/s], Decompressed: 1566
Downloaded: 1689 file(s) [attempted 1689/8459 = 19%, 293 KB/s], Decompressed: 1685
Downloaded: 1731 file(s) [attempted 1731/8459 = 20%, 272 KB/s], Decompressed: 1723
Downloaded: 1767 file(s) [attempted 1767/8459 = 20%, 1079 KB/s], Decompressed: 1764
Downloaded: 1812 file(s) [attempted 1812/8459 = 21%, 61 KB/s], Decompressed: 1798
Downloaded: 1853 file(s) [attempted 1853/8459 = 21%, 636 KB/s], Decompressed: 1798
Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 64 KB/s], Decompressed: 1805
Downloaded: 1928 file(s) [attempted 1928/8459 = 22%, 170 KB/s], Decompressed: 1921
Downloaded: 1963 file(s) [attempted 1963/8459 = 23%, 937 KB/s], Decompressed: 1959
Downloaded: 2004 file(s) [attempted 2004/8459 = 23%, 1388 KB/s], Decompressed: 2000
Downloaded: 2043 file(s) [attempted 2043/8459 = 24%, 243 KB/s], Decompressed: 2034
Downloaded: 2082 file(s) [attempted 2082/8459 = 24%, 104 KB/s], Decompressed: 2072
Downloaded: 2120 file(s) [attempted 2120/8459 = 25%, 1238 KB/s], Decompressed: 2113
Downloaded: 2158 file(s) [attempted 2158/8459 = 25%, 421 KB/s], Decompressed: 2130
Downloaded: 2199 file(s) [attempted 2199/8459 = 25%, 405 KB/s], Decompressed: 2130
Downloaded: 2240 file(s) [attempted 2240/8459 = 26%, 119 KB/s], Decompressed: 2134
Downloaded: 2274 file(s) [attempted 2274/8459 = 26%, 871 KB/s], Decompressed: 2134
Downloaded: 2318 file(s) [attempted 2318/8459 = 27%, 316 KB/s], Decompressed: 2219
Downloaded: 2360 file(s) [attempted 2360/8459 = 27%, 1275 KB/s], Decompressed: 2342
Downloaded: 2394 file(s) [attempted 2394/8459 = 28%, 319 KB/s], Decompressed: 2342
Downloaded: 2435 file(s) [attempted 2435/8459 = 28%, 180 KB/s], Decompressed: 2342
Downloaded: 2476 file(s) [attempted 2476/8459 = 29%, 994 KB/s], Decompressed: 2346
Downloaded: 2514 file(s) [attempted 2514/8459 = 29%, 245 KB/s], Decompressed: 2510
Downloaded: 2558 file(s) [attempted 2558/8459 = 30%, 212 KB/s], Decompressed: 2524
Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 594 KB/s], Decompressed: 2524
Downloaded: 2631 file(s) [attempted 2631/8459 = 31%, 823 KB/s], Decompressed: 2531
Downloaded: 2671 file(s) [attempted 2671/8459 = 31%, 170 KB/s], Decompressed: 2531
Downloaded: 2709 file(s) [attempted 2709/8459 = 32%, 339 KB/s], Decompressed: 2613
Downloaded: 2751 file(s) [attempted 2751/8459 = 32%, 215 KB/s], Decompressed: 2746
Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 628 KB/s], Decompressed: 2780
Downloaded: 2824 file(s) [attempted 2824/8459 = 33%, 54 KB/s], Decompressed: 2818
Downloaded: 2866 file(s) [attempted 2866/8459 = 33%, 23 KB/s], Decompressed: 2863
Downloaded: 2907 file(s) [attempted 2907/8459 = 34%, 791 KB/s], Decompressed: 2869
Downloaded: 2945 file(s) [attempted 2945/8459 = 34%, 564 KB/s], Decompressed: 2869
Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 24 KB/s], Decompressed: 2979
Downloaded: 3023 file(s) [attempted 3023/8459 = 35%, 487 KB/s], Decompressed: 3020
Downloaded: 3068 file(s) [attempted 3068/8459 = 36%, 205 KB/s], Decompressed: 3034
Downloaded: 3109 file(s) [attempted 3109/8459 = 36%, 26 KB/s], Decompressed: 3034
Downloaded: 3143 file(s) [attempted 3143/8459 = 37%, 54 KB/s], Decompressed: 3136
Downloaded: 3188 file(s) [attempted 3188/8459 = 37%, 57 KB/s], Decompressed: 3185
Downloaded: 3229 file(s) [attempted 3229/8459 = 38%, 401 KB/s], Decompressed: 3188
Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 150 KB/s], Decompressed: 3188
Downloaded: 3311 file(s) [attempted 3311/8459 = 39%, 1107 KB/s], Decompressed: 3298
Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 399 KB/s], Decompressed: 3331
Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 76 KB/s], Decompressed: 3331
Downloaded: 3431 file(s) [attempted 3431/8459 = 40%, 45 KB/s], Decompressed: 3338
Downloaded: 3475 file(s) [attempted 3475/8459 = 41%, 1861 KB/s], Decompressed: 3468
Downloaded: 3516 file(s) [attempted 3516/8459 = 41%, 122 KB/s], Decompressed: 3509
Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 228 KB/s], Decompressed: 3550
Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 24 KB/s], Decompressed: 3588
Downloaded: 3629 file(s) [attempted 3629/8459 = 42%, 331 KB/s], Decompressed: 3626
Downloaded: 3677 file(s) [attempted 3677/8459 = 43%, 339 KB/s], Decompressed: 3670
Downloaded: 3718 file(s) [attempted 3718/8459 = 43%, 45 KB/s], Decompressed: 3711
Downloaded: 3756 file(s) [attempted 3756/8459 = 44%, 892 KB/s], Decompressed: 3752
Downloaded: 3797 file(s) [attempted 3797/8459 = 44%, 307 KB/s], Decompressed: 3756
Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 130 KB/s], Decompressed: 3756
Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 234 KB/s], Decompressed: 3859
Downloaded: 3917 file(s) [attempted 3917/8459 = 46%, 48 KB/s], Decompressed: 3859
Downloaded: 3961 file(s) [attempted 3961/8459 = 46%, 288 KB/s], Decompressed: 3865
Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 273 KB/s], Decompressed: 3865
Downloaded: 4036 file(s) [attempted 4036/8459 = 47%, 71 KB/s], Decompressed: 3865
Downloaded: 4074 file(s) [attempted 4074/8459 = 48%, 285 KB/s], Decompressed: 4067
Downloaded: 4112 file(s) [attempted 4112/8459 = 48%, 174 KB/s], Decompressed: 4081
Downloaded: 4153 file(s) [attempted 4153/8459 = 49%, 127 KB/s], Decompressed: 4081
Downloaded: 4197 file(s) [attempted 4197/8459 = 49%, 23 KB/s], Decompressed: 4194
Downloaded: 4238 file(s) [attempted 4238/8459 = 50%, 191 KB/s], Decompressed: 4228
Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 223 KB/s], Decompressed: 4252
Downloaded: 4317 file(s) [attempted 4317/8459 = 51%, 816 KB/s], Decompressed: 4252
Downloaded: 4356 file(s) [attempted 4356/8459 = 51%, 1952 KB/s], Decompressed: 4344
Downloaded: 4401 file(s) [attempted 4401/8459 = 52%, 594 KB/s], Decompressed: 4392
Downloaded: 4437 file(s) [attempted 4437/8459 = 52%, 687 KB/s], Decompressed: 4423
Downloaded: 4471 file(s) [attempted 4471/8459 = 52%, 51 KB/s], Decompressed: 4468
Downloaded: 4512 file(s) [attempted 4512/8459 = 53%, 75 KB/s], Decompressed: 4485
Downloaded: 4560 file(s) [attempted 4560/8459 = 53%, 1542 KB/s], Decompressed: 4485
Downloaded: 4605 file(s) [attempted 4605/8459 = 54%, 117 KB/s], Decompressed: 4601
Downloaded: 4639 file(s) [attempted 4639/8459 = 54%, 67 KB/s], Decompressed: 4635
Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 145 KB/s], Decompressed: 4673
Downloaded: 4718 file(s) [attempted 4718/8459 = 55%, 1413 KB/s], Decompressed: 4673
Downloaded: 4762 file(s) [attempted 4762/8459 = 56%, 384 KB/s], Decompressed: 4673
Downloaded: 4803 file(s) [attempted 4803/8459 = 56%, 148 KB/s], Decompressed: 4793
Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 187 KB/s], Decompressed: 4834
Downloaded: 4877 file(s) [attempted 4877/8459 = 57%, 127 KB/s], Decompressed: 4868
Downloaded: 4916 file(s) [attempted 4916/8459 = 58%, 282 KB/s], Decompressed: 4885
Downloaded: 4961 file(s) [attempted 4961/8459 = 58%, 275 KB/s], Decompressed: 4885
Downloaded: 4998 file(s) [attempted 4998/8459 = 59%, 1116 KB/s], Decompressed: 4892
Downloaded: 5036 file(s) [attempted 5036/8459 = 59%, 558 KB/s], Decompressed: 4892
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 148 KB/s], Decompressed: 5063
Downloaded: 5125 file(s) [attempted 5125/8459 = 60%, 311 KB/s], Decompressed: 5115
Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 1173 KB/s], Decompressed: 5152
Downloaded: 5204 file(s) [attempted 5204/8459 = 61%, 92 KB/s], Decompressed: 5152
Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 762 KB/s], Decompressed: 5156
Downloaded: 5286 file(s) [attempted 5286/8459 = 62%, 351 KB/s], Decompressed: 5282
Downloaded: 5327 file(s) [attempted 5327/8459 = 62%, 1047 KB/s], Decompressed: 5320
Downloaded: 5361 file(s) [attempted 5361/8459 = 63%, 749 KB/s], Decompressed: 5347
Downloaded: 5399 file(s) [attempted 5399/8459 = 63%, 60 KB/s], Decompressed: 5347
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 492 KB/s], Decompressed: 5354
Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 157 KB/s], Decompressed: 5354
Downloaded: 5522 file(s) [attempted 5522/8459 = 65%, 424 KB/s], Decompressed: 5354
Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 171 KB/s], Decompressed: 5443
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 245 KB/s], Decompressed: 5597
Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 648 KB/s], Decompressed: 5604
Downloaded: 5686 file(s) [attempted 5686/8459 = 67%, 130 KB/s], Decompressed: 5604
Downloaded: 5724 file(s) [attempted 5724/8459 = 67%, 166 KB/s], Decompressed: 5717
Downloaded: 5761 file(s) [attempted 5761/8459 = 68%, 208 KB/s], Decompressed: 5724
Downloaded: 5802 file(s) [attempted 5802/8459 = 68%, 492 KB/s], Decompressed: 5724
Downloaded: 5843 file(s) [attempted 5843/8459 = 69%, 244 KB/s], Decompressed: 5731
Downloaded: 5882 file(s) [attempted 5882/8459 = 69%, 718 KB/s], Decompressed: 5731
Downloaded: 5919 file(s) [attempted 5919/8459 = 69%, 501 KB/s], Decompressed: 5898
Downloaded: 5956 file(s) [attempted 5956/8459 = 70%, 559 KB/s], Decompressed: 5946
Downloaded: 5997 file(s) [attempted 5997/8459 = 70%, 308 KB/s], Decompressed: 5987
Downloaded: 6037 file(s) [attempted 6037/8459 = 71%, 689 KB/s], Decompressed: 5987
Downloaded: 6076 file(s) [attempted 6076/8459 = 71%, 622 KB/s], Decompressed: 5994
Downloaded: 6121 file(s) [attempted 6121/8459 = 72%, 191 KB/s], Decompressed: 5994
Downloaded: 6154 file(s) [attempted 6154/8459 = 72%, 1088 KB/s], Decompressed: 6059
Downloaded: 6196 file(s) [attempted 6196/8459 = 73%, 434 KB/s], Decompressed: 6189
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 137 KB/s], Decompressed: 6227
Downloaded: 6275 file(s) [attempted 6275/8459 = 74%, 180 KB/s], Decompressed: 6237
Downloaded: 6316 file(s) [attempted 6316/8459 = 74%, 1055 KB/s], Decompressed: 6237
Downloaded: 6353 file(s) [attempted 6353/8459 = 75%, 319 KB/s], Decompressed: 6244
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 68 KB/s], Decompressed: 6244
Downloaded: 6428 file(s) [attempted 6428/8459 = 75%, 164 KB/s], Decompressed: 6326
Downloaded: 6473 file(s) [attempted 6473/8459 = 76%, 265 KB/s], Decompressed: 6470
Downloaded: 6516 file(s) [attempted 6516/8459 = 77%, 1543 KB/s], Decompressed: 6511
Downloaded: 6555 file(s) [attempted 6555/8459 = 77%, 583 KB/s], Decompressed: 6538
Downloaded: 6588 file(s) [attempted 6588/8459 = 77%, 996 KB/s], Decompressed: 6538
Downloaded: 6630 file(s) [attempted 6630/8459 = 78%, 427 KB/s], Decompressed: 6545
Downloaded: 6669 file(s) [attempted 6669/8459 = 78%, 375 KB/s], Decompressed: 6665
Downloaded: 6713 file(s) [attempted 6713/8459 = 79%, 143 KB/s], Decompressed: 6682
Downloaded: 6757 file(s) [attempted 6757/8459 = 79%, 237 KB/s], Decompressed: 6682
Downloaded: 6791 file(s) [attempted 6791/8459 = 80%, 371 KB/s], Decompressed: 6785
Downloaded: 6829 file(s) [attempted 6829/8459 = 80%, 551 KB/s], Decompressed: 6822
Downloaded: 6871 file(s) [attempted 6871/8459 = 81%, 744 KB/s], Decompressed: 6867
Downloaded: 6911 file(s) [attempted 6911/8459 = 81%, 192 KB/s], Decompressed: 6904
Downloaded: 6952 file(s) [attempted 6952/8459 = 82%, 865 KB/s], Decompressed: 6945
Downloaded: 6990 file(s) [attempted 6990/8459 = 82%, 247 KB/s], Decompressed: 6983
Downloaded: 7028 file(s) [attempted 7028/8459 = 83%, 348 KB/s], Decompressed: 7017
Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 321 KB/s], Decompressed: 7062
Downloaded: 7106 file(s) [attempted 7106/8459 = 84%, 558 KB/s], Decompressed: 7072
Downloaded: 7147 file(s) [attempted 7147/8459 = 84%, 441 KB/s], Decompressed: 7072
Downloaded: 7188 file(s) [attempted 7188/8459 = 84%, 703 KB/s], Decompressed: 7178
Downloaded: 7230 file(s) [attempted 7230/8459 = 85%, 181 KB/s], Decompressed: 7223
Downloaded: 7271 file(s) [attempted 7271/8459 = 85%, 185 KB/s], Decompressed: 7267
Downloaded: 7312 file(s) [attempted 7312/8459 = 86%, 179 KB/s], Decompressed: 7305
Downloaded: 7349 file(s) [attempted 7349/8459 = 86%, 1031 KB/s], Decompressed: 7342
Downloaded: 7394 file(s) [attempted 7394/8459 = 87%, 468 KB/s], Decompressed: 7370
Downloaded: 7431 file(s) [attempted 7431/8459 = 87%, 950 KB/s], Decompressed: 7370
Downloaded: 7469 file(s) [attempted 7469/8459 = 88%, 182 KB/s], Decompressed: 7452
Downloaded: 7505 file(s) [attempted 7505/8459 = 88%, 83 KB/s], Decompressed: 7500
Downloaded: 7548 file(s) [attempted 7548/8459 = 89%, 358 KB/s], Decompressed: 7544
Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 143 KB/s], Decompressed: 7582
Downloaded: 7627 file(s) [attempted 7627/8459 = 90%, 173 KB/s], Decompressed: 7623
Downloaded: 7661 file(s) [attempted 7661/8459 = 90%, 210 KB/s], Decompressed: 7657
Downloaded: 7699 file(s) [attempted 7699/8459 = 91%, 57 KB/s], Decompressed: 7695
Downloaded: 7737 file(s) [attempted 7737/8459 = 91%, 239 KB/s], Decompressed: 7733
Downloaded: 7781 file(s) [attempted 7781/8459 = 91%, 145 KB/s], Decompressed: 7777
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 675 KB/s], Decompressed: 7818
Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 33 KB/s], Decompressed: 7852
Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 644 KB/s], Decompressed: 7893
Downloaded: 7938 file(s) [attempted 7938/8459 = 93%, 358 KB/s], Decompressed: 7931
Downloaded: 7982 file(s) [attempted 7982/8459 = 94%, 293 KB/s], Decompressed: 7945
Downloaded: 8020 file(s) [attempted 8020/8459 = 94%, 245 KB/s], Decompressed: 7945
Downloaded: 8061 file(s) [attempted 8061/8459 = 95%, 237 KB/s], Decompressed: 8054
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 2700 KB/s], Decompressed: 8061
Downloaded: 8143 file(s) [attempted 8143/8459 = 96%, 75 KB/s], Decompressed: 8061
Downloaded: 8181 file(s) [attempted 8181/8459 = 96%, 50 KB/s], Decompressed: 8178
Downloaded: 8222 file(s) [attempted 8222/8459 = 97%, 188 KB/s], Decompressed: 8208
Downloaded: 8256 file(s) [attempted 8256/8459 = 97%, 141 KB/s], Decompressed: 8208
Downloaded: 8297 file(s) [attempted 8297/8459 = 98%, 92 KB/s], Decompressed: 8215
Downloaded: 8338 file(s) [attempted 8338/8459 = 98%, 170 KB/s], Decompressed: 8332
Downloaded: 8379 file(s) [attempted 8379/8459 = 99%, 123 KB/s], Decompressed: 8355
Downloaded: 8420 file(s) [attempted 8420/8459 = 99%, 86 KB/s], Decompressed: 8355
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 93 KB/s], Decompressed: 8441
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 93 KB/s], Decompressed: 8451

lean_checkerexit 1duration 12m 9s · created 7/13/2026, 6:24:38 AM

lake build

✔ [753/764] Built Iut.Foundations.RealLineCopy (84s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.5s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.5s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.5s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.5s)
✔ [763/772] Built Iut.Foundations.QualitativeData (1.0s)
✔ [3384/3393] Built Iut.Foundations.AlgorithmicOutput (1.6s)
✔ [3387/3393] Built Iut.Foundations.AlgorithmicBridge (2.5s)
✔ [3389/3393] Built Iut.Stage1.CorollarySchema (114s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.0s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3393/3407] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (108s)
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 (68s)
⚠ [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.9s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.1s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.6s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.8s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (37s)
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 (190s)
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_buildexit 1duration 2s · created 7/13/2026, 6:24:38 AM

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`