Verification run

Run 362

promachina/iut-lean branch master triggered via github_backfill

succeeded commit c7cfbdfd1126 toolchain lean-v4-30-0 prover lean took 3h 31m · finished 3w 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-554-source
exit_code=Some(0) duration_ms=2772
stderr:
Cloning into '/var/lib/apodeixis/repos/job-554-source'...


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


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


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

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 c7cfbdf Back arbitrary q exact theta by hull obligations

Resolved source revision: c7cfbdfd1126573d6257b09294829e409f3a8107

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=c7cfbdfd1126573d6257b09294829e409f3a8107 provenance={"branch":"master","checked_out_revision":"c7cfbdfd1126573d6257b09294829e409f3a8107","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"c7cfbdfd1126573d6257b09294829e409f3a8107","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: 24/31 module hit(s), 7 miss(es)
Lean semantic module cache: stable superset runner maps 7 missing module(s) to 6 weighted target group(s) capped at target weight 32, but will attempt them in one Lean invocation
Lean semantic module cache: trying stable superset runner for 7 missing module(s) with 31 imported module candidate(s)
Lean semantic module cache: stable superset runner target set maps to 6 weighted batch(es), but will run in one Lean invocation so the superset import is paid once
Lean semantic module cache: checkpointed 1 module fragment row(s) from stable superset runner
Lean semantic module cache: stable superset runner extracted 7 missing module(s) in one Lean invocation
Lean semantic module cache: extracted 7 missing module(s) in bounded batches; wrote merged semantic response

$ lake exe cache get
exit_code=Some(0) duration_ms=49847
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: 16 file(s) [attempted 16/8459 = 0%, 2 KB/s], Decompressed: 14
Downloaded: 41 file(s) [attempted 41/8459 = 0%, 13 KB/s], Decompressed: 37
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 447 KB/s], Decompressed: 62
Downloaded: 93 file(s) [attempted 93/8459 = 1%, 493 KB/s], Decompressed: 92
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 245 KB/s], Decompressed: 121
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 73 KB/s], Decompressed: 155
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 40 KB/s], Decompressed: 192
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 576 KB/s], Decompressed: 227
Downloaded: 264 file(s) [attempted 264/8459 = 3%, 754 KB/s], Decompressed: 261
Downloaded: 306 file(s) [attempted 306/8459 = 3%, 432 KB/s], Decompressed: 302
Downloaded: 350 file(s) [attempted 350/8459 = 4%, 281 KB/s], Decompressed: 347
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 77 KB/s], Decompressed: 384
Downloaded: 425 file(s) [attempted 425/8459 = 5%, 116 KB/s], Decompressed: 412
Downloaded: 460 file(s) [attempted 460/8459 = 5%, 76 KB/s], Decompressed: 453
Downloaded: 498 file(s) [attempted 498/8459 = 5%, 183 KB/s], Decompressed: 494
Downloaded: 536 file(s) [attempted 536/8459 = 6%, 280 KB/s], Decompressed: 532
Downloaded: 571 file(s) [attempted 571/8459 = 6%, 96 KB/s], Decompressed: 566
Downloaded: 610 file(s) [attempted 610/8459 = 7%, 143 KB/s], Decompressed: 604
Downloaded: 651 file(s) [attempted 651/8459 = 7%, 123 KB/s], Decompressed: 648
Downloaded: 693 file(s) [attempted 693/8459 = 8%, 102 KB/s], Decompressed: 689
Downloaded: 730 file(s) [attempted 730/8459 = 8%, 115 KB/s], Decompressed: 727
Downloaded: 765 file(s) [attempted 765/8459 = 9%, 204 KB/s], Decompressed: 754
Downloaded: 806 file(s) [attempted 806/8459 = 9%, 175 KB/s], Decompressed: 802
Downloaded: 847 file(s) [attempted 847/8459 = 10%, 57 KB/s], Decompressed: 843
Downloaded: 884 file(s) [attempted 884/8459 = 10%, 41 KB/s], Decompressed: 881
Downloaded: 916 file(s) [attempted 916/8459 = 10%, 388 KB/s], Decompressed: 912
Downloaded: 960 file(s) [attempted 960/8459 = 11%, 216 KB/s], Decompressed: 956
Downloaded: 1004 file(s) [attempted 1004/8459 = 11%, 493 KB/s], Decompressed: 1001
Downloaded: 1047 file(s) [attempted 1047/8459 = 12%, 572 KB/s], Decompressed: 1035
Downloaded: 1083 file(s) [attempted 1083/8459 = 12%, 74 KB/s], Decompressed: 1076
Downloaded: 1117 file(s) [attempted 1117/8459 = 13%, 238 KB/s], Decompressed: 1114
Downloaded: 1159 file(s) [attempted 1159/8459 = 13%, 254 KB/s], Decompressed: 1155
Downloaded: 1203 file(s) [attempted 1203/8459 = 14%, 2312 KB/s], Decompressed: 1199
Downloaded: 1237 file(s) [attempted 1237/8459 = 14%, 91 KB/s], Decompressed: 1230
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 261 KB/s], Decompressed: 1268
Downloaded: 1314 file(s) [attempted 1314/8459 = 15%, 44 KB/s], Decompressed: 1309
Downloaded: 1353 file(s) [attempted 1353/8459 = 15%, 339 KB/s], Decompressed: 1350
Downloaded: 1398 file(s) [attempted 1398/8459 = 16%, 204 KB/s], Decompressed: 1384
Downloaded: 1425 file(s) [attempted 1425/8459 = 16%, 617 KB/s], Decompressed: 1415
Downloaded: 1464 file(s) [attempted 1464/8459 = 17%, 474 KB/s], Decompressed: 1459
Downloaded: 1507 file(s) [attempted 1507/8459 = 17%, 24 KB/s], Decompressed: 1504
Downloaded: 1548 file(s) [attempted 1548/8459 = 18%, 165 KB/s], Decompressed: 1542
Downloaded: 1583 file(s) [attempted 1583/8459 = 18%, 948 KB/s], Decompressed: 1572
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 328 KB/s], Decompressed: 1613
Downloaded: 1665 file(s) [attempted 1665/8459 = 19%, 303 KB/s], Decompressed: 1661
Downloaded: 1704 file(s) [attempted 1704/8459 = 20%, 145 KB/s], Decompressed: 1696
Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 955 KB/s], Decompressed: 1733
Downloaded: 1781 file(s) [attempted 1781/8459 = 21%, 25 KB/s], Decompressed: 1771
Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 207 KB/s], Decompressed: 1812
Downloaded: 1861 file(s) [attempted 1861/8459 = 22%, 115 KB/s], Decompressed: 1856
Downloaded: 1897 file(s) [attempted 1897/8459 = 22%, 444 KB/s], Decompressed: 1894
Downloaded: 1939 file(s) [attempted 1939/8459 = 22%, 1325 KB/s], Decompressed: 1928
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 836 KB/s], Decompressed: 1963
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 126 KB/s], Decompressed: 2007
Downloaded: 2052 file(s) [attempted 2052/8459 = 24%, 88 KB/s], Decompressed: 2045
Downloaded: 2089 file(s) [attempted 2089/8459 = 24%, 94 KB/s], Decompressed: 2082
Downloaded: 2130 file(s) [attempted 2130/8459 = 25%, 103 KB/s], Decompressed: 2123
Downloaded: 2158 file(s) [attempted 2158/8459 = 25%, 406 KB/s], Decompressed: 2154
Downloaded: 2203 file(s) [attempted 2203/8459 = 26%, 491 KB/s], Decompressed: 2199
Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 191 KB/s], Decompressed: 2240
Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 292 KB/s], Decompressed: 2271
Downloaded: 2308 file(s) [attempted 2308/8459 = 27%, 133 KB/s], Decompressed: 2301
Downloaded: 2353 file(s) [attempted 2353/8459 = 27%, 844 KB/s], Decompressed: 2349
Downloaded: 2390 file(s) [attempted 2390/8459 = 28%, 457 KB/s], Decompressed: 2387
Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 220 KB/s], Decompressed: 2425
Downloaded: 2466 file(s) [attempted 2466/8459 = 29%, 231 KB/s], Decompressed: 2455
Downloaded: 2503 file(s) [attempted 2503/8459 = 29%, 346 KB/s], Decompressed: 2500
Downloaded: 2548 file(s) [attempted 2548/8459 = 30%, 166 KB/s], Decompressed: 2544
Downloaded: 2585 file(s) [attempted 2585/8459 = 30%, 60 KB/s], Decompressed: 2576
Downloaded: 2623 file(s) [attempted 2623/8459 = 31%, 238 KB/s], Decompressed: 2616
Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 192 KB/s], Decompressed: 2654
Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 230 KB/s], Decompressed: 2698
Downloaded: 2746 file(s) [attempted 2746/8459 = 32%, 43 KB/s], Decompressed: 2743
Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 460 KB/s], Decompressed: 2780
Downloaded: 2822 file(s) [attempted 2822/8459 = 33%, 80 KB/s], Decompressed: 2815
Downloaded: 2859 file(s) [attempted 2859/8459 = 33%, 496 KB/s], Decompressed: 2856
Downloaded: 2904 file(s) [attempted 2904/8459 = 34%, 119 KB/s], Decompressed: 2900
Downloaded: 2941 file(s) [attempted 2941/8459 = 34%, 779 KB/s], Decompressed: 2935
Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 540 KB/s], Decompressed: 2972
Downloaded: 3020 file(s) [attempted 3020/8459 = 35%, 27 KB/s], Decompressed: 3017
Downloaded: 3054 file(s) [attempted 3054/8459 = 36%, 29 KB/s], Decompressed: 3051
Downloaded: 3099 file(s) [attempted 3099/8459 = 36%, 174 KB/s], Decompressed: 3092
Downloaded: 3140 file(s) [attempted 3140/8459 = 37%, 49 KB/s], Decompressed: 3136
Downloaded: 3177 file(s) [attempted 3177/8459 = 37%, 165 KB/s], Decompressed: 3174
Downloaded: 3213 file(s) [attempted 3213/8459 = 37%, 116 KB/s], Decompressed: 3208
Downloaded: 3254 file(s) [attempted 3254/8459 = 38%, 1351 KB/s], Decompressed: 3249
Downloaded: 3292 file(s) [attempted 3292/8459 = 38%, 169 KB/s], Decompressed: 3284
Downloaded: 3328 file(s) [attempted 3328/8459 = 39%, 163 KB/s], Decompressed: 3325
Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 450 KB/s], Decompressed: 3359
Downloaded: 3403 file(s) [attempted 3403/8459 = 40%, 411 KB/s], Decompressed: 3393
Downloaded: 3444 file(s) [attempted 3444/8459 = 40%, 252 KB/s], Decompressed: 3441
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 234 KB/s], Decompressed: 3475
Downloaded: 3521 file(s) [attempted 3521/8459 = 41%, 230 KB/s], Decompressed: 3513
Downloaded: 3557 file(s) [attempted 3557/8459 = 42%, 186 KB/s], Decompressed: 3554
Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 71 KB/s], Decompressed: 3592
Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 189 KB/s], Decompressed: 3636
Downloaded: 3678 file(s) [attempted 3678/8459 = 43%, 71 KB/s], Decompressed: 3670
Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 245 KB/s], Decompressed: 3708
Downloaded: 3756 file(s) [attempted 3756/8459 = 44%, 861 KB/s], Decompressed: 3749
Downloaded: 3794 file(s) [attempted 3794/8459 = 44%, 601 KB/s], Decompressed: 3790
Downloaded: 3835 file(s) [attempted 3835/8459 = 45%, 118 KB/s], Decompressed: 3831
Downloaded: 3872 file(s) [attempted 3872/8459 = 45%, 246 KB/s], Decompressed: 3869
Downloaded: 3907 file(s) [attempted 3907/8459 = 46%, 80 KB/s], Decompressed: 3905
Downloaded: 3948 file(s) [attempted 3948/8459 = 46%, 210 KB/s], Decompressed: 3941
Downloaded: 3985 file(s) [attempted 3985/8459 = 47%, 47 KB/s], Decompressed: 3978
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 1329 KB/s], Decompressed: 4013
Downloaded: 4054 file(s) [attempted 4054/8459 = 47%, 1425 KB/s], Decompressed: 4050
Downloaded: 4093 file(s) [attempted 4093/8459 = 48%, 1375 KB/s], Decompressed: 4088
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 583 KB/s], Decompressed: 4129
Downloaded: 4173 file(s) [attempted 4173/8459 = 49%, 276 KB/s], Decompressed: 4160
Downloaded: 4210 file(s) [attempted 4210/8459 = 49%, 54 KB/s], Decompressed: 4204
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 143 KB/s], Decompressed: 4249
Downloaded: 4291 file(s) [attempted 4291/8459 = 50%, 104 KB/s], Decompressed: 4286
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 50 KB/s], Decompressed: 4321
Downloaded: 4368 file(s) [attempted 4368/8459 = 51%, 412 KB/s], Decompressed: 4365
Downloaded: 4403 file(s) [attempted 4403/8459 = 52%, 197 KB/s], Decompressed: 4399
Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 528 KB/s], Decompressed: 4437
Downloaded: 4481 file(s) [attempted 4481/8459 = 52%, 378 KB/s], Decompressed: 4478
Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 448 KB/s], Decompressed: 4516
Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 459 KB/s], Decompressed: 4550
Downloaded: 4594 file(s) [attempted 4594/8459 = 54%, 38 KB/s], Decompressed: 4591
Downloaded: 4635 file(s) [attempted 4635/8459 = 54%, 1059 KB/s], Decompressed: 4629
Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 140 KB/s], Decompressed: 4673
Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 196 KB/s], Decompressed: 4700
Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 262 KB/s], Decompressed: 4742
Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 339 KB/s], Decompressed: 4786
Downloaded: 4827 file(s) [attempted 4827/8459 = 57%, 72 KB/s], Decompressed: 4820
Downloaded: 4865 file(s) [attempted 4865/8459 = 57%, 343 KB/s], Decompressed: 4861
Downloaded: 4902 file(s) [attempted 4902/8459 = 57%, 566 KB/s], Decompressed: 4896
Downloaded: 4943 file(s) [attempted 4943/8459 = 58%, 486 KB/s], Decompressed: 4940
Downloaded: 4988 file(s) [attempted 4988/8459 = 58%, 105 KB/s], Decompressed: 4981
Downloaded: 5028 file(s) [attempted 5028/8459 = 59%, 220 KB/s], Decompressed: 5015
Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 52 KB/s], Decompressed: 5053
Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 136 KB/s], Decompressed: 5094
Downloaded: 5143 file(s) [attempted 5143/8459 = 60%, 161 KB/s], Decompressed: 5135
Downloaded: 5183 file(s) [attempted 5183/8459 = 61%, 68 KB/s], Decompressed: 5180
Downloaded: 5221 file(s) [attempted 5221/8459 = 61%, 119 KB/s], Decompressed: 5210
Downloaded: 5249 file(s) [attempted 5249/8459 = 62%, 510 KB/s], Decompressed: 5245
Downloaded: 5293 file(s) [attempted 5293/8459 = 62%, 69 KB/s], Decompressed: 5289
Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 187 KB/s], Decompressed: 5330
Downloaded: 5375 file(s) [attempted 5375/8459 = 63%, 320 KB/s], Decompressed: 5364
Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 301 KB/s], Decompressed: 5399
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 961 KB/s], Decompressed: 5440
Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 266 KB/s], Decompressed: 5481
Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 922 KB/s], Decompressed: 5525
Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 298 KB/s], Decompressed: 5549
Downloaded: 5597 file(s) [attempted 5597/8459 = 66%, 82 KB/s], Decompressed: 5594
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 28 KB/s], Decompressed: 5638
Downloaded: 5686 file(s) [attempted 5686/8459 = 67%, 246 KB/s], Decompressed: 5683
Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 287 KB/s], Decompressed: 5724
Downloaded: 5758 file(s) [attempted 5758/8459 = 68%, 359 KB/s], Decompressed: 5751
Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 405 KB/s], Decompressed: 5789
Downloaded: 5840 file(s) [attempted 5840/8459 = 69%, 220 KB/s], Decompressed: 5837
Downloaded: 5885 file(s) [attempted 5885/8459 = 69%, 90 KB/s], Decompressed: 5881
Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 697 KB/s], Decompressed: 5921
Downloaded: 5953 file(s) [attempted 5953/8459 = 70%, 84 KB/s], Decompressed: 5946
Downloaded: 5994 file(s) [attempted 5994/8459 = 70%, 52 KB/s], Decompressed: 5991
Downloaded: 6039 file(s) [attempted 6039/8459 = 71%, 129 KB/s], Decompressed: 6035
Downloaded: 6080 file(s) [attempted 6080/8459 = 71%, 152 KB/s], Decompressed: 6069
Downloaded: 6109 file(s) [attempted 6109/8459 = 72%, 119 KB/s], Decompressed: 6097
Downloaded: 6147 file(s) [attempted 6147/8459 = 72%, 355 KB/s], Decompressed: 6141
Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 200 KB/s], Decompressed: 6186
Downloaded: 6234 file(s) [attempted 6234/8459 = 73%, 641 KB/s], Decompressed: 6220
Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 91 KB/s], Decompressed: 6254
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 693 KB/s], Decompressed: 6288
Downloaded: 6340 file(s) [attempted 6340/8459 = 74%, 54 KB/s], Decompressed: 6336
Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 28 KB/s], Decompressed: 6374
Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 276 KB/s], Decompressed: 6408
Downloaded: 6450 file(s) [attempted 6450/8459 = 76%, 227 KB/s], Decompressed: 6446
Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 1236 KB/s], Decompressed: 6490
Downloaded: 6537 file(s) [attempted 6537/8459 = 77%, 593 KB/s], Decompressed: 6525
Downloaded: 6566 file(s) [attempted 6566/8459 = 77%, 100 KB/s], Decompressed: 6555
Downloaded: 6603 file(s) [attempted 6603/8459 = 78%, 204 KB/s], Decompressed: 6596
Downloaded: 6645 file(s) [attempted 6645/8459 = 78%, 124 KB/s], Decompressed: 6641
Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 233 KB/s], Decompressed: 6682
Downloaded: 6723 file(s) [attempted 6723/8459 = 79%, 165 KB/s], Decompressed: 6716
Downloaded: 6761 file(s) [attempted 6761/8459 = 79%, 338 KB/s], Decompressed: 6757
Downloaded: 6802 file(s) [attempted 6802/8459 = 80%, 23 KB/s], Decompressed: 6795
Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 55 KB/s], Decompressed: 6833
Downloaded: 6877 file(s) [attempted 6877/8459 = 81%, 355 KB/s], Decompressed: 6874
Downloaded: 6915 file(s) [attempted 6915/8459 = 81%, 410 KB/s], Decompressed: 6908
Downloaded: 6952 file(s) [attempted 6952/8459 = 82%, 378 KB/s], Decompressed: 6949
Downloaded: 6993 file(s) [attempted 6993/8459 = 82%, 235 KB/s], Decompressed: 6987
Downloaded: 7031 file(s) [attempted 7031/8459 = 83%, 1741 KB/s], Decompressed: 7024
Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 748 KB/s], Decompressed: 7065
Downloaded: 7110 file(s) [attempted 7110/8459 = 84%, 697 KB/s], Decompressed: 7103
Downloaded: 7149 file(s) [attempted 7149/8459 = 84%, 454 KB/s], Decompressed: 7144
Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 1227 KB/s], Decompressed: 7182
Downloaded: 7226 file(s) [attempted 7226/8459 = 85%, 150 KB/s], Decompressed: 7223
Downloaded: 7264 file(s) [attempted 7264/8459 = 85%, 116 KB/s], Decompressed: 7260
Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 82 KB/s], Decompressed: 7301
Downloaded: 7343 file(s) [attempted 7343/8459 = 86%, 553 KB/s], Decompressed: 7336
Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 182 KB/s], Decompressed: 7377
Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 962 KB/s], Decompressed: 7414
Downloaded: 7459 file(s) [attempted 7459/8459 = 88%, 85 KB/s], Decompressed: 7452
Downloaded: 7503 file(s) [attempted 7503/8459 = 88%, 461 KB/s], Decompressed: 7497
Downloaded: 7544 file(s) [attempted 7544/8459 = 89%, 190 KB/s], Decompressed: 7541
Downloaded: 7580 file(s) [attempted 7580/8459 = 89%, 218 KB/s], Decompressed: 7575
Downloaded: 7620 file(s) [attempted 7620/8459 = 90%, 153 KB/s], Decompressed: 7616
Downloaded: 7658 file(s) [attempted 7658/8459 = 90%, 453 KB/s], Decompressed: 7654
Downloaded: 7696 file(s) [attempted 7696/8459 = 90%, 108 KB/s], Decompressed: 7692
Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 99 KB/s], Decompressed: 7726
Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 310 KB/s], Decompressed: 7763
Downloaded: 7810 file(s) [attempted 7810/8459 = 92%, 171 KB/s], Decompressed: 7801
Downloaded: 7850 file(s) [attempted 7850/8459 = 92%, 306 KB/s], Decompressed: 7842
Downloaded: 7884 file(s) [attempted 7884/8459 = 93%, 86 KB/s], Decompressed: 7876
Downloaded: 7921 file(s) [attempted 7921/8459 = 93%, 31 KB/s], Decompressed: 7917
Downloaded: 7962 file(s) [attempted 7962/8459 = 94%, 179 KB/s], Decompressed: 7948
Downloaded: 8000 file(s) [attempted 8000/8459 = 94%, 304 KB/s], Decompressed: 7996
Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 424 KB/s], Decompressed: 8041
Downloaded: 8083 file(s) [attempted 8083/8459 = 95%, 110 KB/s], Decompressed: 8075
Downloaded: 8123 file(s) [attempted 8123/8459 = 96%, 472 KB/s], Decompressed: 8119
Downloaded: 8164 file(s) [attempted 8164/8459 = 96%, 23 KB/s], Decompressed: 8157
Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 121 KB/s], Decompressed: 8195
Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 102 KB/s], Decompressed: 8239
Downloaded: 8284 file(s) [attempted 8284/8459 = 97%, 527 KB/s], Decompressed: 8278
Downloaded: 8321 file(s) [attempted 8321/8459 = 98%, 374 KB/s], Decompressed: 8311
Downloaded: 8359 file(s) [attempted 8359/8459 = 98%, 131 KB/s], Decompressed: 8352
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 317 KB/s], Decompressed: 8390
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 105 KB/s], Decompressed: 8434
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 105 KB/s], Decompressed: 8448


$ lake build
exit_code=Some(0) duration_ms=314839
stdout:
✔ [3409/3416] Built Iut.Stage1.IUTStage1StepXI (73s)
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (154s)
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) [0x7cd9b47c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7cd9b47bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7cd9b47bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7cd9b46f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7cd9b46f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7cd9b47caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7cd9b4632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7cd9b4632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7cd9b4633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7cd9b46341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7cd9b47c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7cd9b4415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7cd9b47c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7cd9b47c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7cd9b479b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7cd9b4415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7cd9af822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7cd9af60cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7cd9af169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7cd9af169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7cd9ac04524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7cd9ac045305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x57897b4128da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (20s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.3s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (36s)
✔ [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=3192
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=12032427
stdout:
apx-semantic-phase	{"duration_ms":4,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":6,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":331759,"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":0,"module_count":1,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":422,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":422,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":49,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":337087,"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":1,"module_count":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1014,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1014,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":97,"diagnostic_count":15,"duration_ms":7591,"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":334546,"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":7,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1216278,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1216278,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":1892,"diagnostic_count":116,"duration_ms":1560631,"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":341132,"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":1892,"diagnostic_count":116,"duration_ms":89,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":43332215,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":29,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":43332215,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":7804,"diagnostic_count":3119,"duration_ms":6189646,"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":428138,"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":7804,"diagnostic_count":3119,"duration_ms":547,"module_count":1,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":266651932,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":175,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":266651932,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":152,"diagnostic_count":23,"duration_ms":19977,"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":734437,"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":111,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1647482,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":6,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1647482,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":2726,"diagnostic_count":896,"duration_ms":949627,"module_name":"Iut.Stage1.IUTStage1StepXI","module_path":"Iut/Stage1/IUTStage1StepXI.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":778271,"module_count":1,"module_name":"Iut.Stage1.IUTStage1StepXI","module_path":"Iut/Stage1/IUTStage1StepXI.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":2726,"diagnostic_count":896,"duration_ms":133,"module_count":1,"module_name":"Iut.Stage1.IUTStage1StepXI","module_path":"Iut/Stage1/IUTStage1StepXI.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":6,"module_payload_kind":"fragment","ok":true,"payload_bytes":33395505,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":23,"module_index":6,"module_payload_kind":"fragment","ok":true,"payload_bytes":33395505,"phase":"lean_module_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":3338}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":877,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3536,"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 e5c6a7f9c7c521013353176634e2468fe4ab1dee3cb3be167d353e08621c37b7
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":12023838,"ok":true}

Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

git_clone exit 0 duration 3s · created 6/22/2026, 8:18:20 PM

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

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

git_checkout exit 128 duration 4 ms · created 6/22/2026, 8:18:20 PM

git checkout c7cfbdfd1126573d6257b09294829e409f3a8107

fatal: reference is not a tree: c7cfbdfd1126573d6257b09294829e409f3a8107

git_checkout exit 0 duration 1s · created 6/22/2026, 8:18:20 PM

git fetch --depth 1 origin c7cfbdfd1126573d6257b09294829e409f3a8107

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

git_checkout exit 0 duration 142 ms · created 6/22/2026, 8:18:20 PM

git checkout c7cfbdfd1126573d6257b09294829e409f3a8107 (after fetch)

Note: switching to 'c7cfbdfd1126573d6257b09294829e409f3a8107'.

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 c7cfbdf Back arbitrary q exact theta by hull obligations

lake_cache exit 0 duration 50s · created 6/22/2026, 8:18:20 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%, 10 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 2 KB/s], Decompressed: 14
Downloaded: 41 file(s) [attempted 41/8459 = 0%, 13 KB/s], Decompressed: 37
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 447 KB/s], Decompressed: 62
Downloaded: 93 file(s) [attempted 93/8459 = 1%, 493 KB/s], Decompressed: 92
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 245 KB/s], Decompressed: 121
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 73 KB/s], Decompressed: 155
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 40 KB/s], Decompressed: 192
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 576 KB/s], Decompressed: 227
Downloaded: 264 file(s) [attempted 264/8459 = 3%, 754 KB/s], Decompressed: 261
Downloaded: 306 file(s) [attempted 306/8459 = 3%, 432 KB/s], Decompressed: 302
Downloaded: 350 file(s) [attempted 350/8459 = 4%, 281 KB/s], Decompressed: 347
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 77 KB/s], Decompressed: 384
Downloaded: 425 file(s) [attempted 425/8459 = 5%, 116 KB/s], Decompressed: 412
Downloaded: 460 file(s) [attempted 460/8459 = 5%, 76 KB/s], Decompressed: 453
Downloaded: 498 file(s) [attempted 498/8459 = 5%, 183 KB/s], Decompressed: 494
Downloaded: 536 file(s) [attempted 536/8459 = 6%, 280 KB/s], Decompressed: 532
Downloaded: 571 file(s) [attempted 571/8459 = 6%, 96 KB/s], Decompressed: 566
Downloaded: 610 file(s) [attempted 610/8459 = 7%, 143 KB/s], Decompressed: 604
Downloaded: 651 file(s) [attempted 651/8459 = 7%, 123 KB/s], Decompressed: 648
Downloaded: 693 file(s) [attempted 693/8459 = 8%, 102 KB/s], Decompressed: 689
Downloaded: 730 file(s) [attempted 730/8459 = 8%, 115 KB/s], Decompressed: 727
Downloaded: 765 file(s) [attempted 765/8459 = 9%, 204 KB/s], Decompressed: 754
Downloaded: 806 file(s) [attempted 806/8459 = 9%, 175 KB/s], Decompressed: 802
Downloaded: 847 file(s) [attempted 847/8459 = 10%, 57 KB/s], Decompressed: 843
Downloaded: 884 file(s) [attempted 884/8459 = 10%, 41 KB/s], Decompressed: 881
Downloaded: 916 file(s) [attempted 916/8459 = 10%, 388 KB/s], Decompressed: 912
Downloaded: 960 file(s) [attempted 960/8459 = 11%, 216 KB/s], Decompressed: 956
Downloaded: 1004 file(s) [attempted 1004/8459 = 11%, 493 KB/s], Decompressed: 1001
Downloaded: 1047 file(s) [attempted 1047/8459 = 12%, 572 KB/s], Decompressed: 1035
Downloaded: 1083 file(s) [attempted 1083/8459 = 12%, 74 KB/s], Decompressed: 1076
Downloaded: 1117 file(s) [attempted 1117/8459 = 13%, 238 KB/s], Decompressed: 1114
Downloaded: 1159 file(s) [attempted 1159/8459 = 13%, 254 KB/s], Decompressed: 1155
Downloaded: 1203 file(s) [attempted 1203/8459 = 14%, 2312 KB/s], Decompressed: 1199
Downloaded: 1237 file(s) [attempted 1237/8459 = 14%, 91 KB/s], Decompressed: 1230
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 261 KB/s], Decompressed: 1268
Downloaded: 1314 file(s) [attempted 1314/8459 = 15%, 44 KB/s], Decompressed: 1309
Downloaded: 1353 file(s) [attempted 1353/8459 = 15%, 339 KB/s], Decompressed: 1350
Downloaded: 1398 file(s) [attempted 1398/8459 = 16%, 204 KB/s], Decompressed: 1384
Downloaded: 1425 file(s) [attempted 1425/8459 = 16%, 617 KB/s], Decompressed: 1415
Downloaded: 1464 file(s) [attempted 1464/8459 = 17%, 474 KB/s], Decompressed: 1459
Downloaded: 1507 file(s) [attempted 1507/8459 = 17%, 24 KB/s], Decompressed: 1504
Downloaded: 1548 file(s) [attempted 1548/8459 = 18%, 165 KB/s], Decompressed: 1542
Downloaded: 1583 file(s) [attempted 1583/8459 = 18%, 948 KB/s], Decompressed: 1572
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 328 KB/s], Decompressed: 1613
Downloaded: 1665 file(s) [attempted 1665/8459 = 19%, 303 KB/s], Decompressed: 1661
Downloaded: 1704 file(s) [attempted 1704/8459 = 20%, 145 KB/s], Decompressed: 1696
Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 955 KB/s], Decompressed: 1733
Downloaded: 1781 file(s) [attempted 1781/8459 = 21%, 25 KB/s], Decompressed: 1771
Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 207 KB/s], Decompressed: 1812
Downloaded: 1861 file(s) [attempted 1861/8459 = 22%, 115 KB/s], Decompressed: 1856
Downloaded: 1897 file(s) [attempted 1897/8459 = 22%, 444 KB/s], Decompressed: 1894
Downloaded: 1939 file(s) [attempted 1939/8459 = 22%, 1325 KB/s], Decompressed: 1928
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 836 KB/s], Decompressed: 1963
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 126 KB/s], Decompressed: 2007
Downloaded: 2052 file(s) [attempted 2052/8459 = 24%, 88 KB/s], Decompressed: 2045
Downloaded: 2089 file(s) [attempted 2089/8459 = 24%, 94 KB/s], Decompressed: 2082
Downloaded: 2130 file(s) [attempted 2130/8459 = 25%, 103 KB/s], Decompressed: 2123
Downloaded: 2158 file(s) [attempted 2158/8459 = 25%, 406 KB/s], Decompressed: 2154
Downloaded: 2203 file(s) [attempted 2203/8459 = 26%, 491 KB/s], Decompressed: 2199
Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 191 KB/s], Decompressed: 2240
Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 292 KB/s], Decompressed: 2271
Downloaded: 2308 file(s) [attempted 2308/8459 = 27%, 133 KB/s], Decompressed: 2301
Downloaded: 2353 file(s) [attempted 2353/8459 = 27%, 844 KB/s], Decompressed: 2349
Downloaded: 2390 file(s) [attempted 2390/8459 = 28%, 457 KB/s], Decompressed: 2387
Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 220 KB/s], Decompressed: 2425
Downloaded: 2466 file(s) [attempted 2466/8459 = 29%, 231 KB/s], Decompressed: 2455
Downloaded: 2503 file(s) [attempted 2503/8459 = 29%, 346 KB/s], Decompressed: 2500
Downloaded: 2548 file(s) [attempted 2548/8459 = 30%, 166 KB/s], Decompressed: 2544
Downloaded: 2585 file(s) [attempted 2585/8459 = 30%, 60 KB/s], Decompressed: 2576
Downloaded: 2623 file(s) [attempted 2623/8459 = 31%, 238 KB/s], Decompressed: 2616
Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 192 KB/s], Decompressed: 2654
Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 230 KB/s], Decompressed: 2698
Downloaded: 2746 file(s) [attempted 2746/8459 = 32%, 43 KB/s], Decompressed: 2743
Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 460 KB/s], Decompressed: 2780
Downloaded: 2822 file(s) [attempted 2822/8459 = 33%, 80 KB/s], Decompressed: 2815
Downloaded: 2859 file(s) [attempted 2859/8459 = 33%, 496 KB/s], Decompressed: 2856
Downloaded: 2904 file(s) [attempted 2904/8459 = 34%, 119 KB/s], Decompressed: 2900
Downloaded: 2941 file(s) [attempted 2941/8459 = 34%, 779 KB/s], Decompressed: 2935
Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 540 KB/s], Decompressed: 2972
Downloaded: 3020 file(s) [attempted 3020/8459 = 35%, 27 KB/s], Decompressed: 3017
Downloaded: 3054 file(s) [attempted 3054/8459 = 36%, 29 KB/s], Decompressed: 3051
Downloaded: 3099 file(s) [attempted 3099/8459 = 36%, 174 KB/s], Decompressed: 3092
Downloaded: 3140 file(s) [attempted 3140/8459 = 37%, 49 KB/s], Decompressed: 3136
Downloaded: 3177 file(s) [attempted 3177/8459 = 37%, 165 KB/s], Decompressed: 3174
Downloaded: 3213 file(s) [attempted 3213/8459 = 37%, 116 KB/s], Decompressed: 3208
Downloaded: 3254 file(s) [attempted 3254/8459 = 38%, 1351 KB/s], Decompressed: 3249
Downloaded: 3292 file(s) [attempted 3292/8459 = 38%, 169 KB/s], Decompressed: 3284
Downloaded: 3328 file(s) [attempted 3328/8459 = 39%, 163 KB/s], Decompressed: 3325
Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 450 KB/s], Decompressed: 3359
Downloaded: 3403 file(s) [attempted 3403/8459 = 40%, 411 KB/s], Decompressed: 3393
Downloaded: 3444 file(s) [attempted 3444/8459 = 40%, 252 KB/s], Decompressed: 3441
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 234 KB/s], Decompressed: 3475
Downloaded: 3521 file(s) [attempted 3521/8459 = 41%, 230 KB/s], Decompressed: 3513
Downloaded: 3557 file(s) [attempted 3557/8459 = 42%, 186 KB/s], Decompressed: 3554
Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 71 KB/s], Decompressed: 3592
Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 189 KB/s], Decompressed: 3636
Downloaded: 3678 file(s) [attempted 3678/8459 = 43%, 71 KB/s], Decompressed: 3670
Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 245 KB/s], Decompressed: 3708
Downloaded: 3756 file(s) [attempted 3756/8459 = 44%, 861 KB/s], Decompressed: 3749
Downloaded: 3794 file(s) [attempted 3794/8459 = 44%, 601 KB/s], Decompressed: 3790
Downloaded: 3835 file(s) [attempted 3835/8459 = 45%, 118 KB/s], Decompressed: 3831
Downloaded: 3872 file(s) [attempted 3872/8459 = 45%, 246 KB/s], Decompressed: 3869
Downloaded: 3907 file(s) [attempted 3907/8459 = 46%, 80 KB/s], Decompressed: 3905
Downloaded: 3948 file(s) [attempted 3948/8459 = 46%, 210 KB/s], Decompressed: 3941
Downloaded: 3985 file(s) [attempted 3985/8459 = 47%, 47 KB/s], Decompressed: 3978
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 1329 KB/s], Decompressed: 4013
Downloaded: 4054 file(s) [attempted 4054/8459 = 47%, 1425 KB/s], Decompressed: 4050
Downloaded: 4093 file(s) [attempted 4093/8459 = 48%, 1375 KB/s], Decompressed: 4088
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 583 KB/s], Decompressed: 4129
Downloaded: 4173 file(s) [attempted 4173/8459 = 49%, 276 KB/s], Decompressed: 4160
Downloaded: 4210 file(s) [attempted 4210/8459 = 49%, 54 KB/s], Decompressed: 4204
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 143 KB/s], Decompressed: 4249
Downloaded: 4291 file(s) [attempted 4291/8459 = 50%, 104 KB/s], Decompressed: 4286
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 50 KB/s], Decompressed: 4321
Downloaded: 4368 file(s) [attempted 4368/8459 = 51%, 412 KB/s], Decompressed: 4365
Downloaded: 4403 file(s) [attempted 4403/8459 = 52%, 197 KB/s], Decompressed: 4399
Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 528 KB/s], Decompressed: 4437
Downloaded: 4481 file(s) [attempted 4481/8459 = 52%, 378 KB/s], Decompressed: 4478
Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 448 KB/s], Decompressed: 4516
Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 459 KB/s], Decompressed: 4550
Downloaded: 4594 file(s) [attempted 4594/8459 = 54%, 38 KB/s], Decompressed: 4591
Downloaded: 4635 file(s) [attempted 4635/8459 = 54%, 1059 KB/s], Decompressed: 4629
Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 140 KB/s], Decompressed: 4673
Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 196 KB/s], Decompressed: 4700
Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 262 KB/s], Decompressed: 4742
Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 339 KB/s], Decompressed: 4786
Downloaded: 4827 file(s) [attempted 4827/8459 = 57%, 72 KB/s], Decompressed: 4820
Downloaded: 4865 file(s) [attempted 4865/8459 = 57%, 343 KB/s], Decompressed: 4861
Downloaded: 4902 file(s) [attempted 4902/8459 = 57%, 566 KB/s], Decompressed: 4896
Downloaded: 4943 file(s) [attempted 4943/8459 = 58%, 486 KB/s], Decompressed: 4940
Downloaded: 4988 file(s) [attempted 4988/8459 = 58%, 105 KB/s], Decompressed: 4981
Downloaded: 5028 file(s) [attempted 5028/8459 = 59%, 220 KB/s], Decompressed: 5015
Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 52 KB/s], Decompressed: 5053
Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 136 KB/s], Decompressed: 5094
Downloaded: 5143 file(s) [attempted 5143/8459 = 60%, 161 KB/s], Decompressed: 5135
Downloaded: 5183 file(s) [attempted 5183/8459 = 61%, 68 KB/s], Decompressed: 5180
Downloaded: 5221 file(s) [attempted 5221/8459 = 61%, 119 KB/s], Decompressed: 5210
Downloaded: 5249 file(s) [attempted 5249/8459 = 62%, 510 KB/s], Decompressed: 5245
Downloaded: 5293 file(s) [attempted 5293/8459 = 62%, 69 KB/s], Decompressed: 5289
Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 187 KB/s], Decompressed: 5330
Downloaded: 5375 file(s) [attempted 5375/8459 = 63%, 320 KB/s], Decompressed: 5364
Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 301 KB/s], Decompressed: 5399
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 961 KB/s], Decompressed: 5440
Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 266 KB/s], Decompressed: 5481
Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 922 KB/s], Decompressed: 5525
Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 298 KB/s], Decompressed: 5549
Downloaded: 5597 file(s) [attempted 5597/8459 = 66%, 82 KB/s], Decompressed: 5594
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 28 KB/s], Decompressed: 5638
Downloaded: 5686 file(s) [attempted 5686/8459 = 67%, 246 KB/s], Decompressed: 5683
Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 287 KB/s], Decompressed: 5724
Downloaded: 5758 file(s) [attempted 5758/8459 = 68%, 359 KB/s], Decompressed: 5751
Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 405 KB/s], Decompressed: 5789
Downloaded: 5840 file(s) [attempted 5840/8459 = 69%, 220 KB/s], Decompressed: 5837
Downloaded: 5885 file(s) [attempted 5885/8459 = 69%, 90 KB/s], Decompressed: 5881
Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 697 KB/s], Decompressed: 5921
Downloaded: 5953 file(s) [attempted 5953/8459 = 70%, 84 KB/s], Decompressed: 5946
Downloaded: 5994 file(s) [attempted 5994/8459 = 70%, 52 KB/s], Decompressed: 5991
Downloaded: 6039 file(s) [attempted 6039/8459 = 71%, 129 KB/s], Decompressed: 6035
Downloaded: 6080 file(s) [attempted 6080/8459 = 71%, 152 KB/s], Decompressed: 6069
Downloaded: 6109 file(s) [attempted 6109/8459 = 72%, 119 KB/s], Decompressed: 6097
Downloaded: 6147 file(s) [attempted 6147/8459 = 72%, 355 KB/s], Decompressed: 6141
Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 200 KB/s], Decompressed: 6186
Downloaded: 6234 file(s) [attempted 6234/8459 = 73%, 641 KB/s], Decompressed: 6220
Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 91 KB/s], Decompressed: 6254
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 693 KB/s], Decompressed: 6288
Downloaded: 6340 file(s) [attempted 6340/8459 = 74%, 54 KB/s], Decompressed: 6336
Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 28 KB/s], Decompressed: 6374
Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 276 KB/s], Decompressed: 6408
Downloaded: 6450 file(s) [attempted 6450/8459 = 76%, 227 KB/s], Decompressed: 6446
Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 1236 KB/s], Decompressed: 6490
Downloaded: 6537 file(s) [attempted 6537/8459 = 77%, 593 KB/s], Decompressed: 6525
Downloaded: 6566 file(s) [attempted 6566/8459 = 77%, 100 KB/s], Decompressed: 6555
Downloaded: 6603 file(s) [attempted 6603/8459 = 78%, 204 KB/s], Decompressed: 6596
Downloaded: 6645 file(s) [attempted 6645/8459 = 78%, 124 KB/s], Decompressed: 6641
Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 233 KB/s], Decompressed: 6682
Downloaded: 6723 file(s) [attempted 6723/8459 = 79%, 165 KB/s], Decompressed: 6716
Downloaded: 6761 file(s) [attempted 6761/8459 = 79%, 338 KB/s], Decompressed: 6757
Downloaded: 6802 file(s) [attempted 6802/8459 = 80%, 23 KB/s], Decompressed: 6795
Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 55 KB/s], Decompressed: 6833
Downloaded: 6877 file(s) [attempted 6877/8459 = 81%, 355 KB/s], Decompressed: 6874
Downloaded: 6915 file(s) [attempted 6915/8459 = 81%, 410 KB/s], Decompressed: 6908
Downloaded: 6952 file(s) [attempted 6952/8459 = 82%, 378 KB/s], Decompressed: 6949
Downloaded: 6993 file(s) [attempted 6993/8459 = 82%, 235 KB/s], Decompressed: 6987
Downloaded: 7031 file(s) [attempted 7031/8459 = 83%, 1741 KB/s], Decompressed: 7024
Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 748 KB/s], Decompressed: 7065
Downloaded: 7110 file(s) [attempted 7110/8459 = 84%, 697 KB/s], Decompressed: 7103
Downloaded: 7149 file(s) [attempted 7149/8459 = 84%, 454 KB/s], Decompressed: 7144
Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 1227 KB/s], Decompressed: 7182
Downloaded: 7226 file(s) [attempted 7226/8459 = 85%, 150 KB/s], Decompressed: 7223
Downloaded: 7264 file(s) [attempted 7264/8459 = 85%, 116 KB/s], Decompressed: 7260
Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 82 KB/s], Decompressed: 7301
Downloaded: 7343 file(s) [attempted 7343/8459 = 86%, 553 KB/s], Decompressed: 7336
Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 182 KB/s], Decompressed: 7377
Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 962 KB/s], Decompressed: 7414
Downloaded: 7459 file(s) [attempted 7459/8459 = 88%, 85 KB/s], Decompressed: 7452
Downloaded: 7503 file(s) [attempted 7503/8459 = 88%, 461 KB/s], Decompressed: 7497
Downloaded: 7544 file(s) [attempted 7544/8459 = 89%, 190 KB/s], Decompressed: 7541
Downloaded: 7580 file(s) [attempted 7580/8459 = 89%, 218 KB/s], Decompressed: 7575
Downloaded: 7620 file(s) [attempted 7620/8459 = 90%, 153 KB/s], Decompressed: 7616
Downloaded: 7658 file(s) [attempted 7658/8459 = 90%, 453 KB/s], Decompressed: 7654
Downloaded: 7696 file(s) [attempted 7696/8459 = 90%, 108 KB/s], Decompressed: 7692
Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 99 KB/s], Decompressed: 7726
Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 310 KB/s], Decompressed: 7763
Downloaded: 7810 file(s) [attempted 7810/8459 = 92%, 171 KB/s], Decompressed: 7801
Downloaded: 7850 file(s) [attempted 7850/8459 = 92%, 306 KB/s], Decompressed: 7842
Downloaded: 7884 file(s) [attempted 7884/8459 = 93%, 86 KB/s], Decompressed: 7876
Downloaded: 7921 file(s) [attempted 7921/8459 = 93%, 31 KB/s], Decompressed: 7917
Downloaded: 7962 file(s) [attempted 7962/8459 = 94%, 179 KB/s], Decompressed: 7948
Downloaded: 8000 file(s) [attempted 8000/8459 = 94%, 304 KB/s], Decompressed: 7996
Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 424 KB/s], Decompressed: 8041
Downloaded: 8083 file(s) [attempted 8083/8459 = 95%, 110 KB/s], Decompressed: 8075
Downloaded: 8123 file(s) [attempted 8123/8459 = 96%, 472 KB/s], Decompressed: 8119
Downloaded: 8164 file(s) [attempted 8164/8459 = 96%, 23 KB/s], Decompressed: 8157
Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 121 KB/s], Decompressed: 8195
Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 102 KB/s], Decompressed: 8239
Downloaded: 8284 file(s) [attempted 8284/8459 = 97%, 527 KB/s], Decompressed: 8278
Downloaded: 8321 file(s) [attempted 8321/8459 = 98%, 374 KB/s], Decompressed: 8311
Downloaded: 8359 file(s) [attempted 8359/8459 = 98%, 131 KB/s], Decompressed: 8352
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 317 KB/s], Decompressed: 8390
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 105 KB/s], Decompressed: 8434
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 105 KB/s], Decompressed: 8448

lean_checker exit 0 duration 5m 15s · created 6/22/2026, 8:18:20 PM

lake build

✔ [3409/3416] Built Iut.Stage1.IUTStage1StepXI (73s)
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (154s)
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) [0x7cd9b47c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7cd9b47bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7cd9b47bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7cd9b46f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7cd9b46f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7cd9b47caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7cd9b4632923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7cd9b4632b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7cd9b4633827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7cd9b46341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7cd9b47c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7cd9b4415adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7cd9b47c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7cd9b47c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7cd9b479b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7cd9b4415c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7cd9af822638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7cd9af60cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7cd9af169a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7cd9af169f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7cd9ac04524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7cd9ac045305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x57897b4128da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (20s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.3s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (36s)
✔ [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/22/2026, 8:18:20 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 3h 20m · created 6/22/2026, 8:18:20 PM

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

apx-semantic-phase	{"duration_ms":4,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":6,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":331759,"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":0,"module_count":1,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":422,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":422,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":49,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":337087,"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":1,"module_count":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1014,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1014,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":97,"diagnostic_count":15,"duration_ms":7591,"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":334546,"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":7,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1216278,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1216278,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":1892,"diagnostic_count":116,"duration_ms":1560631,"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":341132,"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":1892,"diagnostic_count":116,"duration_ms":89,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":43332215,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":29,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":43332215,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":7804,"diagnostic_count":3119,"duration_ms":6189646,"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":428138,"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":7804,"diagnostic_count":3119,"duration_ms":547,"module_count":1,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":266651932,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":175,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":266651932,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":152,"diagnostic_count":23,"duration_ms":19977,"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":734437,"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":111,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1647482,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":6,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1647482,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":2726,"diagnostic_count":896,"duration_ms":949627,"module_name":"Iut.Stage1.IUTStage1StepXI","module_path":"Iut/Stage1/IUTStage1StepXI.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":778271,"module_count":1,"module_name":"Iut.Stage1.IUTStage1StepXI","module_path":"Iut/Stage1/IUTStage1StepXI.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":2726,"diagnostic_count":896,"duration_ms":133,"module_count":1,"module_name":"Iut.Stage1.IUTStage1StepXI","module_path":"Iut/Stage1/IUTStage1StepXI.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":6,"module_payload_kind":"fragment","ok":true,"payload_bytes":33395505,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":23,"module_index":6,"module_payload_kind":"fragment","ok":true,"payload_bytes":33395505,"phase":"lean_module_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":3338}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":877,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3536,"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 e5c6a7f9c7c521013353176634e2468fe4ab1dee3cb3be167d353e08621c37b7
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":12023838,"ok":true}