Verification run

Run 343

promachina/iut-lean branch master triggered via github_backfill

succeeded commit c85d209b537b toolchain lean-v4-30-0 prover lean took 4h 21m · 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/11/2026, 10:31:58 PM

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

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

git_checkout exit 128 duration 4 ms · created 6/11/2026, 10:31:58 PM

git checkout c85d209b537b38a6c5b64447e71c4501a552ce25

fatal: reference is not a tree: c85d209b537b38a6c5b64447e71c4501a552ce25

git_checkout exit 0 duration 967 ms · created 6/11/2026, 10:31:58 PM

git fetch --depth 1 origin c85d209b537b38a6c5b64447e71c4501a552ce25

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

git_checkout exit 0 duration 112 ms · created 6/11/2026, 10:31:58 PM

git checkout c85d209b537b38a6c5b64447e71c4501a552ce25 (after fetch)

Note: switching to 'c85d209b537b38a6c5b64447e71c4501a552ce25'.

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 c85d209 Add selected scalar parameter valuation hull cover

lake_cache exit 0 duration 1m 10s · created 6/11/2026, 10:31:58 PM

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)

info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: mathlib: checking out revision 'c5ea00351c28e24afc9f0f84379aa41082b1188f'
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
✔ [7/24] Built Cache.Lean (526ms)
✔ [12/24] Built Cache.Lean:c.o (127ms)
✔ [14/24] Built Cache.Init (358ms)
✔ [15/24] Built Cache.IO (1.7s)
✔ [16/24] Built Cache.Init:c.o (75ms)
✔ [17/24] Built Cache.IO:c.o (1.1s)
✔ [18/24] Built Cache.Hashing (905ms)
✔ [19/24] Built Cache.Hashing:c.o (368ms)
✔ [20/24] Built Cache.Requests (1.0s)
✔ [21/24] Built Cache.Requests:c.o (1.8s)
✔ [22/24] Built Cache.Main (894ms)
✔ [23/24] Built Cache.Main:c.o (524ms)
✔ [24/24] Built cache:exe (794ms)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 8 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 1 KB/s], Decompressed: 12
Downloaded: 42 file(s) [attempted 42/8459 = 0%, 11 KB/s], Decompressed: 36
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 42 KB/s], Decompressed: 58
Downloaded: 100 file(s) [attempted 100/8459 = 1%, 49 KB/s], Decompressed: 80
Downloaded: 131 file(s) [attempted 131/8459 = 1%, 357 KB/s], Decompressed: 107
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 73 KB/s], Decompressed: 138
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 198 KB/s], Decompressed: 182
Downloaded: 240 file(s) [attempted 240/8459 = 2%, 421 KB/s], Decompressed: 216
Downloaded: 279 file(s) [attempted 279/8459 = 3%, 918 KB/s], Decompressed: 251
Downloaded: 316 file(s) [attempted 316/8459 = 3%, 336 KB/s], Decompressed: 295
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 23 KB/s], Decompressed: 347
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 1017 KB/s], Decompressed: 374
Downloaded: 429 file(s) [attempted 429/8459 = 5%, 108 KB/s], Decompressed: 412
Downloaded: 470 file(s) [attempted 470/8459 = 5%, 819 KB/s], Decompressed: 429
Downloaded: 511 file(s) [attempted 511/8459 = 6%, 67 KB/s], Decompressed: 473
Downloaded: 552 file(s) [attempted 552/8459 = 6%, 288 KB/s], Decompressed: 518
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 804 KB/s], Decompressed: 542
Downloaded: 624 file(s) [attempted 624/8459 = 7%, 297 KB/s], Decompressed: 600
Downloaded: 669 file(s) [attempted 669/8459 = 7%, 453 KB/s], Decompressed: 621
Downloaded: 710 file(s) [attempted 710/8459 = 8%, 152 KB/s], Decompressed: 672
Downloaded: 754 file(s) [attempted 754/8459 = 8%, 59 KB/s], Decompressed: 737
Downloaded: 799 file(s) [attempted 799/8459 = 9%, 739 KB/s], Decompressed: 771
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 1220 KB/s], Decompressed: 802
Downloaded: 872 file(s) [attempted 872/8459 = 10%, 357 KB/s], Decompressed: 860
Downloaded: 915 file(s) [attempted 915/8459 = 10%, 179 KB/s], Decompressed: 891
Downloaded: 960 file(s) [attempted 960/8459 = 11%, 228 KB/s], Decompressed: 932
Downloaded: 1002 file(s) [attempted 1002/8459 = 11%, 299 KB/s], Decompressed: 973
Downloaded: 1042 file(s) [attempted 1042/8459 = 12%, 45 KB/s], Decompressed: 1015
Downloaded: 1080 file(s) [attempted 1080/8459 = 12%, 42 KB/s], Decompressed: 1035
Downloaded: 1114 file(s) [attempted 1114/8459 = 13%, 403 KB/s], Decompressed: 1059
Downloaded: 1162 file(s) [attempted 1162/8459 = 13%, 1541 KB/s], Decompressed: 1121
Downloaded: 1210 file(s) [attempted 1210/8459 = 14%, 242 KB/s], Decompressed: 1158
Downloaded: 1254 file(s) [attempted 1254/8459 = 14%, 106 KB/s], Decompressed: 1202
Downloaded: 1288 file(s) [attempted 1288/8459 = 15%, 131 KB/s], Decompressed: 1240
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 307 KB/s], Decompressed: 1278
Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 770 KB/s], Decompressed: 1312
Downloaded: 1408 file(s) [attempted 1408/8459 = 16%, 228 KB/s], Decompressed: 1381
Downloaded: 1453 file(s) [attempted 1453/8459 = 17%, 102 KB/s], Decompressed: 1408
Downloaded: 1489 file(s) [attempted 1489/8459 = 17%, 252 KB/s], Decompressed: 1429
Downloaded: 1528 file(s) [attempted 1528/8459 = 18%, 128 KB/s], Decompressed: 1490
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 412 KB/s], Decompressed: 1524
Downloaded: 1610 file(s) [attempted 1610/8459 = 19%, 31 KB/s], Decompressed: 1569
Downloaded: 1651 file(s) [attempted 1651/8459 = 19%, 1898 KB/s], Decompressed: 1603
Downloaded: 1692 file(s) [attempted 1692/8459 = 20%, 278 KB/s], Decompressed: 1665
Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 83 KB/s], Decompressed: 1702
Downloaded: 1778 file(s) [attempted 1778/8459 = 21%, 256 KB/s], Decompressed: 1730
Downloaded: 1822 file(s) [attempted 1822/8459 = 21%, 204 KB/s], Decompressed: 1785
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 142 KB/s], Decompressed: 1819
Downloaded: 1894 file(s) [attempted 1894/8459 = 22%, 463 KB/s], Decompressed: 1843
Downloaded: 1935 file(s) [attempted 1935/8459 = 22%, 72 KB/s], Decompressed: 1877
Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 50 KB/s], Decompressed: 1921
Downloaded: 2017 file(s) [attempted 2017/8459 = 23%, 131 KB/s], Decompressed: 1963
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 39 KB/s], Decompressed: 1997
Downloaded: 2096 file(s) [attempted 2096/8459 = 24%, 336 KB/s], Decompressed: 1997
Downloaded: 2140 file(s) [attempted 2140/8459 = 25%, 623 KB/s], Decompressed: 2058
Downloaded: 2182 file(s) [attempted 2182/8459 = 25%, 54 KB/s], Decompressed: 2058
Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 126 KB/s], Decompressed: 2123
Downloaded: 2260 file(s) [attempted 2260/8459 = 26%, 268 KB/s], Decompressed: 2188
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 1012 KB/s], Decompressed: 2188
Downloaded: 2346 file(s) [attempted 2346/8459 = 27%, 811 KB/s], Decompressed: 2253
Downloaded: 2383 file(s) [attempted 2383/8459 = 28%, 670 KB/s], Decompressed: 2308
Downloaded: 2425 file(s) [attempted 2425/8459 = 28%, 145 KB/s], Decompressed: 2360
Downloaded: 2466 file(s) [attempted 2466/8459 = 29%, 56 KB/s], Decompressed: 2360
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 44 KB/s], Decompressed: 2425
Downloaded: 2548 file(s) [attempted 2548/8459 = 30%, 69 KB/s], Decompressed: 2486
Downloaded: 2589 file(s) [attempted 2589/8459 = 30%, 142 KB/s], Decompressed: 2537
Downloaded: 2626 file(s) [attempted 2626/8459 = 31%, 146 KB/s], Decompressed: 2575
Downloaded: 2661 file(s) [attempted 2661/8459 = 31%, 51 KB/s], Decompressed: 2609
Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 936 KB/s], Decompressed: 2650
Downloaded: 2746 file(s) [attempted 2746/8459 = 32%, 567 KB/s], Decompressed: 2650
Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 403 KB/s], Decompressed: 2702
Downloaded: 2832 file(s) [attempted 2832/8459 = 33%, 31 KB/s], Decompressed: 2753
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 539 KB/s], Decompressed: 2804
Downloaded: 2911 file(s) [attempted 2911/8459 = 34%, 284 KB/s], Decompressed: 2859
Downloaded: 2954 file(s) [attempted 2954/8459 = 34%, 150 KB/s], Decompressed: 2904
Downloaded: 2993 file(s) [attempted 2993/8459 = 35%, 192 KB/s], Decompressed: 2904
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 109 KB/s], Decompressed: 2952
Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 201 KB/s], Decompressed: 3000
Downloaded: 3109 file(s) [attempted 3109/8459 = 36%, 299 KB/s], Decompressed: 3054
Downloaded: 3150 file(s) [attempted 3150/8459 = 37%, 93 KB/s], Decompressed: 3102
Downloaded: 3191 file(s) [attempted 3191/8459 = 37%, 191 KB/s], Decompressed: 3102
Downloaded: 3229 file(s) [attempted 3229/8459 = 38%, 162 KB/s], Decompressed: 3147
Downloaded: 3270 file(s) [attempted 3270/8459 = 38%, 338 KB/s], Decompressed: 3201
Downloaded: 3311 file(s) [attempted 3311/8459 = 39%, 214 KB/s], Decompressed: 3249
Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 234 KB/s], Decompressed: 3297
Downloaded: 3392 file(s) [attempted 3392/8459 = 40%, 542 KB/s], Decompressed: 3297
Downloaded: 3431 file(s) [attempted 3431/8459 = 40%, 24 KB/s], Decompressed: 3345
Downloaded: 3468 file(s) [attempted 3468/8459 = 40%, 293 KB/s], Decompressed: 3393
Downloaded: 3513 file(s) [attempted 3513/8459 = 41%, 62 KB/s], Decompressed: 3472
Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 139 KB/s], Decompressed: 3509
Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 169 KB/s], Decompressed: 3544
Downloaded: 3626 file(s) [attempted 3626/8459 = 42%, 733 KB/s], Decompressed: 3602
Downloaded: 3670 file(s) [attempted 3670/8459 = 43%, 446 KB/s], Decompressed: 3622
Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 256 KB/s], Decompressed: 3660
Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 192 KB/s], Decompressed: 3698
Downloaded: 3787 file(s) [attempted 3787/8459 = 44%, 89 KB/s], Decompressed: 3759
Downloaded: 3824 file(s) [attempted 3824/8459 = 45%, 385 KB/s], Decompressed: 3780
Downloaded: 3869 file(s) [attempted 3869/8459 = 45%, 135 KB/s], Decompressed: 3835
Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 1591 KB/s], Decompressed: 3869
Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 234 KB/s], Decompressed: 3906
Downloaded: 3989 file(s) [attempted 3989/8459 = 47%, 26 KB/s], Decompressed: 3934
Downloaded: 4026 file(s) [attempted 4026/8459 = 47%, 1338 KB/s], Decompressed: 3995
Downloaded: 4071 file(s) [attempted 4071/8459 = 48%, 290 KB/s], Decompressed: 4023
Downloaded: 4115 file(s) [attempted 4115/8459 = 48%, 328 KB/s], Decompressed: 4060
Downloaded: 4153 file(s) [attempted 4153/8459 = 49%, 129 KB/s], Decompressed: 4095
Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 402 KB/s], Decompressed: 4139
Downloaded: 4232 file(s) [attempted 4232/8459 = 50%, 531 KB/s], Decompressed: 4184
Downloaded: 4273 file(s) [attempted 4273/8459 = 50%, 215 KB/s], Decompressed: 4184
Downloaded: 4310 file(s) [attempted 4310/8459 = 50%, 331 KB/s], Decompressed: 4225
Downloaded: 4348 file(s) [attempted 4348/8459 = 51%, 167 KB/s], Decompressed: 4276
Downloaded: 4392 file(s) [attempted 4392/8459 = 51%, 352 KB/s], Decompressed: 4276
Downloaded: 4430 file(s) [attempted 4430/8459 = 52%, 115 KB/s], Decompressed: 4344
Downloaded: 4468 file(s) [attempted 4468/8459 = 52%, 537 KB/s], Decompressed: 4403
Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 374 KB/s], Decompressed: 4457
Downloaded: 4550 file(s) [attempted 4550/8459 = 53%, 107 KB/s], Decompressed: 4457
Downloaded: 4591 file(s) [attempted 4591/8459 = 54%, 333 KB/s], Decompressed: 4509
Downloaded: 4625 file(s) [attempted 4625/8459 = 54%, 242 KB/s], Decompressed: 4567
Downloaded: 4663 file(s) [attempted 4663/8459 = 55%, 64 KB/s], Decompressed: 4567
Downloaded: 4707 file(s) [attempted 4707/8459 = 55%, 191 KB/s], Decompressed: 4622
Downloaded: 4755 file(s) [attempted 4755/8459 = 56%, 92 KB/s], Decompressed: 4683
Downloaded: 4796 file(s) [attempted 4796/8459 = 56%, 593 KB/s], Decompressed: 4683
Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 184 KB/s], Decompressed: 4748
Downloaded: 4875 file(s) [attempted 4875/8459 = 57%, 272 KB/s], Decompressed: 4807
Downloaded: 4913 file(s) [attempted 4913/8459 = 58%, 219 KB/s], Decompressed: 4858
Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 1259 KB/s], Decompressed: 4906
Downloaded: 5002 file(s) [attempted 5002/8459 = 59%, 235 KB/s], Decompressed: 4906
Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 438 KB/s], Decompressed: 4957
Downloaded: 5077 file(s) [attempted 5077/8459 = 60%, 320 KB/s], Decompressed: 5005
Downloaded: 5115 file(s) [attempted 5115/8459 = 60%, 1709 KB/s], Decompressed: 5060
Downloaded: 5156 file(s) [attempted 5156/8459 = 60%, 146 KB/s], Decompressed: 5060
Downloaded: 5197 file(s) [attempted 5197/8459 = 61%, 178 KB/s], Decompressed: 5111
Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 89 KB/s], Decompressed: 5169
Downloaded: 5295 file(s) [attempted 5295/8459 = 62%, 1429 KB/s], Decompressed: 5227
Downloaded: 5327 file(s) [attempted 5327/8459 = 62%, 316 KB/s], Decompressed: 5275
Downloaded: 5368 file(s) [attempted 5368/8459 = 63%, 431 KB/s], Decompressed: 5310
Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 266 KB/s], Decompressed: 5347
Downloaded: 5447 file(s) [attempted 5447/8459 = 64%, 725 KB/s], Decompressed: 5395
Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 1077 KB/s], Decompressed: 5395
Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 140 KB/s], Decompressed: 5447
Downloaded: 5570 file(s) [attempted 5570/8459 = 65%, 94 KB/s], Decompressed: 5494
Downloaded: 5607 file(s) [attempted 5607/8459 = 66%, 180 KB/s], Decompressed: 5549
Downloaded: 5648 file(s) [attempted 5648/8459 = 66%, 213 KB/s], Decompressed: 5549
Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 139 KB/s], Decompressed: 5601
Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 458 KB/s], Decompressed: 5652
Downloaded: 5772 file(s) [attempted 5772/8459 = 68%, 454 KB/s], Decompressed: 5707
Downloaded: 5809 file(s) [attempted 5809/8459 = 68%, 805 KB/s], Decompressed: 5707
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 628 KB/s], Decompressed: 5768
Downloaded: 5891 file(s) [attempted 5891/8459 = 69%, 48 KB/s], Decompressed: 5823
Downloaded: 5932 file(s) [attempted 5932/8459 = 70%, 107 KB/s], Decompressed: 5823
Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 41 KB/s], Decompressed: 5881
Downloaded: 6011 file(s) [attempted 6011/8459 = 71%, 122 KB/s], Decompressed: 5936
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 343 KB/s], Decompressed: 5984
Downloaded: 6090 file(s) [attempted 6090/8459 = 71%, 286 KB/s], Decompressed: 6039
Downloaded: 6134 file(s) [attempted 6134/8459 = 72%, 870 KB/s], Decompressed: 6039
Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 548 KB/s], Decompressed: 6086
Downloaded: 6213 file(s) [attempted 6213/8459 = 73%, 404 KB/s], Decompressed: 6138
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 33 KB/s], Decompressed: 6138
Downloaded: 6288 file(s) [attempted 6288/8459 = 74%, 375 KB/s], Decompressed: 6206
Downloaded: 6329 file(s) [attempted 6329/8459 = 74%, 364 KB/s], Decompressed: 6206
Downloaded: 6371 file(s) [attempted 6371/8459 = 75%, 347 KB/s], Decompressed: 6278
Downloaded: 6405 file(s) [attempted 6405/8459 = 75%, 222 KB/s], Decompressed: 6278
Downloaded: 6446 file(s) [attempted 6446/8459 = 76%, 729 KB/s], Decompressed: 6353
Downloaded: 6487 file(s) [attempted 6487/8459 = 76%, 382 KB/s], Decompressed: 6353
Downloaded: 6525 file(s) [attempted 6525/8459 = 77%, 516 KB/s], Decompressed: 6432
Downloaded: 6566 file(s) [attempted 6566/8459 = 77%, 89 KB/s], Decompressed: 6432
Downloaded: 6607 file(s) [attempted 6607/8459 = 78%, 166 KB/s], Decompressed: 6501
Downloaded: 6648 file(s) [attempted 6648/8459 = 78%, 263 KB/s], Decompressed: 6569
Downloaded: 6689 file(s) [attempted 6689/8459 = 79%, 384 KB/s], Decompressed: 6631
Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 249 KB/s], Decompressed: 6679
Downloaded: 6768 file(s) [attempted 6768/8459 = 80%, 70 KB/s], Decompressed: 6720
Downloaded: 6809 file(s) [attempted 6809/8459 = 80%, 166 KB/s], Decompressed: 6720
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 85 KB/s], Decompressed: 6764
Downloaded: 6884 file(s) [attempted 6884/8459 = 81%, 867 KB/s], Decompressed: 6815
Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 92 KB/s], Decompressed: 6867
Downloaded: 6966 file(s) [attempted 6966/8459 = 82%, 54 KB/s], Decompressed: 6911
Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 368 KB/s], Decompressed: 6911
Downloaded: 7044 file(s) [attempted 7044/8459 = 83%, 570 KB/s], Decompressed: 6963
Downloaded: 7086 file(s) [attempted 7086/8459 = 83%, 758 KB/s], Decompressed: 7011
Downloaded: 7127 file(s) [attempted 7127/8459 = 84%, 214 KB/s], Decompressed: 7055
Downloaded: 7168 file(s) [attempted 7168/8459 = 84%, 81 KB/s], Decompressed: 7130
Downloaded: 7206 file(s) [attempted 7206/8459 = 85%, 840 KB/s], Decompressed: 7165
Downloaded: 7247 file(s) [attempted 7247/8459 = 85%, 121 KB/s], Decompressed: 7202
Downloaded: 7284 file(s) [attempted 7284/8459 = 86%, 33 KB/s], Decompressed: 7236
Downloaded: 7322 file(s) [attempted 7322/8459 = 86%, 94 KB/s], Decompressed: 7236
Downloaded: 7363 file(s) [attempted 7363/8459 = 87%, 244 KB/s], Decompressed: 7325
Downloaded: 7401 file(s) [attempted 7401/8459 = 87%, 294 KB/s], Decompressed: 7363
Downloaded: 7445 file(s) [attempted 7445/8459 = 88%, 63 KB/s], Decompressed: 7397
Downloaded: 7479 file(s) [attempted 7479/8459 = 88%, 334 KB/s], Decompressed: 7425
Downloaded: 7520 file(s) [attempted 7520/8459 = 88%, 563 KB/s], Decompressed: 7464
Downloaded: 7558 file(s) [attempted 7558/8459 = 89%, 558 KB/s], Decompressed: 7500
Downloaded: 7599 file(s) [attempted 7599/8459 = 89%, 424 KB/s], Decompressed: 7534
Downloaded: 7644 file(s) [attempted 7644/8459 = 90%, 188 KB/s], Decompressed: 7568
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 281 KB/s], Decompressed: 7615
Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 186 KB/s], Decompressed: 7654
Downloaded: 7767 file(s) [attempted 7767/8459 = 91%, 98 KB/s], Decompressed: 7733
Downloaded: 7808 file(s) [attempted 7808/8459 = 92%, 456 KB/s], Decompressed: 7760
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 2303 KB/s], Decompressed: 7801
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 57 KB/s], Decompressed: 7801
Downloaded: 7924 file(s) [attempted 7924/8459 = 93%, 48 KB/s], Decompressed: 7842
Downloaded: 7965 file(s) [attempted 7965/8459 = 94%, 176 KB/s], Decompressed: 7893
Downloaded: 8003 file(s) [attempted 8003/8459 = 94%, 3658 KB/s], Decompressed: 7945
Downloaded: 8047 file(s) [attempted 8047/8459 = 95%, 79 KB/s], Decompressed: 7945
Downloaded: 8085 file(s) [attempted 8085/8459 = 95%, 529 KB/s], Decompressed: 8000
Downloaded: 8123 file(s) [attempted 8123/8459 = 96%, 36 KB/s], Decompressed: 8058
Downloaded: 8167 file(s) [attempted 8167/8459 = 96%, 108 KB/s], Decompressed: 8058
Downloaded: 8208 file(s) [attempted 8208/8459 = 97%, 1050 KB/s], Decompressed: 8119
Downloaded: 8249 file(s) [attempted 8249/8459 = 97%, 315 KB/s], Decompressed: 8178
Downloaded: 8290 file(s) [attempted 8290/8459 = 98%, 498 KB/s], Decompressed: 8178
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 311 KB/s], Decompressed: 8236
Downloaded: 8366 file(s) [attempted 8366/8459 = 98%, 403 KB/s], Decompressed: 8294
Downloaded: 8410 file(s) [attempted 8410/8459 = 99%, 49 KB/s], Decompressed: 8294
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 171 KB/s], Decompressed: 8355
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 171 KB/s], Decompressed: 8414

lean_checker exit 0 duration 4m 49s · created 6/11/2026, 10:31:58 PM

lake build

✔ [3401/3416] Built Iut.Stage1.IUTStage1SourceCore (43s)
✔ [3402/3416] Built Iut.Stage1.IUTStage1Remark312Absorption (3.0s)
✔ [3403/3416] Built Iut.Stage1.IUTStage1IUTIVAlgebra (10s)
✔ [3404/3416] Built Iut.Stage1.IUTStage1FiniteLabels (4.3s)
✔ [3405/3416] Built Iut.Stage1.IUTStage1StepX (4.9s)
✔ [3406/3416] Built Iut.Stage1.IUTStage1Gaussian (9.0s)
✔ [3407/3416] Built Iut.Stage1.IUTStage1HodgeSHE (5.4s)
✔ [3408/3416] Built Iut.Stage1.IUTStage1Theorem311 (4.6s)
✔ [3409/3416] Built Iut.Stage1.IUTStage1StepXI (17s)
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (128s)
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) [0x7aa1ee9c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7aa1ee9bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7aa1ee9bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7aa1ee8f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7aa1ee8f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7aa1ee9caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7aa1ee832923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7aa1ee832b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7aa1ee833827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7aa1ee8341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7aa1ee9c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7aa1ee615adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7aa1ee9c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7aa1ee9c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7aa1ee99b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7aa1ee615c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7aa1e9a22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7aa1e980cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7aa1e9369a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7aa1e9369f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7aa1e624524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7aa1e6245305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5a23780648da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (3.6s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.1s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (35s)
✔ [3414/3416] Built Iut.Basic (2.5s)
✔ [3415/3416] Built Iut (2.5s)
Build completed successfully (3416 jobs).

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

blueprint_build exit 1 duration 3s · created 6/11/2026, 10:31:58 PM

lake build :blueprint

warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: unknown package facet `blueprint`

semantic_extract exit 0 duration 26s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 32m 46s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 5m 30s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 6m 48s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 5m 53s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 6m 3s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 6m 34s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 7m 34s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 6m 44s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 18m 16s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 1h 41m · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 6m 24s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 6m 1s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 31m 19s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 5m 40s · created 6/11/2026, 10:31:58 PM

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

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

semantic_extract exit 0 duration 5m 45s · created 6/11/2026, 10:31:58 PM

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

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