Verification run

Run 344

promachina/iut-lean branch master triggered via github_backfill

succeeded commit 4445261e2486 toolchain lean-v4-30-0 prover lean took 4h 22m · finished 5w ago

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_clone exit 0 duration 2s · created 6/12/2026, 5:08:39 AM

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

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

git_checkout exit 128 duration 3 ms · created 6/12/2026, 5:08:39 AM

git checkout 4445261e2486aeba78303822dbc533a70f82cd5c

fatal: reference is not a tree: 4445261e2486aeba78303822dbc533a70f82cd5c

git_checkout exit 0 duration 935 ms · created 6/12/2026, 5:08:39 AM

git fetch --depth 1 origin 4445261e2486aeba78303822dbc533a70f82cd5c

From https://github.com/promachina/iut-lean
 * branch            4445261e2486aeba78303822dbc533a70f82cd5c -> FETCH_HEAD

git_checkout exit 0 duration 168 ms · created 6/12/2026, 5:08:39 AM

git checkout 4445261e2486aeba78303822dbc533a70f82cd5c (after fetch)

Note: switching to '4445261e2486aeba78303822dbc533a70f82cd5c'.

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 4445261 Add nonzero scalar multiplication hull source

lake_cache exit 0 duration 35s · created 6/12/2026, 5:08:39 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%, 9 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 1 KB/s], Decompressed: 12
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 15 KB/s], Decompressed: 36
Downloaded: 66 file(s) [attempted 66/8459 = 0%, 26 KB/s], Decompressed: 61
Downloaded: 93 file(s) [attempted 93/8459 = 1%, 184 KB/s], Decompressed: 89
Downloaded: 127 file(s) [attempted 127/8459 = 1%, 285 KB/s], Decompressed: 121
Downloaded: 164 file(s) [attempted 164/8459 = 1%, 381 KB/s], Decompressed: 158
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 170 KB/s], Decompressed: 196
Downloaded: 239 file(s) [attempted 239/8459 = 2%, 258 KB/s], Decompressed: 234
Downloaded: 276 file(s) [attempted 276/8459 = 3%, 157 KB/s], Decompressed: 271
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 158 KB/s], Decompressed: 309
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 561 KB/s], Decompressed: 350
Downloaded: 395 file(s) [attempted 395/8459 = 4%, 1040 KB/s], Decompressed: 391
Downloaded: 436 file(s) [attempted 436/8459 = 5%, 83 KB/s], Decompressed: 432
Downloaded: 477 file(s) [attempted 477/8459 = 5%, 94 KB/s], Decompressed: 473
Downloaded: 514 file(s) [attempted 514/8459 = 6%, 1116 KB/s], Decompressed: 511
Downloaded: 552 file(s) [attempted 552/8459 = 6%, 124 KB/s], Decompressed: 549
Downloaded: 593 file(s) [attempted 593/8459 = 7%, 271 KB/s], Decompressed: 586
Downloaded: 634 file(s) [attempted 634/8459 = 7%, 64 KB/s], Decompressed: 631
Downloaded: 676 file(s) [attempted 676/8459 = 7%, 63 KB/s], Decompressed: 672
Downloaded: 713 file(s) [attempted 713/8459 = 8%, 1073 KB/s], Decompressed: 710
Downloaded: 754 file(s) [attempted 754/8459 = 8%, 122 KB/s], Decompressed: 751
Downloaded: 799 file(s) [attempted 799/8459 = 9%, 529 KB/s], Decompressed: 795
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 75 KB/s], Decompressed: 833
Downloaded: 881 file(s) [attempted 881/8459 = 10%, 70 KB/s], Decompressed: 878
Downloaded: 922 file(s) [attempted 922/8459 = 10%, 466 KB/s], Decompressed: 915
Downloaded: 960 file(s) [attempted 960/8459 = 11%, 32 KB/s], Decompressed: 956
Downloaded: 1004 file(s) [attempted 1004/8459 = 11%, 83 KB/s], Decompressed: 1001
Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 24 KB/s], Decompressed: 1042
Downloaded: 1083 file(s) [attempted 1083/8459 = 12%, 257 KB/s], Decompressed: 1080
Downloaded: 1127 file(s) [attempted 1127/8459 = 13%, 283 KB/s], Decompressed: 1124
Downloaded: 1162 file(s) [attempted 1162/8459 = 13%, 496 KB/s], Decompressed: 1158
Downloaded: 1203 file(s) [attempted 1203/8459 = 14%, 33 KB/s], Decompressed: 1199
Downloaded: 1241 file(s) [attempted 1241/8459 = 14%, 616 KB/s], Decompressed: 1237
Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 132 KB/s], Decompressed: 1278
Downloaded: 1327 file(s) [attempted 1327/8459 = 15%, 1039 KB/s], Decompressed: 1319
Downloaded: 1360 file(s) [attempted 1360/8459 = 16%, 614 KB/s], Decompressed: 1353
Downloaded: 1401 file(s) [attempted 1401/8459 = 16%, 61 KB/s], Decompressed: 1398
Downloaded: 1442 file(s) [attempted 1442/8459 = 17%, 307 KB/s], Decompressed: 1435
Downloaded: 1481 file(s) [attempted 1481/8459 = 17%, 1404 KB/s], Decompressed: 1473
Downloaded: 1519 file(s) [attempted 1519/8459 = 17%, 75 KB/s], Decompressed: 1514
Downloaded: 1557 file(s) [attempted 1557/8459 = 18%, 62 KB/s], Decompressed: 1552
Downloaded: 1600 file(s) [attempted 1600/8459 = 18%, 383 KB/s], Decompressed: 1596
Downloaded: 1637 file(s) [attempted 1637/8459 = 19%, 492 KB/s], Decompressed: 1634
Downloaded: 1680 file(s) [attempted 1680/8459 = 19%, 152 KB/s], Decompressed: 1675
Downloaded: 1718 file(s) [attempted 1718/8459 = 20%, 155 KB/s], Decompressed: 1713
Downloaded: 1757 file(s) [attempted 1757/8459 = 20%, 70 KB/s], Decompressed: 1750
Downloaded: 1795 file(s) [attempted 1795/8459 = 21%, 36 KB/s], Decompressed: 1791
Downloaded: 1836 file(s) [attempted 1836/8459 = 21%, 473 KB/s], Decompressed: 1832
Downloaded: 1876 file(s) [attempted 1876/8459 = 22%, 263 KB/s], Decompressed: 1870
Downloaded: 1918 file(s) [attempted 1918/8459 = 22%, 473 KB/s], Decompressed: 1911
Downloaded: 1956 file(s) [attempted 1956/8459 = 23%, 78 KB/s], Decompressed: 1952
Downloaded: 1998 file(s) [attempted 1998/8459 = 23%, 109 KB/s], Decompressed: 1993
Downloaded: 2032 file(s) [attempted 2032/8459 = 24%, 660 KB/s], Decompressed: 2028
Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 338 KB/s], Decompressed: 2062
Downloaded: 2108 file(s) [attempted 2108/8459 = 24%, 652 KB/s], Decompressed: 2103
Downloaded: 2147 file(s) [attempted 2147/8459 = 25%, 625 KB/s], Decompressed: 2144
Downloaded: 2192 file(s) [attempted 2192/8459 = 25%, 216 KB/s], Decompressed: 2188
Downloaded: 2230 file(s) [attempted 2230/8459 = 26%, 304 KB/s], Decompressed: 2226
Downloaded: 2267 file(s) [attempted 2267/8459 = 26%, 334 KB/s], Decompressed: 2260
Downloaded: 2308 file(s) [attempted 2308/8459 = 27%, 202 KB/s], Decompressed: 2305
Downloaded: 2348 file(s) [attempted 2348/8459 = 27%, 321 KB/s], Decompressed: 2342
Downloaded: 2390 file(s) [attempted 2390/8459 = 28%, 79 KB/s], Decompressed: 2387
Downloaded: 2435 file(s) [attempted 2435/8459 = 28%, 464 KB/s], Decompressed: 2428
Downloaded: 2469 file(s) [attempted 2469/8459 = 29%, 1511 KB/s], Decompressed: 2466
Downloaded: 2510 file(s) [attempted 2510/8459 = 29%, 126 KB/s], Decompressed: 2507
Downloaded: 2548 file(s) [attempted 2548/8459 = 30%, 70 KB/s], Decompressed: 2544
Downloaded: 2587 file(s) [attempted 2587/8459 = 30%, 370 KB/s], Decompressed: 2582
Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 148 KB/s], Decompressed: 2626
Downloaded: 2668 file(s) [attempted 2668/8459 = 31%, 248 KB/s], Decompressed: 2664
Downloaded: 2706 file(s) [attempted 2706/8459 = 31%, 472 KB/s], Decompressed: 2698
Downloaded: 2746 file(s) [attempted 2746/8459 = 32%, 93 KB/s], Decompressed: 2739
Downloaded: 2784 file(s) [attempted 2784/8459 = 32%, 838 KB/s], Decompressed: 2780
Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 38 KB/s], Decompressed: 2825
Downloaded: 2863 file(s) [attempted 2863/8459 = 33%, 23 KB/s], Decompressed: 2859
Downloaded: 2907 file(s) [attempted 2907/8459 = 34%, 391 KB/s], Decompressed: 2900
Downloaded: 2941 file(s) [attempted 2941/8459 = 34%, 826 KB/s], Decompressed: 2934
Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 23 KB/s], Decompressed: 2979
Downloaded: 3024 file(s) [attempted 3024/8459 = 35%, 88 KB/s], Decompressed: 3020
Downloaded: 3061 file(s) [attempted 3061/8459 = 36%, 2068 KB/s], Decompressed: 3058
Downloaded: 3101 file(s) [attempted 3101/8459 = 36%, 470 KB/s], Decompressed: 3095
Downloaded: 3140 file(s) [attempted 3140/8459 = 37%, 512 KB/s], Decompressed: 3136
Downloaded: 3177 file(s) [attempted 3177/8459 = 37%, 83 KB/s], Decompressed: 3174
Downloaded: 3225 file(s) [attempted 3225/8459 = 38%, 52 KB/s], Decompressed: 3219
Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 66 KB/s], Decompressed: 3266
Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 40 KB/s], Decompressed: 3314
Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 50 KB/s], Decompressed: 3352
Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 1110 KB/s], Decompressed: 3386
Downloaded: 3434 file(s) [attempted 3434/8459 = 40%, 111 KB/s], Decompressed: 3431
Downloaded: 3475 file(s) [attempted 3475/8459 = 41%, 327 KB/s], Decompressed: 3472
Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 951 KB/s], Decompressed: 3516
Downloaded: 3557 file(s) [attempted 3557/8459 = 42%, 86 KB/s], Decompressed: 3554
Downloaded: 3598 file(s) [attempted 3598/8459 = 42%, 182 KB/s], Decompressed: 3595
Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 135 KB/s], Decompressed: 3636
Downloaded: 3684 file(s) [attempted 3684/8459 = 43%, 30 KB/s], Decompressed: 3677
Downloaded: 3722 file(s) [attempted 3722/8459 = 44%, 131 KB/s], Decompressed: 3718
Downloaded: 3769 file(s) [attempted 3769/8459 = 44%, 1399 KB/s], Decompressed: 3763
Downloaded: 3801 file(s) [attempted 3801/8459 = 44%, 391 KB/s], Decompressed: 3797
Downloaded: 3841 file(s) [attempted 3841/8459 = 45%, 416 KB/s], Decompressed: 3838
Downloaded: 3886 file(s) [attempted 3886/8459 = 45%, 144 KB/s], Decompressed: 3882
Downloaded: 3929 file(s) [attempted 3929/8459 = 46%, 176 KB/s], Decompressed: 3924
Downloaded: 3965 file(s) [attempted 3965/8459 = 46%, 125 KB/s], Decompressed: 3961
Downloaded: 4007 file(s) [attempted 4007/8459 = 47%, 48 KB/s], Decompressed: 4002
Downloaded: 4043 file(s) [attempted 4043/8459 = 47%, 594 KB/s], Decompressed: 4036
Downloaded: 4084 file(s) [attempted 4084/8459 = 48%, 233 KB/s], Decompressed: 4081
Downloaded: 4129 file(s) [attempted 4129/8459 = 48%, 145 KB/s], Decompressed: 4122
Downloaded: 4164 file(s) [attempted 4164/8459 = 49%, 203 KB/s], Decompressed: 4160
Downloaded: 4208 file(s) [attempted 4208/8459 = 49%, 183 KB/s], Decompressed: 4204
Downloaded: 4245 file(s) [attempted 4245/8459 = 50%, 518 KB/s], Decompressed: 4242
Downloaded: 4286 file(s) [attempted 4286/8459 = 50%, 64 KB/s], Decompressed: 4283
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 107 KB/s], Decompressed: 4324
Downloaded: 4365 file(s) [attempted 4365/8459 = 51%, 385 KB/s], Decompressed: 4362
Downloaded: 4409 file(s) [attempted 4409/8459 = 52%, 85 KB/s], Decompressed: 4406
Downloaded: 4451 file(s) [attempted 4451/8459 = 52%, 194 KB/s], Decompressed: 4447
Downloaded: 4486 file(s) [attempted 4486/8459 = 53%, 91 KB/s], Decompressed: 4481
Downloaded: 4526 file(s) [attempted 4526/8459 = 53%, 198 KB/s], Decompressed: 4522
Downloaded: 4563 file(s) [attempted 4563/8459 = 53%, 75 KB/s], Decompressed: 4560
Downloaded: 4606 file(s) [attempted 4606/8459 = 54%, 115 KB/s], Decompressed: 4601
Downloaded: 4646 file(s) [attempted 4646/8459 = 54%, 24 KB/s], Decompressed: 4642
Downloaded: 4683 file(s) [attempted 4683/8459 = 55%, 97 KB/s], Decompressed: 4680
Downloaded: 4724 file(s) [attempted 4724/8459 = 55%, 413 KB/s], Decompressed: 4721
Downloaded: 4764 file(s) [attempted 4764/8459 = 56%, 376 KB/s], Decompressed: 4759
Downloaded: 4806 file(s) [attempted 4806/8459 = 56%, 393 KB/s], Decompressed: 4800
Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 98 KB/s], Decompressed: 4837
Downloaded: 4880 file(s) [attempted 4880/8459 = 57%, 139 KB/s], Decompressed: 4875
Downloaded: 4923 file(s) [attempted 4923/8459 = 58%, 29 KB/s], Decompressed: 4919
Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 247 KB/s], Decompressed: 4961
Downloaded: 5008 file(s) [attempted 5008/8459 = 59%, 61 KB/s], Decompressed: 5005
Downloaded: 5049 file(s) [attempted 5049/8459 = 59%, 220 KB/s], Decompressed: 5043
Downloaded: 5087 file(s) [attempted 5087/8459 = 60%, 101 KB/s], Decompressed: 5080
Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 594 KB/s], Decompressed: 5125
Downloaded: 5169 file(s) [attempted 5169/8459 = 61%, 367 KB/s], Decompressed: 5159
Downloaded: 5207 file(s) [attempted 5207/8459 = 61%, 572 KB/s], Decompressed: 5200
Downloaded: 5246 file(s) [attempted 5246/8459 = 62%, 714 KB/s], Decompressed: 5241
Downloaded: 5286 file(s) [attempted 5286/8459 = 62%, 350 KB/s], Decompressed: 5280
Downloaded: 5323 file(s) [attempted 5323/8459 = 62%, 109 KB/s], Decompressed: 5320
Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 414 KB/s], Decompressed: 5361
Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 59 KB/s], Decompressed: 5399
Downloaded: 5446 file(s) [attempted 5446/8459 = 64%, 972 KB/s], Decompressed: 5443
Downloaded: 5494 file(s) [attempted 5494/8459 = 64%, 625 KB/s], Decompressed: 5491
Downloaded: 5535 file(s) [attempted 5535/8459 = 65%, 129 KB/s], Decompressed: 5525
Downloaded: 5573 file(s) [attempted 5573/8459 = 65%, 122 KB/s], Decompressed: 5570
Downloaded: 5613 file(s) [attempted 5613/8459 = 66%, 389 KB/s], Decompressed: 5607
Downloaded: 5649 file(s) [attempted 5649/8459 = 66%, 115 KB/s], Decompressed: 5642
Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 615 KB/s], Decompressed: 5683
Downloaded: 5734 file(s) [attempted 5734/8459 = 67%, 285 KB/s], Decompressed: 5727
Downloaded: 5774 file(s) [attempted 5774/8459 = 68%, 610 KB/s], Decompressed: 5767
Downloaded: 5809 file(s) [attempted 5809/8459 = 68%, 683 KB/s], Decompressed: 5806
Downloaded: 5847 file(s) [attempted 5847/8459 = 69%, 445 KB/s], Decompressed: 5843
Downloaded: 5885 file(s) [attempted 5885/8459 = 69%, 453 KB/s], Decompressed: 5881
Downloaded: 5926 file(s) [attempted 5926/8459 = 70%, 391 KB/s], Decompressed: 5922
Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 45 KB/s], Decompressed: 5967
Downloaded: 6011 file(s) [attempted 6011/8459 = 71%, 612 KB/s], Decompressed: 6009
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 333 KB/s], Decompressed: 6042
Downloaded: 6091 file(s) [attempted 6091/8459 = 72%, 735 KB/s], Decompressed: 6086
Downloaded: 6134 file(s) [attempted 6134/8459 = 72%, 227 KB/s], Decompressed: 6128
Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 549 KB/s], Decompressed: 6172
Downloaded: 6214 file(s) [attempted 6214/8459 = 73%, 40 KB/s], Decompressed: 6210
Downloaded: 6251 file(s) [attempted 6251/8459 = 73%, 155 KB/s], Decompressed: 6247
Downloaded: 6288 file(s) [attempted 6288/8459 = 74%, 370 KB/s], Decompressed: 6285
Downloaded: 6333 file(s) [attempted 6333/8459 = 74%, 468 KB/s], Decompressed: 6329
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 92 KB/s], Decompressed: 6371
Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 492 KB/s], Decompressed: 6408
Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 743 KB/s], Decompressed: 6447
Downloaded: 6490 file(s) [attempted 6490/8459 = 76%, 407 KB/s], Decompressed: 6487
Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 56 KB/s], Decompressed: 6528
Downloaded: 6572 file(s) [attempted 6572/8459 = 77%, 24 KB/s], Decompressed: 6566
Downloaded: 6613 file(s) [attempted 6613/8459 = 78%, 531 KB/s], Decompressed: 6603
Downloaded: 6651 file(s) [attempted 6651/8459 = 78%, 288 KB/s], Decompressed: 6648
Downloaded: 6692 file(s) [attempted 6692/8459 = 79%, 146 KB/s], Decompressed: 6690
Downloaded: 6733 file(s) [attempted 6733/8459 = 79%, 436 KB/s], Decompressed: 6730
Downloaded: 6774 file(s) [attempted 6774/8459 = 80%, 41 KB/s], Decompressed: 6771
Downloaded: 6815 file(s) [attempted 6815/8459 = 80%, 388 KB/s], Decompressed: 6809
Downloaded: 6853 file(s) [attempted 6853/8459 = 81%, 296 KB/s], Decompressed: 6850
Downloaded: 6892 file(s) [attempted 6892/8459 = 81%, 108 KB/s], Decompressed: 6887
Downloaded: 6932 file(s) [attempted 6932/8459 = 81%, 193 KB/s], Decompressed: 6928
Downloaded: 6976 file(s) [attempted 6976/8459 = 82%, 593 KB/s], Decompressed: 6973
Downloaded: 7021 file(s) [attempted 7021/8459 = 83%, 259 KB/s], Decompressed: 7017
Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 300 KB/s], Decompressed: 7052
Downloaded: 7096 file(s) [attempted 7096/8459 = 83%, 648 KB/s], Decompressed: 7089
Downloaded: 7134 file(s) [attempted 7134/8459 = 84%, 147 KB/s], Decompressed: 7130
Downloaded: 7176 file(s) [attempted 7176/8459 = 84%, 511 KB/s], Decompressed: 7171
Downloaded: 7219 file(s) [attempted 7219/8459 = 85%, 615 KB/s], Decompressed: 7212
Downloaded: 7253 file(s) [attempted 7253/8459 = 85%, 1454 KB/s], Decompressed: 7250
Downloaded: 7297 file(s) [attempted 7297/8459 = 86%, 79 KB/s], Decompressed: 7288
Downloaded: 7332 file(s) [attempted 7332/8459 = 86%, 583 KB/s], Decompressed: 7329
Downloaded: 7373 file(s) [attempted 7373/8459 = 87%, 242 KB/s], Decompressed: 7370
Downloaded: 7414 file(s) [attempted 7414/8459 = 87%, 345 KB/s], Decompressed: 7407
Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 208 KB/s], Decompressed: 7445
Downloaded: 7493 file(s) [attempted 7493/8459 = 88%, 312 KB/s], Decompressed: 7490
Downloaded: 7534 file(s) [attempted 7534/8459 = 89%, 128 KB/s], Decompressed: 7531
Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 284 KB/s], Decompressed: 7568
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 487 KB/s], Decompressed: 7609
Downloaded: 7650 file(s) [attempted 7650/8459 = 90%, 218 KB/s], Decompressed: 7647
Downloaded: 7692 file(s) [attempted 7692/8459 = 90%, 461 KB/s], Decompressed: 7688
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 443 KB/s], Decompressed: 7729
Downloaded: 7774 file(s) [attempted 7774/8459 = 91%, 1692 KB/s], Decompressed: 7767
Downloaded: 7812 file(s) [attempted 7812/8459 = 92%, 22 KB/s], Decompressed: 7808
Downloaded: 7851 file(s) [attempted 7851/8459 = 92%, 319 KB/s], Decompressed: 7842
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 261 KB/s], Decompressed: 7887
Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 655 KB/s], Decompressed: 7928
Downloaded: 7970 file(s) [attempted 7970/8459 = 94%, 375 KB/s], Decompressed: 7965
Downloaded: 8006 file(s) [attempted 8006/8459 = 94%, 133 KB/s], Decompressed: 8003
Downloaded: 8048 file(s) [attempted 8048/8459 = 95%, 145 KB/s], Decompressed: 8044
Downloaded: 8085 file(s) [attempted 8085/8459 = 95%, 353 KB/s], Decompressed: 8082
Downloaded: 8133 file(s) [attempted 8133/8459 = 96%, 724 KB/s], Decompressed: 8130
Downloaded: 8176 file(s) [attempted 8176/8459 = 96%, 1563 KB/s], Decompressed: 8164
Downloaded: 8212 file(s) [attempted 8212/8459 = 97%, 754 KB/s], Decompressed: 8208
Downloaded: 8253 file(s) [attempted 8253/8459 = 97%, 528 KB/s], Decompressed: 8249
Downloaded: 8297 file(s) [attempted 8297/8459 = 98%, 592 KB/s], Decompressed: 8294
Downloaded: 8338 file(s) [attempted 8338/8459 = 98%, 198 KB/s], Decompressed: 8335
Downloaded: 8380 file(s) [attempted 8380/8459 = 99%, 50 KB/s], Decompressed: 8376
Downloaded: 8418 file(s) [attempted 8418/8459 = 99%, 426 KB/s], Decompressed: 8414
Downloaded: 8452 file(s) [attempted 8452/8459 = 99%, 464 KB/s], Decompressed: 8448
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 464 KB/s], Decompressed: 8455

lean_checker exit 0 duration 4m 54s · created 6/12/2026, 5:08:39 AM

lake build

✔ [3401/3416] Built Iut.Stage1.IUTStage1SourceCore (44s)
✔ [3402/3416] Built Iut.Stage1.IUTStage1Remark312Absorption (2.9s)
✔ [3403/3416] Built Iut.Stage1.IUTStage1IUTIVAlgebra (9.6s)
✔ [3404/3416] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
✔ [3405/3416] Built Iut.Stage1.IUTStage1StepX (4.9s)
✔ [3406/3416] Built Iut.Stage1.IUTStage1Gaussian (9.1s)
✔ [3407/3416] Built Iut.Stage1.IUTStage1HodgeSHE (5.6s)
✔ [3408/3416] Built Iut.Stage1.IUTStage1Theorem311 (4.4s)
✔ [3409/3416] Built Iut.Stage1.IUTStage1StepXI (17s)
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (131s)
info: stderr:
PANIC at _private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:71:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
backtrace:
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x767a823c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x767a823bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x767a823bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x767a822f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x767a822f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x767a823caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x767a82232923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x767a82232b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x767a82233827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x767a822341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x767a823c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x767a82015adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x767a823c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x767a823c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x767a8239b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x767a82015c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x767a7d422638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x767a7d20cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x767a7cd69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x767a7cd69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x767a79c4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x767a79c45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x6018a32268da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (6.4s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.1s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (35s)
✔ [3414/3416] Built Iut.Basic (2.4s)
✔ [3415/3416] Built Iut (2.3s)
Build completed successfully (3416 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

blueprint_build exit 1 duration 1s · created 6/12/2026, 5:08:39 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`

semantic_extract exit 0 duration 33m 30s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache bfb182654d7b9700f9355f8b52499cc4492003178b72375149f6f9c7a1a5f587
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 43s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)

lean semantic helper: restored compiled static runner cache b0ddeaaa2553229aaff1dc72c131add56ca5eaf65331b57c95c4ac371fadb91f
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 7m 7s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)

lean semantic helper: restored compiled static runner cache e538f0251f041ef0b337d3bd2b02e2800bdae1a864fbf6b2380b52ffeb000535
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 9s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)

lean semantic helper: restored compiled static runner cache 75b5977bf3c3f7790c74f7fcdf61319b52a6563d7e4b9f6920235cee9e6766b3
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 17s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)

lean semantic helper: restored compiled static runner cache b1361ddd4d800407fee97079d7c69334e9fa98f8d8138ea91735fd01a42f86a2
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 47s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)

lean semantic helper: restored compiled static runner cache 03585dcb70610534a4ce74449195125e05e01fddbca11f3263fb9006bd27c14e
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 7m 43s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006)

lean semantic helper: restored compiled static runner cache 08877232589cf9db425b8187c7f232d1869e5ec11e14304e9a4a61a9b73231aa
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 50s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007)

lean semantic helper: restored compiled static runner cache e73538885b586c3d3ade36b614bd08578304e5f0d861b518f22c5a691c41fbd9
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 18m 34s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00008)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 65fabd7e7df1b452e46f9c3eb6b9e7ca725f4f923d32213045a2f009b6bf280e
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 1h 40m · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00009)

lean semantic helper: restored compiled static runner cache 0efd485e0463b19f5c2e2a591158e669acbf0d05b6feb20ce1b85cba88b2befe
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 18s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00010)

lean semantic helper: restored compiled static runner cache 8ce5ff6c967baef3842b8fb460ab7dc29b28a04bbb424be955c4371e23608184
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 1s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00011)

lean semantic helper: restored compiled static runner cache 6247def1945279a6946b34517b575ac426a9bd22cc4c3ceb7a79dc06ef4083db
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 31m 42s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00012)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 6826dec7a6436d0dde2f46e1a4619ed9742540870ae4e08fc12ca16bc53c3fe7
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 37s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00013)

lean semantic helper: restored compiled static runner cache 60b5e07f9f538c271c74b7f6a814efcb4304463fa74b69c58466604298c0acfe
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 40s · created 6/12/2026, 5:08:39 AM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00014)

lean semantic helper: restored compiled static runner cache e103fd3939aed645f6a64b867308ee472e79eb2af9586b744c189d70ac5f91ea
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes