Verification run

Run 350

promachina/iut-lean branch master triggered via github_backfill

succeeded commit f1665fa0a3eb toolchain lean-v4-30-0 prover lean took 2h 56m · 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-458-source
exit_code=Some(0) duration_ms=2467
stderr:
Cloning into '/var/lib/apodeixis/repos/job-458-source'...


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


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


$ git checkout f1665fa0a3eb746dc9b4f7eed1d0e24383c1de4b (after fetch)
exit_code=Some(0) duration_ms=155
stderr:
Note: switching to 'f1665fa0a3eb746dc9b4f7eed1d0e24383c1de4b'.

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 f1665fa Add forward valuation unit ball transport

Resolved source revision: f1665fa0a3eb746dc9b4f7eed1d0e24383c1de4b

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=f1665fa0a3eb746dc9b4f7eed1d0e24383c1de4b provenance={"branch":"master","checked_out_revision":"f1665fa0a3eb746dc9b4f7eed1d0e24383c1de4b","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"f1665fa0a3eb746dc9b4f7eed1d0e24383c1de4b","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: 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: 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: checkpointed 1 module fragment row(s) from batch extract-batch-00005
Lean semantic module cache: extracted 6 missing module(s) in bounded batches; wrote merged semantic response

$ lake exe cache get
exit_code=Some(0) duration_ms=46817
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%, 10 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 11 KB/s], Decompressed: 12
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 21 KB/s], Decompressed: 38
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 319 KB/s], Decompressed: 62
Downloaded: 98 file(s) [attempted 98/8459 = 1%, 59 KB/s], Decompressed: 96
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 244 KB/s], Decompressed: 131
Downloaded: 165 file(s) [attempted 165/8459 = 1%, 79 KB/s], Decompressed: 158
Downloaded: 203 file(s) [attempted 203/8459 = 2%, 318 KB/s], Decompressed: 199
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 219 KB/s], Decompressed: 230
Downloaded: 278 file(s) [attempted 278/8459 = 3%, 180 KB/s], Decompressed: 275
Downloaded: 329 file(s) [attempted 329/8459 = 3%, 159 KB/s], Decompressed: 326
Downloaded: 374 file(s) [attempted 374/8459 = 4%, 145 KB/s], Decompressed: 367
Downloaded: 417 file(s) [attempted 417/8459 = 4%, 26 KB/s], Decompressed: 412
Downloaded: 453 file(s) [attempted 453/8459 = 5%, 57 KB/s], Decompressed: 439
Downloaded: 490 file(s) [attempted 490/8459 = 5%, 552 KB/s], Decompressed: 487
Downloaded: 532 file(s) [attempted 532/8459 = 6%, 181 KB/s], Decompressed: 525
Downloaded: 574 file(s) [attempted 574/8459 = 6%, 557 KB/s], Decompressed: 569
Downloaded: 617 file(s) [attempted 617/8459 = 7%, 791 KB/s], Decompressed: 609
Downloaded: 652 file(s) [attempted 652/8459 = 7%, 349 KB/s], Decompressed: 648
Downloaded: 696 file(s) [attempted 696/8459 = 8%, 77 KB/s], Decompressed: 693
Downloaded: 737 file(s) [attempted 737/8459 = 8%, 84 KB/s], Decompressed: 730
Downloaded: 780 file(s) [attempted 780/8459 = 9%, 71 KB/s], Decompressed: 775
Downloaded: 816 file(s) [attempted 816/8459 = 9%, 181 KB/s], Decompressed: 809
Downloaded: 855 file(s) [attempted 855/8459 = 10%, 562 KB/s], Decompressed: 850
Downloaded: 898 file(s) [attempted 898/8459 = 10%, 158 KB/s], Decompressed: 891
Downloaded: 942 file(s) [attempted 942/8459 = 11%, 164 KB/s], Decompressed: 932
Downloaded: 980 file(s) [attempted 980/8459 = 11%, 528 KB/s], Decompressed: 970
Downloaded: 1018 file(s) [attempted 1018/8459 = 12%, 450 KB/s], Decompressed: 1004
Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 343 KB/s], Decompressed: 1059
Downloaded: 1107 file(s) [attempted 1107/8459 = 13%, 1924 KB/s], Decompressed: 1059
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 332 KB/s], Decompressed: 1059
Downloaded: 1192 file(s) [attempted 1192/8459 = 14%, 30 KB/s], Decompressed: 1186
Downloaded: 1232 file(s) [attempted 1232/8459 = 14%, 87 KB/s], Decompressed: 1227
Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 100 KB/s], Decompressed: 1257
Downloaded: 1312 file(s) [attempted 1312/8459 = 15%, 838 KB/s], Decompressed: 1305
Downloaded: 1353 file(s) [attempted 1353/8459 = 15%, 217 KB/s], Decompressed: 1350
Downloaded: 1395 file(s) [attempted 1395/8459 = 16%, 217 KB/s], Decompressed: 1391
Downloaded: 1435 file(s) [attempted 1435/8459 = 16%, 23 KB/s], Decompressed: 1432
Downloaded: 1477 file(s) [attempted 1477/8459 = 17%, 1646 KB/s], Decompressed: 1466
Downloaded: 1518 file(s) [attempted 1518/8459 = 17%, 987 KB/s], Decompressed: 1513
Downloaded: 1555 file(s) [attempted 1555/8459 = 18%, 259 KB/s], Decompressed: 1546
Downloaded: 1593 file(s) [attempted 1593/8459 = 18%, 135 KB/s], Decompressed: 1589
Downloaded: 1637 file(s) [attempted 1637/8459 = 19%, 45 KB/s], Decompressed: 1631
Downloaded: 1682 file(s) [attempted 1682/8459 = 19%, 44 KB/s], Decompressed: 1668
Downloaded: 1723 file(s) [attempted 1723/8459 = 20%, 166 KB/s], Decompressed: 1713
Downloaded: 1761 file(s) [attempted 1761/8459 = 20%, 352 KB/s], Decompressed: 1750
Downloaded: 1798 file(s) [attempted 1798/8459 = 21%, 956 KB/s], Decompressed: 1795
Downloaded: 1839 file(s) [attempted 1839/8459 = 21%, 465 KB/s], Decompressed: 1836
Downloaded: 1885 file(s) [attempted 1885/8459 = 22%, 22 KB/s], Decompressed: 1880
Downloaded: 1928 file(s) [attempted 1928/8459 = 22%, 76 KB/s], Decompressed: 1925
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 453 KB/s], Decompressed: 1962
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 56 KB/s], Decompressed: 1997
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 202 KB/s], Decompressed: 2045
Downloaded: 2093 file(s) [attempted 2093/8459 = 24%, 41 KB/s], Decompressed: 2089
Downloaded: 2132 file(s) [attempted 2132/8459 = 25%, 45 KB/s], Decompressed: 2123
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 942 KB/s], Decompressed: 2173
Downloaded: 2223 file(s) [attempted 2223/8459 = 26%, 126 KB/s], Decompressed: 2212
Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 358 KB/s], Decompressed: 2257
Downloaded: 2305 file(s) [attempted 2305/8459 = 27%, 1463 KB/s], Decompressed: 2298
Downloaded: 2349 file(s) [attempted 2349/8459 = 27%, 396 KB/s], Decompressed: 2339
Downloaded: 2394 file(s) [attempted 2394/8459 = 28%, 43 KB/s], Decompressed: 2383
Downloaded: 2433 file(s) [attempted 2433/8459 = 28%, 192 KB/s], Decompressed: 2424
Downloaded: 2469 file(s) [attempted 2469/8459 = 29%, 483 KB/s], Decompressed: 2432
Downloaded: 2513 file(s) [attempted 2513/8459 = 29%, 658 KB/s], Decompressed: 2432
Downloaded: 2555 file(s) [attempted 2555/8459 = 30%, 1488 KB/s], Decompressed: 2551
Downloaded: 2602 file(s) [attempted 2602/8459 = 30%, 289 KB/s], Decompressed: 2596
Downloaded: 2650 file(s) [attempted 2650/8459 = 31%, 358 KB/s], Decompressed: 2644
Downloaded: 2698 file(s) [attempted 2698/8459 = 31%, 36 KB/s], Decompressed: 2695
Downloaded: 2743 file(s) [attempted 2743/8459 = 32%, 58 KB/s], Decompressed: 2736
Downloaded: 2780 file(s) [attempted 2780/8459 = 32%, 56 KB/s], Decompressed: 2774
Downloaded: 2821 file(s) [attempted 2821/8459 = 33%, 729 KB/s], Decompressed: 2815
Downloaded: 2863 file(s) [attempted 2863/8459 = 33%, 500 KB/s], Decompressed: 2856
Downloaded: 2904 file(s) [attempted 2904/8459 = 34%, 993 KB/s], Decompressed: 2876
Downloaded: 2945 file(s) [attempted 2945/8459 = 34%, 134 KB/s], Decompressed: 2934
Downloaded: 2989 file(s) [attempted 2989/8459 = 35%, 685 KB/s], Decompressed: 2986
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 164 KB/s], Decompressed: 3030
Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 362 KB/s], Decompressed: 3068
Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 664 KB/s], Decompressed: 3112
Downloaded: 3157 file(s) [attempted 3157/8459 = 37%, 82 KB/s], Decompressed: 3155
Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 94 KB/s], Decompressed: 3191
Downloaded: 3236 file(s) [attempted 3236/8459 = 38%, 239 KB/s], Decompressed: 3232
Downloaded: 3280 file(s) [attempted 3280/8459 = 38%, 246 KB/s], Decompressed: 3263
Downloaded: 3322 file(s) [attempted 3322/8459 = 39%, 865 KB/s], Decompressed: 3318
Downloaded: 3366 file(s) [attempted 3366/8459 = 39%, 949 KB/s], Decompressed: 3362
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 660 KB/s], Decompressed: 3403
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 65 KB/s], Decompressed: 3437
Downloaded: 3489 file(s) [attempted 3489/8459 = 41%, 191 KB/s], Decompressed: 3482
Downloaded: 3526 file(s) [attempted 3526/8459 = 41%, 137 KB/s], Decompressed: 3525
Downloaded: 3571 file(s) [attempted 3571/8459 = 42%, 359 KB/s], Decompressed: 3564
Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 39 KB/s], Decompressed: 3605
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 206 KB/s], Decompressed: 3646
Downloaded: 3694 file(s) [attempted 3694/8459 = 43%, 189 KB/s], Decompressed: 3680
Downloaded: 3739 file(s) [attempted 3739/8459 = 44%, 282 KB/s], Decompressed: 3735
Downloaded: 3787 file(s) [attempted 3787/8459 = 44%, 93 KB/s], Decompressed: 3780
Downloaded: 3828 file(s) [attempted 3828/8459 = 45%, 125 KB/s], Decompressed: 3817
Downloaded: 3865 file(s) [attempted 3865/8459 = 45%, 54 KB/s], Decompressed: 3862
Downloaded: 3910 file(s) [attempted 3910/8459 = 46%, 155 KB/s], Decompressed: 3906
Downloaded: 3949 file(s) [attempted 3949/8459 = 46%, 341 KB/s], Decompressed: 3944
Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 205 KB/s], Decompressed: 3989
Downloaded: 4036 file(s) [attempted 4036/8459 = 47%, 942 KB/s], Decompressed: 4019
Downloaded: 4077 file(s) [attempted 4077/8459 = 48%, 865 KB/s], Decompressed: 4074
Downloaded: 4122 file(s) [attempted 4122/8459 = 48%, 136 KB/s], Decompressed: 4119
Downloaded: 4160 file(s) [attempted 4160/8459 = 49%, 114 KB/s], Decompressed: 4156
Downloaded: 4201 file(s) [attempted 4201/8459 = 49%, 429 KB/s], Decompressed: 4194
Downloaded: 4245 file(s) [attempted 4245/8459 = 50%, 522 KB/s], Decompressed: 4238
Downloaded: 4286 file(s) [attempted 4286/8459 = 50%, 59 KB/s], Decompressed: 4279
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 2030 KB/s], Decompressed: 4320
Downloaded: 4372 file(s) [attempted 4372/8459 = 51%, 291 KB/s], Decompressed: 4371
Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 75 KB/s], Decompressed: 4409
Downloaded: 4457 file(s) [attempted 4457/8459 = 52%, 227 KB/s], Decompressed: 4447
Downloaded: 4497 file(s) [attempted 4497/8459 = 53%, 237 KB/s], Decompressed: 4492
Downloaded: 4539 file(s) [attempted 4539/8459 = 53%, 23 KB/s], Decompressed: 4536
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 646 KB/s], Decompressed: 4581
Downloaded: 4625 file(s) [attempted 4625/8459 = 54%, 274 KB/s], Decompressed: 4622
Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 73 KB/s], Decompressed: 4659
Downloaded: 4707 file(s) [attempted 4707/8459 = 55%, 179 KB/s], Decompressed: 4700
Downloaded: 4748 file(s) [attempted 4748/8459 = 56%, 659 KB/s], Decompressed: 4738
Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 110 KB/s], Decompressed: 4782
Downloaded: 4831 file(s) [attempted 4831/8459 = 57%, 54 KB/s], Decompressed: 4824
Downloaded: 4871 file(s) [attempted 4871/8459 = 57%, 617 KB/s], Decompressed: 4868
Downloaded: 4913 file(s) [attempted 4913/8459 = 58%, 230 KB/s], Decompressed: 4899
Downloaded: 4955 file(s) [attempted 4955/8459 = 58%, 1409 KB/s], Decompressed: 4950
Downloaded: 4996 file(s) [attempted 4996/8459 = 59%, 474 KB/s], Decompressed: 4988
Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 247 KB/s], Decompressed: 5038
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 144 KB/s], Decompressed: 5073
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 524 KB/s], Decompressed: 5118
Downloaded: 5169 file(s) [attempted 5169/8459 = 61%, 77 KB/s], Decompressed: 5162
Downloaded: 5216 file(s) [attempted 5216/8459 = 61%, 67 KB/s], Decompressed: 5210
Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 40 KB/s], Decompressed: 5251
Downloaded: 5300 file(s) [attempted 5300/8459 = 62%, 33 KB/s], Decompressed: 5296
Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 418 KB/s], Decompressed: 5327
Downloaded: 5376 file(s) [attempted 5376/8459 = 63%, 55 KB/s], Decompressed: 5371
Downloaded: 5419 file(s) [attempted 5419/8459 = 64%, 242 KB/s], Decompressed: 5416
Downloaded: 5460 file(s) [attempted 5460/8459 = 64%, 167 KB/s], Decompressed: 5457
Downloaded: 5505 file(s) [attempted 5505/8459 = 65%, 156 KB/s], Decompressed: 5501
Downloaded: 5546 file(s) [attempted 5546/8459 = 65%, 1631 KB/s], Decompressed: 5535
Downloaded: 5583 file(s) [attempted 5583/8459 = 66%, 1152 KB/s], Decompressed: 5580
Downloaded: 5628 file(s) [attempted 5628/8459 = 66%, 1474 KB/s], Decompressed: 5621
Downloaded: 5669 file(s) [attempted 5669/8459 = 67%, 1819 KB/s], Decompressed: 5665
Downloaded: 5713 file(s) [attempted 5713/8459 = 67%, 200 KB/s], Decompressed: 5703
Downloaded: 5751 file(s) [attempted 5751/8459 = 67%, 854 KB/s], Decompressed: 5744
Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 138 KB/s], Decompressed: 5789
Downloaded: 5834 file(s) [attempted 5834/8459 = 68%, 112 KB/s], Decompressed: 5826
Downloaded: 5874 file(s) [attempted 5874/8459 = 69%, 160 KB/s], Decompressed: 5871
Downloaded: 5917 file(s) [attempted 5917/8459 = 69%, 266 KB/s], Decompressed: 5912
Downloaded: 5956 file(s) [attempted 5956/8459 = 70%, 150 KB/s], Decompressed: 5949
Downloaded: 5997 file(s) [attempted 5997/8459 = 70%, 242 KB/s], Decompressed: 5994
Downloaded: 6040 file(s) [attempted 6040/8459 = 71%, 669 KB/s], Decompressed: 6032
Downloaded: 6080 file(s) [attempted 6080/8459 = 71%, 357 KB/s], Decompressed: 6076
Downloaded: 6124 file(s) [attempted 6124/8459 = 72%, 421 KB/s], Decompressed: 6103
Downloaded: 6162 file(s) [attempted 6162/8459 = 72%, 78 KB/s], Decompressed: 6151
Downloaded: 6203 file(s) [attempted 6203/8459 = 73%, 108 KB/s], Decompressed: 6199
Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 107 KB/s], Decompressed: 6237
Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 51 KB/s], Decompressed: 6281
Downloaded: 6329 file(s) [attempted 6329/8459 = 74%, 376 KB/s], Decompressed: 6323
Downloaded: 6370 file(s) [attempted 6370/8459 = 75%, 377 KB/s], Decompressed: 6364
Downloaded: 6412 file(s) [attempted 6412/8459 = 75%, 308 KB/s], Decompressed: 6408
Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 765 KB/s], Decompressed: 6446
Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 446 KB/s], Decompressed: 6487
Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 404 KB/s], Decompressed: 6535
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 360 KB/s], Decompressed: 6579
Downloaded: 6624 file(s) [attempted 6624/8459 = 78%, 328 KB/s], Decompressed: 6617
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 203 KB/s], Decompressed: 6661
Downloaded: 6709 file(s) [attempted 6709/8459 = 79%, 460 KB/s], Decompressed: 6703
Downloaded: 6750 file(s) [attempted 6750/8459 = 79%, 53 KB/s], Decompressed: 6749
Downloaded: 6791 file(s) [attempted 6791/8459 = 80%, 76 KB/s], Decompressed: 6788
Downloaded: 6832 file(s) [attempted 6832/8459 = 80%, 40 KB/s], Decompressed: 6829
Downloaded: 6870 file(s) [attempted 6870/8459 = 81%, 1014 KB/s], Decompressed: 6863
Downloaded: 6915 file(s) [attempted 6915/8459 = 81%, 427 KB/s], Decompressed: 6911
Downloaded: 6962 file(s) [attempted 6962/8459 = 82%, 657 KB/s], Decompressed: 6959
Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 1850 KB/s], Decompressed: 7000
Downloaded: 7045 file(s) [attempted 7045/8459 = 83%, 638 KB/s], Decompressed: 7041
Downloaded: 7086 file(s) [attempted 7086/8459 = 83%, 49 KB/s], Decompressed: 7081
Downloaded: 7127 file(s) [attempted 7127/8459 = 84%, 32 KB/s], Decompressed: 7123
Downloaded: 7175 file(s) [attempted 7175/8459 = 84%, 319 KB/s], Decompressed: 7171
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 352 KB/s], Decompressed: 7216
Downloaded: 7263 file(s) [attempted 7263/8459 = 85%, 187 KB/s], Decompressed: 7253
Downloaded: 7301 file(s) [attempted 7301/8459 = 86%, 2077 KB/s], Decompressed: 7294
Downloaded: 7342 file(s) [attempted 7342/8459 = 86%, 579 KB/s], Decompressed: 7339
Downloaded: 7387 file(s) [attempted 7387/8459 = 87%, 300 KB/s], Decompressed: 7383
Downloaded: 7430 file(s) [attempted 7430/8459 = 87%, 641 KB/s], Decompressed: 7421
Downloaded: 7468 file(s) [attempted 7468/8459 = 88%, 381 KB/s], Decompressed: 7455
Downloaded: 7510 file(s) [attempted 7510/8459 = 88%, 224 KB/s], Decompressed: 7504
Downloaded: 7551 file(s) [attempted 7551/8459 = 89%, 97 KB/s], Decompressed: 7544
Downloaded: 7592 file(s) [attempted 7592/8459 = 89%, 922 KB/s], Decompressed: 7589
Downloaded: 7637 file(s) [attempted 7637/8459 = 90%, 147 KB/s], Decompressed: 7602
Downloaded: 7681 file(s) [attempted 7681/8459 = 90%, 152 KB/s], Decompressed: 7602
Downloaded: 7722 file(s) [attempted 7722/8459 = 91%, 205 KB/s], Decompressed: 7715
Downloaded: 7763 file(s) [attempted 7763/8459 = 91%, 302 KB/s], Decompressed: 7756
Downloaded: 7804 file(s) [attempted 7804/8459 = 92%, 39 KB/s], Decompressed: 7798
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 46 KB/s], Decompressed: 7845
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 1129 KB/s], Decompressed: 7883
Downloaded: 7930 file(s) [attempted 7930/8459 = 93%, 353 KB/s], Decompressed: 7924
Downloaded: 7972 file(s) [attempted 7972/8459 = 94%, 1967 KB/s], Decompressed: 7962
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 60 KB/s], Decompressed: 8006
Downloaded: 8054 file(s) [attempted 8054/8459 = 95%, 79 KB/s], Decompressed: 8051
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 726 KB/s], Decompressed: 8095
Downloaded: 8143 file(s) [attempted 8143/8459 = 96%, 498 KB/s], Decompressed: 8126
Downloaded: 8177 file(s) [attempted 8177/8459 = 96%, 413 KB/s], Decompressed: 8126
Downloaded: 8218 file(s) [attempted 8218/8459 = 97%, 781 KB/s], Decompressed: 8133
Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 118 KB/s], Decompressed: 8256
Downloaded: 8304 file(s) [attempted 8304/8459 = 98%, 1166 KB/s], Decompressed: 8301
Downloaded: 8342 file(s) [attempted 8342/8459 = 98%, 168 KB/s], Decompressed: 8338
Downloaded: 8390 file(s) [attempted 8390/8459 = 99%, 96 KB/s], Decompressed: 8386
Downloaded: 8435 file(s) [attempted 8435/8459 = 99%, 1221 KB/s], Decompressed: 8427
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 706 KB/s], Decompressed: 8448
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 706 KB/s], Decompressed: 8448


$ lake build
exit_code=Some(0) duration_ms=283311
stdout:
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (199s)
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) [0x777c88bc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x777c88bbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x777c88bbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x777c88af3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x777c88af4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x777c88bcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x777c88a32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x777c88a32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x777c88a33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x777c88a341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x777c88bc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x777c88815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x777c88bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x777c88bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x777c88b9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x777c88815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x777c83c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x777c83a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x777c83569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x777c83569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x777c8044524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x777c80445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x565e86fed8da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (8.6s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.2s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (36s)
✔ [3414/3416] Built Iut.Basic (2.4s)
✔ [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=1873
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=6309971
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 9f37206e2636b9fcba731da964cb85888b9c4622589473ea56617d8434018523
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
exit_code=Some(0) duration_ms=475324
stderr:
lean semantic helper: restored compiled static runner cache 8ce5ff6c967baef3842b8fb460ab7dc29b28a04bbb424be955c4371e23608184
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
exit_code=Some(0) duration_ms=385208
stderr:
lean semantic helper: restored compiled static runner cache 6247def1945279a6946b34517b575ac426a9bd22cc4c3ceb7a79dc06ef4083db
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)
exit_code=Some(0) duration_ms=1919466
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 0a56713efc3fb36836e26e948f524d8b4ee40be0b10b64f7fe543aa113f4b38d
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)
exit_code=Some(0) duration_ms=348480
stderr:
lean semantic helper: restored compiled static runner cache 60b5e07f9f538c271c74b7f6a814efcb4304463fa74b69c58466604298c0acfe
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)
exit_code=Some(0) duration_ms=343983
stderr:
lean semantic helper: restored compiled static runner cache e103fd3939aed645f6a64b867308ee472e79eb2af9586b744c189d70ac5f91ea
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

git_clone exit 0 duration 2s · created 6/16/2026, 8:59:58 AM

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

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

git_checkout exit 128 duration 1 ms · created 6/16/2026, 8:59:58 AM

git checkout f1665fa0a3eb746dc9b4f7eed1d0e24383c1de4b

fatal: reference is not a tree: f1665fa0a3eb746dc9b4f7eed1d0e24383c1de4b

git_checkout exit 0 duration 1s · created 6/16/2026, 8:59:58 AM

git fetch --depth 1 origin f1665fa0a3eb746dc9b4f7eed1d0e24383c1de4b

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

git_checkout exit 0 duration 155 ms · created 6/16/2026, 8:59:58 AM

git checkout f1665fa0a3eb746dc9b4f7eed1d0e24383c1de4b (after fetch)

Note: switching to 'f1665fa0a3eb746dc9b4f7eed1d0e24383c1de4b'.

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 f1665fa Add forward valuation unit ball transport

lake_cache exit 0 duration 47s · created 6/16/2026, 8:59:58 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%, 10 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 11 KB/s], Decompressed: 12
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 21 KB/s], Decompressed: 38
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 319 KB/s], Decompressed: 62
Downloaded: 98 file(s) [attempted 98/8459 = 1%, 59 KB/s], Decompressed: 96
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 244 KB/s], Decompressed: 131
Downloaded: 165 file(s) [attempted 165/8459 = 1%, 79 KB/s], Decompressed: 158
Downloaded: 203 file(s) [attempted 203/8459 = 2%, 318 KB/s], Decompressed: 199
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 219 KB/s], Decompressed: 230
Downloaded: 278 file(s) [attempted 278/8459 = 3%, 180 KB/s], Decompressed: 275
Downloaded: 329 file(s) [attempted 329/8459 = 3%, 159 KB/s], Decompressed: 326
Downloaded: 374 file(s) [attempted 374/8459 = 4%, 145 KB/s], Decompressed: 367
Downloaded: 417 file(s) [attempted 417/8459 = 4%, 26 KB/s], Decompressed: 412
Downloaded: 453 file(s) [attempted 453/8459 = 5%, 57 KB/s], Decompressed: 439
Downloaded: 490 file(s) [attempted 490/8459 = 5%, 552 KB/s], Decompressed: 487
Downloaded: 532 file(s) [attempted 532/8459 = 6%, 181 KB/s], Decompressed: 525
Downloaded: 574 file(s) [attempted 574/8459 = 6%, 557 KB/s], Decompressed: 569
Downloaded: 617 file(s) [attempted 617/8459 = 7%, 791 KB/s], Decompressed: 609
Downloaded: 652 file(s) [attempted 652/8459 = 7%, 349 KB/s], Decompressed: 648
Downloaded: 696 file(s) [attempted 696/8459 = 8%, 77 KB/s], Decompressed: 693
Downloaded: 737 file(s) [attempted 737/8459 = 8%, 84 KB/s], Decompressed: 730
Downloaded: 780 file(s) [attempted 780/8459 = 9%, 71 KB/s], Decompressed: 775
Downloaded: 816 file(s) [attempted 816/8459 = 9%, 181 KB/s], Decompressed: 809
Downloaded: 855 file(s) [attempted 855/8459 = 10%, 562 KB/s], Decompressed: 850
Downloaded: 898 file(s) [attempted 898/8459 = 10%, 158 KB/s], Decompressed: 891
Downloaded: 942 file(s) [attempted 942/8459 = 11%, 164 KB/s], Decompressed: 932
Downloaded: 980 file(s) [attempted 980/8459 = 11%, 528 KB/s], Decompressed: 970
Downloaded: 1018 file(s) [attempted 1018/8459 = 12%, 450 KB/s], Decompressed: 1004
Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 343 KB/s], Decompressed: 1059
Downloaded: 1107 file(s) [attempted 1107/8459 = 13%, 1924 KB/s], Decompressed: 1059
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 332 KB/s], Decompressed: 1059
Downloaded: 1192 file(s) [attempted 1192/8459 = 14%, 30 KB/s], Decompressed: 1186
Downloaded: 1232 file(s) [attempted 1232/8459 = 14%, 87 KB/s], Decompressed: 1227
Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 100 KB/s], Decompressed: 1257
Downloaded: 1312 file(s) [attempted 1312/8459 = 15%, 838 KB/s], Decompressed: 1305
Downloaded: 1353 file(s) [attempted 1353/8459 = 15%, 217 KB/s], Decompressed: 1350
Downloaded: 1395 file(s) [attempted 1395/8459 = 16%, 217 KB/s], Decompressed: 1391
Downloaded: 1435 file(s) [attempted 1435/8459 = 16%, 23 KB/s], Decompressed: 1432
Downloaded: 1477 file(s) [attempted 1477/8459 = 17%, 1646 KB/s], Decompressed: 1466
Downloaded: 1518 file(s) [attempted 1518/8459 = 17%, 987 KB/s], Decompressed: 1513
Downloaded: 1555 file(s) [attempted 1555/8459 = 18%, 259 KB/s], Decompressed: 1546
Downloaded: 1593 file(s) [attempted 1593/8459 = 18%, 135 KB/s], Decompressed: 1589
Downloaded: 1637 file(s) [attempted 1637/8459 = 19%, 45 KB/s], Decompressed: 1631
Downloaded: 1682 file(s) [attempted 1682/8459 = 19%, 44 KB/s], Decompressed: 1668
Downloaded: 1723 file(s) [attempted 1723/8459 = 20%, 166 KB/s], Decompressed: 1713
Downloaded: 1761 file(s) [attempted 1761/8459 = 20%, 352 KB/s], Decompressed: 1750
Downloaded: 1798 file(s) [attempted 1798/8459 = 21%, 956 KB/s], Decompressed: 1795
Downloaded: 1839 file(s) [attempted 1839/8459 = 21%, 465 KB/s], Decompressed: 1836
Downloaded: 1885 file(s) [attempted 1885/8459 = 22%, 22 KB/s], Decompressed: 1880
Downloaded: 1928 file(s) [attempted 1928/8459 = 22%, 76 KB/s], Decompressed: 1925
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 453 KB/s], Decompressed: 1962
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 56 KB/s], Decompressed: 1997
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 202 KB/s], Decompressed: 2045
Downloaded: 2093 file(s) [attempted 2093/8459 = 24%, 41 KB/s], Decompressed: 2089
Downloaded: 2132 file(s) [attempted 2132/8459 = 25%, 45 KB/s], Decompressed: 2123
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 942 KB/s], Decompressed: 2173
Downloaded: 2223 file(s) [attempted 2223/8459 = 26%, 126 KB/s], Decompressed: 2212
Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 358 KB/s], Decompressed: 2257
Downloaded: 2305 file(s) [attempted 2305/8459 = 27%, 1463 KB/s], Decompressed: 2298
Downloaded: 2349 file(s) [attempted 2349/8459 = 27%, 396 KB/s], Decompressed: 2339
Downloaded: 2394 file(s) [attempted 2394/8459 = 28%, 43 KB/s], Decompressed: 2383
Downloaded: 2433 file(s) [attempted 2433/8459 = 28%, 192 KB/s], Decompressed: 2424
Downloaded: 2469 file(s) [attempted 2469/8459 = 29%, 483 KB/s], Decompressed: 2432
Downloaded: 2513 file(s) [attempted 2513/8459 = 29%, 658 KB/s], Decompressed: 2432
Downloaded: 2555 file(s) [attempted 2555/8459 = 30%, 1488 KB/s], Decompressed: 2551
Downloaded: 2602 file(s) [attempted 2602/8459 = 30%, 289 KB/s], Decompressed: 2596
Downloaded: 2650 file(s) [attempted 2650/8459 = 31%, 358 KB/s], Decompressed: 2644
Downloaded: 2698 file(s) [attempted 2698/8459 = 31%, 36 KB/s], Decompressed: 2695
Downloaded: 2743 file(s) [attempted 2743/8459 = 32%, 58 KB/s], Decompressed: 2736
Downloaded: 2780 file(s) [attempted 2780/8459 = 32%, 56 KB/s], Decompressed: 2774
Downloaded: 2821 file(s) [attempted 2821/8459 = 33%, 729 KB/s], Decompressed: 2815
Downloaded: 2863 file(s) [attempted 2863/8459 = 33%, 500 KB/s], Decompressed: 2856
Downloaded: 2904 file(s) [attempted 2904/8459 = 34%, 993 KB/s], Decompressed: 2876
Downloaded: 2945 file(s) [attempted 2945/8459 = 34%, 134 KB/s], Decompressed: 2934
Downloaded: 2989 file(s) [attempted 2989/8459 = 35%, 685 KB/s], Decompressed: 2986
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 164 KB/s], Decompressed: 3030
Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 362 KB/s], Decompressed: 3068
Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 664 KB/s], Decompressed: 3112
Downloaded: 3157 file(s) [attempted 3157/8459 = 37%, 82 KB/s], Decompressed: 3155
Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 94 KB/s], Decompressed: 3191
Downloaded: 3236 file(s) [attempted 3236/8459 = 38%, 239 KB/s], Decompressed: 3232
Downloaded: 3280 file(s) [attempted 3280/8459 = 38%, 246 KB/s], Decompressed: 3263
Downloaded: 3322 file(s) [attempted 3322/8459 = 39%, 865 KB/s], Decompressed: 3318
Downloaded: 3366 file(s) [attempted 3366/8459 = 39%, 949 KB/s], Decompressed: 3362
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 660 KB/s], Decompressed: 3403
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 65 KB/s], Decompressed: 3437
Downloaded: 3489 file(s) [attempted 3489/8459 = 41%, 191 KB/s], Decompressed: 3482
Downloaded: 3526 file(s) [attempted 3526/8459 = 41%, 137 KB/s], Decompressed: 3525
Downloaded: 3571 file(s) [attempted 3571/8459 = 42%, 359 KB/s], Decompressed: 3564
Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 39 KB/s], Decompressed: 3605
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 206 KB/s], Decompressed: 3646
Downloaded: 3694 file(s) [attempted 3694/8459 = 43%, 189 KB/s], Decompressed: 3680
Downloaded: 3739 file(s) [attempted 3739/8459 = 44%, 282 KB/s], Decompressed: 3735
Downloaded: 3787 file(s) [attempted 3787/8459 = 44%, 93 KB/s], Decompressed: 3780
Downloaded: 3828 file(s) [attempted 3828/8459 = 45%, 125 KB/s], Decompressed: 3817
Downloaded: 3865 file(s) [attempted 3865/8459 = 45%, 54 KB/s], Decompressed: 3862
Downloaded: 3910 file(s) [attempted 3910/8459 = 46%, 155 KB/s], Decompressed: 3906
Downloaded: 3949 file(s) [attempted 3949/8459 = 46%, 341 KB/s], Decompressed: 3944
Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 205 KB/s], Decompressed: 3989
Downloaded: 4036 file(s) [attempted 4036/8459 = 47%, 942 KB/s], Decompressed: 4019
Downloaded: 4077 file(s) [attempted 4077/8459 = 48%, 865 KB/s], Decompressed: 4074
Downloaded: 4122 file(s) [attempted 4122/8459 = 48%, 136 KB/s], Decompressed: 4119
Downloaded: 4160 file(s) [attempted 4160/8459 = 49%, 114 KB/s], Decompressed: 4156
Downloaded: 4201 file(s) [attempted 4201/8459 = 49%, 429 KB/s], Decompressed: 4194
Downloaded: 4245 file(s) [attempted 4245/8459 = 50%, 522 KB/s], Decompressed: 4238
Downloaded: 4286 file(s) [attempted 4286/8459 = 50%, 59 KB/s], Decompressed: 4279
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 2030 KB/s], Decompressed: 4320
Downloaded: 4372 file(s) [attempted 4372/8459 = 51%, 291 KB/s], Decompressed: 4371
Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 75 KB/s], Decompressed: 4409
Downloaded: 4457 file(s) [attempted 4457/8459 = 52%, 227 KB/s], Decompressed: 4447
Downloaded: 4497 file(s) [attempted 4497/8459 = 53%, 237 KB/s], Decompressed: 4492
Downloaded: 4539 file(s) [attempted 4539/8459 = 53%, 23 KB/s], Decompressed: 4536
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 646 KB/s], Decompressed: 4581
Downloaded: 4625 file(s) [attempted 4625/8459 = 54%, 274 KB/s], Decompressed: 4622
Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 73 KB/s], Decompressed: 4659
Downloaded: 4707 file(s) [attempted 4707/8459 = 55%, 179 KB/s], Decompressed: 4700
Downloaded: 4748 file(s) [attempted 4748/8459 = 56%, 659 KB/s], Decompressed: 4738
Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 110 KB/s], Decompressed: 4782
Downloaded: 4831 file(s) [attempted 4831/8459 = 57%, 54 KB/s], Decompressed: 4824
Downloaded: 4871 file(s) [attempted 4871/8459 = 57%, 617 KB/s], Decompressed: 4868
Downloaded: 4913 file(s) [attempted 4913/8459 = 58%, 230 KB/s], Decompressed: 4899
Downloaded: 4955 file(s) [attempted 4955/8459 = 58%, 1409 KB/s], Decompressed: 4950
Downloaded: 4996 file(s) [attempted 4996/8459 = 59%, 474 KB/s], Decompressed: 4988
Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 247 KB/s], Decompressed: 5038
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 144 KB/s], Decompressed: 5073
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 524 KB/s], Decompressed: 5118
Downloaded: 5169 file(s) [attempted 5169/8459 = 61%, 77 KB/s], Decompressed: 5162
Downloaded: 5216 file(s) [attempted 5216/8459 = 61%, 67 KB/s], Decompressed: 5210
Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 40 KB/s], Decompressed: 5251
Downloaded: 5300 file(s) [attempted 5300/8459 = 62%, 33 KB/s], Decompressed: 5296
Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 418 KB/s], Decompressed: 5327
Downloaded: 5376 file(s) [attempted 5376/8459 = 63%, 55 KB/s], Decompressed: 5371
Downloaded: 5419 file(s) [attempted 5419/8459 = 64%, 242 KB/s], Decompressed: 5416
Downloaded: 5460 file(s) [attempted 5460/8459 = 64%, 167 KB/s], Decompressed: 5457
Downloaded: 5505 file(s) [attempted 5505/8459 = 65%, 156 KB/s], Decompressed: 5501
Downloaded: 5546 file(s) [attempted 5546/8459 = 65%, 1631 KB/s], Decompressed: 5535
Downloaded: 5583 file(s) [attempted 5583/8459 = 66%, 1152 KB/s], Decompressed: 5580
Downloaded: 5628 file(s) [attempted 5628/8459 = 66%, 1474 KB/s], Decompressed: 5621
Downloaded: 5669 file(s) [attempted 5669/8459 = 67%, 1819 KB/s], Decompressed: 5665
Downloaded: 5713 file(s) [attempted 5713/8459 = 67%, 200 KB/s], Decompressed: 5703
Downloaded: 5751 file(s) [attempted 5751/8459 = 67%, 854 KB/s], Decompressed: 5744
Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 138 KB/s], Decompressed: 5789
Downloaded: 5834 file(s) [attempted 5834/8459 = 68%, 112 KB/s], Decompressed: 5826
Downloaded: 5874 file(s) [attempted 5874/8459 = 69%, 160 KB/s], Decompressed: 5871
Downloaded: 5917 file(s) [attempted 5917/8459 = 69%, 266 KB/s], Decompressed: 5912
Downloaded: 5956 file(s) [attempted 5956/8459 = 70%, 150 KB/s], Decompressed: 5949
Downloaded: 5997 file(s) [attempted 5997/8459 = 70%, 242 KB/s], Decompressed: 5994
Downloaded: 6040 file(s) [attempted 6040/8459 = 71%, 669 KB/s], Decompressed: 6032
Downloaded: 6080 file(s) [attempted 6080/8459 = 71%, 357 KB/s], Decompressed: 6076
Downloaded: 6124 file(s) [attempted 6124/8459 = 72%, 421 KB/s], Decompressed: 6103
Downloaded: 6162 file(s) [attempted 6162/8459 = 72%, 78 KB/s], Decompressed: 6151
Downloaded: 6203 file(s) [attempted 6203/8459 = 73%, 108 KB/s], Decompressed: 6199
Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 107 KB/s], Decompressed: 6237
Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 51 KB/s], Decompressed: 6281
Downloaded: 6329 file(s) [attempted 6329/8459 = 74%, 376 KB/s], Decompressed: 6323
Downloaded: 6370 file(s) [attempted 6370/8459 = 75%, 377 KB/s], Decompressed: 6364
Downloaded: 6412 file(s) [attempted 6412/8459 = 75%, 308 KB/s], Decompressed: 6408
Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 765 KB/s], Decompressed: 6446
Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 446 KB/s], Decompressed: 6487
Downloaded: 6538 file(s) [attempted 6538/8459 = 77%, 404 KB/s], Decompressed: 6535
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 360 KB/s], Decompressed: 6579
Downloaded: 6624 file(s) [attempted 6624/8459 = 78%, 328 KB/s], Decompressed: 6617
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 203 KB/s], Decompressed: 6661
Downloaded: 6709 file(s) [attempted 6709/8459 = 79%, 460 KB/s], Decompressed: 6703
Downloaded: 6750 file(s) [attempted 6750/8459 = 79%, 53 KB/s], Decompressed: 6749
Downloaded: 6791 file(s) [attempted 6791/8459 = 80%, 76 KB/s], Decompressed: 6788
Downloaded: 6832 file(s) [attempted 6832/8459 = 80%, 40 KB/s], Decompressed: 6829
Downloaded: 6870 file(s) [attempted 6870/8459 = 81%, 1014 KB/s], Decompressed: 6863
Downloaded: 6915 file(s) [attempted 6915/8459 = 81%, 427 KB/s], Decompressed: 6911
Downloaded: 6962 file(s) [attempted 6962/8459 = 82%, 657 KB/s], Decompressed: 6959
Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 1850 KB/s], Decompressed: 7000
Downloaded: 7045 file(s) [attempted 7045/8459 = 83%, 638 KB/s], Decompressed: 7041
Downloaded: 7086 file(s) [attempted 7086/8459 = 83%, 49 KB/s], Decompressed: 7081
Downloaded: 7127 file(s) [attempted 7127/8459 = 84%, 32 KB/s], Decompressed: 7123
Downloaded: 7175 file(s) [attempted 7175/8459 = 84%, 319 KB/s], Decompressed: 7171
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 352 KB/s], Decompressed: 7216
Downloaded: 7263 file(s) [attempted 7263/8459 = 85%, 187 KB/s], Decompressed: 7253
Downloaded: 7301 file(s) [attempted 7301/8459 = 86%, 2077 KB/s], Decompressed: 7294
Downloaded: 7342 file(s) [attempted 7342/8459 = 86%, 579 KB/s], Decompressed: 7339
Downloaded: 7387 file(s) [attempted 7387/8459 = 87%, 300 KB/s], Decompressed: 7383
Downloaded: 7430 file(s) [attempted 7430/8459 = 87%, 641 KB/s], Decompressed: 7421
Downloaded: 7468 file(s) [attempted 7468/8459 = 88%, 381 KB/s], Decompressed: 7455
Downloaded: 7510 file(s) [attempted 7510/8459 = 88%, 224 KB/s], Decompressed: 7504
Downloaded: 7551 file(s) [attempted 7551/8459 = 89%, 97 KB/s], Decompressed: 7544
Downloaded: 7592 file(s) [attempted 7592/8459 = 89%, 922 KB/s], Decompressed: 7589
Downloaded: 7637 file(s) [attempted 7637/8459 = 90%, 147 KB/s], Decompressed: 7602
Downloaded: 7681 file(s) [attempted 7681/8459 = 90%, 152 KB/s], Decompressed: 7602
Downloaded: 7722 file(s) [attempted 7722/8459 = 91%, 205 KB/s], Decompressed: 7715
Downloaded: 7763 file(s) [attempted 7763/8459 = 91%, 302 KB/s], Decompressed: 7756
Downloaded: 7804 file(s) [attempted 7804/8459 = 92%, 39 KB/s], Decompressed: 7798
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 46 KB/s], Decompressed: 7845
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 1129 KB/s], Decompressed: 7883
Downloaded: 7930 file(s) [attempted 7930/8459 = 93%, 353 KB/s], Decompressed: 7924
Downloaded: 7972 file(s) [attempted 7972/8459 = 94%, 1967 KB/s], Decompressed: 7962
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 60 KB/s], Decompressed: 8006
Downloaded: 8054 file(s) [attempted 8054/8459 = 95%, 79 KB/s], Decompressed: 8051
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 726 KB/s], Decompressed: 8095
Downloaded: 8143 file(s) [attempted 8143/8459 = 96%, 498 KB/s], Decompressed: 8126
Downloaded: 8177 file(s) [attempted 8177/8459 = 96%, 413 KB/s], Decompressed: 8126
Downloaded: 8218 file(s) [attempted 8218/8459 = 97%, 781 KB/s], Decompressed: 8133
Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 118 KB/s], Decompressed: 8256
Downloaded: 8304 file(s) [attempted 8304/8459 = 98%, 1166 KB/s], Decompressed: 8301
Downloaded: 8342 file(s) [attempted 8342/8459 = 98%, 168 KB/s], Decompressed: 8338
Downloaded: 8390 file(s) [attempted 8390/8459 = 99%, 96 KB/s], Decompressed: 8386
Downloaded: 8435 file(s) [attempted 8435/8459 = 99%, 1221 KB/s], Decompressed: 8427
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 706 KB/s], Decompressed: 8448
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 706 KB/s], Decompressed: 8448

lean_checker exit 0 duration 4m 43s · created 6/16/2026, 8:59:58 AM

lake build

ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (199s)
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) [0x777c88bc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x777c88bbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x777c88bbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x777c88af3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x777c88af4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x777c88bcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x777c88a32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x777c88a32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x777c88a33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x777c88a341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x777c88bc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x777c88815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x777c88bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x777c88bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x777c88b9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x777c88815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x777c83c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x777c83a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x777c83569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x777c83569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x777c8044524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x777c80445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x565e86fed8da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (8.6s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.2s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (36s)
✔ [3414/3416] Built Iut.Basic (2.4s)
✔ [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 2s · created 6/16/2026, 8:59:58 AM

lake build :blueprint

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

semantic_extract exit 0 duration 1h 45m · created 6/16/2026, 8:59:58 AM

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

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

semantic_extract exit 0 duration 7m 55s · created 6/16/2026, 8:59:58 AM

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

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

semantic_extract exit 0 duration 6m 25s · created 6/16/2026, 8:59:58 AM

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

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

semantic_extract exit 0 duration 31m 59s · created 6/16/2026, 8:59:58 AM

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

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

semantic_extract exit 0 duration 5m 48s · created 6/16/2026, 8:59:58 AM

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

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

semantic_extract exit 0 duration 5m 44s · created 6/16/2026, 8:59:58 AM

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

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