Verification run

Run 355

promachina/iut-lean branch master triggered via github_backfill

failed commit 520d2b53b0c2 toolchain lean-v4-30-0 prover lean took 2h 11m · finished 4w ago

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000) failed with exit code none (process did not exit cleanly) (toolchain lean-v4-30-0, command: <command argv unavailable>)

Open project

Package inputs

This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.

Trust verification

Recomputes trust checks from the recorded attestations, manifest, and command history.

(verification not run)

Manifest

Loads the published files manifest and location metadata for this job.

(manifest not loaded)

Verifier log excerpt

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


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


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


$ git checkout 520d2b53b0c2bdd73d07980fce1f044e8c9a0f58 (after fetch)
exit_code=Some(0) duration_ms=139
stderr:
Note: switching to '520d2b53b0c2bdd73d07980fce1f044e8c9a0f58'.

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 520d2b5 Derive local log coordinate product images

Resolved source revision: 520d2b53b0c2bdd73d07980fce1f044e8c9a0f58

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=520d2b53b0c2bdd73d07980fce1f044e8c9a0f58 provenance={"branch":"master","checked_out_revision":"520d2b53b0c2bdd73d07980fce1f044e8c9a0f58","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"520d2b53b0c2bdd73d07980fce1f044e8c9a0f58","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: 25/31 module hit(s), 6 miss(es)
Lean semantic module cache: stable superset runner skipped for 6 weighted target module(s); target weighting would require 5 batch(es) at max target modules 32
Lean semantic module cache: capping exact extraction batch extract-batch-00000 at 3600s; total exact budget remaining is 7200s
Lean semantic module cache: extraction batch extract-batch-00000 failed for module Iut/Stage1/IUTStage1FrobenioidShift.lean; continuing with remaining modules
Lean semantic module cache: extraction batch extract-batch-00000 did not fully complete; continuing with remaining batches
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: checkpointed 1 module fragment row(s) from batch extract-batch-00003
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00004
Lean semantic module cache: extraction batch extract-batch-00005 consumed the exact extraction budget; not splitting further
Lean semantic module cache: extraction batch extract-batch-00005 did not fully complete; continuing with remaining batches
Lean semantic module cache: extracted 4 module fragment(s) before one or more module failures; leaving full semantic response unwritten

$ lake exe cache get
exit_code=Some(0) duration_ms=44186
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%, 12 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 21 KB/s], Decompressed: 12
Downloaded: 40 file(s) [attempted 40/8459 = 0%, 12 KB/s], Decompressed: 37
Downloaded: 64 file(s) [attempted 64/8459 = 0%, 57 KB/s], Decompressed: 61
Downloaded: 94 file(s) [attempted 94/8459 = 1%, 39 KB/s], Decompressed: 64
Downloaded: 120 file(s) [attempted 120/8459 = 1%, 175 KB/s], Decompressed: 64
Downloaded: 155 file(s) [attempted 155/8459 = 1%, 278 KB/s], Decompressed: 151
Downloaded: 193 file(s) [attempted 193/8459 = 2%, 160 KB/s], Decompressed: 189
Downloaded: 227 file(s) [attempted 227/8459 = 2%, 289 KB/s], Decompressed: 220
Downloaded: 267 file(s) [attempted 267/8459 = 3%, 175 KB/s], Decompressed: 258
Downloaded: 302 file(s) [attempted 302/8459 = 3%, 319 KB/s], Decompressed: 299
Downloaded: 343 file(s) [attempted 343/8459 = 4%, 95 KB/s], Decompressed: 340
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 101 KB/s], Decompressed: 384
Downloaded: 427 file(s) [attempted 427/8459 = 5%, 117 KB/s], Decompressed: 422
Downloaded: 466 file(s) [attempted 466/8459 = 5%, 500 KB/s], Decompressed: 463
Downloaded: 508 file(s) [attempted 508/8459 = 6%, 699 KB/s], Decompressed: 504
Downloaded: 549 file(s) [attempted 549/8459 = 6%, 552 KB/s], Decompressed: 542
Downloaded: 587 file(s) [attempted 587/8459 = 6%, 69 KB/s], Decompressed: 580
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 158 KB/s], Decompressed: 593
Downloaded: 665 file(s) [attempted 665/8459 = 7%, 509 KB/s], Decompressed: 593
Downloaded: 706 file(s) [attempted 706/8459 = 8%, 1162 KB/s], Decompressed: 699
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 242 KB/s], Decompressed: 744
Downloaded: 785 file(s) [attempted 785/8459 = 9%, 107 KB/s], Decompressed: 778
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 166 KB/s], Decompressed: 823
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 1787 KB/s], Decompressed: 857
Downloaded: 912 file(s) [attempted 912/8459 = 10%, 563 KB/s], Decompressed: 908
Downloaded: 953 file(s) [attempted 953/8459 = 11%, 33 KB/s], Decompressed: 946
Downloaded: 987 file(s) [attempted 987/8459 = 11%, 259 KB/s], Decompressed: 980
Downloaded: 1028 file(s) [attempted 1028/8459 = 12%, 978 KB/s], Decompressed: 1025
Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 74 KB/s], Decompressed: 1073
Downloaded: 1119 file(s) [attempted 1119/8459 = 13%, 1132 KB/s], Decompressed: 1110
Downloaded: 1165 file(s) [attempted 1165/8459 = 13%, 328 KB/s], Decompressed: 1158
Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 335 KB/s], Decompressed: 1197
Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 471 KB/s], Decompressed: 1240
Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 141 KB/s], Decompressed: 1278
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 302 KB/s], Decompressed: 1323
Downloaded: 1374 file(s) [attempted 1374/8459 = 16%, 30 KB/s], Decompressed: 1370
Downloaded: 1415 file(s) [attempted 1415/8459 = 16%, 405 KB/s], Decompressed: 1412
Downloaded: 1454 file(s) [attempted 1454/8459 = 17%, 239 KB/s], Decompressed: 1447
Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 256 KB/s], Decompressed: 1487
Downloaded: 1535 file(s) [attempted 1535/8459 = 18%, 172 KB/s], Decompressed: 1531
Downloaded: 1577 file(s) [attempted 1577/8459 = 18%, 80 KB/s], Decompressed: 1569
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 333 KB/s], Decompressed: 1576
Downloaded: 1661 file(s) [attempted 1661/8459 = 19%, 304 KB/s], Decompressed: 1576
Downloaded: 1699 file(s) [attempted 1699/8459 = 20%, 465 KB/s], Decompressed: 1692
Downloaded: 1737 file(s) [attempted 1737/8459 = 20%, 272 KB/s], Decompressed: 1733
Downloaded: 1778 file(s) [attempted 1778/8459 = 21%, 253 KB/s], Decompressed: 1774
Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 311 KB/s], Decompressed: 1815
Downloaded: 1860 file(s) [attempted 1860/8459 = 21%, 2125 KB/s], Decompressed: 1856
Downloaded: 1898 file(s) [attempted 1898/8459 = 22%, 468 KB/s], Decompressed: 1891
Downloaded: 1935 file(s) [attempted 1935/8459 = 22%, 62 KB/s], Decompressed: 1928
Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 43 KB/s], Decompressed: 1969
Downloaded: 2014 file(s) [attempted 2014/8459 = 23%, 294 KB/s], Decompressed: 2010
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 109 KB/s], Decompressed: 2055
Downloaded: 2103 file(s) [attempted 2103/8459 = 24%, 53 KB/s], Decompressed: 2096
Downloaded: 2144 file(s) [attempted 2144/8459 = 25%, 508 KB/s], Decompressed: 2137
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 196 KB/s], Decompressed: 2171
Downloaded: 2223 file(s) [attempted 2223/8459 = 26%, 41 KB/s], Decompressed: 2216
Downloaded: 2260 file(s) [attempted 2260/8459 = 26%, 281 KB/s], Decompressed: 2253
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 265 KB/s], Decompressed: 2294
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 67 KB/s], Decompressed: 2332
Downloaded: 2380 file(s) [attempted 2380/8459 = 28%, 787 KB/s], Decompressed: 2377
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 34 KB/s], Decompressed: 2411
Downloaded: 2462 file(s) [attempted 2462/8459 = 29%, 24 KB/s], Decompressed: 2455
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 150 KB/s], Decompressed: 2503
Downloaded: 2551 file(s) [attempted 2551/8459 = 30%, 233 KB/s], Decompressed: 2544
Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 142 KB/s], Decompressed: 2582
Downloaded: 2626 file(s) [attempted 2626/8459 = 31%, 152 KB/s], Decompressed: 2623
Downloaded: 2671 file(s) [attempted 2671/8459 = 31%, 181 KB/s], Decompressed: 2664
Downloaded: 2715 file(s) [attempted 2715/8459 = 32%, 174 KB/s], Decompressed: 2712
Downloaded: 2758 file(s) [attempted 2758/8459 = 32%, 667 KB/s], Decompressed: 2750
Downloaded: 2794 file(s) [attempted 2794/8459 = 33%, 1828 KB/s], Decompressed: 2756
Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 264 KB/s], Decompressed: 2756
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 552 KB/s], Decompressed: 2869
Downloaded: 2924 file(s) [attempted 2924/8459 = 34%, 618 KB/s], Decompressed: 2917
Downloaded: 2969 file(s) [attempted 2969/8459 = 35%, 1176 KB/s], Decompressed: 2952
Downloaded: 3006 file(s) [attempted 3006/8459 = 35%, 43 KB/s], Decompressed: 3003
Downloaded: 3047 file(s) [attempted 3047/8459 = 36%, 359 KB/s], Decompressed: 3044
Downloaded: 3086 file(s) [attempted 3086/8459 = 36%, 237 KB/s], Decompressed: 3082
Downloaded: 3127 file(s) [attempted 3127/8459 = 36%, 681 KB/s], Decompressed: 3119
Downloaded: 3166 file(s) [attempted 3166/8459 = 37%, 66 KB/s], Decompressed: 3160
Downloaded: 3208 file(s) [attempted 3208/8459 = 37%, 654 KB/s], Decompressed: 3205
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 1443 KB/s], Decompressed: 3242
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 189 KB/s], Decompressed: 3287
Downloaded: 3331 file(s) [attempted 3331/8459 = 39%, 804 KB/s], Decompressed: 3325
Downloaded: 3372 file(s) [attempted 3372/8459 = 39%, 295 KB/s], Decompressed: 3369
Downloaded: 3415 file(s) [attempted 3415/8459 = 40%, 159 KB/s], Decompressed: 3410
Downloaded: 3458 file(s) [attempted 3458/8459 = 40%, 377 KB/s], Decompressed: 3444
Downloaded: 3496 file(s) [attempted 3496/8459 = 41%, 113 KB/s], Decompressed: 3485
Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 151 KB/s], Decompressed: 3523
Downloaded: 3574 file(s) [attempted 3574/8459 = 42%, 206 KB/s], Decompressed: 3571
Downloaded: 3615 file(s) [attempted 3615/8459 = 42%, 790 KB/s], Decompressed: 3612
Downloaded: 3660 file(s) [attempted 3660/8459 = 43%, 61 KB/s], Decompressed: 3653
Downloaded: 3704 file(s) [attempted 3704/8459 = 43%, 86 KB/s], Decompressed: 3698
Downloaded: 3746 file(s) [attempted 3746/8459 = 44%, 277 KB/s], Decompressed: 3742
Downloaded: 3785 file(s) [attempted 3785/8459 = 44%, 54 KB/s], Decompressed: 3780
Downloaded: 3824 file(s) [attempted 3824/8459 = 45%, 303 KB/s], Decompressed: 3817
Downloaded: 3862 file(s) [attempted 3862/8459 = 45%, 800 KB/s], Decompressed: 3858
Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 54 KB/s], Decompressed: 3903
Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 411 KB/s], Decompressed: 3951
Downloaded: 3995 file(s) [attempted 3995/8459 = 47%, 133 KB/s], Decompressed: 3989
Downloaded: 4033 file(s) [attempted 4033/8459 = 47%, 281 KB/s], Decompressed: 4026
Downloaded: 4067 file(s) [attempted 4067/8459 = 48%, 252 KB/s], Decompressed: 4064
Downloaded: 4108 file(s) [attempted 4108/8459 = 48%, 169 KB/s], Decompressed: 4105
Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 266 KB/s], Decompressed: 4149
Downloaded: 4201 file(s) [attempted 4201/8459 = 49%, 207 KB/s], Decompressed: 4194
Downloaded: 4241 file(s) [attempted 4241/8459 = 50%, 184 KB/s], Decompressed: 4235
Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 525 KB/s], Decompressed: 4276
Downloaded: 4320 file(s) [attempted 4320/8459 = 51%, 535 KB/s], Decompressed: 4314
Downloaded: 4360 file(s) [attempted 4360/8459 = 51%, 109 KB/s], Decompressed: 4351
Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 495 KB/s], Decompressed: 4392
Downloaded: 4440 file(s) [attempted 4440/8459 = 52%, 793 KB/s], Decompressed: 4437
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 84 KB/s], Decompressed: 4474
Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 184 KB/s], Decompressed: 4512
Downloaded: 4560 file(s) [attempted 4560/8459 = 53%, 979 KB/s], Decompressed: 4546
Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 749 KB/s], Decompressed: 4594
Downloaded: 4642 file(s) [attempted 4642/8459 = 54%, 413 KB/s], Decompressed: 4635
Downloaded: 4683 file(s) [attempted 4683/8459 = 55%, 141 KB/s], Decompressed: 4673
Downloaded: 4718 file(s) [attempted 4718/8459 = 55%, 297 KB/s], Decompressed: 4714
Downloaded: 4759 file(s) [attempted 4759/8459 = 56%, 632 KB/s], Decompressed: 4748
Downloaded: 4806 file(s) [attempted 4806/8459 = 56%, 447 KB/s], Decompressed: 4800
Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 62 KB/s], Decompressed: 4851
Downloaded: 4902 file(s) [attempted 4902/8459 = 57%, 889 KB/s], Decompressed: 4895
Downloaded: 4947 file(s) [attempted 4947/8459 = 58%, 425 KB/s], Decompressed: 4919
Downloaded: 4984 file(s) [attempted 4984/8459 = 58%, 53 KB/s], Decompressed: 4981
Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 119 KB/s], Decompressed: 5017
Downloaded: 5063 file(s) [attempted 5063/8459 = 59%, 150 KB/s], Decompressed: 5056
Downloaded: 5105 file(s) [attempted 5105/8459 = 60%, 2092 KB/s], Decompressed: 5101
Downloaded: 5149 file(s) [attempted 5149/8459 = 60%, 140 KB/s], Decompressed: 5145
Downloaded: 5190 file(s) [attempted 5190/8459 = 61%, 93 KB/s], Decompressed: 5186
Downloaded: 5222 file(s) [attempted 5222/8459 = 61%, 51 KB/s], Decompressed: 5217
Downloaded: 5264 file(s) [attempted 5264/8459 = 62%, 390 KB/s], Decompressed: 5258
Downloaded: 5306 file(s) [attempted 5306/8459 = 62%, 28 KB/s], Decompressed: 5299
Downloaded: 5351 file(s) [attempted 5351/8459 = 63%, 901 KB/s], Decompressed: 5337
Downloaded: 5395 file(s) [attempted 5395/8459 = 63%, 195 KB/s], Decompressed: 5337
Downloaded: 5433 file(s) [attempted 5433/8459 = 64%, 1049 KB/s], Decompressed: 5340
Downloaded: 5470 file(s) [attempted 5470/8459 = 64%, 24 KB/s], Decompressed: 5467
Downloaded: 5511 file(s) [attempted 5511/8459 = 65%, 113 KB/s], Decompressed: 5508
Downloaded: 5555 file(s) [attempted 5555/8459 = 65%, 313 KB/s], Decompressed: 5549
Downloaded: 5594 file(s) [attempted 5594/8459 = 66%, 90 KB/s], Decompressed: 5590
Downloaded: 5631 file(s) [attempted 5631/8459 = 66%, 140 KB/s], Decompressed: 5628
Downloaded: 5672 file(s) [attempted 5672/8459 = 67%, 351 KB/s], Decompressed: 5669
Downloaded: 5717 file(s) [attempted 5717/8459 = 67%, 58 KB/s], Decompressed: 5713
Downloaded: 5754 file(s) [attempted 5754/8459 = 68%, 63 KB/s], Decompressed: 5751
Downloaded: 5802 file(s) [attempted 5802/8459 = 68%, 107 KB/s], Decompressed: 5799
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 279 KB/s], Decompressed: 5847
Downloaded: 5891 file(s) [attempted 5891/8459 = 69%, 456 KB/s], Decompressed: 5888
Downloaded: 5932 file(s) [attempted 5932/8459 = 70%, 1101 KB/s], Decompressed: 5926
Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 43 KB/s], Decompressed: 5963
Downloaded: 6008 file(s) [attempted 6008/8459 = 71%, 409 KB/s], Decompressed: 6004
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 338 KB/s], Decompressed: 6049
Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 40 KB/s], Decompressed: 6090
Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 224 KB/s], Decompressed: 6134
Downloaded: 6186 file(s) [attempted 6186/8459 = 73%, 693 KB/s], Decompressed: 6179
Downloaded: 6223 file(s) [attempted 6223/8459 = 73%, 57 KB/s], Decompressed: 6216
Downloaded: 6268 file(s) [attempted 6268/8459 = 74%, 91 KB/s], Decompressed: 6261
Downloaded: 6305 file(s) [attempted 6305/8459 = 74%, 555 KB/s], Decompressed: 6292
Downloaded: 6347 file(s) [attempted 6347/8459 = 75%, 825 KB/s], Decompressed: 6292
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 61 KB/s], Decompressed: 6295
Downloaded: 6426 file(s) [attempted 6426/8459 = 75%, 162 KB/s], Decompressed: 6422
Downloaded: 6470 file(s) [attempted 6470/8459 = 76%, 190 KB/s], Decompressed: 6466
Downloaded: 6507 file(s) [attempted 6507/8459 = 76%, 157 KB/s], Decompressed: 6504
Downloaded: 6552 file(s) [attempted 6552/8459 = 77%, 484 KB/s], Decompressed: 6548
Downloaded: 6593 file(s) [attempted 6593/8459 = 77%, 402 KB/s], Decompressed: 6583
Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 413 KB/s], Decompressed: 6627
Downloaded: 6672 file(s) [attempted 6672/8459 = 78%, 64 KB/s], Decompressed: 6655
Downloaded: 6713 file(s) [attempted 6713/8459 = 79%, 136 KB/s], Decompressed: 6655
Downloaded: 6750 file(s) [attempted 6750/8459 = 79%, 230 KB/s], Decompressed: 6740
Downloaded: 6791 file(s) [attempted 6791/8459 = 80%, 603 KB/s], Decompressed: 6785
Downloaded: 6833 file(s) [attempted 6833/8459 = 80%, 129 KB/s], Decompressed: 6829
Downloaded: 6873 file(s) [attempted 6873/8459 = 81%, 783 KB/s], Decompressed: 6863
Downloaded: 6911 file(s) [attempted 6911/8459 = 81%, 596 KB/s], Decompressed: 6880
Downloaded: 6949 file(s) [attempted 6949/8459 = 82%, 210 KB/s], Decompressed: 6939
Downloaded: 6993 file(s) [attempted 6993/8459 = 82%, 96 KB/s], Decompressed: 6986
Downloaded: 7034 file(s) [attempted 7034/8459 = 83%, 41 KB/s], Decompressed: 7031
Downloaded: 7079 file(s) [attempted 7079/8459 = 83%, 504 KB/s], Decompressed: 7075
Downloaded: 7122 file(s) [attempted 7122/8459 = 84%, 502 KB/s], Decompressed: 7106
Downloaded: 7160 file(s) [attempted 7160/8459 = 84%, 97 KB/s], Decompressed: 7151
Downloaded: 7195 file(s) [attempted 7195/8459 = 85%, 45 KB/s], Decompressed: 7188
Downloaded: 7236 file(s) [attempted 7236/8459 = 85%, 1237 KB/s], Decompressed: 7229
Downloaded: 7277 file(s) [attempted 7277/8459 = 86%, 225 KB/s], Decompressed: 7274
Downloaded: 7318 file(s) [attempted 7318/8459 = 86%, 715 KB/s], Decompressed: 7315
Downloaded: 7360 file(s) [attempted 7360/8459 = 87%, 265 KB/s], Decompressed: 7353
Downloaded: 7398 file(s) [attempted 7398/8459 = 87%, 989 KB/s], Decompressed: 7383
Downloaded: 7442 file(s) [attempted 7442/8459 = 87%, 131 KB/s], Decompressed: 7383
Downloaded: 7486 file(s) [attempted 7486/8459 = 88%, 302 KB/s], Decompressed: 7472
Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 590 KB/s], Decompressed: 7520
Downloaded: 7568 file(s) [attempted 7568/8459 = 89%, 129 KB/s], Decompressed: 7561
Downloaded: 7606 file(s) [attempted 7606/8459 = 89%, 286 KB/s], Decompressed: 7602
Downloaded: 7644 file(s) [attempted 7644/8459 = 90%, 212 KB/s], Decompressed: 7640
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 23 KB/s], Decompressed: 7681
Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 593 KB/s], Decompressed: 7722
Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 87 KB/s], Decompressed: 7763
Downloaded: 7804 file(s) [attempted 7804/8459 = 92%, 39 KB/s], Decompressed: 7801
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 83 KB/s], Decompressed: 7845
Downloaded: 7893 file(s) [attempted 7893/8459 = 93%, 1241 KB/s], Decompressed: 7890
Downloaded: 7938 file(s) [attempted 7938/8459 = 93%, 362 KB/s], Decompressed: 7928
Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 691 KB/s], Decompressed: 7965
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 346 KB/s], Decompressed: 8006
Downloaded: 8054 file(s) [attempted 8054/8459 = 95%, 178 KB/s], Decompressed: 8051
Downloaded: 8099 file(s) [attempted 8099/8459 = 95%, 48 KB/s], Decompressed: 8095
Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 405 KB/s], Decompressed: 8133
Downloaded: 8177 file(s) [attempted 8177/8459 = 96%, 53 KB/s], Decompressed: 8171
Downloaded: 8219 file(s) [attempted 8219/8459 = 97%, 206 KB/s], Decompressed: 8215
Downloaded: 8263 file(s) [attempted 8263/8459 = 97%, 108 KB/s], Decompressed: 8260
Downloaded: 8307 file(s) [attempted 8307/8459 = 98%, 428 KB/s], Decompressed: 8297
Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 273 KB/s], Decompressed: 8345
Downloaded: 8396 file(s) [attempted 8396/8459 = 99%, 198 KB/s], Decompressed: 8376
Downloaded: 8440 file(s) [attempted 8440/8459 = 99%, 78 KB/s], Decompressed: 8434
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 78 KB/s], Decompressed: 8455


$ lake build
exit_code=Some(0) duration_ms=386567
stdout:
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (279s)
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) [0x754ca01c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x754ca01bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x754ca01bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x754ca00f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x754ca00f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x754ca01caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x754ca0032923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x754ca0032b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x754ca0033827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x754ca00341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x754ca01c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x754c9fe15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x754ca01c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x754ca01c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x754ca019b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x754c9fe15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x754c9b222638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x754c9b00cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x754c9ab69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x754c9ab69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x754c97a4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x754c97a45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x61fe221bf8da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (36s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.2s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (36s)
✔ [3414/3416] Built Iut.Basic (2.8s)
✔ [3415/3416] Built Iut (2.4s)
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=4271
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=None duration_ms=3600010
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":4500}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":288,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"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":16321,"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 52d7faa2fd62cd8e6f3458f198c63f8514e44037c8e1a4d289d14abcb2bdbf7b
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
/usr/bin/podman timed out after 3600s
podman cleanup removed verifier container apx-verifier-job-505-runtime-semantic_extract-261493-1781753441862918444-3

$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
exit_code=Some(0) duration_ms=462864
stdout:
apx-semantic-phase	{"duration_ms":19,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":97,"diagnostic_count":15,"duration_ms":7825,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":97,"dependency_count":189,"diagnostic_count":2058,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":360858,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":97,"dependency_count":189,"diagnostic_count":2058,"duration_ms":392,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":3002937,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":7,"ok":true,"payload_bytes":3002937,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":19}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1148,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":29,"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":87099,"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 e3fa4d1fbe84e5886c94fb1b31908363fca91724499ec5146134019b77f9059b
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":373360,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
exit_code=Some(0) duration_ms=402131
stdout:
apx-semantic-phase	{"duration_ms":23,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":152,"diagnostic_count":23,"duration_ms":12273,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":152,"dependency_count":468,"diagnostic_count":1820,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":378557,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":152,"dependency_count":468,"diagnostic_count":1820,"duration_ms":810,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":2722873,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":26,"ok":true,"payload_bytes":2722873,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":15}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":108,"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":4079,"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 786986c6af0dedf3e9ec63882cc3d8b7516bc3bda1de52d7f9f42ffe8587f721
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":396838,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)
exit_code=Some(0) duration_ms=2105283
stdout:
apx-semantic-phase	{"duration_ms":18,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":1886,"diagnostic_count":116,"duration_ms":1540276,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":1886,"dependency_count":2620,"diagnostic_count":33507,"duration_ms":1,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":446729,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1886,"dependency_count":2620,"diagnostic_count":33507,"duration_ms":8606,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":66476453,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":104,"ok":true,"payload_bytes":66476453,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":984,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":13,"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":89742,"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 2c70abe394342d4f8a486999015fcbdcc87f8b7d94fb8fc3c669f13f5800cae1
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":2011276,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)
exit_code=Some(0) duration_ms=468353
stdout:
apx-semantic-phase	{"duration_ms":19,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":127,"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":382557,"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":67,"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":5,"ok":true,"payload_bytes":1330,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":27}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1022,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"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":79282,"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 36fcc643bb2eb5b2e27720e2f30fa913d31611fbdc30a90c6dab8d05e6f0f563
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":387097,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)
exit_code=None duration_ms=160005
stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":119,"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":4188,"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 7519ca41925738515ce62b3bd49a58f02a5d863e8763755ce1f1bd68c2f2fca1
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
/usr/bin/podman timed out after 160s
podman cleanup removed verifier container apx-verifier-job-505-runtime-semantic_extract-261493-1781760484662820894-8
Stored Lean workspace build cache

Command runs

git_clone exit 0 duration 2s · created 6/18/2026, 5:31:00 AM

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

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

git_checkout exit 128 duration 1 ms · created 6/18/2026, 5:31:00 AM

git checkout 520d2b53b0c2bdd73d07980fce1f044e8c9a0f58

fatal: reference is not a tree: 520d2b53b0c2bdd73d07980fce1f044e8c9a0f58

git_checkout exit 0 duration 1s · created 6/18/2026, 5:31:00 AM

git fetch --depth 1 origin 520d2b53b0c2bdd73d07980fce1f044e8c9a0f58

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

git_checkout exit 0 duration 139 ms · created 6/18/2026, 5:31:00 AM

git checkout 520d2b53b0c2bdd73d07980fce1f044e8c9a0f58 (after fetch)

Note: switching to '520d2b53b0c2bdd73d07980fce1f044e8c9a0f58'.

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 520d2b5 Derive local log coordinate product images

lake_cache exit 0 duration 44s · created 6/18/2026, 5:31:00 AM

lake exe cache get

Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)

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

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 12 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 21 KB/s], Decompressed: 12
Downloaded: 40 file(s) [attempted 40/8459 = 0%, 12 KB/s], Decompressed: 37
Downloaded: 64 file(s) [attempted 64/8459 = 0%, 57 KB/s], Decompressed: 61
Downloaded: 94 file(s) [attempted 94/8459 = 1%, 39 KB/s], Decompressed: 64
Downloaded: 120 file(s) [attempted 120/8459 = 1%, 175 KB/s], Decompressed: 64
Downloaded: 155 file(s) [attempted 155/8459 = 1%, 278 KB/s], Decompressed: 151
Downloaded: 193 file(s) [attempted 193/8459 = 2%, 160 KB/s], Decompressed: 189
Downloaded: 227 file(s) [attempted 227/8459 = 2%, 289 KB/s], Decompressed: 220
Downloaded: 267 file(s) [attempted 267/8459 = 3%, 175 KB/s], Decompressed: 258
Downloaded: 302 file(s) [attempted 302/8459 = 3%, 319 KB/s], Decompressed: 299
Downloaded: 343 file(s) [attempted 343/8459 = 4%, 95 KB/s], Decompressed: 340
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 101 KB/s], Decompressed: 384
Downloaded: 427 file(s) [attempted 427/8459 = 5%, 117 KB/s], Decompressed: 422
Downloaded: 466 file(s) [attempted 466/8459 = 5%, 500 KB/s], Decompressed: 463
Downloaded: 508 file(s) [attempted 508/8459 = 6%, 699 KB/s], Decompressed: 504
Downloaded: 549 file(s) [attempted 549/8459 = 6%, 552 KB/s], Decompressed: 542
Downloaded: 587 file(s) [attempted 587/8459 = 6%, 69 KB/s], Decompressed: 580
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 158 KB/s], Decompressed: 593
Downloaded: 665 file(s) [attempted 665/8459 = 7%, 509 KB/s], Decompressed: 593
Downloaded: 706 file(s) [attempted 706/8459 = 8%, 1162 KB/s], Decompressed: 699
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 242 KB/s], Decompressed: 744
Downloaded: 785 file(s) [attempted 785/8459 = 9%, 107 KB/s], Decompressed: 778
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 166 KB/s], Decompressed: 823
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 1787 KB/s], Decompressed: 857
Downloaded: 912 file(s) [attempted 912/8459 = 10%, 563 KB/s], Decompressed: 908
Downloaded: 953 file(s) [attempted 953/8459 = 11%, 33 KB/s], Decompressed: 946
Downloaded: 987 file(s) [attempted 987/8459 = 11%, 259 KB/s], Decompressed: 980
Downloaded: 1028 file(s) [attempted 1028/8459 = 12%, 978 KB/s], Decompressed: 1025
Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 74 KB/s], Decompressed: 1073
Downloaded: 1119 file(s) [attempted 1119/8459 = 13%, 1132 KB/s], Decompressed: 1110
Downloaded: 1165 file(s) [attempted 1165/8459 = 13%, 328 KB/s], Decompressed: 1158
Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 335 KB/s], Decompressed: 1197
Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 471 KB/s], Decompressed: 1240
Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 141 KB/s], Decompressed: 1278
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 302 KB/s], Decompressed: 1323
Downloaded: 1374 file(s) [attempted 1374/8459 = 16%, 30 KB/s], Decompressed: 1370
Downloaded: 1415 file(s) [attempted 1415/8459 = 16%, 405 KB/s], Decompressed: 1412
Downloaded: 1454 file(s) [attempted 1454/8459 = 17%, 239 KB/s], Decompressed: 1447
Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 256 KB/s], Decompressed: 1487
Downloaded: 1535 file(s) [attempted 1535/8459 = 18%, 172 KB/s], Decompressed: 1531
Downloaded: 1577 file(s) [attempted 1577/8459 = 18%, 80 KB/s], Decompressed: 1569
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 333 KB/s], Decompressed: 1576
Downloaded: 1661 file(s) [attempted 1661/8459 = 19%, 304 KB/s], Decompressed: 1576
Downloaded: 1699 file(s) [attempted 1699/8459 = 20%, 465 KB/s], Decompressed: 1692
Downloaded: 1737 file(s) [attempted 1737/8459 = 20%, 272 KB/s], Decompressed: 1733
Downloaded: 1778 file(s) [attempted 1778/8459 = 21%, 253 KB/s], Decompressed: 1774
Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 311 KB/s], Decompressed: 1815
Downloaded: 1860 file(s) [attempted 1860/8459 = 21%, 2125 KB/s], Decompressed: 1856
Downloaded: 1898 file(s) [attempted 1898/8459 = 22%, 468 KB/s], Decompressed: 1891
Downloaded: 1935 file(s) [attempted 1935/8459 = 22%, 62 KB/s], Decompressed: 1928
Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 43 KB/s], Decompressed: 1969
Downloaded: 2014 file(s) [attempted 2014/8459 = 23%, 294 KB/s], Decompressed: 2010
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 109 KB/s], Decompressed: 2055
Downloaded: 2103 file(s) [attempted 2103/8459 = 24%, 53 KB/s], Decompressed: 2096
Downloaded: 2144 file(s) [attempted 2144/8459 = 25%, 508 KB/s], Decompressed: 2137
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 196 KB/s], Decompressed: 2171
Downloaded: 2223 file(s) [attempted 2223/8459 = 26%, 41 KB/s], Decompressed: 2216
Downloaded: 2260 file(s) [attempted 2260/8459 = 26%, 281 KB/s], Decompressed: 2253
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 265 KB/s], Decompressed: 2294
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 67 KB/s], Decompressed: 2332
Downloaded: 2380 file(s) [attempted 2380/8459 = 28%, 787 KB/s], Decompressed: 2377
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 34 KB/s], Decompressed: 2411
Downloaded: 2462 file(s) [attempted 2462/8459 = 29%, 24 KB/s], Decompressed: 2455
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 150 KB/s], Decompressed: 2503
Downloaded: 2551 file(s) [attempted 2551/8459 = 30%, 233 KB/s], Decompressed: 2544
Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 142 KB/s], Decompressed: 2582
Downloaded: 2626 file(s) [attempted 2626/8459 = 31%, 152 KB/s], Decompressed: 2623
Downloaded: 2671 file(s) [attempted 2671/8459 = 31%, 181 KB/s], Decompressed: 2664
Downloaded: 2715 file(s) [attempted 2715/8459 = 32%, 174 KB/s], Decompressed: 2712
Downloaded: 2758 file(s) [attempted 2758/8459 = 32%, 667 KB/s], Decompressed: 2750
Downloaded: 2794 file(s) [attempted 2794/8459 = 33%, 1828 KB/s], Decompressed: 2756
Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 264 KB/s], Decompressed: 2756
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 552 KB/s], Decompressed: 2869
Downloaded: 2924 file(s) [attempted 2924/8459 = 34%, 618 KB/s], Decompressed: 2917
Downloaded: 2969 file(s) [attempted 2969/8459 = 35%, 1176 KB/s], Decompressed: 2952
Downloaded: 3006 file(s) [attempted 3006/8459 = 35%, 43 KB/s], Decompressed: 3003
Downloaded: 3047 file(s) [attempted 3047/8459 = 36%, 359 KB/s], Decompressed: 3044
Downloaded: 3086 file(s) [attempted 3086/8459 = 36%, 237 KB/s], Decompressed: 3082
Downloaded: 3127 file(s) [attempted 3127/8459 = 36%, 681 KB/s], Decompressed: 3119
Downloaded: 3166 file(s) [attempted 3166/8459 = 37%, 66 KB/s], Decompressed: 3160
Downloaded: 3208 file(s) [attempted 3208/8459 = 37%, 654 KB/s], Decompressed: 3205
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 1443 KB/s], Decompressed: 3242
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 189 KB/s], Decompressed: 3287
Downloaded: 3331 file(s) [attempted 3331/8459 = 39%, 804 KB/s], Decompressed: 3325
Downloaded: 3372 file(s) [attempted 3372/8459 = 39%, 295 KB/s], Decompressed: 3369
Downloaded: 3415 file(s) [attempted 3415/8459 = 40%, 159 KB/s], Decompressed: 3410
Downloaded: 3458 file(s) [attempted 3458/8459 = 40%, 377 KB/s], Decompressed: 3444
Downloaded: 3496 file(s) [attempted 3496/8459 = 41%, 113 KB/s], Decompressed: 3485
Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 151 KB/s], Decompressed: 3523
Downloaded: 3574 file(s) [attempted 3574/8459 = 42%, 206 KB/s], Decompressed: 3571
Downloaded: 3615 file(s) [attempted 3615/8459 = 42%, 790 KB/s], Decompressed: 3612
Downloaded: 3660 file(s) [attempted 3660/8459 = 43%, 61 KB/s], Decompressed: 3653
Downloaded: 3704 file(s) [attempted 3704/8459 = 43%, 86 KB/s], Decompressed: 3698
Downloaded: 3746 file(s) [attempted 3746/8459 = 44%, 277 KB/s], Decompressed: 3742
Downloaded: 3785 file(s) [attempted 3785/8459 = 44%, 54 KB/s], Decompressed: 3780
Downloaded: 3824 file(s) [attempted 3824/8459 = 45%, 303 KB/s], Decompressed: 3817
Downloaded: 3862 file(s) [attempted 3862/8459 = 45%, 800 KB/s], Decompressed: 3858
Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 54 KB/s], Decompressed: 3903
Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 411 KB/s], Decompressed: 3951
Downloaded: 3995 file(s) [attempted 3995/8459 = 47%, 133 KB/s], Decompressed: 3989
Downloaded: 4033 file(s) [attempted 4033/8459 = 47%, 281 KB/s], Decompressed: 4026
Downloaded: 4067 file(s) [attempted 4067/8459 = 48%, 252 KB/s], Decompressed: 4064
Downloaded: 4108 file(s) [attempted 4108/8459 = 48%, 169 KB/s], Decompressed: 4105
Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 266 KB/s], Decompressed: 4149
Downloaded: 4201 file(s) [attempted 4201/8459 = 49%, 207 KB/s], Decompressed: 4194
Downloaded: 4241 file(s) [attempted 4241/8459 = 50%, 184 KB/s], Decompressed: 4235
Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 525 KB/s], Decompressed: 4276
Downloaded: 4320 file(s) [attempted 4320/8459 = 51%, 535 KB/s], Decompressed: 4314
Downloaded: 4360 file(s) [attempted 4360/8459 = 51%, 109 KB/s], Decompressed: 4351
Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 495 KB/s], Decompressed: 4392
Downloaded: 4440 file(s) [attempted 4440/8459 = 52%, 793 KB/s], Decompressed: 4437
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 84 KB/s], Decompressed: 4474
Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 184 KB/s], Decompressed: 4512
Downloaded: 4560 file(s) [attempted 4560/8459 = 53%, 979 KB/s], Decompressed: 4546
Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 749 KB/s], Decompressed: 4594
Downloaded: 4642 file(s) [attempted 4642/8459 = 54%, 413 KB/s], Decompressed: 4635
Downloaded: 4683 file(s) [attempted 4683/8459 = 55%, 141 KB/s], Decompressed: 4673
Downloaded: 4718 file(s) [attempted 4718/8459 = 55%, 297 KB/s], Decompressed: 4714
Downloaded: 4759 file(s) [attempted 4759/8459 = 56%, 632 KB/s], Decompressed: 4748
Downloaded: 4806 file(s) [attempted 4806/8459 = 56%, 447 KB/s], Decompressed: 4800
Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 62 KB/s], Decompressed: 4851
Downloaded: 4902 file(s) [attempted 4902/8459 = 57%, 889 KB/s], Decompressed: 4895
Downloaded: 4947 file(s) [attempted 4947/8459 = 58%, 425 KB/s], Decompressed: 4919
Downloaded: 4984 file(s) [attempted 4984/8459 = 58%, 53 KB/s], Decompressed: 4981
Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 119 KB/s], Decompressed: 5017
Downloaded: 5063 file(s) [attempted 5063/8459 = 59%, 150 KB/s], Decompressed: 5056
Downloaded: 5105 file(s) [attempted 5105/8459 = 60%, 2092 KB/s], Decompressed: 5101
Downloaded: 5149 file(s) [attempted 5149/8459 = 60%, 140 KB/s], Decompressed: 5145
Downloaded: 5190 file(s) [attempted 5190/8459 = 61%, 93 KB/s], Decompressed: 5186
Downloaded: 5222 file(s) [attempted 5222/8459 = 61%, 51 KB/s], Decompressed: 5217
Downloaded: 5264 file(s) [attempted 5264/8459 = 62%, 390 KB/s], Decompressed: 5258
Downloaded: 5306 file(s) [attempted 5306/8459 = 62%, 28 KB/s], Decompressed: 5299
Downloaded: 5351 file(s) [attempted 5351/8459 = 63%, 901 KB/s], Decompressed: 5337
Downloaded: 5395 file(s) [attempted 5395/8459 = 63%, 195 KB/s], Decompressed: 5337
Downloaded: 5433 file(s) [attempted 5433/8459 = 64%, 1049 KB/s], Decompressed: 5340
Downloaded: 5470 file(s) [attempted 5470/8459 = 64%, 24 KB/s], Decompressed: 5467
Downloaded: 5511 file(s) [attempted 5511/8459 = 65%, 113 KB/s], Decompressed: 5508
Downloaded: 5555 file(s) [attempted 5555/8459 = 65%, 313 KB/s], Decompressed: 5549
Downloaded: 5594 file(s) [attempted 5594/8459 = 66%, 90 KB/s], Decompressed: 5590
Downloaded: 5631 file(s) [attempted 5631/8459 = 66%, 140 KB/s], Decompressed: 5628
Downloaded: 5672 file(s) [attempted 5672/8459 = 67%, 351 KB/s], Decompressed: 5669
Downloaded: 5717 file(s) [attempted 5717/8459 = 67%, 58 KB/s], Decompressed: 5713
Downloaded: 5754 file(s) [attempted 5754/8459 = 68%, 63 KB/s], Decompressed: 5751
Downloaded: 5802 file(s) [attempted 5802/8459 = 68%, 107 KB/s], Decompressed: 5799
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 279 KB/s], Decompressed: 5847
Downloaded: 5891 file(s) [attempted 5891/8459 = 69%, 456 KB/s], Decompressed: 5888
Downloaded: 5932 file(s) [attempted 5932/8459 = 70%, 1101 KB/s], Decompressed: 5926
Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 43 KB/s], Decompressed: 5963
Downloaded: 6008 file(s) [attempted 6008/8459 = 71%, 409 KB/s], Decompressed: 6004
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 338 KB/s], Decompressed: 6049
Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 40 KB/s], Decompressed: 6090
Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 224 KB/s], Decompressed: 6134
Downloaded: 6186 file(s) [attempted 6186/8459 = 73%, 693 KB/s], Decompressed: 6179
Downloaded: 6223 file(s) [attempted 6223/8459 = 73%, 57 KB/s], Decompressed: 6216
Downloaded: 6268 file(s) [attempted 6268/8459 = 74%, 91 KB/s], Decompressed: 6261
Downloaded: 6305 file(s) [attempted 6305/8459 = 74%, 555 KB/s], Decompressed: 6292
Downloaded: 6347 file(s) [attempted 6347/8459 = 75%, 825 KB/s], Decompressed: 6292
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 61 KB/s], Decompressed: 6295
Downloaded: 6426 file(s) [attempted 6426/8459 = 75%, 162 KB/s], Decompressed: 6422
Downloaded: 6470 file(s) [attempted 6470/8459 = 76%, 190 KB/s], Decompressed: 6466
Downloaded: 6507 file(s) [attempted 6507/8459 = 76%, 157 KB/s], Decompressed: 6504
Downloaded: 6552 file(s) [attempted 6552/8459 = 77%, 484 KB/s], Decompressed: 6548
Downloaded: 6593 file(s) [attempted 6593/8459 = 77%, 402 KB/s], Decompressed: 6583
Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 413 KB/s], Decompressed: 6627
Downloaded: 6672 file(s) [attempted 6672/8459 = 78%, 64 KB/s], Decompressed: 6655
Downloaded: 6713 file(s) [attempted 6713/8459 = 79%, 136 KB/s], Decompressed: 6655
Downloaded: 6750 file(s) [attempted 6750/8459 = 79%, 230 KB/s], Decompressed: 6740
Downloaded: 6791 file(s) [attempted 6791/8459 = 80%, 603 KB/s], Decompressed: 6785
Downloaded: 6833 file(s) [attempted 6833/8459 = 80%, 129 KB/s], Decompressed: 6829
Downloaded: 6873 file(s) [attempted 6873/8459 = 81%, 783 KB/s], Decompressed: 6863
Downloaded: 6911 file(s) [attempted 6911/8459 = 81%, 596 KB/s], Decompressed: 6880
Downloaded: 6949 file(s) [attempted 6949/8459 = 82%, 210 KB/s], Decompressed: 6939
Downloaded: 6993 file(s) [attempted 6993/8459 = 82%, 96 KB/s], Decompressed: 6986
Downloaded: 7034 file(s) [attempted 7034/8459 = 83%, 41 KB/s], Decompressed: 7031
Downloaded: 7079 file(s) [attempted 7079/8459 = 83%, 504 KB/s], Decompressed: 7075
Downloaded: 7122 file(s) [attempted 7122/8459 = 84%, 502 KB/s], Decompressed: 7106
Downloaded: 7160 file(s) [attempted 7160/8459 = 84%, 97 KB/s], Decompressed: 7151
Downloaded: 7195 file(s) [attempted 7195/8459 = 85%, 45 KB/s], Decompressed: 7188
Downloaded: 7236 file(s) [attempted 7236/8459 = 85%, 1237 KB/s], Decompressed: 7229
Downloaded: 7277 file(s) [attempted 7277/8459 = 86%, 225 KB/s], Decompressed: 7274
Downloaded: 7318 file(s) [attempted 7318/8459 = 86%, 715 KB/s], Decompressed: 7315
Downloaded: 7360 file(s) [attempted 7360/8459 = 87%, 265 KB/s], Decompressed: 7353
Downloaded: 7398 file(s) [attempted 7398/8459 = 87%, 989 KB/s], Decompressed: 7383
Downloaded: 7442 file(s) [attempted 7442/8459 = 87%, 131 KB/s], Decompressed: 7383
Downloaded: 7486 file(s) [attempted 7486/8459 = 88%, 302 KB/s], Decompressed: 7472
Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 590 KB/s], Decompressed: 7520
Downloaded: 7568 file(s) [attempted 7568/8459 = 89%, 129 KB/s], Decompressed: 7561
Downloaded: 7606 file(s) [attempted 7606/8459 = 89%, 286 KB/s], Decompressed: 7602
Downloaded: 7644 file(s) [attempted 7644/8459 = 90%, 212 KB/s], Decompressed: 7640
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 23 KB/s], Decompressed: 7681
Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 593 KB/s], Decompressed: 7722
Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 87 KB/s], Decompressed: 7763
Downloaded: 7804 file(s) [attempted 7804/8459 = 92%, 39 KB/s], Decompressed: 7801
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 83 KB/s], Decompressed: 7845
Downloaded: 7893 file(s) [attempted 7893/8459 = 93%, 1241 KB/s], Decompressed: 7890
Downloaded: 7938 file(s) [attempted 7938/8459 = 93%, 362 KB/s], Decompressed: 7928
Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 691 KB/s], Decompressed: 7965
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 346 KB/s], Decompressed: 8006
Downloaded: 8054 file(s) [attempted 8054/8459 = 95%, 178 KB/s], Decompressed: 8051
Downloaded: 8099 file(s) [attempted 8099/8459 = 95%, 48 KB/s], Decompressed: 8095
Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 405 KB/s], Decompressed: 8133
Downloaded: 8177 file(s) [attempted 8177/8459 = 96%, 53 KB/s], Decompressed: 8171
Downloaded: 8219 file(s) [attempted 8219/8459 = 97%, 206 KB/s], Decompressed: 8215
Downloaded: 8263 file(s) [attempted 8263/8459 = 97%, 108 KB/s], Decompressed: 8260
Downloaded: 8307 file(s) [attempted 8307/8459 = 98%, 428 KB/s], Decompressed: 8297
Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 273 KB/s], Decompressed: 8345
Downloaded: 8396 file(s) [attempted 8396/8459 = 99%, 198 KB/s], Decompressed: 8376
Downloaded: 8440 file(s) [attempted 8440/8459 = 99%, 78 KB/s], Decompressed: 8434
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 78 KB/s], Decompressed: 8455

semantic_extract exit 0 duration 35m 5s · created 6/18/2026, 5:31:00 AM

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

apx-semantic-phase	{"duration_ms":18,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":1886,"diagnostic_count":116,"duration_ms":1540276,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":1886,"dependency_count":2620,"diagnostic_count":33507,"duration_ms":1,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":446729,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1886,"dependency_count":2620,"diagnostic_count":33507,"duration_ms":8606,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":66476453,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":104,"ok":true,"payload_bytes":66476453,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":984,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":13,"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":89742,"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 2c70abe394342d4f8a486999015fcbdcc87f8b7d94fb8fc3c669f13f5800cae1
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":2011276,"ok":true}

lean_checker exit 0 duration 6m 27s · created 6/18/2026, 5:31:00 AM

lake build

ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (279s)
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) [0x754ca01c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x754ca01bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x754ca01bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x754ca00f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x754ca00f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x754ca01caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x754ca0032923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x754ca0032b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x754ca0033827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x754ca00341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x754ca01c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x754c9fe15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x754ca01c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x754ca01c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x754ca019b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x754c9fe15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x754c9b222638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x754c9b00cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x754c9ab69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x754c9ab69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x754c97a4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x754c97a45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x61fe221bf8da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (36s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.2s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (36s)
✔ [3414/3416] Built Iut.Basic (2.8s)
✔ [3415/3416] Built Iut (2.4s)
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 4s · created 6/18/2026, 5:31:00 AM

lake build :blueprint

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

semantic_extract exit - duration 1h 0m · created 6/18/2026, 5:31:00 AM

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

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"core_compile","duration_ms":4500}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":288,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"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":16321,"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 52d7faa2fd62cd8e6f3458f198c63f8514e44037c8e1a4d289d14abcb2bdbf7b
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
/usr/bin/podman timed out after 3600s
podman cleanup removed verifier container apx-verifier-job-505-runtime-semantic_extract-261493-1781753441862918444-3

semantic_extract exit 0 duration 7m 43s · created 6/18/2026, 5:31:00 AM

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

apx-semantic-phase	{"duration_ms":19,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":97,"diagnostic_count":15,"duration_ms":7825,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":97,"dependency_count":189,"diagnostic_count":2058,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":360858,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":97,"dependency_count":189,"diagnostic_count":2058,"duration_ms":392,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":3002937,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":7,"ok":true,"payload_bytes":3002937,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":19}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1148,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":29,"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":87099,"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 e3fa4d1fbe84e5886c94fb1b31908363fca91724499ec5146134019b77f9059b
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":373360,"ok":true}

semantic_extract exit 0 duration 6m 42s · created 6/18/2026, 5:31:00 AM

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

apx-semantic-phase	{"duration_ms":23,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":152,"diagnostic_count":23,"duration_ms":12273,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":152,"dependency_count":468,"diagnostic_count":1820,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":378557,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":152,"dependency_count":468,"diagnostic_count":1820,"duration_ms":810,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":2722873,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":26,"ok":true,"payload_bytes":2722873,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":15}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":108,"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":4079,"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 786986c6af0dedf3e9ec63882cc3d8b7516bc3bda1de52d7f9f42ffe8587f721
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":396838,"ok":true}

semantic_extract exit 0 duration 7m 48s · created 6/18/2026, 5:31:00 AM

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

apx-semantic-phase	{"duration_ms":19,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":127,"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":382557,"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":67,"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":5,"ok":true,"payload_bytes":1330,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":27}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1022,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"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":79282,"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 36fcc643bb2eb5b2e27720e2f30fa913d31611fbdc30a90c6dab8d05e6f0f563
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":387097,"ok":true}

semantic_extract exit - duration 2m 40s · created 6/18/2026, 5:31:00 AM

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

apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":119,"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":4188,"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 7519ca41925738515ce62b3bd49a58f02a5d863e8763755ce1f1bd68c2f2fca1
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
/usr/bin/podman timed out after 160s
podman cleanup removed verifier container apx-verifier-job-505-runtime-semantic_extract-261493-1781760484662820894-8