Verification run

Run 340

promachina/iut-lean branch master triggered via manual

failed commit 71ef5dc5e76d toolchain lean-v4-30-0 prover lean took 5h 18m · finished 5w ago

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007) failed with exit code 1 (toolchain lean-v4-30-0, command: <command argv unavailable>)

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_clone exit 0 duration 3s · created 6/11/2026, 12:22:22 AM

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

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

git_checkout exit 128 duration 1 ms · created 6/11/2026, 12:22:22 AM

git checkout 71ef5dc5e76d60469a81a05df5dd9473c8c42975

fatal: reference is not a tree: 71ef5dc5e76d60469a81a05df5dd9473c8c42975

git_checkout exit 0 duration 1s · created 6/11/2026, 12:22:22 AM

git fetch --depth 1 origin 71ef5dc5e76d60469a81a05df5dd9473c8c42975

From https://github.com/promachina/iut-lean
 * branch            71ef5dc5e76d60469a81a05df5dd9473c8c42975 -> FETCH_HEAD

git_checkout exit 0 duration 139 ms · created 6/11/2026, 12:22:22 AM

git checkout 71ef5dc5e76d60469a81a05df5dd9473c8c42975 (after fetch)

Note: switching to '71ef5dc5e76d60469a81a05df5dd9473c8c42975'.

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 71ef5dc Add coordinate scalar valuation hull cover

lake_cache exit 0 duration 37s · created 6/11/2026, 12:22:22 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%, 8 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 4 KB/s], Decompressed: 13
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 92 KB/s], Decompressed: 34
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 27 KB/s], Decompressed: 65
Downloaded: 100 file(s) [attempted 100/8459 = 1%, 322 KB/s], Decompressed: 96
Downloaded: 141 file(s) [attempted 141/8459 = 1%, 595 KB/s], Decompressed: 134
Downloaded: 175 file(s) [attempted 175/8459 = 2%, 210 KB/s], Decompressed: 169
Downloaded: 216 file(s) [attempted 216/8459 = 2%, 213 KB/s], Decompressed: 213
Downloaded: 261 file(s) [attempted 261/8459 = 3%, 336 KB/s], Decompressed: 258
Downloaded: 309 file(s) [attempted 309/8459 = 3%, 450 KB/s], Decompressed: 307
Downloaded: 348 file(s) [attempted 348/8459 = 4%, 23 KB/s], Decompressed: 343
Downloaded: 386 file(s) [attempted 386/8459 = 4%, 41 KB/s], Decompressed: 377
Downloaded: 419 file(s) [attempted 419/8459 = 4%, 97 KB/s], Decompressed: 415
Downloaded: 460 file(s) [attempted 460/8459 = 5%, 73 KB/s], Decompressed: 456
Downloaded: 504 file(s) [attempted 504/8459 = 5%, 146 KB/s], Decompressed: 497
Downloaded: 547 file(s) [attempted 547/8459 = 6%, 29 KB/s], Decompressed: 542
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 48 KB/s], Decompressed: 576
Downloaded: 621 file(s) [attempted 621/8459 = 7%, 708 KB/s], Decompressed: 617
Downloaded: 662 file(s) [attempted 662/8459 = 7%, 47 KB/s], Decompressed: 655
Downloaded: 707 file(s) [attempted 707/8459 = 8%, 1203 KB/s], Decompressed: 703
Downloaded: 744 file(s) [attempted 744/8459 = 8%, 426 KB/s], Decompressed: 741
Downloaded: 782 file(s) [attempted 782/8459 = 9%, 285 KB/s], Decompressed: 771
Downloaded: 819 file(s) [attempted 819/8459 = 9%, 142 KB/s], Decompressed: 816
Downloaded: 862 file(s) [attempted 862/8459 = 10%, 438 KB/s], Decompressed: 857
Downloaded: 905 file(s) [attempted 905/8459 = 10%, 46 KB/s], Decompressed: 898
Downloaded: 946 file(s) [attempted 946/8459 = 11%, 179 KB/s], Decompressed: 939
Downloaded: 984 file(s) [attempted 984/8459 = 11%, 119 KB/s], Decompressed: 980
Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 463 KB/s], Decompressed: 1018
Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 231 KB/s], Decompressed: 1066
Downloaded: 1114 file(s) [attempted 1114/8459 = 13%, 448 KB/s], Decompressed: 1110
Downloaded: 1158 file(s) [attempted 1158/8459 = 13%, 267 KB/s], Decompressed: 1151
Downloaded: 1192 file(s) [attempted 1192/8459 = 14%, 62 KB/s], Decompressed: 1189
Downloaded: 1230 file(s) [attempted 1230/8459 = 14%, 232 KB/s], Decompressed: 1223
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 679 KB/s], Decompressed: 1268
Downloaded: 1319 file(s) [attempted 1319/8459 = 15%, 790 KB/s], Decompressed: 1316
Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 800 KB/s], Decompressed: 1364
Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 108 KB/s], Decompressed: 1415
Downloaded: 1466 file(s) [attempted 1466/8459 = 17%, 195 KB/s], Decompressed: 1459
Downloaded: 1501 file(s) [attempted 1501/8459 = 17%, 174 KB/s], Decompressed: 1494
Downloaded: 1542 file(s) [attempted 1542/8459 = 18%, 65 KB/s], Decompressed: 1538
Downloaded: 1584 file(s) [attempted 1584/8459 = 18%, 697 KB/s], Decompressed: 1579
Downloaded: 1625 file(s) [attempted 1625/8459 = 19%, 213 KB/s], Decompressed: 1620
Downloaded: 1665 file(s) [attempted 1665/8459 = 19%, 477 KB/s], Decompressed: 1661
Downloaded: 1702 file(s) [attempted 1702/8459 = 20%, 459 KB/s], Decompressed: 1699
Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 108 KB/s], Decompressed: 1740
Downloaded: 1781 file(s) [attempted 1781/8459 = 21%, 26 KB/s], Decompressed: 1778
Downloaded: 1826 file(s) [attempted 1826/8459 = 21%, 217 KB/s], Decompressed: 1822
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 1488 KB/s], Decompressed: 1856
Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 90 KB/s], Decompressed: 1901
Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 97 KB/s], Decompressed: 1939
Downloaded: 1983 file(s) [attempted 1983/8459 = 23%, 76 KB/s], Decompressed: 1980
Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 118 KB/s], Decompressed: 2022
Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 25 KB/s], Decompressed: 2058
Downloaded: 2110 file(s) [attempted 2110/8459 = 24%, 363 KB/s], Decompressed: 2103
Downloaded: 2149 file(s) [attempted 2149/8459 = 25%, 187 KB/s], Decompressed: 2140
Downloaded: 2182 file(s) [attempted 2182/8459 = 25%, 580 KB/s], Decompressed: 2178
Downloaded: 2226 file(s) [attempted 2226/8459 = 26%, 310 KB/s], Decompressed: 2223
Downloaded: 2271 file(s) [attempted 2271/8459 = 26%, 595 KB/s], Decompressed: 2267
Downloaded: 2314 file(s) [attempted 2314/8459 = 27%, 113 KB/s], Decompressed: 2308
Downloaded: 2349 file(s) [attempted 2349/8459 = 27%, 366 KB/s], Decompressed: 2346
Downloaded: 2387 file(s) [attempted 2387/8459 = 28%, 657 KB/s], Decompressed: 2383
Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 24 KB/s], Decompressed: 2425
Downloaded: 2472 file(s) [attempted 2472/8459 = 29%, 110 KB/s], Decompressed: 2469
Downloaded: 2517 file(s) [attempted 2517/8459 = 29%, 233 KB/s], Decompressed: 2513
Downloaded: 2551 file(s) [attempted 2551/8459 = 30%, 223 KB/s], Decompressed: 2544
Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 580 KB/s], Decompressed: 2589
Downloaded: 2637 file(s) [attempted 2637/8459 = 31%, 96 KB/s], Decompressed: 2633
Downloaded: 2681 file(s) [attempted 2681/8459 = 31%, 28 KB/s], Decompressed: 2678
Downloaded: 2726 file(s) [attempted 2726/8459 = 32%, 103 KB/s], Decompressed: 2722
Downloaded: 2756 file(s) [attempted 2756/8459 = 32%, 231 KB/s], Decompressed: 2753
Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 1202 KB/s], Decompressed: 2794
Downloaded: 2839 file(s) [attempted 2839/8459 = 33%, 254 KB/s], Decompressed: 2835
Downloaded: 2883 file(s) [attempted 2883/8459 = 34%, 77 KB/s], Decompressed: 2880
Downloaded: 2924 file(s) [attempted 2924/8459 = 34%, 213 KB/s], Decompressed: 2917
Downloaded: 2965 file(s) [attempted 2965/8459 = 35%, 227 KB/s], Decompressed: 2958
Downloaded: 2999 file(s) [attempted 2999/8459 = 35%, 105 KB/s], Decompressed: 2996
Downloaded: 3041 file(s) [attempted 3041/8459 = 35%, 230 KB/s], Decompressed: 3034
Downloaded: 3085 file(s) [attempted 3085/8459 = 36%, 334 KB/s], Decompressed: 3082
Downloaded: 3130 file(s) [attempted 3130/8459 = 37%, 161 KB/s], Decompressed: 3126
Downloaded: 3177 file(s) [attempted 3177/8459 = 37%, 81 KB/s], Decompressed: 3174
Downloaded: 3213 file(s) [attempted 3213/8459 = 37%, 80 KB/s], Decompressed: 3208
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 44 KB/s], Decompressed: 3246
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 314 KB/s], Decompressed: 3287
Downloaded: 3335 file(s) [attempted 3335/8459 = 39%, 157 KB/s], Decompressed: 3331
Downloaded: 3379 file(s) [attempted 3379/8459 = 39%, 257 KB/s], Decompressed: 3376
Downloaded: 3410 file(s) [attempted 3410/8459 = 40%, 733 KB/s], Decompressed: 3407
Downloaded: 3451 file(s) [attempted 3451/8459 = 40%, 336 KB/s], Decompressed: 3448
Downloaded: 3496 file(s) [attempted 3496/8459 = 41%, 1963 KB/s], Decompressed: 3492
Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 271 KB/s], Decompressed: 3533
Downloaded: 3581 file(s) [attempted 3581/8459 = 42%, 73 KB/s], Decompressed: 3574
Downloaded: 3615 file(s) [attempted 3615/8459 = 42%, 469 KB/s], Decompressed: 3605
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 1404 KB/s], Decompressed: 3650
Downloaded: 3699 file(s) [attempted 3699/8459 = 43%, 1134 KB/s], Decompressed: 3694
Downloaded: 3742 file(s) [attempted 3742/8459 = 44%, 189 KB/s], Decompressed: 3739
Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 164 KB/s], Decompressed: 3773
Downloaded: 3821 file(s) [attempted 3821/8459 = 45%, 378 KB/s], Decompressed: 3814
Downloaded: 3858 file(s) [attempted 3858/8459 = 45%, 90 KB/s], Decompressed: 3852
Downloaded: 3900 file(s) [attempted 3900/8459 = 46%, 128 KB/s], Decompressed: 3896
Downloaded: 3941 file(s) [attempted 3941/8459 = 46%, 225 KB/s], Decompressed: 3937
Downloaded: 3982 file(s) [attempted 3982/8459 = 47%, 56 KB/s], Decompressed: 3978
Downloaded: 4023 file(s) [attempted 4023/8459 = 47%, 487 KB/s], Decompressed: 4016
Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 390 KB/s], Decompressed: 4058
Downloaded: 4101 file(s) [attempted 4101/8459 = 48%, 341 KB/s], Decompressed: 4095
Downloaded: 4146 file(s) [attempted 4146/8459 = 49%, 98 KB/s], Decompressed: 4143
Downloaded: 4187 file(s) [attempted 4187/8459 = 49%, 450 KB/s], Decompressed: 4180
Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 364 KB/s], Decompressed: 4221
Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 543 KB/s], Decompressed: 4266
Downloaded: 4310 file(s) [attempted 4310/8459 = 50%, 889 KB/s], Decompressed: 4307
Downloaded: 4348 file(s) [attempted 4348/8459 = 51%, 534 KB/s], Decompressed: 4344
Downloaded: 4388 file(s) [attempted 4388/8459 = 51%, 1285 KB/s], Decompressed: 4382
Downloaded: 4433 file(s) [attempted 4433/8459 = 52%, 129 KB/s], Decompressed: 4430
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 421 KB/s], Decompressed: 4474
Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 554 KB/s], Decompressed: 4513
Downloaded: 4550 file(s) [attempted 4550/8459 = 53%, 1127 KB/s], Decompressed: 4546
Downloaded: 4594 file(s) [attempted 4594/8459 = 54%, 41 KB/s], Decompressed: 4587
Downloaded: 4639 file(s) [attempted 4639/8459 = 54%, 65 KB/s], Decompressed: 4635
Downloaded: 4681 file(s) [attempted 4681/8459 = 55%, 465 KB/s], Decompressed: 4676
Downloaded: 4724 file(s) [attempted 4724/8459 = 55%, 315 KB/s], Decompressed: 4721
Downloaded: 4765 file(s) [attempted 4765/8459 = 56%, 378 KB/s], Decompressed: 4762
Downloaded: 4802 file(s) [attempted 4802/8459 = 56%, 105 KB/s], Decompressed: 4796
Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 327 KB/s], Decompressed: 4837
Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 1061 KB/s], Decompressed: 4882
Downloaded: 4924 file(s) [attempted 4924/8459 = 58%, 403 KB/s], Decompressed: 4919
Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 304 KB/s], Decompressed: 4964
Downloaded: 5008 file(s) [attempted 5008/8459 = 59%, 65 KB/s], Decompressed: 4998
Downloaded: 5049 file(s) [attempted 5049/8459 = 59%, 159 KB/s], Decompressed: 5046
Downloaded: 5088 file(s) [attempted 5088/8459 = 60%, 202 KB/s], Decompressed: 5084
Downloaded: 5132 file(s) [attempted 5132/8459 = 60%, 588 KB/s], Decompressed: 5128
Downloaded: 5176 file(s) [attempted 5176/8459 = 61%, 712 KB/s], Decompressed: 5169
Downloaded: 5217 file(s) [attempted 5217/8459 = 61%, 64 KB/s], Decompressed: 5210
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 775 KB/s], Decompressed: 5255
Downloaded: 5296 file(s) [attempted 5296/8459 = 62%, 778 KB/s], Decompressed: 5292
Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 720 KB/s], Decompressed: 5334
Downloaded: 5378 file(s) [attempted 5378/8459 = 63%, 462 KB/s], Decompressed: 5375
Downloaded: 5420 file(s) [attempted 5420/8459 = 64%, 123 KB/s], Decompressed: 5416
Downloaded: 5460 file(s) [attempted 5460/8459 = 64%, 75 KB/s], Decompressed: 5453
Downloaded: 5498 file(s) [attempted 5498/8459 = 64%, 308 KB/s], Decompressed: 5491
Downloaded: 5539 file(s) [attempted 5539/8459 = 65%, 239 KB/s], Decompressed: 5535
Downloaded: 5583 file(s) [attempted 5583/8459 = 66%, 340 KB/s], Decompressed: 5580
Downloaded: 5624 file(s) [attempted 5624/8459 = 66%, 515 KB/s], Decompressed: 5621
Downloaded: 5662 file(s) [attempted 5662/8459 = 66%, 248 KB/s], Decompressed: 5659
Downloaded: 5703 file(s) [attempted 5703/8459 = 67%, 198 KB/s], Decompressed: 5696
Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 41 KB/s], Decompressed: 5737
Downloaded: 5785 file(s) [attempted 5785/8459 = 68%, 248 KB/s], Decompressed: 5778
Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 101 KB/s], Decompressed: 5823
Downloaded: 5867 file(s) [attempted 5867/8459 = 69%, 175 KB/s], Decompressed: 5864
Downloaded: 5913 file(s) [attempted 5913/8459 = 69%, 68 KB/s], Decompressed: 5908
Downloaded: 5953 file(s) [attempted 5953/8459 = 70%, 280 KB/s], Decompressed: 5946
Downloaded: 5994 file(s) [attempted 5994/8459 = 70%, 314 KB/s], Decompressed: 5987
Downloaded: 6028 file(s) [attempted 6028/8459 = 71%, 328 KB/s], Decompressed: 6025
Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 256 KB/s], Decompressed: 6066
Downloaded: 6117 file(s) [attempted 6117/8459 = 72%, 446 KB/s], Decompressed: 6110
Downloaded: 6162 file(s) [attempted 6162/8459 = 72%, 210 KB/s], Decompressed: 6158
Downloaded: 6203 file(s) [attempted 6203/8459 = 73%, 623 KB/s], Decompressed: 6196
Downloaded: 6240 file(s) [attempted 6240/8459 = 73%, 565 KB/s], Decompressed: 6234
Downloaded: 6278 file(s) [attempted 6278/8459 = 74%, 606 KB/s], Decompressed: 6275
Downloaded: 6319 file(s) [attempted 6319/8459 = 74%, 590 KB/s], Decompressed: 6316
Downloaded: 6364 file(s) [attempted 6364/8459 = 75%, 1080 KB/s], Decompressed: 6360
Downloaded: 6405 file(s) [attempted 6405/8459 = 75%, 34 KB/s], Decompressed: 6401
Downloaded: 6446 file(s) [attempted 6446/8459 = 76%, 38 KB/s], Decompressed: 6442
Downloaded: 6483 file(s) [attempted 6483/8459 = 76%, 402 KB/s], Decompressed: 6477
Downloaded: 6524 file(s) [attempted 6524/8459 = 77%, 88 KB/s], Decompressed: 6521
Downloaded: 6569 file(s) [attempted 6569/8459 = 77%, 89 KB/s], Decompressed: 6562
Downloaded: 6608 file(s) [attempted 6608/8459 = 78%, 243 KB/s], Decompressed: 6607
Downloaded: 6652 file(s) [attempted 6652/8459 = 78%, 451 KB/s], Decompressed: 6644
Downloaded: 6692 file(s) [attempted 6692/8459 = 79%, 383 KB/s], Decompressed: 6685
Downloaded: 6733 file(s) [attempted 6733/8459 = 79%, 421 KB/s], Decompressed: 6730
Downloaded: 6774 file(s) [attempted 6774/8459 = 80%, 282 KB/s], Decompressed: 6771
Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 135 KB/s], Decompressed: 6809
Downloaded: 6856 file(s) [attempted 6856/8459 = 81%, 104 KB/s], Decompressed: 6853
Downloaded: 6901 file(s) [attempted 6901/8459 = 81%, 105 KB/s], Decompressed: 6894
Downloaded: 6935 file(s) [attempted 6935/8459 = 81%, 183 KB/s], Decompressed: 6932
Downloaded: 6976 file(s) [attempted 6976/8459 = 82%, 56 KB/s], Decompressed: 6973
Downloaded: 7021 file(s) [attempted 7021/8459 = 83%, 113 KB/s], Decompressed: 7017
Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 1165 KB/s], Decompressed: 7062
Downloaded: 7106 file(s) [attempted 7106/8459 = 84%, 345 KB/s], Decompressed: 7103
Downloaded: 7138 file(s) [attempted 7138/8459 = 84%, 485 KB/s], Decompressed: 7134
Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 109 KB/s], Decompressed: 7171
Downloaded: 7226 file(s) [attempted 7226/8459 = 85%, 763 KB/s], Decompressed: 7223
Downloaded: 7269 file(s) [attempted 7269/8459 = 85%, 81 KB/s], Decompressed: 7260
Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 141 KB/s], Decompressed: 7301
Downloaded: 7340 file(s) [attempted 7340/8459 = 86%, 116 KB/s], Decompressed: 7336
Downloaded: 7383 file(s) [attempted 7383/8459 = 87%, 64 KB/s], Decompressed: 7380
Downloaded: 7428 file(s) [attempted 7428/8459 = 87%, 563 KB/s], Decompressed: 7425
Downloaded: 7472 file(s) [attempted 7472/8459 = 88%, 181 KB/s], Decompressed: 7466
Downloaded: 7509 file(s) [attempted 7509/8459 = 88%, 221 KB/s], Decompressed: 7503
Downloaded: 7544 file(s) [attempted 7544/8459 = 89%, 168 KB/s], Decompressed: 7537
Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 161 KB/s], Decompressed: 7585
Downloaded: 7637 file(s) [attempted 7637/8459 = 90%, 197 KB/s], Decompressed: 7633
Downloaded: 7681 file(s) [attempted 7681/8459 = 90%, 564 KB/s], Decompressed: 7678
Downloaded: 7722 file(s) [attempted 7722/8459 = 91%, 744 KB/s], Decompressed: 7712
Downloaded: 7757 file(s) [attempted 7757/8459 = 91%, 760 KB/s], Decompressed: 7753
Downloaded: 7794 file(s) [attempted 7794/8459 = 92%, 511 KB/s], Decompressed: 7791
Downloaded: 7839 file(s) [attempted 7839/8459 = 92%, 299 KB/s], Decompressed: 7835
Downloaded: 7883 file(s) [attempted 7883/8459 = 93%, 981 KB/s], Decompressed: 7880
Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 47 KB/s], Decompressed: 7924
Downloaded: 7965 file(s) [attempted 7965/8459 = 94%, 182 KB/s], Decompressed: 7955
Downloaded: 8000 file(s) [attempted 8000/8459 = 94%, 224 KB/s], Decompressed: 7996
Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 501 KB/s], Decompressed: 8041
Downloaded: 8086 file(s) [attempted 8086/8459 = 95%, 189 KB/s], Decompressed: 8082
Downloaded: 8133 file(s) [attempted 8133/8459 = 96%, 174 KB/s], Decompressed: 8130
Downloaded: 8169 file(s) [attempted 8169/8459 = 96%, 306 KB/s], Decompressed: 8160
Downloaded: 8205 file(s) [attempted 8205/8459 = 96%, 154 KB/s], Decompressed: 8201
Downloaded: 8249 file(s) [attempted 8249/8459 = 97%, 191 KB/s], Decompressed: 8246
Downloaded: 8291 file(s) [attempted 8291/8459 = 98%, 494 KB/s], Decompressed: 8287
Downloaded: 8335 file(s) [attempted 8335/8459 = 98%, 87 KB/s], Decompressed: 8331
Downloaded: 8371 file(s) [attempted 8371/8459 = 98%, 622 KB/s], Decompressed: 8362
Downloaded: 8407 file(s) [attempted 8407/8459 = 99%, 247 KB/s], Decompressed: 8403
Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 837 KB/s], Decompressed: 8444
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 837 KB/s], Decompressed: 8455

semantic_extract exit 0 duration 1m 59s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache f04752e91581a87c3d8d8a87c9c62d574535d7f0c9532c8f513c6579555ccc6c
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 1m 52s · created 6/11/2026, 12:22:22 AM

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

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

lean_checker exit 0 duration 4m 54s · created 6/11/2026, 12:22:22 AM

lake build

✔ [3401/3416] Built Iut.Stage1.IUTStage1SourceCore (46s)
✔ [3402/3416] Built Iut.Stage1.IUTStage1Remark312Absorption (3.1s)
✔ [3403/3416] Built Iut.Stage1.IUTStage1IUTIVAlgebra (9.9s)
✔ [3404/3416] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
✔ [3405/3416] Built Iut.Stage1.IUTStage1StepX (4.9s)
✔ [3406/3416] Built Iut.Stage1.IUTStage1Gaussian (9.2s)
✔ [3407/3416] Built Iut.Stage1.IUTStage1HodgeSHE (5.5s)
✔ [3408/3416] Built Iut.Stage1.IUTStage1Theorem311 (4.6s)
✔ [3409/3416] Built Iut.Stage1.IUTStage1StepXI (17s)
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (132s)
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) [0x7792f29c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7792f29bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7792f29bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7792f28f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7792f28f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7792f29caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7792f2832923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7792f2832b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7792f2833827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7792f28341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7792f29c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7792f2615adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7792f29c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7792f29c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7792f299b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7792f2615c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7792eda22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7792ed80cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7792ed369a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7792ed369f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7792ea24524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7792ea245305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5e715c4c08da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (8.4s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.3s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (35s)
✔ [3414/3416] Built Iut.Basic (2.7s)
✔ [3415/3416] Built Iut (2.5s)
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/11/2026, 12:22:22 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_module_facts exit 0 duration 5m 22s · created 6/11/2026, 12:22:22 AM

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

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: 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

semantic_module_facts exit 0 duration 5m 15s · created 6/11/2026, 12:22:22 AM

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

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_module_facts exit 0 duration 1m 45s · created 6/11/2026, 12:22:22 AM

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

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

semantic_module_facts exit 0 duration 1m 47s · created 6/11/2026, 12:22:22 AM

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

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

semantic_module_facts exit 0 duration 1m 44s · created 6/11/2026, 12:22:22 AM

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

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

semantic_module_facts exit 0 duration 1m 47s · created 6/11/2026, 12:22:22 AM

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

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

semantic_module_facts exit 0 duration 5m 14s · created 6/11/2026, 12:22:22 AM

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

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

semantic_module_facts exit 1 duration 2s · created 6/11/2026, 12:22:22 AM

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

.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/build/lib/lean/Iut/Foundations/InitialThetaDataExample.olean' of module Iut.Foundations.InitialThetaDataExample does not exist

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 failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner

semantic_extract exit 0 duration 5m 19s · created 6/11/2026, 12:22:22 AM

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

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

semantic_extract exit 0 duration 5m 14s · created 6/11/2026, 12:22:22 AM

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

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 2m 17s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache 91173b292067b1a93ea64425cc888039ebce7a3e364765ecea90e7a5cbd3d047
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 1m 59s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache 5e719f139e700d3ec36d870eb0df93c69e39d1b25bc64de0e83c7820c297cc88
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 8m 7s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache e925bad531c9c8172209069553d6ef13f8bc4d43ffee8f9f45ce1b2a571648d9
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 1 duration 2s · created 6/11/2026, 12:22:22 AM

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

.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/build/lib/lean/Iut/Foundations/InitialThetaDataExample.olean' of module Iut.Foundations.InitialThetaDataExample does not exist

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 failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner

semantic_extract exit 0 duration 2m 11s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache b8207442bfba00511b560efc544d5ce67b0aa813df3d432a1aba6b1f99808bdf
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 2m 2s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache 56cf09ccb3908696b8e5e7742ce037825c061cf4f72cf51826c370ecdd278b63
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 2m 2s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache 82cff17b2a0859360c864be978661e734ea49f8bd78dbf096db8866b58caf113
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 23s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache a9a06e968839d8b8f7e22b6bb42203d7559473912527ed06adfeb9a10487c71a
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 1m 58s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache 6b68dbdfef85a7b6943bcf3aed743bff07bc5a8789269f4969952ccbec066986
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 1m 57s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache 5a5015d089cfb0ec2d9e00c036585dab768f83e5b768c8aa0991818ae117b9aa
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 4m 54s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache 916ea7b0333772c3e6f8e394e031f32699844624a1add271ecbcb781a9f49e93
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 4m 42s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache 2bfcdcefc85e86330c36ad81e41c2ddb7c7e852d7b70484d888f87d3783eb3ee
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 4m 58s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache ac720950978d81db58a9b7127c0c29b52147e5d60a6dd5804497dee52cf190ea
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 41s · created 6/11/2026, 12:22:22 AM

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

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 31m 10s · created 6/11/2026, 12:22:22 AM

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

lean semantic helper: restored compiled static runner cache f4d9c003c7452016e42c7fead986b54b7a3d6e7471516ee89e90353366820d66
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 4s · created 6/11/2026, 12:22:22 AM

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

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 1h 39m · created 6/11/2026, 12:22:22 AM

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

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 7m 18s · created 6/11/2026, 12:22:22 AM

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

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 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 52s · created 6/11/2026, 12:22:22 AM

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

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 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 47s · created 6/11/2026, 12:22:22 AM

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

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 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 5m 34s · created 6/11/2026, 12:22:22 AM

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

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 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 5m 41s · created 6/11/2026, 12:22:22 AM

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

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 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 143 duration 21m 17s · created 6/11/2026, 12:22:22 AM

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

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 361c3a3115683a95ae5a195d9d3288c0f30083b629ae0efa02efc9266225a437
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 48s · created 6/11/2026, 12:22:22 AM

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

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 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 18m 48s · created 6/11/2026, 12:22:22 AM

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

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 9c9cf2b3451621905e924ca74e022d2283294e8f723d50f83339e66904461aaf
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 57s · created 6/11/2026, 12:22:22 AM

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

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 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 2m 7s · created 6/11/2026, 12:22:22 AM

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

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 b278679b96703b88f46c5058abea7a921c64bde7c3009a5f675db878cd3eba6c
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 5s · created 6/11/2026, 12:22:22 AM

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

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 789c65a0d29891fa409358efae098c665e03a540d880d2a888005d1f8a1e3e15
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 1 duration 1s · created 6/11/2026, 12:22:22 AM

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

.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/build/lib/lean/Iut/Tools/CheckDecls.olean' of module Iut.Tools.CheckDecls does not exist

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 failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner