Verification run

Run 357

promachina/iut-lean branch master triggered via github_backfill

succeeded commit 274e6323302a toolchain lean-v4-30-0 prover lean took 3h 8m · 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-525-source
exit_code=Some(0) duration_ms=2435
stderr:
Cloning into '/var/lib/apodeixis/repos/job-525-source'...


$ git checkout 274e6323302a5b771a90562d496de45e98c98199
exit_code=Some(128) duration_ms=4
stderr:
fatal: reference is not a tree: 274e6323302a5b771a90562d496de45e98c98199


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


$ git checkout 274e6323302a5b771a90562d496de45e98c98199 (after fetch)
exit_code=Some(0) duration_ms=140
stderr:
Note: switching to '274e6323302a5b771a90562d496de45e98c98199'.

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 274e632 Derive local log preimages placewise

Resolved source revision: 274e6323302a5b771a90562d496de45e98c98199

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=274e6323302a5b771a90562d496de45e98c98199 provenance={"branch":"master","checked_out_revision":"274e6323302a5b771a90562d496de45e98c98199","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"274e6323302a5b771a90562d496de45e98c98199","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: trying stable superset runner for 6 missing module(s) with 31 imported module candidate(s)
Lean semantic module cache: checkpointed 6 module fragment row(s) from stable superset runner
Lean semantic module cache: stable superset runner extracted 6 missing module(s) in one Lean invocation
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=54624
stdout:
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)

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

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 9 KB/s], Decompressed: 13
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 18 KB/s], Decompressed: 32
Downloaded: 66 file(s) [attempted 66/8459 = 0%, 52 KB/s], Decompressed: 64
Downloaded: 91 file(s) [attempted 91/8459 = 1%, 186 KB/s], Decompressed: 82
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 135 KB/s], Decompressed: 117
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 97 KB/s], Decompressed: 155
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 377 KB/s], Decompressed: 196
Downloaded: 240 file(s) [attempted 240/8459 = 2%, 127 KB/s], Decompressed: 237
Downloaded: 282 file(s) [attempted 282/8459 = 3%, 622 KB/s], Decompressed: 276
Downloaded: 313 file(s) [attempted 313/8459 = 3%, 493 KB/s], Decompressed: 309
Downloaded: 357 file(s) [attempted 357/8459 = 4%, 207 KB/s], Decompressed: 353
Downloaded: 395 file(s) [attempted 395/8459 = 4%, 182 KB/s], Decompressed: 391
Downloaded: 439 file(s) [attempted 439/8459 = 5%, 83 KB/s], Decompressed: 432
Downloaded: 481 file(s) [attempted 481/8459 = 5%, 410 KB/s], Decompressed: 470
Downloaded: 518 file(s) [attempted 518/8459 = 6%, 145 KB/s], Decompressed: 504
Downloaded: 552 file(s) [attempted 552/8459 = 6%, 1454 KB/s], Decompressed: 545
Downloaded: 593 file(s) [attempted 593/8459 = 7%, 270 KB/s], Decompressed: 590
Downloaded: 634 file(s) [attempted 634/8459 = 7%, 806 KB/s], Decompressed: 631
Downloaded: 679 file(s) [attempted 679/8459 = 8%, 151 KB/s], Decompressed: 675
Downloaded: 717 file(s) [attempted 717/8459 = 8%, 496 KB/s], Decompressed: 710
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 62 KB/s], Decompressed: 747
Downloaded: 795 file(s) [attempted 795/8459 = 9%, 111 KB/s], Decompressed: 788
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 712 KB/s], Decompressed: 833
Downloaded: 881 file(s) [attempted 881/8459 = 10%, 285 KB/s], Decompressed: 874
Downloaded: 919 file(s) [attempted 919/8459 = 10%, 149 KB/s], Decompressed: 915
Downloaded: 960 file(s) [attempted 960/8459 = 11%, 232 KB/s], Decompressed: 953
Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 558 KB/s], Decompressed: 997
Downloaded: 1042 file(s) [attempted 1042/8459 = 12%, 884 KB/s], Decompressed: 1038
Downloaded: 1083 file(s) [attempted 1083/8459 = 12%, 267 KB/s], Decompressed: 1076
Downloaded: 1124 file(s) [attempted 1124/8459 = 13%, 143 KB/s], Decompressed: 1121
Downloaded: 1169 file(s) [attempted 1169/8459 = 13%, 222 KB/s], Decompressed: 1158
Downloaded: 1203 file(s) [attempted 1203/8459 = 14%, 181 KB/s], Decompressed: 1192
Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 74 KB/s], Decompressed: 1237
Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 544 KB/s], Decompressed: 1278
Downloaded: 1326 file(s) [attempted 1326/8459 = 15%, 1058 KB/s], Decompressed: 1323
Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 136 KB/s], Decompressed: 1360
Downloaded: 1405 file(s) [attempted 1405/8459 = 16%, 428 KB/s], Decompressed: 1398
Downloaded: 1446 file(s) [attempted 1446/8459 = 17%, 152 KB/s], Decompressed: 1439
Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 51 KB/s], Decompressed: 1439
Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 25 KB/s], Decompressed: 1446
Downloaded: 1572 file(s) [attempted 1572/8459 = 18%, 86 KB/s], Decompressed: 1446
Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 192 KB/s], Decompressed: 1446
Downloaded: 1648 file(s) [attempted 1648/8459 = 19%, 336 KB/s], Decompressed: 1637
Downloaded: 1692 file(s) [attempted 1692/8459 = 20%, 156 KB/s], Decompressed: 1685
Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 239 KB/s], Decompressed: 1729
Downloaded: 1774 file(s) [attempted 1774/8459 = 20%, 28 KB/s], Decompressed: 1771
Downloaded: 1816 file(s) [attempted 1816/8459 = 21%, 161 KB/s], Decompressed: 1809
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 128 KB/s], Decompressed: 1853
Downloaded: 1896 file(s) [attempted 1896/8459 = 22%, 43 KB/s], Decompressed: 1891
Downloaded: 1931 file(s) [attempted 1931/8459 = 22%, 292 KB/s], Decompressed: 1925
Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 44 KB/s], Decompressed: 1969
Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 308 KB/s], Decompressed: 2021
Downloaded: 2069 file(s) [attempted 2069/8459 = 24%, 912 KB/s], Decompressed: 2065
Downloaded: 2106 file(s) [attempted 2106/8459 = 24%, 132 KB/s], Decompressed: 2103
Downloaded: 2148 file(s) [attempted 2148/8459 = 25%, 1669 KB/s], Decompressed: 2140
Downloaded: 2185 file(s) [attempted 2185/8459 = 25%, 486 KB/s], Decompressed: 2182
Downloaded: 2225 file(s) [attempted 2225/8459 = 26%, 301 KB/s], Decompressed: 2219
Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 205 KB/s], Decompressed: 2257
Downloaded: 2305 file(s) [attempted 2305/8459 = 27%, 123 KB/s], Decompressed: 2298
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 168 KB/s], Decompressed: 2339
Downloaded: 2380 file(s) [attempted 2380/8459 = 28%, 108 KB/s], Decompressed: 2373
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 35 KB/s], Decompressed: 2414
Downloaded: 2466 file(s) [attempted 2466/8459 = 29%, 242 KB/s], Decompressed: 2462
Downloaded: 2504 file(s) [attempted 2504/8459 = 29%, 89 KB/s], Decompressed: 2496
Downloaded: 2541 file(s) [attempted 2541/8459 = 30%, 331 KB/s], Decompressed: 2534
Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 109 KB/s], Decompressed: 2572
Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 260 KB/s], Decompressed: 2616
Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 589 KB/s], Decompressed: 2654
Downloaded: 2693 file(s) [attempted 2693/8459 = 31%, 334 KB/s], Decompressed: 2688
Downloaded: 2736 file(s) [attempted 2736/8459 = 32%, 123 KB/s], Decompressed: 2729
Downloaded: 2774 file(s) [attempted 2774/8459 = 32%, 243 KB/s], Decompressed: 2763
Downloaded: 2815 file(s) [attempted 2815/8459 = 33%, 776 KB/s], Decompressed: 2811
Downloaded: 2856 file(s) [attempted 2856/8459 = 33%, 324 KB/s], Decompressed: 2849
Downloaded: 2891 file(s) [attempted 2891/8459 = 34%, 28 KB/s], Decompressed: 2887
Downloaded: 2934 file(s) [attempted 2934/8459 = 34%, 110 KB/s], Decompressed: 2924
Downloaded: 2979 file(s) [attempted 2979/8459 = 35%, 594 KB/s], Decompressed: 2924
Downloaded: 3020 file(s) [attempted 3020/8459 = 35%, 200 KB/s], Decompressed: 2928
Downloaded: 3058 file(s) [attempted 3058/8459 = 36%, 312 KB/s], Decompressed: 3051
Downloaded: 3094 file(s) [attempted 3094/8459 = 36%, 300 KB/s], Decompressed: 3088
Downloaded: 3133 file(s) [attempted 3133/8459 = 37%, 1023 KB/s], Decompressed: 3130
Downloaded: 3177 file(s) [attempted 3177/8459 = 37%, 82 KB/s], Decompressed: 3174
Downloaded: 3221 file(s) [attempted 3221/8459 = 38%, 1465 KB/s], Decompressed: 3215
Downloaded: 3253 file(s) [attempted 3253/8459 = 38%, 1418 KB/s], Decompressed: 3242
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 314 KB/s], Decompressed: 3287
Downloaded: 3335 file(s) [attempted 3335/8459 = 39%, 146 KB/s], Decompressed: 3331
Downloaded: 3376 file(s) [attempted 3376/8459 = 39%, 483 KB/s], Decompressed: 3373
Downloaded: 3420 file(s) [attempted 3420/8459 = 40%, 353 KB/s], Decompressed: 3414
Downloaded: 3455 file(s) [attempted 3455/8459 = 40%, 471 KB/s], Decompressed: 3451
Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 192 KB/s], Decompressed: 3489
Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 165 KB/s], Decompressed: 3531
Downloaded: 3575 file(s) [attempted 3575/8459 = 42%, 186 KB/s], Decompressed: 3571
Downloaded: 3617 file(s) [attempted 3617/8459 = 42%, 566 KB/s], Decompressed: 3609
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 692 KB/s], Decompressed: 3646
Downloaded: 3693 file(s) [attempted 3693/8459 = 43%, 53 KB/s], Decompressed: 3687
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 288 KB/s], Decompressed: 3725
Downloaded: 3770 file(s) [attempted 3770/8459 = 44%, 300 KB/s], Decompressed: 3766
Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 101 KB/s], Decompressed: 3807
Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 430 KB/s], Decompressed: 3845
Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 407 KB/s], Decompressed: 3886
Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 69 KB/s], Decompressed: 3927
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 176 KB/s], Decompressed: 3961
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 1864 KB/s], Decompressed: 3961
Downloaded: 4059 file(s) [attempted 4059/8459 = 47%, 384 KB/s], Decompressed: 3961
Downloaded: 4094 file(s) [attempted 4094/8459 = 48%, 182 KB/s], Decompressed: 3968
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 631 KB/s], Decompressed: 4125
Downloaded: 4177 file(s) [attempted 4177/8459 = 49%, 48 KB/s], Decompressed: 4173
Downloaded: 4214 file(s) [attempted 4214/8459 = 49%, 70 KB/s], Decompressed: 4208
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 53 KB/s], Decompressed: 4242
Downloaded: 4286 file(s) [attempted 4286/8459 = 50%, 320 KB/s], Decompressed: 4283
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 187 KB/s], Decompressed: 4324
Downloaded: 4375 file(s) [attempted 4375/8459 = 51%, 166 KB/s], Decompressed: 4368
Downloaded: 4412 file(s) [attempted 4412/8459 = 52%, 1146 KB/s], Decompressed: 4403
Downloaded: 4449 file(s) [attempted 4449/8459 = 52%, 371 KB/s], Decompressed: 4440
Downloaded: 4485 file(s) [attempted 4485/8459 = 53%, 364 KB/s], Decompressed: 4475
Downloaded: 4529 file(s) [attempted 4529/8459 = 53%, 60 KB/s], Decompressed: 4522
Downloaded: 4570 file(s) [attempted 4570/8459 = 54%, 67 KB/s], Decompressed: 4560
Downloaded: 4610 file(s) [attempted 4610/8459 = 54%, 349 KB/s], Decompressed: 4601
Downloaded: 4644 file(s) [attempted 4644/8459 = 54%, 112 KB/s], Decompressed: 4635
Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 360 KB/s], Decompressed: 4666
Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 100 KB/s], Decompressed: 4666
Downloaded: 4769 file(s) [attempted 4769/8459 = 56%, 329 KB/s], Decompressed: 4666
Downloaded: 4808 file(s) [attempted 4808/8459 = 56%, 93 KB/s], Decompressed: 4670
Downloaded: 4848 file(s) [attempted 4848/8459 = 57%, 280 KB/s], Decompressed: 4670
Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 212 KB/s], Decompressed: 4670
Downloaded: 4930 file(s) [attempted 4930/8459 = 58%, 132 KB/s], Decompressed: 4670
Downloaded: 4974 file(s) [attempted 4974/8459 = 58%, 179 KB/s], Decompressed: 4789
Downloaded: 5015 file(s) [attempted 5015/8459 = 59%, 792 KB/s], Decompressed: 4789
Downloaded: 5050 file(s) [attempted 5050/8459 = 59%, 139 KB/s], Decompressed: 4789
Downloaded: 5091 file(s) [attempted 5091/8459 = 60%, 197 KB/s], Decompressed: 4789
Downloaded: 5132 file(s) [attempted 5132/8459 = 60%, 489 KB/s], Decompressed: 4789
Downloaded: 5169 file(s) [attempted 5169/8459 = 61%, 74 KB/s], Decompressed: 4789
Downloaded: 5214 file(s) [attempted 5214/8459 = 61%, 46 KB/s], Decompressed: 4954
Downloaded: 5251 file(s) [attempted 5251/8459 = 62%, 267 KB/s], Decompressed: 4954
Downloaded: 5293 file(s) [attempted 5293/8459 = 62%, 1464 KB/s], Decompressed: 4954
Downloaded: 5332 file(s) [attempted 5332/8459 = 63%, 1021 KB/s], Decompressed: 5323
Downloaded: 5368 file(s) [attempted 5368/8459 = 63%, 1130 KB/s], Decompressed: 5364
Downloaded: 5412 file(s) [attempted 5412/8459 = 63%, 164 KB/s], Decompressed: 5409
Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 351 KB/s], Decompressed: 5450
Downloaded: 5498 file(s) [attempted 5498/8459 = 64%, 301 KB/s], Decompressed: 5481
Downloaded: 5539 file(s) [attempted 5539/8459 = 65%, 301 KB/s], Decompressed: 5481
Downloaded: 5573 file(s) [attempted 5573/8459 = 65%, 830 KB/s], Decompressed: 5481
Downloaded: 5618 file(s) [attempted 5618/8459 = 66%, 1117 KB/s], Decompressed: 5481
Downloaded: 5666 file(s) [attempted 5666/8459 = 66%, 229 KB/s], Decompressed: 5490
Downloaded: 5710 file(s) [attempted 5710/8459 = 67%, 565 KB/s], Decompressed: 5700
Downloaded: 5748 file(s) [attempted 5748/8459 = 67%, 30 KB/s], Decompressed: 5744
Downloaded: 5789 file(s) [attempted 5789/8459 = 68%, 63 KB/s], Decompressed: 5785
Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 102 KB/s], Decompressed: 5789
Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 206 KB/s], Decompressed: 5789
Downloaded: 5905 file(s) [attempted 5905/8459 = 69%, 71 KB/s], Decompressed: 5792
Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 352 KB/s], Decompressed: 5891
Downloaded: 5980 file(s) [attempted 5980/8459 = 70%, 1497 KB/s], Decompressed: 5912
Downloaded: 6018 file(s) [attempted 6018/8459 = 71%, 291 KB/s], Decompressed: 5912
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 167 KB/s], Decompressed: 5970
Downloaded: 6100 file(s) [attempted 6100/8459 = 72%, 57 KB/s], Decompressed: 6035
Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 126 KB/s], Decompressed: 6035
Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 548 KB/s], Decompressed: 6035
Downloaded: 6217 file(s) [attempted 6217/8459 = 73%, 309 KB/s], Decompressed: 6035
Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 69 KB/s], Decompressed: 6035
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 240 KB/s], Decompressed: 6086
Downloaded: 6336 file(s) [attempted 6336/8459 = 74%, 777 KB/s], Decompressed: 6086
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 491 KB/s], Decompressed: 6295
Downloaded: 6418 file(s) [attempted 6418/8459 = 75%, 1595 KB/s], Decompressed: 6295
Downloaded: 6460 file(s) [attempted 6460/8459 = 76%, 620 KB/s], Decompressed: 6343
Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 77 KB/s], Decompressed: 6343
Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 47 KB/s], Decompressed: 6343
Downloaded: 6576 file(s) [attempted 6576/8459 = 77%, 496 KB/s], Decompressed: 6425
Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 93 KB/s], Decompressed: 6425
Downloaded: 6661 file(s) [attempted 6661/8459 = 78%, 336 KB/s], Decompressed: 6562
Downloaded: 6696 file(s) [attempted 6696/8459 = 79%, 47 KB/s], Decompressed: 6562
Downloaded: 6733 file(s) [attempted 6733/8459 = 79%, 397 KB/s], Decompressed: 6562
Downloaded: 6778 file(s) [attempted 6778/8459 = 80%, 977 KB/s], Decompressed: 6641
Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 127 KB/s], Decompressed: 6641
Downloaded: 6863 file(s) [attempted 6863/8459 = 81%, 109 KB/s], Decompressed: 6641
Downloaded: 6908 file(s) [attempted 6908/8459 = 81%, 223 KB/s], Decompressed: 6641
Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 449 KB/s], Decompressed: 6641
Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 110 KB/s], Decompressed: 6747
Downloaded: 7021 file(s) [attempted 7021/8459 = 83%, 451 KB/s], Decompressed: 6747
Downloaded: 7062 file(s) [attempted 7062/8459 = 83%, 87 KB/s], Decompressed: 6747
Downloaded: 7103 file(s) [attempted 7103/8459 = 83%, 180 KB/s], Decompressed: 6963
Downloaded: 7139 file(s) [attempted 7139/8459 = 84%, 114 KB/s], Decompressed: 7134
Downloaded: 7182 file(s) [attempted 7182/8459 = 84%, 287 KB/s], Decompressed: 7171
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 281 KB/s], Decompressed: 7171
Downloaded: 7264 file(s) [attempted 7264/8459 = 85%, 121 KB/s], Decompressed: 7171
Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 146 KB/s], Decompressed: 7178
Downloaded: 7342 file(s) [attempted 7342/8459 = 86%, 526 KB/s], Decompressed: 7178
Downloaded: 7387 file(s) [attempted 7387/8459 = 87%, 243 KB/s], Decompressed: 7178
Downloaded: 7428 file(s) [attempted 7428/8459 = 87%, 101 KB/s], Decompressed: 7271
Downloaded: 7473 file(s) [attempted 7473/8459 = 88%, 180 KB/s], Decompressed: 7271
Downloaded: 7517 file(s) [attempted 7517/8459 = 88%, 195 KB/s], Decompressed: 7271
Downloaded: 7552 file(s) [attempted 7552/8459 = 89%, 948 KB/s], Decompressed: 7271
Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 142 KB/s], Decompressed: 7572
Downloaded: 7630 file(s) [attempted 7630/8459 = 90%, 129 KB/s], Decompressed: 7623
Downloaded: 7671 file(s) [attempted 7671/8459 = 90%, 38 KB/s], Decompressed: 7637
Downloaded: 7712 file(s) [attempted 7712/8459 = 91%, 126 KB/s], Decompressed: 7637
Downloaded: 7750 file(s) [attempted 7750/8459 = 91%, 219 KB/s], Decompressed: 7637
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 112 KB/s], Decompressed: 7640
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 487 KB/s], Decompressed: 7640
Downloaded: 7869 file(s) [attempted 7869/8459 = 93%, 487 KB/s], Decompressed: 7640
Downloaded: 7909 file(s) [attempted 7909/8459 = 93%, 1540 KB/s], Decompressed: 7897
Downloaded: 7943 file(s) [attempted 7943/8459 = 93%, 38 KB/s], Decompressed: 7931
Downloaded: 7981 file(s) [attempted 7981/8459 = 94%, 211 KB/s], Decompressed: 7972
Downloaded: 8023 file(s) [attempted 8023/8459 = 94%, 244 KB/s], Decompressed: 8020
Downloaded: 8068 file(s) [attempted 8068/8459 = 95%, 77 KB/s], Decompressed: 8054
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 150 KB/s], Decompressed: 8099
Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 78 KB/s], Decompressed: 8133
Downloaded: 8177 file(s) [attempted 8177/8459 = 96%, 51 KB/s], Decompressed: 8174
Downloaded: 8220 file(s) [attempted 8220/8459 = 97%, 99 KB/s], Decompressed: 8215
Downloaded: 8256 file(s) [attempted 8256/8459 = 97%, 137 KB/s], Decompressed: 8253
Downloaded: 8296 file(s) [attempted 8296/8459 = 98%, 93 KB/s], Decompressed: 8290
Downloaded: 8335 file(s) [attempted 8335/8459 = 98%, 82 KB/s], Decompressed: 8328
Downloaded: 8373 file(s) [attempted 8373/8459 = 98%, 771 KB/s], Decompressed: 8369
Downloaded: 8412 file(s) [attempted 8412/8459 = 99%, 974 KB/s], Decompressed: 8407
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 87 KB/s], Decompressed: 8444
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 87 KB/s], Decompressed: 8455


$ lake build
exit_code=Some(0) duration_ms=320004
stdout:
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (240s)
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) [0x71dad6dc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x71dad6dbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x71dad6dbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x71dad6cf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x71dad6cf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x71dad6dcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x71dad6c32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x71dad6c32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x71dad6c33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x71dad6c341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x71dad6dc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x71dad6a15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x71dad6dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x71dad6dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x71dad6d9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x71dad6a15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x71dad1e22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x71dad1c0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x71dad1769a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x71dad1769f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x71dace64524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x71dace645305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5de27bfb08da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (7.9s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.3s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (35s)
✔ [3414/3416] Built Iut.Basic (2.5s)
✔ [3415/3416] Built Iut (2.5s)
Build completed successfully (3416 jobs).

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=3214
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-stable-superset)
exit_code=Some(0) duration_ms=10570925
stdout:
apx-semantic-phase	{"duration_ms":5,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":9,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":328368,"module_count":1,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":56,"module_count":1,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"ok":true,"payload_bytes":738,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"ok":true,"payload_bytes":738,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":81,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":332937,"module_count":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":56,"module_count":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"ok":true,"payload_bytes":1330,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"ok":true,"payload_bytes":1330,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":97,"diagnostic_count":15,"duration_ms":7530,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":330199,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":97,"diagnostic_count":15,"duration_ms":393,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"ok":true,"payload_bytes":3002937,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":2,"ok":true,"payload_bytes":3002937,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":1888,"diagnostic_count":116,"duration_ms":1534050,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":346976,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1888,"diagnostic_count":116,"duration_ms":7425,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"ok":true,"payload_bytes":66851125,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":48,"module_index":3,"ok":true,"payload_bytes":66851125,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":7706,"diagnostic_count":3080,"duration_ms":6091253,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":502588,"module_count":1,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":7706,"diagnostic_count":3080,"duration_ms":39094,"module_count":1,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"ok":true,"payload_bytes":460841742,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":495,"module_index":4,"ok":true,"payload_bytes":460841742,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":152,"diagnostic_count":23,"duration_ms":25038,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":916383,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":152,"diagnostic_count":23,"duration_ms":1094,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":5,"ok":true,"payload_bytes":2722873,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":4,"module_index":5,"ok":true,"payload_bytes":2722873,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":9844,"diagnostic_count":3234,"duration_ms":57650,"module_count":6,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":534535836,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1283,"ok":true,"payload_bytes":534535836,"phase":"lean_json_write"}

stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"core_compile","duration_ms":3386}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":353,"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":3448,"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 5e463795818150aa4211cd980cc51c16a0f42edef395609205431c2db2b498db
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":10546498,"ok":true}

Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

git_clone exit 0 duration 2s · created 6/18/2026, 1:51:01 PM

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

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

git_checkout exit 128 duration 4 ms · created 6/18/2026, 1:51:01 PM

git checkout 274e6323302a5b771a90562d496de45e98c98199

fatal: reference is not a tree: 274e6323302a5b771a90562d496de45e98c98199

git_checkout exit 0 duration 1s · created 6/18/2026, 1:51:01 PM

git fetch --depth 1 origin 274e6323302a5b771a90562d496de45e98c98199

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

git_checkout exit 0 duration 140 ms · created 6/18/2026, 1:51:01 PM

git checkout 274e6323302a5b771a90562d496de45e98c98199 (after fetch)

Note: switching to '274e6323302a5b771a90562d496de45e98c98199'.

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 274e632 Derive local log preimages placewise

lake_cache exit 0 duration 55s · created 6/18/2026, 1:51:01 PM

lake exe cache get

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

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

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 9 KB/s], Decompressed: 13
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 18 KB/s], Decompressed: 32
Downloaded: 66 file(s) [attempted 66/8459 = 0%, 52 KB/s], Decompressed: 64
Downloaded: 91 file(s) [attempted 91/8459 = 1%, 186 KB/s], Decompressed: 82
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 135 KB/s], Decompressed: 117
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 97 KB/s], Decompressed: 155
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 377 KB/s], Decompressed: 196
Downloaded: 240 file(s) [attempted 240/8459 = 2%, 127 KB/s], Decompressed: 237
Downloaded: 282 file(s) [attempted 282/8459 = 3%, 622 KB/s], Decompressed: 276
Downloaded: 313 file(s) [attempted 313/8459 = 3%, 493 KB/s], Decompressed: 309
Downloaded: 357 file(s) [attempted 357/8459 = 4%, 207 KB/s], Decompressed: 353
Downloaded: 395 file(s) [attempted 395/8459 = 4%, 182 KB/s], Decompressed: 391
Downloaded: 439 file(s) [attempted 439/8459 = 5%, 83 KB/s], Decompressed: 432
Downloaded: 481 file(s) [attempted 481/8459 = 5%, 410 KB/s], Decompressed: 470
Downloaded: 518 file(s) [attempted 518/8459 = 6%, 145 KB/s], Decompressed: 504
Downloaded: 552 file(s) [attempted 552/8459 = 6%, 1454 KB/s], Decompressed: 545
Downloaded: 593 file(s) [attempted 593/8459 = 7%, 270 KB/s], Decompressed: 590
Downloaded: 634 file(s) [attempted 634/8459 = 7%, 806 KB/s], Decompressed: 631
Downloaded: 679 file(s) [attempted 679/8459 = 8%, 151 KB/s], Decompressed: 675
Downloaded: 717 file(s) [attempted 717/8459 = 8%, 496 KB/s], Decompressed: 710
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 62 KB/s], Decompressed: 747
Downloaded: 795 file(s) [attempted 795/8459 = 9%, 111 KB/s], Decompressed: 788
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 712 KB/s], Decompressed: 833
Downloaded: 881 file(s) [attempted 881/8459 = 10%, 285 KB/s], Decompressed: 874
Downloaded: 919 file(s) [attempted 919/8459 = 10%, 149 KB/s], Decompressed: 915
Downloaded: 960 file(s) [attempted 960/8459 = 11%, 232 KB/s], Decompressed: 953
Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 558 KB/s], Decompressed: 997
Downloaded: 1042 file(s) [attempted 1042/8459 = 12%, 884 KB/s], Decompressed: 1038
Downloaded: 1083 file(s) [attempted 1083/8459 = 12%, 267 KB/s], Decompressed: 1076
Downloaded: 1124 file(s) [attempted 1124/8459 = 13%, 143 KB/s], Decompressed: 1121
Downloaded: 1169 file(s) [attempted 1169/8459 = 13%, 222 KB/s], Decompressed: 1158
Downloaded: 1203 file(s) [attempted 1203/8459 = 14%, 181 KB/s], Decompressed: 1192
Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 74 KB/s], Decompressed: 1237
Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 544 KB/s], Decompressed: 1278
Downloaded: 1326 file(s) [attempted 1326/8459 = 15%, 1058 KB/s], Decompressed: 1323
Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 136 KB/s], Decompressed: 1360
Downloaded: 1405 file(s) [attempted 1405/8459 = 16%, 428 KB/s], Decompressed: 1398
Downloaded: 1446 file(s) [attempted 1446/8459 = 17%, 152 KB/s], Decompressed: 1439
Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 51 KB/s], Decompressed: 1439
Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 25 KB/s], Decompressed: 1446
Downloaded: 1572 file(s) [attempted 1572/8459 = 18%, 86 KB/s], Decompressed: 1446
Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 192 KB/s], Decompressed: 1446
Downloaded: 1648 file(s) [attempted 1648/8459 = 19%, 336 KB/s], Decompressed: 1637
Downloaded: 1692 file(s) [attempted 1692/8459 = 20%, 156 KB/s], Decompressed: 1685
Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 239 KB/s], Decompressed: 1729
Downloaded: 1774 file(s) [attempted 1774/8459 = 20%, 28 KB/s], Decompressed: 1771
Downloaded: 1816 file(s) [attempted 1816/8459 = 21%, 161 KB/s], Decompressed: 1809
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 128 KB/s], Decompressed: 1853
Downloaded: 1896 file(s) [attempted 1896/8459 = 22%, 43 KB/s], Decompressed: 1891
Downloaded: 1931 file(s) [attempted 1931/8459 = 22%, 292 KB/s], Decompressed: 1925
Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 44 KB/s], Decompressed: 1969
Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 308 KB/s], Decompressed: 2021
Downloaded: 2069 file(s) [attempted 2069/8459 = 24%, 912 KB/s], Decompressed: 2065
Downloaded: 2106 file(s) [attempted 2106/8459 = 24%, 132 KB/s], Decompressed: 2103
Downloaded: 2148 file(s) [attempted 2148/8459 = 25%, 1669 KB/s], Decompressed: 2140
Downloaded: 2185 file(s) [attempted 2185/8459 = 25%, 486 KB/s], Decompressed: 2182
Downloaded: 2225 file(s) [attempted 2225/8459 = 26%, 301 KB/s], Decompressed: 2219
Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 205 KB/s], Decompressed: 2257
Downloaded: 2305 file(s) [attempted 2305/8459 = 27%, 123 KB/s], Decompressed: 2298
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 168 KB/s], Decompressed: 2339
Downloaded: 2380 file(s) [attempted 2380/8459 = 28%, 108 KB/s], Decompressed: 2373
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 35 KB/s], Decompressed: 2414
Downloaded: 2466 file(s) [attempted 2466/8459 = 29%, 242 KB/s], Decompressed: 2462
Downloaded: 2504 file(s) [attempted 2504/8459 = 29%, 89 KB/s], Decompressed: 2496
Downloaded: 2541 file(s) [attempted 2541/8459 = 30%, 331 KB/s], Decompressed: 2534
Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 109 KB/s], Decompressed: 2572
Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 260 KB/s], Decompressed: 2616
Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 589 KB/s], Decompressed: 2654
Downloaded: 2693 file(s) [attempted 2693/8459 = 31%, 334 KB/s], Decompressed: 2688
Downloaded: 2736 file(s) [attempted 2736/8459 = 32%, 123 KB/s], Decompressed: 2729
Downloaded: 2774 file(s) [attempted 2774/8459 = 32%, 243 KB/s], Decompressed: 2763
Downloaded: 2815 file(s) [attempted 2815/8459 = 33%, 776 KB/s], Decompressed: 2811
Downloaded: 2856 file(s) [attempted 2856/8459 = 33%, 324 KB/s], Decompressed: 2849
Downloaded: 2891 file(s) [attempted 2891/8459 = 34%, 28 KB/s], Decompressed: 2887
Downloaded: 2934 file(s) [attempted 2934/8459 = 34%, 110 KB/s], Decompressed: 2924
Downloaded: 2979 file(s) [attempted 2979/8459 = 35%, 594 KB/s], Decompressed: 2924
Downloaded: 3020 file(s) [attempted 3020/8459 = 35%, 200 KB/s], Decompressed: 2928
Downloaded: 3058 file(s) [attempted 3058/8459 = 36%, 312 KB/s], Decompressed: 3051
Downloaded: 3094 file(s) [attempted 3094/8459 = 36%, 300 KB/s], Decompressed: 3088
Downloaded: 3133 file(s) [attempted 3133/8459 = 37%, 1023 KB/s], Decompressed: 3130
Downloaded: 3177 file(s) [attempted 3177/8459 = 37%, 82 KB/s], Decompressed: 3174
Downloaded: 3221 file(s) [attempted 3221/8459 = 38%, 1465 KB/s], Decompressed: 3215
Downloaded: 3253 file(s) [attempted 3253/8459 = 38%, 1418 KB/s], Decompressed: 3242
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 314 KB/s], Decompressed: 3287
Downloaded: 3335 file(s) [attempted 3335/8459 = 39%, 146 KB/s], Decompressed: 3331
Downloaded: 3376 file(s) [attempted 3376/8459 = 39%, 483 KB/s], Decompressed: 3373
Downloaded: 3420 file(s) [attempted 3420/8459 = 40%, 353 KB/s], Decompressed: 3414
Downloaded: 3455 file(s) [attempted 3455/8459 = 40%, 471 KB/s], Decompressed: 3451
Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 192 KB/s], Decompressed: 3489
Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 165 KB/s], Decompressed: 3531
Downloaded: 3575 file(s) [attempted 3575/8459 = 42%, 186 KB/s], Decompressed: 3571
Downloaded: 3617 file(s) [attempted 3617/8459 = 42%, 566 KB/s], Decompressed: 3609
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 692 KB/s], Decompressed: 3646
Downloaded: 3693 file(s) [attempted 3693/8459 = 43%, 53 KB/s], Decompressed: 3687
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 288 KB/s], Decompressed: 3725
Downloaded: 3770 file(s) [attempted 3770/8459 = 44%, 300 KB/s], Decompressed: 3766
Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 101 KB/s], Decompressed: 3807
Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 430 KB/s], Decompressed: 3845
Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 407 KB/s], Decompressed: 3886
Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 69 KB/s], Decompressed: 3927
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 176 KB/s], Decompressed: 3961
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 1864 KB/s], Decompressed: 3961
Downloaded: 4059 file(s) [attempted 4059/8459 = 47%, 384 KB/s], Decompressed: 3961
Downloaded: 4094 file(s) [attempted 4094/8459 = 48%, 182 KB/s], Decompressed: 3968
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 631 KB/s], Decompressed: 4125
Downloaded: 4177 file(s) [attempted 4177/8459 = 49%, 48 KB/s], Decompressed: 4173
Downloaded: 4214 file(s) [attempted 4214/8459 = 49%, 70 KB/s], Decompressed: 4208
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 53 KB/s], Decompressed: 4242
Downloaded: 4286 file(s) [attempted 4286/8459 = 50%, 320 KB/s], Decompressed: 4283
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 187 KB/s], Decompressed: 4324
Downloaded: 4375 file(s) [attempted 4375/8459 = 51%, 166 KB/s], Decompressed: 4368
Downloaded: 4412 file(s) [attempted 4412/8459 = 52%, 1146 KB/s], Decompressed: 4403
Downloaded: 4449 file(s) [attempted 4449/8459 = 52%, 371 KB/s], Decompressed: 4440
Downloaded: 4485 file(s) [attempted 4485/8459 = 53%, 364 KB/s], Decompressed: 4475
Downloaded: 4529 file(s) [attempted 4529/8459 = 53%, 60 KB/s], Decompressed: 4522
Downloaded: 4570 file(s) [attempted 4570/8459 = 54%, 67 KB/s], Decompressed: 4560
Downloaded: 4610 file(s) [attempted 4610/8459 = 54%, 349 KB/s], Decompressed: 4601
Downloaded: 4644 file(s) [attempted 4644/8459 = 54%, 112 KB/s], Decompressed: 4635
Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 360 KB/s], Decompressed: 4666
Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 100 KB/s], Decompressed: 4666
Downloaded: 4769 file(s) [attempted 4769/8459 = 56%, 329 KB/s], Decompressed: 4666
Downloaded: 4808 file(s) [attempted 4808/8459 = 56%, 93 KB/s], Decompressed: 4670
Downloaded: 4848 file(s) [attempted 4848/8459 = 57%, 280 KB/s], Decompressed: 4670
Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 212 KB/s], Decompressed: 4670
Downloaded: 4930 file(s) [attempted 4930/8459 = 58%, 132 KB/s], Decompressed: 4670
Downloaded: 4974 file(s) [attempted 4974/8459 = 58%, 179 KB/s], Decompressed: 4789
Downloaded: 5015 file(s) [attempted 5015/8459 = 59%, 792 KB/s], Decompressed: 4789
Downloaded: 5050 file(s) [attempted 5050/8459 = 59%, 139 KB/s], Decompressed: 4789
Downloaded: 5091 file(s) [attempted 5091/8459 = 60%, 197 KB/s], Decompressed: 4789
Downloaded: 5132 file(s) [attempted 5132/8459 = 60%, 489 KB/s], Decompressed: 4789
Downloaded: 5169 file(s) [attempted 5169/8459 = 61%, 74 KB/s], Decompressed: 4789
Downloaded: 5214 file(s) [attempted 5214/8459 = 61%, 46 KB/s], Decompressed: 4954
Downloaded: 5251 file(s) [attempted 5251/8459 = 62%, 267 KB/s], Decompressed: 4954
Downloaded: 5293 file(s) [attempted 5293/8459 = 62%, 1464 KB/s], Decompressed: 4954
Downloaded: 5332 file(s) [attempted 5332/8459 = 63%, 1021 KB/s], Decompressed: 5323
Downloaded: 5368 file(s) [attempted 5368/8459 = 63%, 1130 KB/s], Decompressed: 5364
Downloaded: 5412 file(s) [attempted 5412/8459 = 63%, 164 KB/s], Decompressed: 5409
Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 351 KB/s], Decompressed: 5450
Downloaded: 5498 file(s) [attempted 5498/8459 = 64%, 301 KB/s], Decompressed: 5481
Downloaded: 5539 file(s) [attempted 5539/8459 = 65%, 301 KB/s], Decompressed: 5481
Downloaded: 5573 file(s) [attempted 5573/8459 = 65%, 830 KB/s], Decompressed: 5481
Downloaded: 5618 file(s) [attempted 5618/8459 = 66%, 1117 KB/s], Decompressed: 5481
Downloaded: 5666 file(s) [attempted 5666/8459 = 66%, 229 KB/s], Decompressed: 5490
Downloaded: 5710 file(s) [attempted 5710/8459 = 67%, 565 KB/s], Decompressed: 5700
Downloaded: 5748 file(s) [attempted 5748/8459 = 67%, 30 KB/s], Decompressed: 5744
Downloaded: 5789 file(s) [attempted 5789/8459 = 68%, 63 KB/s], Decompressed: 5785
Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 102 KB/s], Decompressed: 5789
Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 206 KB/s], Decompressed: 5789
Downloaded: 5905 file(s) [attempted 5905/8459 = 69%, 71 KB/s], Decompressed: 5792
Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 352 KB/s], Decompressed: 5891
Downloaded: 5980 file(s) [attempted 5980/8459 = 70%, 1497 KB/s], Decompressed: 5912
Downloaded: 6018 file(s) [attempted 6018/8459 = 71%, 291 KB/s], Decompressed: 5912
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 167 KB/s], Decompressed: 5970
Downloaded: 6100 file(s) [attempted 6100/8459 = 72%, 57 KB/s], Decompressed: 6035
Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 126 KB/s], Decompressed: 6035
Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 548 KB/s], Decompressed: 6035
Downloaded: 6217 file(s) [attempted 6217/8459 = 73%, 309 KB/s], Decompressed: 6035
Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 69 KB/s], Decompressed: 6035
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 240 KB/s], Decompressed: 6086
Downloaded: 6336 file(s) [attempted 6336/8459 = 74%, 777 KB/s], Decompressed: 6086
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 491 KB/s], Decompressed: 6295
Downloaded: 6418 file(s) [attempted 6418/8459 = 75%, 1595 KB/s], Decompressed: 6295
Downloaded: 6460 file(s) [attempted 6460/8459 = 76%, 620 KB/s], Decompressed: 6343
Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 77 KB/s], Decompressed: 6343
Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 47 KB/s], Decompressed: 6343
Downloaded: 6576 file(s) [attempted 6576/8459 = 77%, 496 KB/s], Decompressed: 6425
Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 93 KB/s], Decompressed: 6425
Downloaded: 6661 file(s) [attempted 6661/8459 = 78%, 336 KB/s], Decompressed: 6562
Downloaded: 6696 file(s) [attempted 6696/8459 = 79%, 47 KB/s], Decompressed: 6562
Downloaded: 6733 file(s) [attempted 6733/8459 = 79%, 397 KB/s], Decompressed: 6562
Downloaded: 6778 file(s) [attempted 6778/8459 = 80%, 977 KB/s], Decompressed: 6641
Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 127 KB/s], Decompressed: 6641
Downloaded: 6863 file(s) [attempted 6863/8459 = 81%, 109 KB/s], Decompressed: 6641
Downloaded: 6908 file(s) [attempted 6908/8459 = 81%, 223 KB/s], Decompressed: 6641
Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 449 KB/s], Decompressed: 6641
Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 110 KB/s], Decompressed: 6747
Downloaded: 7021 file(s) [attempted 7021/8459 = 83%, 451 KB/s], Decompressed: 6747
Downloaded: 7062 file(s) [attempted 7062/8459 = 83%, 87 KB/s], Decompressed: 6747
Downloaded: 7103 file(s) [attempted 7103/8459 = 83%, 180 KB/s], Decompressed: 6963
Downloaded: 7139 file(s) [attempted 7139/8459 = 84%, 114 KB/s], Decompressed: 7134
Downloaded: 7182 file(s) [attempted 7182/8459 = 84%, 287 KB/s], Decompressed: 7171
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 281 KB/s], Decompressed: 7171
Downloaded: 7264 file(s) [attempted 7264/8459 = 85%, 121 KB/s], Decompressed: 7171
Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 146 KB/s], Decompressed: 7178
Downloaded: 7342 file(s) [attempted 7342/8459 = 86%, 526 KB/s], Decompressed: 7178
Downloaded: 7387 file(s) [attempted 7387/8459 = 87%, 243 KB/s], Decompressed: 7178
Downloaded: 7428 file(s) [attempted 7428/8459 = 87%, 101 KB/s], Decompressed: 7271
Downloaded: 7473 file(s) [attempted 7473/8459 = 88%, 180 KB/s], Decompressed: 7271
Downloaded: 7517 file(s) [attempted 7517/8459 = 88%, 195 KB/s], Decompressed: 7271
Downloaded: 7552 file(s) [attempted 7552/8459 = 89%, 948 KB/s], Decompressed: 7271
Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 142 KB/s], Decompressed: 7572
Downloaded: 7630 file(s) [attempted 7630/8459 = 90%, 129 KB/s], Decompressed: 7623
Downloaded: 7671 file(s) [attempted 7671/8459 = 90%, 38 KB/s], Decompressed: 7637
Downloaded: 7712 file(s) [attempted 7712/8459 = 91%, 126 KB/s], Decompressed: 7637
Downloaded: 7750 file(s) [attempted 7750/8459 = 91%, 219 KB/s], Decompressed: 7637
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 112 KB/s], Decompressed: 7640
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 487 KB/s], Decompressed: 7640
Downloaded: 7869 file(s) [attempted 7869/8459 = 93%, 487 KB/s], Decompressed: 7640
Downloaded: 7909 file(s) [attempted 7909/8459 = 93%, 1540 KB/s], Decompressed: 7897
Downloaded: 7943 file(s) [attempted 7943/8459 = 93%, 38 KB/s], Decompressed: 7931
Downloaded: 7981 file(s) [attempted 7981/8459 = 94%, 211 KB/s], Decompressed: 7972
Downloaded: 8023 file(s) [attempted 8023/8459 = 94%, 244 KB/s], Decompressed: 8020
Downloaded: 8068 file(s) [attempted 8068/8459 = 95%, 77 KB/s], Decompressed: 8054
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 150 KB/s], Decompressed: 8099
Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 78 KB/s], Decompressed: 8133
Downloaded: 8177 file(s) [attempted 8177/8459 = 96%, 51 KB/s], Decompressed: 8174
Downloaded: 8220 file(s) [attempted 8220/8459 = 97%, 99 KB/s], Decompressed: 8215
Downloaded: 8256 file(s) [attempted 8256/8459 = 97%, 137 KB/s], Decompressed: 8253
Downloaded: 8296 file(s) [attempted 8296/8459 = 98%, 93 KB/s], Decompressed: 8290
Downloaded: 8335 file(s) [attempted 8335/8459 = 98%, 82 KB/s], Decompressed: 8328
Downloaded: 8373 file(s) [attempted 8373/8459 = 98%, 771 KB/s], Decompressed: 8369
Downloaded: 8412 file(s) [attempted 8412/8459 = 99%, 974 KB/s], Decompressed: 8407
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 87 KB/s], Decompressed: 8444
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 87 KB/s], Decompressed: 8455

lean_checker exit 0 duration 5m 20s · created 6/18/2026, 1:51:01 PM

lake build

ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (240s)
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) [0x71dad6dc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x71dad6dbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x71dad6dbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x71dad6cf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x71dad6cf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x71dad6dcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x71dad6c32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x71dad6c32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x71dad6c33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x71dad6c341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x71dad6dc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x71dad6a15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x71dad6dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x71dad6dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x71dad6d9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x71dad6a15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x71dad1e22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x71dad1c0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x71dad1769a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x71dad1769f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x71dace64524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x71dace645305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5de27bfb08da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (7.9s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.3s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (35s)
✔ [3414/3416] Built Iut.Basic (2.5s)
✔ [3415/3416] Built Iut (2.5s)
Build completed successfully (3416 jobs).

warning: 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 3s · created 6/18/2026, 1:51:01 PM

lake build :blueprint

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

semantic_extract exit 0 duration 2h 56m · created 6/18/2026, 1:51:01 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)

apx-semantic-phase	{"duration_ms":5,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":9,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":328368,"module_count":1,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":56,"module_count":1,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"ok":true,"payload_bytes":738,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"ok":true,"payload_bytes":738,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":81,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":332937,"module_count":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":56,"module_count":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"ok":true,"payload_bytes":1330,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"ok":true,"payload_bytes":1330,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":97,"diagnostic_count":15,"duration_ms":7530,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":330199,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":97,"diagnostic_count":15,"duration_ms":393,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"ok":true,"payload_bytes":3002937,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":2,"ok":true,"payload_bytes":3002937,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":1888,"diagnostic_count":116,"duration_ms":1534050,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":346976,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":1888,"diagnostic_count":116,"duration_ms":7425,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"ok":true,"payload_bytes":66851125,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":48,"module_index":3,"ok":true,"payload_bytes":66851125,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":7706,"diagnostic_count":3080,"duration_ms":6091253,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":502588,"module_count":1,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":7706,"diagnostic_count":3080,"duration_ms":39094,"module_count":1,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"ok":true,"payload_bytes":460841742,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":495,"module_index":4,"ok":true,"payload_bytes":460841742,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":152,"diagnostic_count":23,"duration_ms":25038,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":916383,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":152,"diagnostic_count":23,"duration_ms":1094,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":5,"ok":true,"payload_bytes":2722873,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":4,"module_index":5,"ok":true,"payload_bytes":2722873,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":9844,"diagnostic_count":3234,"duration_ms":57650,"module_count":6,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":534535836,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1283,"ok":true,"payload_bytes":534535836,"phase":"lean_json_write"}

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"core_compile","duration_ms":3386}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":353,"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":3448,"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 5e463795818150aa4211cd980cc51c16a0f42edef395609205431c2db2b498db
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":10546498,"ok":true}