Verification run

Run 1061

promachina/iut-leanbranch mastertriggered via poller

failedcommit b167fb14c9ebtoolchain lean-v4-30-0prover leantook 11m 49s · 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 3s · created 7/13/2026, 5:48:04 AM

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

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

git_checkoutexit 0duration 96 ms · created 7/13/2026, 5:48:04 AM

git checkout b167fb14c9eb07e79ab8df9e3f585fb9392334a8

Note: switching to 'b167fb14c9eb07e79ab8df9e3f585fb9392334a8'.

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 b167fb1 Project local analytic signed bound

lake_cacheexit 0duration 57s · created 7/13/2026, 5:48:04 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%, 12 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 12 KB/s], Decompressed: 13
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 79 KB/s], Decompressed: 37
Downloaded: 66 file(s) [attempted 66/8459 = 0%, 55 KB/s], Decompressed: 64
Downloaded: 96 file(s) [attempted 96/8459 = 1%, 52 KB/s], Decompressed: 89
Downloaded: 131 file(s) [attempted 131/8459 = 1%, 267 KB/s], Decompressed: 124
Downloaded: 165 file(s) [attempted 165/8459 = 1%, 63 KB/s], Decompressed: 162
Downloaded: 203 file(s) [attempted 203/8459 = 2%, 319 KB/s], Decompressed: 199
Downloaded: 238 file(s) [attempted 238/8459 = 2%, 521 KB/s], Decompressed: 234
Downloaded: 271 file(s) [attempted 271/8459 = 3%, 1071 KB/s], Decompressed: 268
Downloaded: 307 file(s) [attempted 307/8459 = 3%, 79 KB/s], Decompressed: 302
Downloaded: 343 file(s) [attempted 343/8459 = 4%, 258 KB/s], Decompressed: 340
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 137 KB/s], Decompressed: 384
Downloaded: 429 file(s) [attempted 429/8459 = 5%, 245 KB/s], Decompressed: 425
Downloaded: 466 file(s) [attempted 466/8459 = 5%, 450 KB/s], Decompressed: 463
Downloaded: 501 file(s) [attempted 501/8459 = 5%, 391 KB/s], Decompressed: 490
Downloaded: 539 file(s) [attempted 539/8459 = 6%, 346 KB/s], Decompressed: 535
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 312 KB/s], Decompressed: 580
Downloaded: 633 file(s) [attempted 633/8459 = 7%, 206 KB/s], Decompressed: 627
Downloaded: 669 file(s) [attempted 669/8459 = 7%, 91 KB/s], Decompressed: 658
Downloaded: 706 file(s) [attempted 706/8459 = 8%, 475 KB/s], Decompressed: 699
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 243 KB/s], Decompressed: 744
Downloaded: 792 file(s) [attempted 792/8459 = 9%, 222 KB/s], Decompressed: 785
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 221 KB/s], Decompressed: 830
Downloaded: 881 file(s) [attempted 881/8459 = 10%, 39 KB/s], Decompressed: 874
Downloaded: 915 file(s) [attempted 915/8459 = 10%, 581 KB/s], Decompressed: 912
Downloaded: 956 file(s) [attempted 956/8459 = 11%, 32 KB/s], Decompressed: 953
Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 324 KB/s], Decompressed: 997
Downloaded: 1042 file(s) [attempted 1042/8459 = 12%, 1375 KB/s], Decompressed: 1038
Downloaded: 1080 file(s) [attempted 1080/8459 = 12%, 215 KB/s], Decompressed: 1076
Downloaded: 1121 file(s) [attempted 1121/8459 = 13%, 217 KB/s], Decompressed: 1115
Downloaded: 1158 file(s) [attempted 1158/8459 = 13%, 931 KB/s], Decompressed: 1155
Downloaded: 1199 file(s) [attempted 1199/8459 = 14%, 279 KB/s], Decompressed: 1192
Downloaded: 1240 file(s) [attempted 1240/8459 = 14%, 35 KB/s], Decompressed: 1237
Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 97 KB/s], Decompressed: 1271
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 158 KB/s], Decompressed: 1326
Downloaded: 1374 file(s) [attempted 1374/8459 = 16%, 168 KB/s], Decompressed: 1367
Downloaded: 1412 file(s) [attempted 1412/8459 = 16%, 99 KB/s], Decompressed: 1401
Downloaded: 1449 file(s) [attempted 1449/8459 = 17%, 713 KB/s], Decompressed: 1446
Downloaded: 1492 file(s) [attempted 1492/8459 = 17%, 318 KB/s], Decompressed: 1487
Downloaded: 1535 file(s) [attempted 1535/8459 = 18%, 168 KB/s], Decompressed: 1531
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 417 KB/s], Decompressed: 1572
Downloaded: 1617 file(s) [attempted 1617/8459 = 19%, 424 KB/s], Decompressed: 1613
Downloaded: 1653 file(s) [attempted 1653/8459 = 19%, 133 KB/s], Decompressed: 1634
Downloaded: 1692 file(s) [attempted 1692/8459 = 20%, 1254 KB/s], Decompressed: 1685
Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 304 KB/s], Decompressed: 1730
Downloaded: 1778 file(s) [attempted 1778/8459 = 21%, 201 KB/s], Decompressed: 1771
Downloaded: 1815 file(s) [attempted 1815/8459 = 21%, 163 KB/s], Decompressed: 1808
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 75 KB/s], Decompressed: 1850
Downloaded: 1897 file(s) [attempted 1897/8459 = 22%, 467 KB/s], Decompressed: 1894
Downloaded: 1937 file(s) [attempted 1937/8459 = 22%, 346 KB/s], Decompressed: 1928
Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 40 KB/s], Decompressed: 1973
Downloaded: 2021 file(s) [attempted 2021/8459 = 23%, 436 KB/s], Decompressed: 2017
Downloaded: 2062 file(s) [attempted 2062/8459 = 24%, 56 KB/s], Decompressed: 2051
Downloaded: 2103 file(s) [attempted 2103/8459 = 24%, 358 KB/s], Decompressed: 2099
Downloaded: 2141 file(s) [attempted 2141/8459 = 25%, 946 KB/s], Decompressed: 2137
Downloaded: 2180 file(s) [attempted 2180/8459 = 25%, 57 KB/s], Decompressed: 2175
Downloaded: 2223 file(s) [attempted 2223/8459 = 26%, 121 KB/s], Decompressed: 2219
Downloaded: 2260 file(s) [attempted 2260/8459 = 26%, 513 KB/s], Decompressed: 2253
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 277 KB/s], Decompressed: 2298
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 37 KB/s], Decompressed: 2339
Downloaded: 2387 file(s) [attempted 2387/8459 = 28%, 472 KB/s], Decompressed: 2377
Downloaded: 2428 file(s) [attempted 2428/8459 = 28%, 813 KB/s], Decompressed: 2421
Downloaded: 2467 file(s) [attempted 2467/8459 = 29%, 23 KB/s], Decompressed: 2462
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 177 KB/s], Decompressed: 2503
Downloaded: 2551 file(s) [attempted 2551/8459 = 30%, 241 KB/s], Decompressed: 2544
Downloaded: 2597 file(s) [attempted 2597/8459 = 30%, 1851 KB/s], Decompressed: 2589
Downloaded: 2633 file(s) [attempted 2633/8459 = 31%, 493 KB/s], Decompressed: 2626
Downloaded: 2671 file(s) [attempted 2671/8459 = 31%, 386 KB/s], Decompressed: 2661
Downloaded: 2714 file(s) [attempted 2714/8459 = 32%, 180 KB/s], Decompressed: 2709
Downloaded: 2756 file(s) [attempted 2756/8459 = 32%, 238 KB/s], Decompressed: 2753
Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 82 KB/s], Decompressed: 2794
Downloaded: 2839 file(s) [attempted 2839/8459 = 33%, 84 KB/s], Decompressed: 2828
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 23 KB/s], Decompressed: 2869
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 74 KB/s], Decompressed: 2914
Downloaded: 2959 file(s) [attempted 2959/8459 = 34%, 903 KB/s], Decompressed: 2952
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 429 KB/s], Decompressed: 2993
Downloaded: 3037 file(s) [attempted 3037/8459 = 35%, 156 KB/s], Decompressed: 3034
Downloaded: 3082 file(s) [attempted 3082/8459 = 36%, 451 KB/s], Decompressed: 3071
Downloaded: 3123 file(s) [attempted 3123/8459 = 36%, 1014 KB/s], Decompressed: 3109
Downloaded: 3167 file(s) [attempted 3167/8459 = 37%, 321 KB/s], Decompressed: 3160
Downloaded: 3201 file(s) [attempted 3201/8459 = 37%, 68 KB/s], Decompressed: 3191
Downloaded: 3240 file(s) [attempted 3240/8459 = 38%, 581 KB/s], Decompressed: 3236
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 136 KB/s], Decompressed: 3280
Downloaded: 3328 file(s) [attempted 3328/8459 = 39%, 185 KB/s], Decompressed: 3325
Downloaded: 3372 file(s) [attempted 3372/8459 = 39%, 115 KB/s], Decompressed: 3369
Downloaded: 3414 file(s) [attempted 3414/8459 = 40%, 205 KB/s], Decompressed: 3410
Downloaded: 3452 file(s) [attempted 3452/8459 = 40%, 400 KB/s], Decompressed: 3444
Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 424 KB/s], Decompressed: 3489
Downloaded: 3533 file(s) [attempted 3533/8459 = 41%, 70 KB/s], Decompressed: 3526
Downloaded: 3574 file(s) [attempted 3574/8459 = 42%, 286 KB/s], Decompressed: 3571
Downloaded: 3619 file(s) [attempted 3619/8459 = 42%, 791 KB/s], Decompressed: 3612
Downloaded: 3663 file(s) [attempted 3663/8459 = 43%, 412 KB/s], Decompressed: 3657
Downloaded: 3709 file(s) [attempted 3709/8459 = 43%, 267 KB/s], Decompressed: 3704
Downloaded: 3748 file(s) [attempted 3748/8459 = 44%, 291 KB/s], Decompressed: 3739
Downloaded: 3787 file(s) [attempted 3787/8459 = 44%, 489 KB/s], Decompressed: 3780
Downloaded: 3828 file(s) [attempted 3828/8459 = 45%, 1190 KB/s], Decompressed: 3800
Downloaded: 3872 file(s) [attempted 3872/8459 = 45%, 180 KB/s], Decompressed: 3865
Downloaded: 3909 file(s) [attempted 3909/8459 = 46%, 82 KB/s], Decompressed: 3903
Downloaded: 3951 file(s) [attempted 3951/8459 = 46%, 372 KB/s], Decompressed: 3947
Downloaded: 3995 file(s) [attempted 3995/8459 = 47%, 132 KB/s], Decompressed: 3992
Downloaded: 4036 file(s) [attempted 4036/8459 = 47%, 100 KB/s], Decompressed: 4033
Downloaded: 4075 file(s) [attempted 4075/8459 = 48%, 126 KB/s], Decompressed: 4071
Downloaded: 4115 file(s) [attempted 4115/8459 = 48%, 333 KB/s], Decompressed: 4108
Downloaded: 4154 file(s) [attempted 4154/8459 = 49%, 48 KB/s], Decompressed: 4149
Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 395 KB/s], Decompressed: 4190
Downloaded: 4235 file(s) [attempted 4235/8459 = 50%, 86 KB/s], Decompressed: 4228
Downloaded: 4278 file(s) [attempted 4278/8459 = 50%, 543 KB/s], Decompressed: 4269
Downloaded: 4320 file(s) [attempted 4320/8459 = 51%, 304 KB/s], Decompressed: 4317
Downloaded: 4365 file(s) [attempted 4365/8459 = 51%, 28 KB/s], Decompressed: 4358
Downloaded: 4399 file(s) [attempted 4399/8459 = 52%, 312 KB/s], Decompressed: 4392
Downloaded: 4440 file(s) [attempted 4440/8459 = 52%, 742 KB/s], Decompressed: 4437
Downloaded: 4481 file(s) [attempted 4481/8459 = 52%, 82 KB/s], Decompressed: 4474
Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 471 KB/s], Decompressed: 4519
Downloaded: 4567 file(s) [attempted 4567/8459 = 53%, 71 KB/s], Decompressed: 4560
Downloaded: 4608 file(s) [attempted 4608/8459 = 54%, 46 KB/s], Decompressed: 4601
Downloaded: 4646 file(s) [attempted 4646/8459 = 54%, 406 KB/s], Decompressed: 4642
Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 51 KB/s], Decompressed: 4683
Downloaded: 4729 file(s) [attempted 4729/8459 = 55%, 224 KB/s], Decompressed: 4724
Downloaded: 4769 file(s) [attempted 4769/8459 = 56%, 36 KB/s], Decompressed: 4759
Downloaded: 4806 file(s) [attempted 4806/8459 = 56%, 447 KB/s], Decompressed: 4803
Downloaded: 4851 file(s) [attempted 4851/8459 = 57%, 462 KB/s], Decompressed: 4848
Downloaded: 4892 file(s) [attempted 4892/8459 = 57%, 124 KB/s], Decompressed: 4887
Downloaded: 4930 file(s) [attempted 4930/8459 = 58%, 73 KB/s], Decompressed: 4926
Downloaded: 4971 file(s) [attempted 4971/8459 = 58%, 169 KB/s], Decompressed: 4967
Downloaded: 5015 file(s) [attempted 5015/8459 = 59%, 73 KB/s], Decompressed: 5009
Downloaded: 5053 file(s) [attempted 5053/8459 = 59%, 224 KB/s], Decompressed: 5039
Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 527 KB/s], Decompressed: 5077
Downloaded: 5139 file(s) [attempted 5139/8459 = 60%, 32 KB/s], Decompressed: 5135
Downloaded: 5181 file(s) [attempted 5181/8459 = 61%, 72 KB/s], Decompressed: 5173
Downloaded: 5221 file(s) [attempted 5221/8459 = 61%, 78 KB/s], Decompressed: 5217
Downloaded: 5265 file(s) [attempted 5265/8459 = 62%, 285 KB/s], Decompressed: 5262
Downloaded: 5306 file(s) [attempted 5306/8459 = 62%, 391 KB/s], Decompressed: 5299
Downloaded: 5347 file(s) [attempted 5347/8459 = 63%, 150 KB/s], Decompressed: 5344
Downloaded: 5390 file(s) [attempted 5390/8459 = 63%, 74 KB/s], Decompressed: 5381
Downloaded: 5429 file(s) [attempted 5429/8459 = 64%, 70 KB/s], Decompressed: 5426
Downloaded: 5470 file(s) [attempted 5470/8459 = 64%, 937 KB/s], Decompressed: 5467
Downloaded: 5513 file(s) [attempted 5513/8459 = 65%, 100 KB/s], Decompressed: 5505
Downloaded: 5553 file(s) [attempted 5553/8459 = 65%, 237 KB/s], Decompressed: 5549
Downloaded: 5594 file(s) [attempted 5594/8459 = 66%, 74 KB/s], Decompressed: 5590
Downloaded: 5638 file(s) [attempted 5638/8459 = 66%, 371 KB/s], Decompressed: 5631
Downloaded: 5679 file(s) [attempted 5679/8459 = 67%, 798 KB/s], Decompressed: 5676
Downloaded: 5724 file(s) [attempted 5724/8459 = 67%, 309 KB/s], Decompressed: 5713
Downloaded: 5768 file(s) [attempted 5768/8459 = 68%, 491 KB/s], Decompressed: 5761
Downloaded: 5809 file(s) [attempted 5809/8459 = 68%, 689 KB/s], Decompressed: 5802
Downloaded: 5844 file(s) [attempted 5844/8459 = 69%, 127 KB/s], Decompressed: 5840
Downloaded: 5888 file(s) [attempted 5888/8459 = 69%, 473 KB/s], Decompressed: 5884
Downloaded: 5931 file(s) [attempted 5931/8459 = 70%, 1200 KB/s], Decompressed: 5926
Downloaded: 5971 file(s) [attempted 5971/8459 = 70%, 607 KB/s], Decompressed: 5967
Downloaded: 6011 file(s) [attempted 6011/8459 = 71%, 1084 KB/s], Decompressed: 6004
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 40 KB/s], Decompressed: 6049
Downloaded: 6096 file(s) [attempted 6096/8459 = 72%, 555 KB/s], Decompressed: 6090
Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 146 KB/s], Decompressed: 6134
Downloaded: 6179 file(s) [attempted 6179/8459 = 73%, 46 KB/s], Decompressed: 6175
Downloaded: 6216 file(s) [attempted 6216/8459 = 73%, 306 KB/s], Decompressed: 6213
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 40 KB/s], Decompressed: 6251
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 759 KB/s], Decompressed: 6292
Downloaded: 6340 file(s) [attempted 6340/8459 = 74%, 695 KB/s], Decompressed: 6333
Downloaded: 6381 file(s) [attempted 6381/8459 = 75%, 282 KB/s], Decompressed: 6377
Downloaded: 6419 file(s) [attempted 6419/8459 = 75%, 194 KB/s], Decompressed: 6415
Downloaded: 6459 file(s) [attempted 6459/8459 = 76%, 123 KB/s], Decompressed: 6456
Downloaded: 6504 file(s) [attempted 6504/8459 = 76%, 32 KB/s], Decompressed: 6497
Downloaded: 6545 file(s) [attempted 6545/8459 = 77%, 559 KB/s], Decompressed: 6542
Downloaded: 6586 file(s) [attempted 6586/8459 = 77%, 338 KB/s], Decompressed: 6583
Downloaded: 6624 file(s) [attempted 6624/8459 = 78%, 323 KB/s], Decompressed: 6620
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 81 KB/s], Decompressed: 6651
Downloaded: 6708 file(s) [attempted 6708/8459 = 79%, 170 KB/s], Decompressed: 6682
Downloaded: 6747 file(s) [attempted 6747/8459 = 79%, 1057 KB/s], Decompressed: 6743
Downloaded: 6788 file(s) [attempted 6788/8459 = 80%, 237 KB/s], Decompressed: 6785
Downloaded: 6832 file(s) [attempted 6832/8459 = 80%, 330 KB/s], Decompressed: 6829
Downloaded: 6877 file(s) [attempted 6877/8459 = 81%, 653 KB/s], Decompressed: 6874
Downloaded: 6918 file(s) [attempted 6918/8459 = 81%, 35 KB/s], Decompressed: 6911
Downloaded: 6956 file(s) [attempted 6956/8459 = 82%, 47 KB/s], Decompressed: 6949
Downloaded: 6998 file(s) [attempted 6998/8459 = 82%, 472 KB/s], Decompressed: 6993
Downloaded: 7038 file(s) [attempted 7038/8459 = 83%, 132 KB/s], Decompressed: 7034
Downloaded: 7079 file(s) [attempted 7079/8459 = 83%, 773 KB/s], Decompressed: 7075
Downloaded: 7123 file(s) [attempted 7123/8459 = 84%, 219 KB/s], Decompressed: 7120
Downloaded: 7161 file(s) [attempted 7161/8459 = 84%, 93 KB/s], Decompressed: 7154
Downloaded: 7202 file(s) [attempted 7202/8459 = 85%, 25 KB/s], Decompressed: 7199
Downloaded: 7244 file(s) [attempted 7244/8459 = 85%, 465 KB/s], Decompressed: 7240
Downloaded: 7284 file(s) [attempted 7284/8459 = 86%, 165 KB/s], Decompressed: 7277
Downloaded: 7325 file(s) [attempted 7325/8459 = 86%, 71 KB/s], Decompressed: 7322
Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 74 KB/s], Decompressed: 7359
Downloaded: 7401 file(s) [attempted 7401/8459 = 87%, 451 KB/s], Decompressed: 7397
Downloaded: 7448 file(s) [attempted 7448/8459 = 88%, 121 KB/s], Decompressed: 7442
Downloaded: 7496 file(s) [attempted 7496/8459 = 88%, 106 KB/s], Decompressed: 7486
Downloaded: 7537 file(s) [attempted 7537/8459 = 89%, 218 KB/s], Decompressed: 7531
Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 122 KB/s], Decompressed: 7572
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 513 KB/s], Decompressed: 7609
Downloaded: 7657 file(s) [attempted 7657/8459 = 90%, 1684 KB/s], Decompressed: 7654
Downloaded: 7702 file(s) [attempted 7702/8459 = 91%, 1198 KB/s], Decompressed: 7698
Downloaded: 7739 file(s) [attempted 7739/8459 = 91%, 156 KB/s], Decompressed: 7733
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 83 KB/s], Decompressed: 7756
Downloaded: 7821 file(s) [attempted 7821/8459 = 92%, 226 KB/s], Decompressed: 7815
Downloaded: 7863 file(s) [attempted 7863/8459 = 92%, 33 KB/s], Decompressed: 7859
Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 450 KB/s], Decompressed: 7900
Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 1839 KB/s], Decompressed: 7945
Downloaded: 7996 file(s) [attempted 7996/8459 = 94%, 285 KB/s], Decompressed: 7989
Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 29 KB/s], Decompressed: 8030
Downloaded: 8078 file(s) [attempted 8078/8459 = 95%, 1204 KB/s], Decompressed: 8064
Downloaded: 8119 file(s) [attempted 8119/8459 = 95%, 41 KB/s], Decompressed: 8116
Downloaded: 8160 file(s) [attempted 8160/8459 = 96%, 190 KB/s], Decompressed: 8153
Downloaded: 8199 file(s) [attempted 8199/8459 = 96%, 32 KB/s], Decompressed: 8195
Downloaded: 8239 file(s) [attempted 8239/8459 = 97%, 258 KB/s], Decompressed: 8232
Downloaded: 8281 file(s) [attempted 8281/8459 = 97%, 82 KB/s], Decompressed: 8277
Downloaded: 8323 file(s) [attempted 8323/8459 = 98%, 370 KB/s], Decompressed: 8318
Downloaded: 8364 file(s) [attempted 8364/8459 = 98%, 210 KB/s], Decompressed: 8360
Downloaded: 8403 file(s) [attempted 8403/8459 = 99%, 130 KB/s], Decompressed: 8400
Downloaded: 8437 file(s) [attempted 8437/8459 = 99%, 365 KB/s], Decompressed: 8431
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 365 KB/s], Decompressed: 8451

lean_checkerexit 1duration 7m 41s · created 7/13/2026, 5:48:04 AM

lake build

✔ [753/764] Built Iut.Foundations.RealLineCopy (23s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.9s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.0s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.7s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/781] Built Iut.Foundations.QualitativeData (2.3s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.8s)
✔ [3388/3393] Built Iut.Stage1.CorollarySchema (31s)
✔ [3390/3394] Built Iut.Stage1.SourceObligations (3.1s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.7s)
✔ [3393/3405] Built Iut.Stage1.IUTStage1Data (3.3s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (85s)
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 (29s)
⚠ [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.2s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.9s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.8s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (24s)
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 (174s)
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, 5:48:04 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`