Verification run

Run 351

promachina/iut-lean branch master triggered via github_backfill

succeeded commit 36e5dae3a085 toolchain lean-v4-30-0 prover lean took 56m 17s · finished 4w 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

$ git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-460-source
exit_code=Some(0) duration_ms=2390
stderr:
Cloning into '/var/lib/apodeixis/repos/job-460-source'...


$ git checkout 36e5dae3a085089f07c2c01ee15e3f650476aae1
exit_code=Some(128) duration_ms=1
stderr:
fatal: reference is not a tree: 36e5dae3a085089f07c2c01ee15e3f650476aae1


$ git fetch --depth 1 origin 36e5dae3a085089f07c2c01ee15e3f650476aae1
exit_code=Some(0) duration_ms=1028
stderr:
From https://github.com/promachina/iut-lean
 * branch            36e5dae3a085089f07c2c01ee15e3f650476aae1 -> FETCH_HEAD


$ git checkout 36e5dae3a085089f07c2c01ee15e3f650476aae1 (after fetch)
exit_code=Some(0) duration_ms=147
stderr:
Note: switching to '36e5dae3a085089f07c2c01ee15e3f650476aae1'.

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 36e5dae Derive valuation unit ball coordinate transport

Resolved source revision: 36e5dae3a085089f07c2c01ee15e3f650476aae1

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=36e5dae3a085089f07c2c01ee15e3f650476aae1 provenance={"branch":"master","checked_out_revision":"36e5dae3a085089f07c2c01ee15e3f650476aae1","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"36e5dae3a085089f07c2c01ee15e3f650476aae1","used_missing_commit_fetch":true}
Resolved toolchain: lean-v4-30-0 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
Restored Lean workspace build cache
Restored 9 Lean dependency package snapshot(s)
Prepared 9 shared Lean git mirror alias(es)
Lean semantic module cache: computed 31 module hash fact(s) from source and olean files; skipping Lean module-facts probe
Lean semantic module cache: 28/31 module hit(s), 3 miss(es)
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00000
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00001
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00002
Lean semantic module cache: extracted 3 missing module(s) in bounded batches; wrote merged semantic response

$ lake exe cache get
exit_code=Some(0) duration_ms=40434
stdout:
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)

stderr:
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: 14 file(s) [attempted 14/8459 = 0%, 5 KB/s], Decompressed: 12
Downloaded: 40 file(s) [attempted 40/8459 = 0%, 26 KB/s], Decompressed: 39
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 25 KB/s], Decompressed: 65
Downloaded: 93 file(s) [attempted 93/8459 = 1%, 549 KB/s], Decompressed: 89
Downloaded: 127 file(s) [attempted 127/8459 = 1%, 158 KB/s], Decompressed: 121
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 724 KB/s], Decompressed: 155
Downloaded: 200 file(s) [attempted 200/8459 = 2%, 372 KB/s], Decompressed: 196
Downloaded: 237 file(s) [attempted 237/8459 = 2%, 956 KB/s], Decompressed: 230
Downloaded: 270 file(s) [attempted 270/8459 = 3%, 1321 KB/s], Decompressed: 264
Downloaded: 309 file(s) [attempted 309/8459 = 3%, 80 KB/s], Decompressed: 302
Downloaded: 347 file(s) [attempted 347/8459 = 4%, 723 KB/s], Decompressed: 343
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 1062 KB/s], Decompressed: 384
Downloaded: 429 file(s) [attempted 429/8459 = 5%, 28 KB/s], Decompressed: 422
Downloaded: 463 file(s) [attempted 463/8459 = 5%, 337 KB/s], Decompressed: 456
Downloaded: 501 file(s) [attempted 501/8459 = 5%, 831 KB/s], Decompressed: 497
Downloaded: 542 file(s) [attempted 542/8459 = 6%, 299 KB/s], Decompressed: 538
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 66 KB/s], Decompressed: 583
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 42 KB/s], Decompressed: 624
Downloaded: 665 file(s) [attempted 665/8459 = 7%, 84 KB/s], Decompressed: 658
Downloaded: 700 file(s) [attempted 700/8459 = 8%, 150 KB/s], Decompressed: 693
Downloaded: 741 file(s) [attempted 741/8459 = 8%, 285 KB/s], Decompressed: 737
Downloaded: 782 file(s) [attempted 782/8459 = 9%, 118 KB/s], Decompressed: 778
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 189 KB/s], Decompressed: 812
Downloaded: 864 file(s) [attempted 864/8459 = 10%, 389 KB/s], Decompressed: 857
Downloaded: 899 file(s) [attempted 899/8459 = 10%, 29 KB/s], Decompressed: 895
Downloaded: 939 file(s) [attempted 939/8459 = 11%, 329 KB/s], Decompressed: 936
Downloaded: 977 file(s) [attempted 977/8459 = 11%, 587 KB/s], Decompressed: 973
Downloaded: 1015 file(s) [attempted 1015/8459 = 11%, 197 KB/s], Decompressed: 1011
Downloaded: 1056 file(s) [attempted 1056/8459 = 12%, 251 KB/s], Decompressed: 1052
Downloaded: 1093 file(s) [attempted 1093/8459 = 12%, 567 KB/s], Decompressed: 1090
Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 66 KB/s], Decompressed: 1127
Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 624 KB/s], Decompressed: 1169
Downloaded: 1216 file(s) [attempted 1216/8459 = 14%, 141 KB/s], Decompressed: 1213
Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 107 KB/s], Decompressed: 1251
Downloaded: 1295 file(s) [attempted 1295/8459 = 15%, 126 KB/s], Decompressed: 1292
Downloaded: 1336 file(s) [attempted 1336/8459 = 15%, 1174 KB/s], Decompressed: 1329
Downloaded: 1374 file(s) [attempted 1374/8459 = 16%, 1119 KB/s], Decompressed: 1364
Downloaded: 1415 file(s) [attempted 1415/8459 = 16%, 382 KB/s], Decompressed: 1408
Downloaded: 1456 file(s) [attempted 1456/8459 = 17%, 349 KB/s], Decompressed: 1449
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 168 KB/s], Decompressed: 1490
Downloaded: 1535 file(s) [attempted 1535/8459 = 18%, 377 KB/s], Decompressed: 1528
Downloaded: 1574 file(s) [attempted 1574/8459 = 18%, 110 KB/s], Decompressed: 1569
Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 186 KB/s], Decompressed: 1610
Downloaded: 1655 file(s) [attempted 1655/8459 = 19%, 82 KB/s], Decompressed: 1644
Downloaded: 1696 file(s) [attempted 1696/8459 = 20%, 1087 KB/s], Decompressed: 1689
Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 305 KB/s], Decompressed: 1726
Downloaded: 1774 file(s) [attempted 1774/8459 = 20%, 725 KB/s], Decompressed: 1771
Downloaded: 1813 file(s) [attempted 1813/8459 = 21%, 87 KB/s], Decompressed: 1805
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 32 KB/s], Decompressed: 1852
Downloaded: 1895 file(s) [attempted 1895/8459 = 22%, 461 KB/s], Decompressed: 1884
Downloaded: 1932 file(s) [attempted 1932/8459 = 22%, 282 KB/s], Decompressed: 1928
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 253 KB/s], Decompressed: 1966
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 260 KB/s], Decompressed: 2004
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 186 KB/s], Decompressed: 2045
Downloaded: 2086 file(s) [attempted 2086/8459 = 24%, 98 KB/s], Decompressed: 2082
Downloaded: 2127 file(s) [attempted 2127/8459 = 25%, 86 KB/s], Decompressed: 2123
Downloaded: 2168 file(s) [attempted 2168/8459 = 25%, 541 KB/s], Decompressed: 2164
Downloaded: 2207 file(s) [attempted 2207/8459 = 26%, 144 KB/s], Decompressed: 2202
Downloaded: 2240 file(s) [attempted 2240/8459 = 26%, 194 KB/s], Decompressed: 2236
Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 300 KB/s], Decompressed: 2277
Downloaded: 2318 file(s) [attempted 2318/8459 = 27%, 432 KB/s], Decompressed: 2308
Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 1770 KB/s], Decompressed: 2353
Downloaded: 2390 file(s) [attempted 2390/8459 = 28%, 89 KB/s], Decompressed: 2383
Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 565 KB/s], Decompressed: 2428
Downloaded: 2479 file(s) [attempted 2479/8459 = 29%, 357 KB/s], Decompressed: 2472
Downloaded: 2520 file(s) [attempted 2520/8459 = 29%, 222 KB/s], Decompressed: 2514
Downloaded: 2558 file(s) [attempted 2558/8459 = 30%, 423 KB/s], Decompressed: 2548
Downloaded: 2594 file(s) [attempted 2594/8459 = 30%, 155 KB/s], Decompressed: 2589
Downloaded: 2637 file(s) [attempted 2637/8459 = 31%, 295 KB/s], Decompressed: 2633
Downloaded: 2678 file(s) [attempted 2678/8459 = 31%, 797 KB/s], Decompressed: 2674
Downloaded: 2722 file(s) [attempted 2722/8459 = 32%, 307 KB/s], Decompressed: 2715
Downloaded: 2763 file(s) [attempted 2763/8459 = 32%, 56 KB/s], Decompressed: 2758
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 66 KB/s], Decompressed: 2798
Downloaded: 2842 file(s) [attempted 2842/8459 = 33%, 199 KB/s], Decompressed: 2839
Downloaded: 2881 file(s) [attempted 2881/8459 = 34%, 119 KB/s], Decompressed: 2876
Downloaded: 2924 file(s) [attempted 2924/8459 = 34%, 80 KB/s], Decompressed: 2917
Downloaded: 2960 file(s) [attempted 2960/8459 = 34%, 316 KB/s], Decompressed: 2948
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 930 KB/s], Decompressed: 2993
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 1064 KB/s], Decompressed: 3030
Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 510 KB/s], Decompressed: 3071
Downloaded: 3123 file(s) [attempted 3123/8459 = 36%, 664 KB/s], Decompressed: 3112
Downloaded: 3160 file(s) [attempted 3160/8459 = 37%, 424 KB/s], Decompressed: 3157
Downloaded: 3201 file(s) [attempted 3201/8459 = 37%, 36 KB/s], Decompressed: 3191
Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 1059 KB/s], Decompressed: 3229
Downloaded: 3275 file(s) [attempted 3275/8459 = 38%, 884 KB/s], Decompressed: 3266
Downloaded: 3318 file(s) [attempted 3318/8459 = 39%, 386 KB/s], Decompressed: 3307
Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 51 KB/s], Decompressed: 3349
Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 74 KB/s], Decompressed: 3383
Downloaded: 3433 file(s) [attempted 3433/8459 = 40%, 43 KB/s], Decompressed: 3424
Downloaded: 3468 file(s) [attempted 3468/8459 = 40%, 1034 KB/s], Decompressed: 3462
Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 24 KB/s], Decompressed: 3499
Downloaded: 3547 file(s) [attempted 3547/8459 = 41%, 23 KB/s], Decompressed: 3544
Downloaded: 3581 file(s) [attempted 3581/8459 = 42%, 119 KB/s], Decompressed: 3578
Downloaded: 3623 file(s) [attempted 3623/8459 = 42%, 932 KB/s], Decompressed: 3620
Downloaded: 3663 file(s) [attempted 3663/8459 = 43%, 329 KB/s], Decompressed: 3657
Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 39 KB/s], Decompressed: 3694
Downloaded: 3742 file(s) [attempted 3742/8459 = 44%, 74 KB/s], Decompressed: 3741
Downloaded: 3776 file(s) [attempted 3776/8459 = 44%, 291 KB/s], Decompressed: 3770
Downloaded: 3821 file(s) [attempted 3821/8459 = 45%, 57 KB/s], Decompressed: 3817
Downloaded: 3865 file(s) [attempted 3865/8459 = 45%, 355 KB/s], Decompressed: 3859
Downloaded: 3905 file(s) [attempted 3905/8459 = 46%, 53 KB/s], Decompressed: 3900
Downloaded: 3945 file(s) [attempted 3945/8459 = 46%, 218 KB/s], Decompressed: 3937
Downloaded: 3982 file(s) [attempted 3982/8459 = 47%, 119 KB/s], Decompressed: 3975
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 801 KB/s], Decompressed: 4016
Downloaded: 4063 file(s) [attempted 4063/8459 = 48%, 376 KB/s], Decompressed: 4054
Downloaded: 4102 file(s) [attempted 4102/8459 = 48%, 324 KB/s], Decompressed: 4098
Downloaded: 4145 file(s) [attempted 4145/8459 = 49%, 928 KB/s], Decompressed: 4136
Downloaded: 4178 file(s) [attempted 4178/8459 = 49%, 2269 KB/s], Decompressed: 4173
Downloaded: 4214 file(s) [attempted 4214/8459 = 49%, 399 KB/s], Decompressed: 4208
Downloaded: 4256 file(s) [attempted 4256/8459 = 50%, 46 KB/s], Decompressed: 4252
Downloaded: 4293 file(s) [attempted 4293/8459 = 50%, 95 KB/s], Decompressed: 4290
Downloaded: 4334 file(s) [attempted 4334/8459 = 51%, 301 KB/s], Decompressed: 4327
Downloaded: 4372 file(s) [attempted 4372/8459 = 51%, 261 KB/s], Decompressed: 4368
Downloaded: 4406 file(s) [attempted 4406/8459 = 52%, 85 KB/s], Decompressed: 4399
Downloaded: 4443 file(s) [attempted 4443/8459 = 52%, 193 KB/s], Decompressed: 4433
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 376 KB/s], Decompressed: 4475
Downloaded: 4516 file(s) [attempted 4516/8459 = 53%, 529 KB/s], Decompressed: 4512
Downloaded: 4550 file(s) [attempted 4550/8459 = 53%, 312 KB/s], Decompressed: 4546
Downloaded: 4580 file(s) [attempted 4580/8459 = 54%, 580 KB/s], Decompressed: 4574
Downloaded: 4615 file(s) [attempted 4615/8459 = 54%, 487 KB/s], Decompressed: 4608
Downloaded: 4646 file(s) [attempted 4646/8459 = 54%, 33 KB/s], Decompressed: 4642
Downloaded: 4680 file(s) [attempted 4680/8459 = 55%, 208 KB/s], Decompressed: 4676
Downloaded: 4714 file(s) [attempted 4714/8459 = 55%, 394 KB/s], Decompressed: 4711
Downloaded: 4748 file(s) [attempted 4748/8459 = 56%, 1264 KB/s], Decompressed: 4741
Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 482 KB/s], Decompressed: 4789
Downloaded: 4831 file(s) [attempted 4831/8459 = 57%, 117 KB/s], Decompressed: 4827
Downloaded: 4875 file(s) [attempted 4875/8459 = 57%, 1581 KB/s], Decompressed: 4872
Downloaded: 4907 file(s) [attempted 4907/8459 = 58%, 161 KB/s], Decompressed: 4902
Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 334 KB/s], Decompressed: 4943
Downloaded: 4991 file(s) [attempted 4991/8459 = 59%, 1064 KB/s], Decompressed: 4988
Downloaded: 5032 file(s) [attempted 5032/8459 = 59%, 351 KB/s], Decompressed: 5029
Downloaded: 5073 file(s) [attempted 5073/8459 = 59%, 316 KB/s], Decompressed: 5070
Downloaded: 5104 file(s) [attempted 5104/8459 = 60%, 112 KB/s], Decompressed: 5101
Downloaded: 5145 file(s) [attempted 5145/8459 = 60%, 850 KB/s], Decompressed: 5142
Downloaded: 5190 file(s) [attempted 5190/8459 = 61%, 102 KB/s], Decompressed: 5183
Downloaded: 5228 file(s) [attempted 5228/8459 = 61%, 104 KB/s], Decompressed: 5225
Downloaded: 5267 file(s) [attempted 5267/8459 = 62%, 76 KB/s], Decompressed: 5258
Downloaded: 5302 file(s) [attempted 5302/8459 = 62%, 390 KB/s], Decompressed: 5296
Downloaded: 5344 file(s) [attempted 5344/8459 = 63%, 715 KB/s], Decompressed: 5334
Downloaded: 5385 file(s) [attempted 5385/8459 = 63%, 122 KB/s], Decompressed: 5378
Downloaded: 5429 file(s) [attempted 5429/8459 = 64%, 195 KB/s], Decompressed: 5423
Downloaded: 5470 file(s) [attempted 5470/8459 = 64%, 22 KB/s], Decompressed: 5464
Downloaded: 5508 file(s) [attempted 5508/8459 = 65%, 36 KB/s], Decompressed: 5505
Downloaded: 5549 file(s) [attempted 5549/8459 = 65%, 315 KB/s], Decompressed: 5539
Downloaded: 5590 file(s) [attempted 5590/8459 = 66%, 314 KB/s], Decompressed: 5587
Downloaded: 5631 file(s) [attempted 5631/8459 = 66%, 26 KB/s], Decompressed: 5624
Downloaded: 5672 file(s) [attempted 5672/8459 = 67%, 68 KB/s], Decompressed: 5669
Downloaded: 5713 file(s) [attempted 5713/8459 = 67%, 52 KB/s], Decompressed: 5707
Downloaded: 5751 file(s) [attempted 5751/8459 = 67%, 453 KB/s], Decompressed: 5744
Downloaded: 5791 file(s) [attempted 5791/8459 = 68%, 128 KB/s], Decompressed: 5785
Downloaded: 5831 file(s) [attempted 5831/8459 = 68%, 1447 KB/s], Decompressed: 5826
Downloaded: 5868 file(s) [attempted 5868/8459 = 69%, 159 KB/s], Decompressed: 5864
Downloaded: 5904 file(s) [attempted 5904/8459 = 69%, 327 KB/s], Decompressed: 5898
Downloaded: 5943 file(s) [attempted 5943/8459 = 70%, 641 KB/s], Decompressed: 5936
Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 72 KB/s], Decompressed: 5980
Downloaded: 6028 file(s) [attempted 6028/8459 = 71%, 139 KB/s], Decompressed: 6025
Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 22 KB/s], Decompressed: 6063
Downloaded: 6104 file(s) [attempted 6104/8459 = 72%, 55 KB/s], Decompressed: 6097
Downloaded: 6145 file(s) [attempted 6145/8459 = 72%, 46 KB/s], Decompressed: 6141
Downloaded: 6186 file(s) [attempted 6186/8459 = 73%, 688 KB/s], Decompressed: 6182
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 138 KB/s], Decompressed: 6227
Downloaded: 6271 file(s) [attempted 6271/8459 = 74%, 48 KB/s], Decompressed: 6268
Downloaded: 6309 file(s) [attempted 6309/8459 = 74%, 164 KB/s], Decompressed: 6306
Downloaded: 6343 file(s) [attempted 6343/8459 = 74%, 55 KB/s], Decompressed: 6342
Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 29 KB/s], Decompressed: 6381
Downloaded: 6428 file(s) [attempted 6428/8459 = 75%, 290 KB/s], Decompressed: 6422
Downloaded: 6466 file(s) [attempted 6466/8459 = 76%, 824 KB/s], Decompressed: 6456
Downloaded: 6502 file(s) [attempted 6502/8459 = 76%, 101 KB/s], Decompressed: 6497
Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 194 KB/s], Decompressed: 6535
Downloaded: 6579 file(s) [attempted 6579/8459 = 77%, 475 KB/s], Decompressed: 6573
Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 320 KB/s], Decompressed: 6610
Downloaded: 6658 file(s) [attempted 6658/8459 = 78%, 185 KB/s], Decompressed: 6652
Downloaded: 6692 file(s) [attempted 6692/8459 = 79%, 913 KB/s], Decompressed: 6689
Downloaded: 6733 file(s) [attempted 6733/8459 = 79%, 439 KB/s], Decompressed: 6726
Downloaded: 6773 file(s) [attempted 6773/8459 = 80%, 104 KB/s], Decompressed: 6764
Downloaded: 6812 file(s) [attempted 6812/8459 = 80%, 33 KB/s], Decompressed: 6805
Downloaded: 6847 file(s) [attempted 6847/8459 = 80%, 33 KB/s], Decompressed: 6843
Downloaded: 6889 file(s) [attempted 6889/8459 = 81%, 71 KB/s], Decompressed: 6880
Downloaded: 6926 file(s) [attempted 6926/8459 = 81%, 302 KB/s], Decompressed: 6918
Downloaded: 6966 file(s) [attempted 6966/8459 = 82%, 183 KB/s], Decompressed: 6963
Downloaded: 7001 file(s) [attempted 7001/8459 = 82%, 122 KB/s], Decompressed: 6993
Downloaded: 7042 file(s) [attempted 7042/8459 = 83%, 377 KB/s], Decompressed: 7038
Downloaded: 7080 file(s) [attempted 7080/8459 = 83%, 43 KB/s], Decompressed: 7076
Downloaded: 7118 file(s) [attempted 7118/8459 = 84%, 260 KB/s], Decompressed: 7113
Downloaded: 7158 file(s) [attempted 7158/8459 = 84%, 106 KB/s], Decompressed: 7151
Downloaded: 7199 file(s) [attempted 7199/8459 = 85%, 191 KB/s], Decompressed: 7195
Downloaded: 7236 file(s) [attempted 7236/8459 = 85%, 1111 KB/s], Decompressed: 7233
Downloaded: 7274 file(s) [attempted 7274/8459 = 85%, 174 KB/s], Decompressed: 7267
Downloaded: 7308 file(s) [attempted 7308/8459 = 86%, 351 KB/s], Decompressed: 7305
Downloaded: 7349 file(s) [attempted 7349/8459 = 86%, 105 KB/s], Decompressed: 7343
Downloaded: 7394 file(s) [attempted 7394/8459 = 87%, 457 KB/s], Decompressed: 7387
Downloaded: 7432 file(s) [attempted 7432/8459 = 87%, 150 KB/s], Decompressed: 7428
Downloaded: 7469 file(s) [attempted 7469/8459 = 88%, 473 KB/s], Decompressed: 7462
Downloaded: 7507 file(s) [attempted 7507/8459 = 88%, 80 KB/s], Decompressed: 7503
Downloaded: 7551 file(s) [attempted 7551/8459 = 89%, 594 KB/s], Decompressed: 7544
Downloaded: 7591 file(s) [attempted 7591/8459 = 89%, 136 KB/s], Decompressed: 7585
Downloaded: 7630 file(s) [attempted 7630/8459 = 90%, 53 KB/s], Decompressed: 7623
Downloaded: 7659 file(s) [attempted 7659/8459 = 90%, 143 KB/s], Decompressed: 7654
Downloaded: 7702 file(s) [attempted 7702/8459 = 91%, 85 KB/s], Decompressed: 7695
Downloaded: 7746 file(s) [attempted 7746/8459 = 91%, 281 KB/s], Decompressed: 7740
Downloaded: 7787 file(s) [attempted 7787/8459 = 92%, 1028 KB/s], Decompressed: 7784
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 657 KB/s], Decompressed: 7818
Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 471 KB/s], Decompressed: 7852
Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 805 KB/s], Decompressed: 7897
Downloaded: 7943 file(s) [attempted 7943/8459 = 93%, 237 KB/s], Decompressed: 7935
Downloaded: 7977 file(s) [attempted 7977/8459 = 94%, 88 KB/s], Decompressed: 7972
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 276 KB/s], Decompressed: 8006
Downloaded: 8054 file(s) [attempted 8054/8459 = 95%, 177 KB/s], Decompressed: 8051
Downloaded: 8095 file(s) [attempted 8095/8459 = 95%, 504 KB/s], Decompressed: 8092
Downloaded: 8134 file(s) [attempted 8134/8459 = 96%, 66 KB/s], Decompressed: 8126
Downloaded: 8167 file(s) [attempted 8167/8459 = 96%, 751 KB/s], Decompressed: 8160
Downloaded: 8208 file(s) [attempted 8208/8459 = 97%, 124 KB/s], Decompressed: 8205
Downloaded: 8249 file(s) [attempted 8249/8459 = 97%, 313 KB/s], Decompressed: 8247
Downloaded: 8290 file(s) [attempted 8290/8459 = 98%, 488 KB/s], Decompressed: 8280
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 313 KB/s], Decompressed: 8321
Downloaded: 8366 file(s) [attempted 8366/8459 = 98%, 473 KB/s], Decompressed: 8362
Downloaded: 8407 file(s) [attempted 8407/8459 = 99%, 138 KB/s], Decompressed: 8403
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 173 KB/s], Decompressed: 8444
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 105 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 105 KB/s], Decompressed: 8455


$ lake build
exit_code=Some(0) duration_ms=265309
stdout:
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (184s)
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) [0x76199b3c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x76199b3bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x76199b3bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x76199b2f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x76199b2f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x76199b3caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x76199b232923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x76199b232b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x76199b233827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x76199b2341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x76199b3c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x76199b015adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x76199b3c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x76199b3c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x76199b39b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x76199b015c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x761996422638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x76199620cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x761995d69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x761995d69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x76199b85324a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x76199b853305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5bd4ddcc08da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (13s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.5s)
✔ [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).

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


$ lake build :blueprint
exit_code=Some(1) duration_ms=1821
stderr:
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`


blueprint_build failed; continuing (non-fatal phase).

$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
exit_code=Some(0) duration_ms=1996806
stdout:
apx-semantic-phase	{"duration_ms":5,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":1882,"diagnostic_count":116,"duration_ms":1573741,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":1882,"dependency_count":2616,"diagnostic_count":33240,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":392230,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1882,"dependency_count":2616,"diagnostic_count":33240,"duration_ms":1754,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":65769146,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":46,"ok":true,"payload_bytes":65769146,"phase":"lean_json_write"}

stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"core_compile","duration_ms":3546}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":210,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 0539d9fd3a0f3bf578f2f97e2c5fe79dc6261eae49f7d1e570aba201b3f702b6
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":40,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1990114,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
exit_code=Some(0) duration_ms=431317
stdout:
apx-semantic-phase	{"duration_ms":11,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":132,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":1,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":376403,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1,"dependency_count":0,"diagnostic_count":0,"duration_ms":83,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":1330,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":1330,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":18}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":156,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 1d35f17e8a5e2a4f7eb2e38812720399852ea8f1a139b919203fe67b11f92c80
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":36,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":430580,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
exit_code=Some(0) duration_ms=389132
stdout:
apx-semantic-phase	{"duration_ms":2,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":8,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":355550,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":51,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":738,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":738,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":162,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":28963,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 1efb022e29a187ab0ac03706f29926a53fd827a39730c76c52602cb79bfbc075
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":359486,"ok":true}

Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

git_clone exit 0 duration 2s · created 6/16/2026, 2:12:00 PM

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

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

git_checkout exit 128 duration 1 ms · created 6/16/2026, 2:12:00 PM

git checkout 36e5dae3a085089f07c2c01ee15e3f650476aae1

fatal: reference is not a tree: 36e5dae3a085089f07c2c01ee15e3f650476aae1

git_checkout exit 0 duration 1s · created 6/16/2026, 2:12:00 PM

git fetch --depth 1 origin 36e5dae3a085089f07c2c01ee15e3f650476aae1

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

git_checkout exit 0 duration 147 ms · created 6/16/2026, 2:12:00 PM

git checkout 36e5dae3a085089f07c2c01ee15e3f650476aae1 (after fetch)

Note: switching to '36e5dae3a085089f07c2c01ee15e3f650476aae1'.

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 36e5dae Derive valuation unit ball coordinate transport

lake_cache exit 0 duration 40s · created 6/16/2026, 2:12:00 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)

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: 14 file(s) [attempted 14/8459 = 0%, 5 KB/s], Decompressed: 12
Downloaded: 40 file(s) [attempted 40/8459 = 0%, 26 KB/s], Decompressed: 39
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 25 KB/s], Decompressed: 65
Downloaded: 93 file(s) [attempted 93/8459 = 1%, 549 KB/s], Decompressed: 89
Downloaded: 127 file(s) [attempted 127/8459 = 1%, 158 KB/s], Decompressed: 121
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 724 KB/s], Decompressed: 155
Downloaded: 200 file(s) [attempted 200/8459 = 2%, 372 KB/s], Decompressed: 196
Downloaded: 237 file(s) [attempted 237/8459 = 2%, 956 KB/s], Decompressed: 230
Downloaded: 270 file(s) [attempted 270/8459 = 3%, 1321 KB/s], Decompressed: 264
Downloaded: 309 file(s) [attempted 309/8459 = 3%, 80 KB/s], Decompressed: 302
Downloaded: 347 file(s) [attempted 347/8459 = 4%, 723 KB/s], Decompressed: 343
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 1062 KB/s], Decompressed: 384
Downloaded: 429 file(s) [attempted 429/8459 = 5%, 28 KB/s], Decompressed: 422
Downloaded: 463 file(s) [attempted 463/8459 = 5%, 337 KB/s], Decompressed: 456
Downloaded: 501 file(s) [attempted 501/8459 = 5%, 831 KB/s], Decompressed: 497
Downloaded: 542 file(s) [attempted 542/8459 = 6%, 299 KB/s], Decompressed: 538
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 66 KB/s], Decompressed: 583
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 42 KB/s], Decompressed: 624
Downloaded: 665 file(s) [attempted 665/8459 = 7%, 84 KB/s], Decompressed: 658
Downloaded: 700 file(s) [attempted 700/8459 = 8%, 150 KB/s], Decompressed: 693
Downloaded: 741 file(s) [attempted 741/8459 = 8%, 285 KB/s], Decompressed: 737
Downloaded: 782 file(s) [attempted 782/8459 = 9%, 118 KB/s], Decompressed: 778
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 189 KB/s], Decompressed: 812
Downloaded: 864 file(s) [attempted 864/8459 = 10%, 389 KB/s], Decompressed: 857
Downloaded: 899 file(s) [attempted 899/8459 = 10%, 29 KB/s], Decompressed: 895
Downloaded: 939 file(s) [attempted 939/8459 = 11%, 329 KB/s], Decompressed: 936
Downloaded: 977 file(s) [attempted 977/8459 = 11%, 587 KB/s], Decompressed: 973
Downloaded: 1015 file(s) [attempted 1015/8459 = 11%, 197 KB/s], Decompressed: 1011
Downloaded: 1056 file(s) [attempted 1056/8459 = 12%, 251 KB/s], Decompressed: 1052
Downloaded: 1093 file(s) [attempted 1093/8459 = 12%, 567 KB/s], Decompressed: 1090
Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 66 KB/s], Decompressed: 1127
Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 624 KB/s], Decompressed: 1169
Downloaded: 1216 file(s) [attempted 1216/8459 = 14%, 141 KB/s], Decompressed: 1213
Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 107 KB/s], Decompressed: 1251
Downloaded: 1295 file(s) [attempted 1295/8459 = 15%, 126 KB/s], Decompressed: 1292
Downloaded: 1336 file(s) [attempted 1336/8459 = 15%, 1174 KB/s], Decompressed: 1329
Downloaded: 1374 file(s) [attempted 1374/8459 = 16%, 1119 KB/s], Decompressed: 1364
Downloaded: 1415 file(s) [attempted 1415/8459 = 16%, 382 KB/s], Decompressed: 1408
Downloaded: 1456 file(s) [attempted 1456/8459 = 17%, 349 KB/s], Decompressed: 1449
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 168 KB/s], Decompressed: 1490
Downloaded: 1535 file(s) [attempted 1535/8459 = 18%, 377 KB/s], Decompressed: 1528
Downloaded: 1574 file(s) [attempted 1574/8459 = 18%, 110 KB/s], Decompressed: 1569
Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 186 KB/s], Decompressed: 1610
Downloaded: 1655 file(s) [attempted 1655/8459 = 19%, 82 KB/s], Decompressed: 1644
Downloaded: 1696 file(s) [attempted 1696/8459 = 20%, 1087 KB/s], Decompressed: 1689
Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 305 KB/s], Decompressed: 1726
Downloaded: 1774 file(s) [attempted 1774/8459 = 20%, 725 KB/s], Decompressed: 1771
Downloaded: 1813 file(s) [attempted 1813/8459 = 21%, 87 KB/s], Decompressed: 1805
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 32 KB/s], Decompressed: 1852
Downloaded: 1895 file(s) [attempted 1895/8459 = 22%, 461 KB/s], Decompressed: 1884
Downloaded: 1932 file(s) [attempted 1932/8459 = 22%, 282 KB/s], Decompressed: 1928
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 253 KB/s], Decompressed: 1966
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 260 KB/s], Decompressed: 2004
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 186 KB/s], Decompressed: 2045
Downloaded: 2086 file(s) [attempted 2086/8459 = 24%, 98 KB/s], Decompressed: 2082
Downloaded: 2127 file(s) [attempted 2127/8459 = 25%, 86 KB/s], Decompressed: 2123
Downloaded: 2168 file(s) [attempted 2168/8459 = 25%, 541 KB/s], Decompressed: 2164
Downloaded: 2207 file(s) [attempted 2207/8459 = 26%, 144 KB/s], Decompressed: 2202
Downloaded: 2240 file(s) [attempted 2240/8459 = 26%, 194 KB/s], Decompressed: 2236
Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 300 KB/s], Decompressed: 2277
Downloaded: 2318 file(s) [attempted 2318/8459 = 27%, 432 KB/s], Decompressed: 2308
Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 1770 KB/s], Decompressed: 2353
Downloaded: 2390 file(s) [attempted 2390/8459 = 28%, 89 KB/s], Decompressed: 2383
Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 565 KB/s], Decompressed: 2428
Downloaded: 2479 file(s) [attempted 2479/8459 = 29%, 357 KB/s], Decompressed: 2472
Downloaded: 2520 file(s) [attempted 2520/8459 = 29%, 222 KB/s], Decompressed: 2514
Downloaded: 2558 file(s) [attempted 2558/8459 = 30%, 423 KB/s], Decompressed: 2548
Downloaded: 2594 file(s) [attempted 2594/8459 = 30%, 155 KB/s], Decompressed: 2589
Downloaded: 2637 file(s) [attempted 2637/8459 = 31%, 295 KB/s], Decompressed: 2633
Downloaded: 2678 file(s) [attempted 2678/8459 = 31%, 797 KB/s], Decompressed: 2674
Downloaded: 2722 file(s) [attempted 2722/8459 = 32%, 307 KB/s], Decompressed: 2715
Downloaded: 2763 file(s) [attempted 2763/8459 = 32%, 56 KB/s], Decompressed: 2758
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 66 KB/s], Decompressed: 2798
Downloaded: 2842 file(s) [attempted 2842/8459 = 33%, 199 KB/s], Decompressed: 2839
Downloaded: 2881 file(s) [attempted 2881/8459 = 34%, 119 KB/s], Decompressed: 2876
Downloaded: 2924 file(s) [attempted 2924/8459 = 34%, 80 KB/s], Decompressed: 2917
Downloaded: 2960 file(s) [attempted 2960/8459 = 34%, 316 KB/s], Decompressed: 2948
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 930 KB/s], Decompressed: 2993
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 1064 KB/s], Decompressed: 3030
Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 510 KB/s], Decompressed: 3071
Downloaded: 3123 file(s) [attempted 3123/8459 = 36%, 664 KB/s], Decompressed: 3112
Downloaded: 3160 file(s) [attempted 3160/8459 = 37%, 424 KB/s], Decompressed: 3157
Downloaded: 3201 file(s) [attempted 3201/8459 = 37%, 36 KB/s], Decompressed: 3191
Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 1059 KB/s], Decompressed: 3229
Downloaded: 3275 file(s) [attempted 3275/8459 = 38%, 884 KB/s], Decompressed: 3266
Downloaded: 3318 file(s) [attempted 3318/8459 = 39%, 386 KB/s], Decompressed: 3307
Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 51 KB/s], Decompressed: 3349
Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 74 KB/s], Decompressed: 3383
Downloaded: 3433 file(s) [attempted 3433/8459 = 40%, 43 KB/s], Decompressed: 3424
Downloaded: 3468 file(s) [attempted 3468/8459 = 40%, 1034 KB/s], Decompressed: 3462
Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 24 KB/s], Decompressed: 3499
Downloaded: 3547 file(s) [attempted 3547/8459 = 41%, 23 KB/s], Decompressed: 3544
Downloaded: 3581 file(s) [attempted 3581/8459 = 42%, 119 KB/s], Decompressed: 3578
Downloaded: 3623 file(s) [attempted 3623/8459 = 42%, 932 KB/s], Decompressed: 3620
Downloaded: 3663 file(s) [attempted 3663/8459 = 43%, 329 KB/s], Decompressed: 3657
Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 39 KB/s], Decompressed: 3694
Downloaded: 3742 file(s) [attempted 3742/8459 = 44%, 74 KB/s], Decompressed: 3741
Downloaded: 3776 file(s) [attempted 3776/8459 = 44%, 291 KB/s], Decompressed: 3770
Downloaded: 3821 file(s) [attempted 3821/8459 = 45%, 57 KB/s], Decompressed: 3817
Downloaded: 3865 file(s) [attempted 3865/8459 = 45%, 355 KB/s], Decompressed: 3859
Downloaded: 3905 file(s) [attempted 3905/8459 = 46%, 53 KB/s], Decompressed: 3900
Downloaded: 3945 file(s) [attempted 3945/8459 = 46%, 218 KB/s], Decompressed: 3937
Downloaded: 3982 file(s) [attempted 3982/8459 = 47%, 119 KB/s], Decompressed: 3975
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 801 KB/s], Decompressed: 4016
Downloaded: 4063 file(s) [attempted 4063/8459 = 48%, 376 KB/s], Decompressed: 4054
Downloaded: 4102 file(s) [attempted 4102/8459 = 48%, 324 KB/s], Decompressed: 4098
Downloaded: 4145 file(s) [attempted 4145/8459 = 49%, 928 KB/s], Decompressed: 4136
Downloaded: 4178 file(s) [attempted 4178/8459 = 49%, 2269 KB/s], Decompressed: 4173
Downloaded: 4214 file(s) [attempted 4214/8459 = 49%, 399 KB/s], Decompressed: 4208
Downloaded: 4256 file(s) [attempted 4256/8459 = 50%, 46 KB/s], Decompressed: 4252
Downloaded: 4293 file(s) [attempted 4293/8459 = 50%, 95 KB/s], Decompressed: 4290
Downloaded: 4334 file(s) [attempted 4334/8459 = 51%, 301 KB/s], Decompressed: 4327
Downloaded: 4372 file(s) [attempted 4372/8459 = 51%, 261 KB/s], Decompressed: 4368
Downloaded: 4406 file(s) [attempted 4406/8459 = 52%, 85 KB/s], Decompressed: 4399
Downloaded: 4443 file(s) [attempted 4443/8459 = 52%, 193 KB/s], Decompressed: 4433
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 376 KB/s], Decompressed: 4475
Downloaded: 4516 file(s) [attempted 4516/8459 = 53%, 529 KB/s], Decompressed: 4512
Downloaded: 4550 file(s) [attempted 4550/8459 = 53%, 312 KB/s], Decompressed: 4546
Downloaded: 4580 file(s) [attempted 4580/8459 = 54%, 580 KB/s], Decompressed: 4574
Downloaded: 4615 file(s) [attempted 4615/8459 = 54%, 487 KB/s], Decompressed: 4608
Downloaded: 4646 file(s) [attempted 4646/8459 = 54%, 33 KB/s], Decompressed: 4642
Downloaded: 4680 file(s) [attempted 4680/8459 = 55%, 208 KB/s], Decompressed: 4676
Downloaded: 4714 file(s) [attempted 4714/8459 = 55%, 394 KB/s], Decompressed: 4711
Downloaded: 4748 file(s) [attempted 4748/8459 = 56%, 1264 KB/s], Decompressed: 4741
Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 482 KB/s], Decompressed: 4789
Downloaded: 4831 file(s) [attempted 4831/8459 = 57%, 117 KB/s], Decompressed: 4827
Downloaded: 4875 file(s) [attempted 4875/8459 = 57%, 1581 KB/s], Decompressed: 4872
Downloaded: 4907 file(s) [attempted 4907/8459 = 58%, 161 KB/s], Decompressed: 4902
Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 334 KB/s], Decompressed: 4943
Downloaded: 4991 file(s) [attempted 4991/8459 = 59%, 1064 KB/s], Decompressed: 4988
Downloaded: 5032 file(s) [attempted 5032/8459 = 59%, 351 KB/s], Decompressed: 5029
Downloaded: 5073 file(s) [attempted 5073/8459 = 59%, 316 KB/s], Decompressed: 5070
Downloaded: 5104 file(s) [attempted 5104/8459 = 60%, 112 KB/s], Decompressed: 5101
Downloaded: 5145 file(s) [attempted 5145/8459 = 60%, 850 KB/s], Decompressed: 5142
Downloaded: 5190 file(s) [attempted 5190/8459 = 61%, 102 KB/s], Decompressed: 5183
Downloaded: 5228 file(s) [attempted 5228/8459 = 61%, 104 KB/s], Decompressed: 5225
Downloaded: 5267 file(s) [attempted 5267/8459 = 62%, 76 KB/s], Decompressed: 5258
Downloaded: 5302 file(s) [attempted 5302/8459 = 62%, 390 KB/s], Decompressed: 5296
Downloaded: 5344 file(s) [attempted 5344/8459 = 63%, 715 KB/s], Decompressed: 5334
Downloaded: 5385 file(s) [attempted 5385/8459 = 63%, 122 KB/s], Decompressed: 5378
Downloaded: 5429 file(s) [attempted 5429/8459 = 64%, 195 KB/s], Decompressed: 5423
Downloaded: 5470 file(s) [attempted 5470/8459 = 64%, 22 KB/s], Decompressed: 5464
Downloaded: 5508 file(s) [attempted 5508/8459 = 65%, 36 KB/s], Decompressed: 5505
Downloaded: 5549 file(s) [attempted 5549/8459 = 65%, 315 KB/s], Decompressed: 5539
Downloaded: 5590 file(s) [attempted 5590/8459 = 66%, 314 KB/s], Decompressed: 5587
Downloaded: 5631 file(s) [attempted 5631/8459 = 66%, 26 KB/s], Decompressed: 5624
Downloaded: 5672 file(s) [attempted 5672/8459 = 67%, 68 KB/s], Decompressed: 5669
Downloaded: 5713 file(s) [attempted 5713/8459 = 67%, 52 KB/s], Decompressed: 5707
Downloaded: 5751 file(s) [attempted 5751/8459 = 67%, 453 KB/s], Decompressed: 5744
Downloaded: 5791 file(s) [attempted 5791/8459 = 68%, 128 KB/s], Decompressed: 5785
Downloaded: 5831 file(s) [attempted 5831/8459 = 68%, 1447 KB/s], Decompressed: 5826
Downloaded: 5868 file(s) [attempted 5868/8459 = 69%, 159 KB/s], Decompressed: 5864
Downloaded: 5904 file(s) [attempted 5904/8459 = 69%, 327 KB/s], Decompressed: 5898
Downloaded: 5943 file(s) [attempted 5943/8459 = 70%, 641 KB/s], Decompressed: 5936
Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 72 KB/s], Decompressed: 5980
Downloaded: 6028 file(s) [attempted 6028/8459 = 71%, 139 KB/s], Decompressed: 6025
Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 22 KB/s], Decompressed: 6063
Downloaded: 6104 file(s) [attempted 6104/8459 = 72%, 55 KB/s], Decompressed: 6097
Downloaded: 6145 file(s) [attempted 6145/8459 = 72%, 46 KB/s], Decompressed: 6141
Downloaded: 6186 file(s) [attempted 6186/8459 = 73%, 688 KB/s], Decompressed: 6182
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 138 KB/s], Decompressed: 6227
Downloaded: 6271 file(s) [attempted 6271/8459 = 74%, 48 KB/s], Decompressed: 6268
Downloaded: 6309 file(s) [attempted 6309/8459 = 74%, 164 KB/s], Decompressed: 6306
Downloaded: 6343 file(s) [attempted 6343/8459 = 74%, 55 KB/s], Decompressed: 6342
Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 29 KB/s], Decompressed: 6381
Downloaded: 6428 file(s) [attempted 6428/8459 = 75%, 290 KB/s], Decompressed: 6422
Downloaded: 6466 file(s) [attempted 6466/8459 = 76%, 824 KB/s], Decompressed: 6456
Downloaded: 6502 file(s) [attempted 6502/8459 = 76%, 101 KB/s], Decompressed: 6497
Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 194 KB/s], Decompressed: 6535
Downloaded: 6579 file(s) [attempted 6579/8459 = 77%, 475 KB/s], Decompressed: 6573
Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 320 KB/s], Decompressed: 6610
Downloaded: 6658 file(s) [attempted 6658/8459 = 78%, 185 KB/s], Decompressed: 6652
Downloaded: 6692 file(s) [attempted 6692/8459 = 79%, 913 KB/s], Decompressed: 6689
Downloaded: 6733 file(s) [attempted 6733/8459 = 79%, 439 KB/s], Decompressed: 6726
Downloaded: 6773 file(s) [attempted 6773/8459 = 80%, 104 KB/s], Decompressed: 6764
Downloaded: 6812 file(s) [attempted 6812/8459 = 80%, 33 KB/s], Decompressed: 6805
Downloaded: 6847 file(s) [attempted 6847/8459 = 80%, 33 KB/s], Decompressed: 6843
Downloaded: 6889 file(s) [attempted 6889/8459 = 81%, 71 KB/s], Decompressed: 6880
Downloaded: 6926 file(s) [attempted 6926/8459 = 81%, 302 KB/s], Decompressed: 6918
Downloaded: 6966 file(s) [attempted 6966/8459 = 82%, 183 KB/s], Decompressed: 6963
Downloaded: 7001 file(s) [attempted 7001/8459 = 82%, 122 KB/s], Decompressed: 6993
Downloaded: 7042 file(s) [attempted 7042/8459 = 83%, 377 KB/s], Decompressed: 7038
Downloaded: 7080 file(s) [attempted 7080/8459 = 83%, 43 KB/s], Decompressed: 7076
Downloaded: 7118 file(s) [attempted 7118/8459 = 84%, 260 KB/s], Decompressed: 7113
Downloaded: 7158 file(s) [attempted 7158/8459 = 84%, 106 KB/s], Decompressed: 7151
Downloaded: 7199 file(s) [attempted 7199/8459 = 85%, 191 KB/s], Decompressed: 7195
Downloaded: 7236 file(s) [attempted 7236/8459 = 85%, 1111 KB/s], Decompressed: 7233
Downloaded: 7274 file(s) [attempted 7274/8459 = 85%, 174 KB/s], Decompressed: 7267
Downloaded: 7308 file(s) [attempted 7308/8459 = 86%, 351 KB/s], Decompressed: 7305
Downloaded: 7349 file(s) [attempted 7349/8459 = 86%, 105 KB/s], Decompressed: 7343
Downloaded: 7394 file(s) [attempted 7394/8459 = 87%, 457 KB/s], Decompressed: 7387
Downloaded: 7432 file(s) [attempted 7432/8459 = 87%, 150 KB/s], Decompressed: 7428
Downloaded: 7469 file(s) [attempted 7469/8459 = 88%, 473 KB/s], Decompressed: 7462
Downloaded: 7507 file(s) [attempted 7507/8459 = 88%, 80 KB/s], Decompressed: 7503
Downloaded: 7551 file(s) [attempted 7551/8459 = 89%, 594 KB/s], Decompressed: 7544
Downloaded: 7591 file(s) [attempted 7591/8459 = 89%, 136 KB/s], Decompressed: 7585
Downloaded: 7630 file(s) [attempted 7630/8459 = 90%, 53 KB/s], Decompressed: 7623
Downloaded: 7659 file(s) [attempted 7659/8459 = 90%, 143 KB/s], Decompressed: 7654
Downloaded: 7702 file(s) [attempted 7702/8459 = 91%, 85 KB/s], Decompressed: 7695
Downloaded: 7746 file(s) [attempted 7746/8459 = 91%, 281 KB/s], Decompressed: 7740
Downloaded: 7787 file(s) [attempted 7787/8459 = 92%, 1028 KB/s], Decompressed: 7784
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 657 KB/s], Decompressed: 7818
Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 471 KB/s], Decompressed: 7852
Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 805 KB/s], Decompressed: 7897
Downloaded: 7943 file(s) [attempted 7943/8459 = 93%, 237 KB/s], Decompressed: 7935
Downloaded: 7977 file(s) [attempted 7977/8459 = 94%, 88 KB/s], Decompressed: 7972
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 276 KB/s], Decompressed: 8006
Downloaded: 8054 file(s) [attempted 8054/8459 = 95%, 177 KB/s], Decompressed: 8051
Downloaded: 8095 file(s) [attempted 8095/8459 = 95%, 504 KB/s], Decompressed: 8092
Downloaded: 8134 file(s) [attempted 8134/8459 = 96%, 66 KB/s], Decompressed: 8126
Downloaded: 8167 file(s) [attempted 8167/8459 = 96%, 751 KB/s], Decompressed: 8160
Downloaded: 8208 file(s) [attempted 8208/8459 = 97%, 124 KB/s], Decompressed: 8205
Downloaded: 8249 file(s) [attempted 8249/8459 = 97%, 313 KB/s], Decompressed: 8247
Downloaded: 8290 file(s) [attempted 8290/8459 = 98%, 488 KB/s], Decompressed: 8280
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 313 KB/s], Decompressed: 8321
Downloaded: 8366 file(s) [attempted 8366/8459 = 98%, 473 KB/s], Decompressed: 8362
Downloaded: 8407 file(s) [attempted 8407/8459 = 99%, 138 KB/s], Decompressed: 8403
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 173 KB/s], Decompressed: 8444
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 105 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 105 KB/s], Decompressed: 8455

lean_checker exit 0 duration 4m 25s · created 6/16/2026, 2:12:00 PM

lake build

ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (184s)
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) [0x76199b3c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x76199b3bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x76199b3bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x76199b2f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x76199b2f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x76199b3caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x76199b232923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x76199b232b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x76199b233827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x76199b2341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x76199b3c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x76199b015adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x76199b3c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x76199b3c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x76199b39b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x76199b015c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x761996422638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x76199620cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x761995d69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x761995d69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x76199b85324a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x76199b853305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5bd4ddcc08da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (13s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.5s)
✔ [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 2s · created 6/16/2026, 2:12:00 PM

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 17s · created 6/16/2026, 2:12:00 PM

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

apx-semantic-phase	{"duration_ms":5,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":1882,"diagnostic_count":116,"duration_ms":1573741,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":1882,"dependency_count":2616,"diagnostic_count":33240,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":392230,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1882,"dependency_count":2616,"diagnostic_count":33240,"duration_ms":1754,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":65769146,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":46,"ok":true,"payload_bytes":65769146,"phase":"lean_json_write"}

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"core_compile","duration_ms":3546}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":210,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 0539d9fd3a0f3bf578f2f97e2c5fe79dc6261eae49f7d1e570aba201b3f702b6
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":40,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1990114,"ok":true}

semantic_extract exit 0 duration 7m 11s · created 6/16/2026, 2:12:00 PM

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

apx-semantic-phase	{"duration_ms":11,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":132,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":1,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":376403,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1,"dependency_count":0,"diagnostic_count":0,"duration_ms":83,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":1330,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":1330,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":18}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":156,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 1d35f17e8a5e2a4f7eb2e38812720399852ea8f1a139b919203fe67b11f92c80
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":36,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":430580,"ok":true}

semantic_extract exit 0 duration 6m 29s · created 6/16/2026, 2:12:00 PM

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

apx-semantic-phase	{"duration_ms":2,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":8,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":355550,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":51,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":738,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":738,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":162,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":28963,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 1efb022e29a187ab0ac03706f29926a53fd827a39730c76c52602cb79bfbc075
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":359486,"ok":true}