Verification run

Run 356

promachina/iut-lean branch master triggered via github_backfill

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


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


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


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

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 6fb8e7c Split local log coordinate image laws

Resolved source revision: 6fb8e7cbe61c5fe4a4156a80558581b359775840

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=6fb8e7cbe61c5fe4a4156a80558581b359775840 provenance={"branch":"master","checked_out_revision":"6fb8e7cbe61c5fe4a4156a80558581b359775840","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"6fb8e7cbe61c5fe4a4156a80558581b359775840","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=52968
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: 15 file(s) [attempted 15/8459 = 0%, 1 KB/s], Decompressed: 12
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 16 KB/s], Decompressed: 35
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 26 KB/s], Decompressed: 62
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 442 KB/s], Decompressed: 83
Downloaded: 121 file(s) [attempted 121/8459 = 1%, 154 KB/s], Decompressed: 114
Downloaded: 151 file(s) [attempted 151/8459 = 1%, 123 KB/s], Decompressed: 141
Downloaded: 189 file(s) [attempted 189/8459 = 2%, 236 KB/s], Decompressed: 182
Downloaded: 223 file(s) [attempted 223/8459 = 2%, 838 KB/s], Decompressed: 216
Downloaded: 261 file(s) [attempted 261/8459 = 3%, 214 KB/s], Decompressed: 258
Downloaded: 295 file(s) [attempted 295/8459 = 3%, 105 KB/s], Decompressed: 288
Downloaded: 336 file(s) [attempted 336/8459 = 3%, 46 KB/s], Decompressed: 333
Downloaded: 374 file(s) [attempted 374/8459 = 4%, 279 KB/s], Decompressed: 367
Downloaded: 412 file(s) [attempted 412/8459 = 4%, 303 KB/s], Decompressed: 408
Downloaded: 453 file(s) [attempted 453/8459 = 5%, 77 KB/s], Decompressed: 449
Downloaded: 490 file(s) [attempted 490/8459 = 5%, 546 KB/s], Decompressed: 487
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 243 KB/s], Decompressed: 521
Downloaded: 566 file(s) [attempted 566/8459 = 6%, 539 KB/s], Decompressed: 559
Downloaded: 610 file(s) [attempted 610/8459 = 7%, 131 KB/s], Decompressed: 603
Downloaded: 655 file(s) [attempted 655/8459 = 7%, 350 KB/s], Decompressed: 651
Downloaded: 696 file(s) [attempted 696/8459 = 8%, 91 KB/s], Decompressed: 686
Downloaded: 734 file(s) [attempted 734/8459 = 8%, 438 KB/s], Decompressed: 723
Downloaded: 770 file(s) [attempted 770/8459 = 9%, 189 KB/s], Decompressed: 761
Downloaded: 806 file(s) [attempted 806/8459 = 9%, 173 KB/s], Decompressed: 771
Downloaded: 847 file(s) [attempted 847/8459 = 10%, 60 KB/s], Decompressed: 771
Downloaded: 888 file(s) [attempted 888/8459 = 10%, 219 KB/s], Decompressed: 884
Downloaded: 925 file(s) [attempted 925/8459 = 10%, 137 KB/s], Decompressed: 919
Downloaded: 967 file(s) [attempted 967/8459 = 11%, 188 KB/s], Decompressed: 963
Downloaded: 1004 file(s) [attempted 1004/8459 = 11%, 514 KB/s], Decompressed: 997
Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 851 KB/s], Decompressed: 1038
Downloaded: 1084 file(s) [attempted 1084/8459 = 12%, 80 KB/s], Decompressed: 1076
Downloaded: 1121 file(s) [attempted 1121/8459 = 13%, 213 KB/s], Decompressed: 1114
Downloaded: 1162 file(s) [attempted 1162/8459 = 13%, 1536 KB/s], Decompressed: 1151
Downloaded: 1199 file(s) [attempted 1199/8459 = 14%, 2434 KB/s], Decompressed: 1186
Downloaded: 1240 file(s) [attempted 1240/8459 = 14%, 90 KB/s], Decompressed: 1186
Downloaded: 1278 file(s) [attempted 1278/8459 = 15%, 297 KB/s], Decompressed: 1189
Downloaded: 1319 file(s) [attempted 1319/8459 = 15%, 131 KB/s], Decompressed: 1316
Downloaded: 1364 file(s) [attempted 1364/8459 = 16%, 205 KB/s], Decompressed: 1360
Downloaded: 1401 file(s) [attempted 1401/8459 = 16%, 62 KB/s], Decompressed: 1394
Downloaded: 1442 file(s) [attempted 1442/8459 = 17%, 304 KB/s], Decompressed: 1435
Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 53 KB/s], Decompressed: 1477
Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 199 KB/s], Decompressed: 1518
Downloaded: 1562 file(s) [attempted 1562/8459 = 18%, 307 KB/s], Decompressed: 1559
Downloaded: 1603 file(s) [attempted 1603/8459 = 18%, 106 KB/s], Decompressed: 1593
Downloaded: 1641 file(s) [attempted 1641/8459 = 19%, 219 KB/s], Decompressed: 1637
Downloaded: 1682 file(s) [attempted 1682/8459 = 19%, 593 KB/s], Decompressed: 1680
Downloaded: 1720 file(s) [attempted 1720/8459 = 20%, 141 KB/s], Decompressed: 1716
Downloaded: 1761 file(s) [attempted 1761/8459 = 20%, 306 KB/s], Decompressed: 1757
Downloaded: 1798 file(s) [attempted 1798/8459 = 21%, 909 KB/s], Decompressed: 1795
Downloaded: 1836 file(s) [attempted 1836/8459 = 21%, 399 KB/s], Decompressed: 1819
Downloaded: 1874 file(s) [attempted 1874/8459 = 22%, 261 KB/s], Decompressed: 1867
Downloaded: 1906 file(s) [attempted 1906/8459 = 22%, 138 KB/s], Decompressed: 1901
Downloaded: 1948 file(s) [attempted 1948/8459 = 23%, 418 KB/s], Decompressed: 1939
Downloaded: 1986 file(s) [attempted 1986/8459 = 23%, 117 KB/s], Decompressed: 1980
Downloaded: 2023 file(s) [attempted 2023/8459 = 23%, 771 KB/s], Decompressed: 2017
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 88 KB/s], Decompressed: 2055
Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 1074 KB/s], Decompressed: 2096
Downloaded: 2142 file(s) [attempted 2142/8459 = 25%, 509 KB/s], Decompressed: 2137
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 107 KB/s], Decompressed: 2175
Downloaded: 2216 file(s) [attempted 2216/8459 = 26%, 115 KB/s], Decompressed: 2212
Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 1094 KB/s], Decompressed: 2253
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 97 KB/s], Decompressed: 2298
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 184 KB/s], Decompressed: 2336
Downloaded: 2384 file(s) [attempted 2384/8459 = 28%, 415 KB/s], Decompressed: 2380
Downloaded: 2418 file(s) [attempted 2418/8459 = 28%, 249 KB/s], Decompressed: 2414
Downloaded: 2462 file(s) [attempted 2462/8459 = 29%, 24 KB/s], Decompressed: 2459
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 148 KB/s], Decompressed: 2500
Downloaded: 2548 file(s) [attempted 2548/8459 = 30%, 1247 KB/s], Decompressed: 2544
Downloaded: 2586 file(s) [attempted 2586/8459 = 30%, 281 KB/s], Decompressed: 2582
Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 78 KB/s], Decompressed: 2616
Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 172 KB/s], Decompressed: 2661
Downloaded: 2709 file(s) [attempted 2709/8459 = 32%, 249 KB/s], Decompressed: 2702
Downloaded: 2750 file(s) [attempted 2750/8459 = 32%, 277 KB/s], Decompressed: 2729
Downloaded: 2791 file(s) [attempted 2791/8459 = 32%, 1762 KB/s], Decompressed: 2784
Downloaded: 2822 file(s) [attempted 2822/8459 = 33%, 33 KB/s], Decompressed: 2815
Downloaded: 2866 file(s) [attempted 2866/8459 = 33%, 39 KB/s], Decompressed: 2859
Downloaded: 2911 file(s) [attempted 2911/8459 = 34%, 705 KB/s], Decompressed: 2907
Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 149 KB/s], Decompressed: 2948
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 230 KB/s], Decompressed: 2989
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 114 KB/s], Decompressed: 3027
Downloaded: 3069 file(s) [attempted 3069/8459 = 36%, 194 KB/s], Decompressed: 3065
Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 59 KB/s], Decompressed: 3109
Downloaded: 3157 file(s) [attempted 3157/8459 = 37%, 427 KB/s], Decompressed: 3153
Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 24 KB/s], Decompressed: 3188
Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 1063 KB/s], Decompressed: 3225
Downloaded: 3266 file(s) [attempted 3266/8459 = 38%, 141 KB/s], Decompressed: 3260
Downloaded: 3311 file(s) [attempted 3311/8459 = 39%, 1154 KB/s], Decompressed: 3307
Downloaded: 3359 file(s) [attempted 3359/8459 = 39%, 79 KB/s], Decompressed: 3355
Downloaded: 3403 file(s) [attempted 3403/8459 = 40%, 418 KB/s], Decompressed: 3396
Downloaded: 3442 file(s) [attempted 3442/8459 = 40%, 67 KB/s], Decompressed: 3434
Downloaded: 3475 file(s) [attempted 3475/8459 = 41%, 139 KB/s], Decompressed: 3468
Downloaded: 3513 file(s) [attempted 3513/8459 = 41%, 547 KB/s], Decompressed: 3509
Downloaded: 3559 file(s) [attempted 3559/8459 = 42%, 229 KB/s], Decompressed: 3554
Downloaded: 3602 file(s) [attempted 3602/8459 = 42%, 382 KB/s], Decompressed: 3600
Downloaded: 3643 file(s) [attempted 3643/8459 = 43%, 332 KB/s], Decompressed: 3639
Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 198 KB/s], Decompressed: 3670
Downloaded: 3715 file(s) [attempted 3715/8459 = 43%, 62 KB/s], Decompressed: 3711
Downloaded: 3759 file(s) [attempted 3759/8459 = 44%, 41 KB/s], Decompressed: 3752
Downloaded: 3804 file(s) [attempted 3804/8459 = 44%, 848 KB/s], Decompressed: 3800
Downloaded: 3845 file(s) [attempted 3845/8459 = 45%, 930 KB/s], Decompressed: 3841
Downloaded: 3882 file(s) [attempted 3882/8459 = 45%, 26 KB/s], Decompressed: 3876
Downloaded: 3920 file(s) [attempted 3920/8459 = 46%, 208 KB/s], Decompressed: 3913
Downloaded: 3958 file(s) [attempted 3958/8459 = 46%, 88 KB/s], Decompressed: 3954
Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 77 KB/s], Decompressed: 3995
Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 738 KB/s], Decompressed: 4030
Downloaded: 4072 file(s) [attempted 4072/8459 = 48%, 130 KB/s], Decompressed: 4067
Downloaded: 4109 file(s) [attempted 4109/8459 = 48%, 438 KB/s], Decompressed: 4105
Downloaded: 4150 file(s) [attempted 4150/8459 = 49%, 372 KB/s], Decompressed: 4146
Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 239 KB/s], Decompressed: 4193
Downloaded: 4236 file(s) [attempted 4236/8459 = 50%, 81 KB/s], Decompressed: 4232
Downloaded: 4273 file(s) [attempted 4273/8459 = 50%, 214 KB/s], Decompressed: 4266
Downloaded: 4311 file(s) [attempted 4311/8459 = 50%, 84 KB/s], Decompressed: 4304
Downloaded: 4348 file(s) [attempted 4348/8459 = 51%, 160 KB/s], Decompressed: 4345
Downloaded: 4393 file(s) [attempted 4393/8459 = 51%, 37 KB/s], Decompressed: 4389
Downloaded: 4437 file(s) [attempted 4437/8459 = 52%, 101 KB/s], Decompressed: 4434
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 81 KB/s], Decompressed: 4472
Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 75 KB/s], Decompressed: 4506
Downloaded: 4550 file(s) [attempted 4550/8459 = 53%, 1156 KB/s], Decompressed: 4547
Downloaded: 4591 file(s) [attempted 4591/8459 = 54%, 328 KB/s], Decompressed: 4588
Downloaded: 4636 file(s) [attempted 4636/8459 = 54%, 55 KB/s], Decompressed: 4632
Downloaded: 4678 file(s) [attempted 4678/8459 = 55%, 447 KB/s], Decompressed: 4670
Downloaded: 4711 file(s) [attempted 4711/8459 = 55%, 179 KB/s], Decompressed: 4708
Downloaded: 4752 file(s) [attempted 4752/8459 = 56%, 142 KB/s], Decompressed: 4745
Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 49 KB/s], Decompressed: 4790
Downloaded: 4841 file(s) [attempted 4841/8459 = 57%, 153 KB/s], Decompressed: 4834
Downloaded: 4886 file(s) [attempted 4886/8459 = 57%, 820 KB/s], Decompressed: 4882
Downloaded: 4927 file(s) [attempted 4927/8459 = 58%, 74 KB/s], Decompressed: 4923
Downloaded: 4968 file(s) [attempted 4968/8459 = 58%, 244 KB/s], Decompressed: 4964
Downloaded: 5007 file(s) [attempted 5007/8459 = 59%, 307 KB/s], Decompressed: 5003
Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 378 KB/s], Decompressed: 5040
Downloaded: 5081 file(s) [attempted 5081/8459 = 60%, 1087 KB/s], Decompressed: 5077
Downloaded: 5120 file(s) [attempted 5120/8459 = 60%, 49 KB/s], Decompressed: 5115
Downloaded: 5160 file(s) [attempted 5160/8459 = 61%, 139 KB/s], Decompressed: 5156
Downloaded: 5201 file(s) [attempted 5201/8459 = 61%, 835 KB/s], Decompressed: 5194
Downloaded: 5235 file(s) [attempted 5235/8459 = 61%, 412 KB/s], Decompressed: 5231
Downloaded: 5279 file(s) [attempted 5279/8459 = 62%, 302 KB/s], Decompressed: 5272
Downloaded: 5320 file(s) [attempted 5320/8459 = 62%, 222 KB/s], Decompressed: 5317
Downloaded: 5361 file(s) [attempted 5361/8459 = 63%, 163 KB/s], Decompressed: 5355
Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 81 KB/s], Decompressed: 5396
Downloaded: 5440 file(s) [attempted 5440/8459 = 64%, 147 KB/s], Decompressed: 5433
Downloaded: 5481 file(s) [attempted 5481/8459 = 64%, 68 KB/s], Decompressed: 5478
Downloaded: 5526 file(s) [attempted 5526/8459 = 65%, 122 KB/s], Decompressed: 5519
Downloaded: 5563 file(s) [attempted 5563/8459 = 65%, 118 KB/s], Decompressed: 5556
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 240 KB/s], Decompressed: 5598
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 29 KB/s], Decompressed: 5628
Downloaded: 5676 file(s) [attempted 5676/8459 = 67%, 58 KB/s], Decompressed: 5673
Downloaded: 5718 file(s) [attempted 5718/8459 = 67%, 218 KB/s], Decompressed: 5714
Downloaded: 5755 file(s) [attempted 5755/8459 = 68%, 86 KB/s], Decompressed: 5752
Downloaded: 5796 file(s) [attempted 5796/8459 = 68%, 133 KB/s], Decompressed: 5793
Downloaded: 5837 file(s) [attempted 5837/8459 = 69%, 127 KB/s], Decompressed: 5834
Downloaded: 5878 file(s) [attempted 5878/8459 = 69%, 155 KB/s], Decompressed: 5875
Downloaded: 5917 file(s) [attempted 5917/8459 = 69%, 501 KB/s], Decompressed: 5911
Downloaded: 5952 file(s) [attempted 5952/8459 = 70%, 748 KB/s], Decompressed: 5947
Downloaded: 5995 file(s) [attempted 5995/8459 = 70%, 302 KB/s], Decompressed: 5991
Downloaded: 6039 file(s) [attempted 6039/8459 = 71%, 680 KB/s], Decompressed: 6032
Downloaded: 6077 file(s) [attempted 6077/8459 = 71%, 265 KB/s], Decompressed: 6070
Downloaded: 6114 file(s) [attempted 6114/8459 = 72%, 30 KB/s], Decompressed: 6107
Downloaded: 6149 file(s) [attempted 6149/8459 = 72%, 1201 KB/s], Decompressed: 6145
Downloaded: 6193 file(s) [attempted 6193/8459 = 73%, 442 KB/s], Decompressed: 6190
Downloaded: 6237 file(s) [attempted 6237/8459 = 73%, 950 KB/s], Decompressed: 6234
Downloaded: 6275 file(s) [attempted 6275/8459 = 74%, 174 KB/s], Decompressed: 6268
Downloaded: 6309 file(s) [attempted 6309/8459 = 74%, 1151 KB/s], Decompressed: 6303
Downloaded: 6347 file(s) [attempted 6347/8459 = 75%, 828 KB/s], Decompressed: 6340
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 700 KB/s], Decompressed: 6385
Downloaded: 6436 file(s) [attempted 6436/8459 = 76%, 207 KB/s], Decompressed: 6429
Downloaded: 6470 file(s) [attempted 6470/8459 = 76%, 52 KB/s], Decompressed: 6463
Downloaded: 6511 file(s) [attempted 6511/8459 = 76%, 141 KB/s], Decompressed: 6504
Downloaded: 6552 file(s) [attempted 6552/8459 = 77%, 312 KB/s], Decompressed: 6545
Downloaded: 6593 file(s) [attempted 6593/8459 = 77%, 458 KB/s], Decompressed: 6590
Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 248 KB/s], Decompressed: 6631
Downloaded: 6676 file(s) [attempted 6676/8459 = 78%, 136 KB/s], Decompressed: 6672
Downloaded: 6714 file(s) [attempted 6714/8459 = 79%, 133 KB/s], Decompressed: 6710
Downloaded: 6751 file(s) [attempted 6751/8459 = 79%, 144 KB/s], Decompressed: 6747
Downloaded: 6793 file(s) [attempted 6793/8459 = 80%, 570 KB/s], Decompressed: 6788
Downloaded: 6833 file(s) [attempted 6833/8459 = 80%, 329 KB/s], Decompressed: 6826
Downloaded: 6874 file(s) [attempted 6874/8459 = 81%, 339 KB/s], Decompressed: 6871
Downloaded: 6912 file(s) [attempted 6912/8459 = 81%, 26 KB/s], Decompressed: 6908
Downloaded: 6953 file(s) [attempted 6953/8459 = 82%, 286 KB/s], Decompressed: 6942
Downloaded: 6990 file(s) [attempted 6990/8459 = 82%, 38 KB/s], Decompressed: 6987
Downloaded: 7031 file(s) [attempted 7031/8459 = 83%, 438 KB/s], Decompressed: 7028
Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 140 KB/s], Decompressed: 7066
Downloaded: 7111 file(s) [attempted 7111/8459 = 84%, 372 KB/s], Decompressed: 7103
Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 112 KB/s], Decompressed: 7141
Downloaded: 7189 file(s) [attempted 7189/8459 = 84%, 66 KB/s], Decompressed: 7185
Downloaded: 7228 file(s) [attempted 7228/8459 = 85%, 1891 KB/s], Decompressed: 7216
Downloaded: 7264 file(s) [attempted 7264/8459 = 85%, 710 KB/s], Decompressed: 7257
Downloaded: 7307 file(s) [attempted 7307/8459 = 86%, 40 KB/s], Decompressed: 7298
Downloaded: 7340 file(s) [attempted 7340/8459 = 86%, 110 KB/s], Decompressed: 7336
Downloaded: 7383 file(s) [attempted 7383/8459 = 87%, 58 KB/s], Decompressed: 7374
Downloaded: 7411 file(s) [attempted 7411/8459 = 87%, 126 KB/s], Decompressed: 7408
Downloaded: 7452 file(s) [attempted 7452/8459 = 88%, 423 KB/s], Decompressed: 7449
Downloaded: 7493 file(s) [attempted 7493/8459 = 88%, 247 KB/s], Decompressed: 7490
Downloaded: 7535 file(s) [attempted 7535/8459 = 89%, 2358 KB/s], Decompressed: 7531
Downloaded: 7576 file(s) [attempted 7576/8459 = 89%, 913 KB/s], Decompressed: 7572
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 202 KB/s], Decompressed: 7606
Downloaded: 7648 file(s) [attempted 7648/8459 = 90%, 41 KB/s], Decompressed: 7644
Downloaded: 7692 file(s) [attempted 7692/8459 = 90%, 372 KB/s], Decompressed: 7689
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 140 KB/s], Decompressed: 7733
Downloaded: 7781 file(s) [attempted 7781/8459 = 91%, 314 KB/s], Decompressed: 7774
Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 226 KB/s], Decompressed: 7808
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 2238 KB/s], Decompressed: 7846
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 59 KB/s], Decompressed: 7887
Downloaded: 7935 file(s) [attempted 7935/8459 = 93%, 351 KB/s], Decompressed: 7928
Downloaded: 7969 file(s) [attempted 7969/8459 = 94%, 98 KB/s], Decompressed: 7962
Downloaded: 8003 file(s) [attempted 8003/8459 = 94%, 53 KB/s], Decompressed: 7997
Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 439 KB/s], Decompressed: 8041
Downloaded: 8089 file(s) [attempted 8089/8459 = 95%, 139 KB/s], Decompressed: 8068
Downloaded: 8133 file(s) [attempted 8133/8459 = 96%, 725 KB/s], Decompressed: 8068
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 741 KB/s], Decompressed: 8075
Downloaded: 8205 file(s) [attempted 8205/8459 = 96%, 1581 KB/s], Decompressed: 8198
Downloaded: 8246 file(s) [attempted 8246/8459 = 97%, 794 KB/s], Decompressed: 8243
Downloaded: 8289 file(s) [attempted 8289/8459 = 97%, 305 KB/s], Decompressed: 8277
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 267 KB/s], Decompressed: 8322
Downloaded: 8359 file(s) [attempted 8359/8459 = 98%, 184 KB/s], Decompressed: 8349
Downloaded: 8397 file(s) [attempted 8397/8459 = 99%, 200 KB/s], Decompressed: 8390
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 271 KB/s], Decompressed: 8435
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 271 KB/s], Decompressed: 8455


$ lake build
exit_code=Some(0) duration_ms=309872
stdout:
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (227s)
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) [0x7278975c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7278975bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7278975bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7278974f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7278974f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7278975caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x727897432923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x727897432b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x727897433827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7278974341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7278975c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x727897215adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7278975c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7278975c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x72789759b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x727897215c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x727892622638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x72789240cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x727891f69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x727891f69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x72788ee4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x72788ee45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x62233a5cc8da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (7.4s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.6s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (35s)
✔ [3414/3416] Built Iut.Basic (2.6s)
✔ [3415/3416] Built Iut (2.4s)
Build completed successfully (3416 jobs).

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


$ lake build :blueprint
exit_code=Some(1) duration_ms=3393
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=10644595
stdout:
apx-semantic-phase	{"duration_ms":5,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":8,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":330959,"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":53,"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":0,"module_index":0,"ok":true,"payload_bytes":738,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":57,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":330160,"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":58,"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":1,"module_index":1,"ok":true,"payload_bytes":1330,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":97,"diagnostic_count":15,"duration_ms":7451,"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":340112,"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":387,"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":1887,"diagnostic_count":116,"duration_ms":1541173,"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":340558,"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":1887,"diagnostic_count":116,"duration_ms":8045,"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":66661196,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":42,"module_index":3,"ok":true,"payload_bytes":66661196,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":7663,"diagnostic_count":3067,"duration_ms":6065208,"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":585295,"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":7663,"diagnostic_count":3067,"duration_ms":41962,"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":458047074,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":575,"module_index":4,"ok":true,"payload_bytes":458047074,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":152,"diagnostic_count":23,"duration_ms":28746,"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":925873,"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":442,"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":2,"module_index":5,"ok":true,"payload_bytes":2722873,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":9800,"diagnostic_count":3221,"duration_ms":50544,"module_count":6,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":531558642,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":530,"ok":true,"payload_bytes":531558642,"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":3206}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":366,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":23,"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":3590,"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 27a55ab67425bb7af335b6c6ec2907713f6b0c4e9e3c2e5e062a62117db37c8d
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":10620745,"ok":true}

Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

git_clone exit 0 duration 3s · created 6/18/2026, 10:12:49 AM

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

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

git_checkout exit 128 duration 1 ms · created 6/18/2026, 10:12:49 AM

git checkout 6fb8e7cbe61c5fe4a4156a80558581b359775840

fatal: reference is not a tree: 6fb8e7cbe61c5fe4a4156a80558581b359775840

git_checkout exit 0 duration 991 ms · created 6/18/2026, 10:12:49 AM

git fetch --depth 1 origin 6fb8e7cbe61c5fe4a4156a80558581b359775840

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

git_checkout exit 0 duration 142 ms · created 6/18/2026, 10:12:49 AM

git checkout 6fb8e7cbe61c5fe4a4156a80558581b359775840 (after fetch)

Note: switching to '6fb8e7cbe61c5fe4a4156a80558581b359775840'.

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 6fb8e7c Split local log coordinate image laws

lake_cache exit 0 duration 53s · created 6/18/2026, 10:12:49 AM

lake exe cache get

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

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

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 1 KB/s], Decompressed: 12
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 16 KB/s], Decompressed: 35
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 26 KB/s], Decompressed: 62
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 442 KB/s], Decompressed: 83
Downloaded: 121 file(s) [attempted 121/8459 = 1%, 154 KB/s], Decompressed: 114
Downloaded: 151 file(s) [attempted 151/8459 = 1%, 123 KB/s], Decompressed: 141
Downloaded: 189 file(s) [attempted 189/8459 = 2%, 236 KB/s], Decompressed: 182
Downloaded: 223 file(s) [attempted 223/8459 = 2%, 838 KB/s], Decompressed: 216
Downloaded: 261 file(s) [attempted 261/8459 = 3%, 214 KB/s], Decompressed: 258
Downloaded: 295 file(s) [attempted 295/8459 = 3%, 105 KB/s], Decompressed: 288
Downloaded: 336 file(s) [attempted 336/8459 = 3%, 46 KB/s], Decompressed: 333
Downloaded: 374 file(s) [attempted 374/8459 = 4%, 279 KB/s], Decompressed: 367
Downloaded: 412 file(s) [attempted 412/8459 = 4%, 303 KB/s], Decompressed: 408
Downloaded: 453 file(s) [attempted 453/8459 = 5%, 77 KB/s], Decompressed: 449
Downloaded: 490 file(s) [attempted 490/8459 = 5%, 546 KB/s], Decompressed: 487
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 243 KB/s], Decompressed: 521
Downloaded: 566 file(s) [attempted 566/8459 = 6%, 539 KB/s], Decompressed: 559
Downloaded: 610 file(s) [attempted 610/8459 = 7%, 131 KB/s], Decompressed: 603
Downloaded: 655 file(s) [attempted 655/8459 = 7%, 350 KB/s], Decompressed: 651
Downloaded: 696 file(s) [attempted 696/8459 = 8%, 91 KB/s], Decompressed: 686
Downloaded: 734 file(s) [attempted 734/8459 = 8%, 438 KB/s], Decompressed: 723
Downloaded: 770 file(s) [attempted 770/8459 = 9%, 189 KB/s], Decompressed: 761
Downloaded: 806 file(s) [attempted 806/8459 = 9%, 173 KB/s], Decompressed: 771
Downloaded: 847 file(s) [attempted 847/8459 = 10%, 60 KB/s], Decompressed: 771
Downloaded: 888 file(s) [attempted 888/8459 = 10%, 219 KB/s], Decompressed: 884
Downloaded: 925 file(s) [attempted 925/8459 = 10%, 137 KB/s], Decompressed: 919
Downloaded: 967 file(s) [attempted 967/8459 = 11%, 188 KB/s], Decompressed: 963
Downloaded: 1004 file(s) [attempted 1004/8459 = 11%, 514 KB/s], Decompressed: 997
Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 851 KB/s], Decompressed: 1038
Downloaded: 1084 file(s) [attempted 1084/8459 = 12%, 80 KB/s], Decompressed: 1076
Downloaded: 1121 file(s) [attempted 1121/8459 = 13%, 213 KB/s], Decompressed: 1114
Downloaded: 1162 file(s) [attempted 1162/8459 = 13%, 1536 KB/s], Decompressed: 1151
Downloaded: 1199 file(s) [attempted 1199/8459 = 14%, 2434 KB/s], Decompressed: 1186
Downloaded: 1240 file(s) [attempted 1240/8459 = 14%, 90 KB/s], Decompressed: 1186
Downloaded: 1278 file(s) [attempted 1278/8459 = 15%, 297 KB/s], Decompressed: 1189
Downloaded: 1319 file(s) [attempted 1319/8459 = 15%, 131 KB/s], Decompressed: 1316
Downloaded: 1364 file(s) [attempted 1364/8459 = 16%, 205 KB/s], Decompressed: 1360
Downloaded: 1401 file(s) [attempted 1401/8459 = 16%, 62 KB/s], Decompressed: 1394
Downloaded: 1442 file(s) [attempted 1442/8459 = 17%, 304 KB/s], Decompressed: 1435
Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 53 KB/s], Decompressed: 1477
Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 199 KB/s], Decompressed: 1518
Downloaded: 1562 file(s) [attempted 1562/8459 = 18%, 307 KB/s], Decompressed: 1559
Downloaded: 1603 file(s) [attempted 1603/8459 = 18%, 106 KB/s], Decompressed: 1593
Downloaded: 1641 file(s) [attempted 1641/8459 = 19%, 219 KB/s], Decompressed: 1637
Downloaded: 1682 file(s) [attempted 1682/8459 = 19%, 593 KB/s], Decompressed: 1680
Downloaded: 1720 file(s) [attempted 1720/8459 = 20%, 141 KB/s], Decompressed: 1716
Downloaded: 1761 file(s) [attempted 1761/8459 = 20%, 306 KB/s], Decompressed: 1757
Downloaded: 1798 file(s) [attempted 1798/8459 = 21%, 909 KB/s], Decompressed: 1795
Downloaded: 1836 file(s) [attempted 1836/8459 = 21%, 399 KB/s], Decompressed: 1819
Downloaded: 1874 file(s) [attempted 1874/8459 = 22%, 261 KB/s], Decompressed: 1867
Downloaded: 1906 file(s) [attempted 1906/8459 = 22%, 138 KB/s], Decompressed: 1901
Downloaded: 1948 file(s) [attempted 1948/8459 = 23%, 418 KB/s], Decompressed: 1939
Downloaded: 1986 file(s) [attempted 1986/8459 = 23%, 117 KB/s], Decompressed: 1980
Downloaded: 2023 file(s) [attempted 2023/8459 = 23%, 771 KB/s], Decompressed: 2017
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 88 KB/s], Decompressed: 2055
Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 1074 KB/s], Decompressed: 2096
Downloaded: 2142 file(s) [attempted 2142/8459 = 25%, 509 KB/s], Decompressed: 2137
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 107 KB/s], Decompressed: 2175
Downloaded: 2216 file(s) [attempted 2216/8459 = 26%, 115 KB/s], Decompressed: 2212
Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 1094 KB/s], Decompressed: 2253
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 97 KB/s], Decompressed: 2298
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 184 KB/s], Decompressed: 2336
Downloaded: 2384 file(s) [attempted 2384/8459 = 28%, 415 KB/s], Decompressed: 2380
Downloaded: 2418 file(s) [attempted 2418/8459 = 28%, 249 KB/s], Decompressed: 2414
Downloaded: 2462 file(s) [attempted 2462/8459 = 29%, 24 KB/s], Decompressed: 2459
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 148 KB/s], Decompressed: 2500
Downloaded: 2548 file(s) [attempted 2548/8459 = 30%, 1247 KB/s], Decompressed: 2544
Downloaded: 2586 file(s) [attempted 2586/8459 = 30%, 281 KB/s], Decompressed: 2582
Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 78 KB/s], Decompressed: 2616
Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 172 KB/s], Decompressed: 2661
Downloaded: 2709 file(s) [attempted 2709/8459 = 32%, 249 KB/s], Decompressed: 2702
Downloaded: 2750 file(s) [attempted 2750/8459 = 32%, 277 KB/s], Decompressed: 2729
Downloaded: 2791 file(s) [attempted 2791/8459 = 32%, 1762 KB/s], Decompressed: 2784
Downloaded: 2822 file(s) [attempted 2822/8459 = 33%, 33 KB/s], Decompressed: 2815
Downloaded: 2866 file(s) [attempted 2866/8459 = 33%, 39 KB/s], Decompressed: 2859
Downloaded: 2911 file(s) [attempted 2911/8459 = 34%, 705 KB/s], Decompressed: 2907
Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 149 KB/s], Decompressed: 2948
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 230 KB/s], Decompressed: 2989
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 114 KB/s], Decompressed: 3027
Downloaded: 3069 file(s) [attempted 3069/8459 = 36%, 194 KB/s], Decompressed: 3065
Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 59 KB/s], Decompressed: 3109
Downloaded: 3157 file(s) [attempted 3157/8459 = 37%, 427 KB/s], Decompressed: 3153
Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 24 KB/s], Decompressed: 3188
Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 1063 KB/s], Decompressed: 3225
Downloaded: 3266 file(s) [attempted 3266/8459 = 38%, 141 KB/s], Decompressed: 3260
Downloaded: 3311 file(s) [attempted 3311/8459 = 39%, 1154 KB/s], Decompressed: 3307
Downloaded: 3359 file(s) [attempted 3359/8459 = 39%, 79 KB/s], Decompressed: 3355
Downloaded: 3403 file(s) [attempted 3403/8459 = 40%, 418 KB/s], Decompressed: 3396
Downloaded: 3442 file(s) [attempted 3442/8459 = 40%, 67 KB/s], Decompressed: 3434
Downloaded: 3475 file(s) [attempted 3475/8459 = 41%, 139 KB/s], Decompressed: 3468
Downloaded: 3513 file(s) [attempted 3513/8459 = 41%, 547 KB/s], Decompressed: 3509
Downloaded: 3559 file(s) [attempted 3559/8459 = 42%, 229 KB/s], Decompressed: 3554
Downloaded: 3602 file(s) [attempted 3602/8459 = 42%, 382 KB/s], Decompressed: 3600
Downloaded: 3643 file(s) [attempted 3643/8459 = 43%, 332 KB/s], Decompressed: 3639
Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 198 KB/s], Decompressed: 3670
Downloaded: 3715 file(s) [attempted 3715/8459 = 43%, 62 KB/s], Decompressed: 3711
Downloaded: 3759 file(s) [attempted 3759/8459 = 44%, 41 KB/s], Decompressed: 3752
Downloaded: 3804 file(s) [attempted 3804/8459 = 44%, 848 KB/s], Decompressed: 3800
Downloaded: 3845 file(s) [attempted 3845/8459 = 45%, 930 KB/s], Decompressed: 3841
Downloaded: 3882 file(s) [attempted 3882/8459 = 45%, 26 KB/s], Decompressed: 3876
Downloaded: 3920 file(s) [attempted 3920/8459 = 46%, 208 KB/s], Decompressed: 3913
Downloaded: 3958 file(s) [attempted 3958/8459 = 46%, 88 KB/s], Decompressed: 3954
Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 77 KB/s], Decompressed: 3995
Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 738 KB/s], Decompressed: 4030
Downloaded: 4072 file(s) [attempted 4072/8459 = 48%, 130 KB/s], Decompressed: 4067
Downloaded: 4109 file(s) [attempted 4109/8459 = 48%, 438 KB/s], Decompressed: 4105
Downloaded: 4150 file(s) [attempted 4150/8459 = 49%, 372 KB/s], Decompressed: 4146
Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 239 KB/s], Decompressed: 4193
Downloaded: 4236 file(s) [attempted 4236/8459 = 50%, 81 KB/s], Decompressed: 4232
Downloaded: 4273 file(s) [attempted 4273/8459 = 50%, 214 KB/s], Decompressed: 4266
Downloaded: 4311 file(s) [attempted 4311/8459 = 50%, 84 KB/s], Decompressed: 4304
Downloaded: 4348 file(s) [attempted 4348/8459 = 51%, 160 KB/s], Decompressed: 4345
Downloaded: 4393 file(s) [attempted 4393/8459 = 51%, 37 KB/s], Decompressed: 4389
Downloaded: 4437 file(s) [attempted 4437/8459 = 52%, 101 KB/s], Decompressed: 4434
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 81 KB/s], Decompressed: 4472
Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 75 KB/s], Decompressed: 4506
Downloaded: 4550 file(s) [attempted 4550/8459 = 53%, 1156 KB/s], Decompressed: 4547
Downloaded: 4591 file(s) [attempted 4591/8459 = 54%, 328 KB/s], Decompressed: 4588
Downloaded: 4636 file(s) [attempted 4636/8459 = 54%, 55 KB/s], Decompressed: 4632
Downloaded: 4678 file(s) [attempted 4678/8459 = 55%, 447 KB/s], Decompressed: 4670
Downloaded: 4711 file(s) [attempted 4711/8459 = 55%, 179 KB/s], Decompressed: 4708
Downloaded: 4752 file(s) [attempted 4752/8459 = 56%, 142 KB/s], Decompressed: 4745
Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 49 KB/s], Decompressed: 4790
Downloaded: 4841 file(s) [attempted 4841/8459 = 57%, 153 KB/s], Decompressed: 4834
Downloaded: 4886 file(s) [attempted 4886/8459 = 57%, 820 KB/s], Decompressed: 4882
Downloaded: 4927 file(s) [attempted 4927/8459 = 58%, 74 KB/s], Decompressed: 4923
Downloaded: 4968 file(s) [attempted 4968/8459 = 58%, 244 KB/s], Decompressed: 4964
Downloaded: 5007 file(s) [attempted 5007/8459 = 59%, 307 KB/s], Decompressed: 5003
Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 378 KB/s], Decompressed: 5040
Downloaded: 5081 file(s) [attempted 5081/8459 = 60%, 1087 KB/s], Decompressed: 5077
Downloaded: 5120 file(s) [attempted 5120/8459 = 60%, 49 KB/s], Decompressed: 5115
Downloaded: 5160 file(s) [attempted 5160/8459 = 61%, 139 KB/s], Decompressed: 5156
Downloaded: 5201 file(s) [attempted 5201/8459 = 61%, 835 KB/s], Decompressed: 5194
Downloaded: 5235 file(s) [attempted 5235/8459 = 61%, 412 KB/s], Decompressed: 5231
Downloaded: 5279 file(s) [attempted 5279/8459 = 62%, 302 KB/s], Decompressed: 5272
Downloaded: 5320 file(s) [attempted 5320/8459 = 62%, 222 KB/s], Decompressed: 5317
Downloaded: 5361 file(s) [attempted 5361/8459 = 63%, 163 KB/s], Decompressed: 5355
Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 81 KB/s], Decompressed: 5396
Downloaded: 5440 file(s) [attempted 5440/8459 = 64%, 147 KB/s], Decompressed: 5433
Downloaded: 5481 file(s) [attempted 5481/8459 = 64%, 68 KB/s], Decompressed: 5478
Downloaded: 5526 file(s) [attempted 5526/8459 = 65%, 122 KB/s], Decompressed: 5519
Downloaded: 5563 file(s) [attempted 5563/8459 = 65%, 118 KB/s], Decompressed: 5556
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 240 KB/s], Decompressed: 5598
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 29 KB/s], Decompressed: 5628
Downloaded: 5676 file(s) [attempted 5676/8459 = 67%, 58 KB/s], Decompressed: 5673
Downloaded: 5718 file(s) [attempted 5718/8459 = 67%, 218 KB/s], Decompressed: 5714
Downloaded: 5755 file(s) [attempted 5755/8459 = 68%, 86 KB/s], Decompressed: 5752
Downloaded: 5796 file(s) [attempted 5796/8459 = 68%, 133 KB/s], Decompressed: 5793
Downloaded: 5837 file(s) [attempted 5837/8459 = 69%, 127 KB/s], Decompressed: 5834
Downloaded: 5878 file(s) [attempted 5878/8459 = 69%, 155 KB/s], Decompressed: 5875
Downloaded: 5917 file(s) [attempted 5917/8459 = 69%, 501 KB/s], Decompressed: 5911
Downloaded: 5952 file(s) [attempted 5952/8459 = 70%, 748 KB/s], Decompressed: 5947
Downloaded: 5995 file(s) [attempted 5995/8459 = 70%, 302 KB/s], Decompressed: 5991
Downloaded: 6039 file(s) [attempted 6039/8459 = 71%, 680 KB/s], Decompressed: 6032
Downloaded: 6077 file(s) [attempted 6077/8459 = 71%, 265 KB/s], Decompressed: 6070
Downloaded: 6114 file(s) [attempted 6114/8459 = 72%, 30 KB/s], Decompressed: 6107
Downloaded: 6149 file(s) [attempted 6149/8459 = 72%, 1201 KB/s], Decompressed: 6145
Downloaded: 6193 file(s) [attempted 6193/8459 = 73%, 442 KB/s], Decompressed: 6190
Downloaded: 6237 file(s) [attempted 6237/8459 = 73%, 950 KB/s], Decompressed: 6234
Downloaded: 6275 file(s) [attempted 6275/8459 = 74%, 174 KB/s], Decompressed: 6268
Downloaded: 6309 file(s) [attempted 6309/8459 = 74%, 1151 KB/s], Decompressed: 6303
Downloaded: 6347 file(s) [attempted 6347/8459 = 75%, 828 KB/s], Decompressed: 6340
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 700 KB/s], Decompressed: 6385
Downloaded: 6436 file(s) [attempted 6436/8459 = 76%, 207 KB/s], Decompressed: 6429
Downloaded: 6470 file(s) [attempted 6470/8459 = 76%, 52 KB/s], Decompressed: 6463
Downloaded: 6511 file(s) [attempted 6511/8459 = 76%, 141 KB/s], Decompressed: 6504
Downloaded: 6552 file(s) [attempted 6552/8459 = 77%, 312 KB/s], Decompressed: 6545
Downloaded: 6593 file(s) [attempted 6593/8459 = 77%, 458 KB/s], Decompressed: 6590
Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 248 KB/s], Decompressed: 6631
Downloaded: 6676 file(s) [attempted 6676/8459 = 78%, 136 KB/s], Decompressed: 6672
Downloaded: 6714 file(s) [attempted 6714/8459 = 79%, 133 KB/s], Decompressed: 6710
Downloaded: 6751 file(s) [attempted 6751/8459 = 79%, 144 KB/s], Decompressed: 6747
Downloaded: 6793 file(s) [attempted 6793/8459 = 80%, 570 KB/s], Decompressed: 6788
Downloaded: 6833 file(s) [attempted 6833/8459 = 80%, 329 KB/s], Decompressed: 6826
Downloaded: 6874 file(s) [attempted 6874/8459 = 81%, 339 KB/s], Decompressed: 6871
Downloaded: 6912 file(s) [attempted 6912/8459 = 81%, 26 KB/s], Decompressed: 6908
Downloaded: 6953 file(s) [attempted 6953/8459 = 82%, 286 KB/s], Decompressed: 6942
Downloaded: 6990 file(s) [attempted 6990/8459 = 82%, 38 KB/s], Decompressed: 6987
Downloaded: 7031 file(s) [attempted 7031/8459 = 83%, 438 KB/s], Decompressed: 7028
Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 140 KB/s], Decompressed: 7066
Downloaded: 7111 file(s) [attempted 7111/8459 = 84%, 372 KB/s], Decompressed: 7103
Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 112 KB/s], Decompressed: 7141
Downloaded: 7189 file(s) [attempted 7189/8459 = 84%, 66 KB/s], Decompressed: 7185
Downloaded: 7228 file(s) [attempted 7228/8459 = 85%, 1891 KB/s], Decompressed: 7216
Downloaded: 7264 file(s) [attempted 7264/8459 = 85%, 710 KB/s], Decompressed: 7257
Downloaded: 7307 file(s) [attempted 7307/8459 = 86%, 40 KB/s], Decompressed: 7298
Downloaded: 7340 file(s) [attempted 7340/8459 = 86%, 110 KB/s], Decompressed: 7336
Downloaded: 7383 file(s) [attempted 7383/8459 = 87%, 58 KB/s], Decompressed: 7374
Downloaded: 7411 file(s) [attempted 7411/8459 = 87%, 126 KB/s], Decompressed: 7408
Downloaded: 7452 file(s) [attempted 7452/8459 = 88%, 423 KB/s], Decompressed: 7449
Downloaded: 7493 file(s) [attempted 7493/8459 = 88%, 247 KB/s], Decompressed: 7490
Downloaded: 7535 file(s) [attempted 7535/8459 = 89%, 2358 KB/s], Decompressed: 7531
Downloaded: 7576 file(s) [attempted 7576/8459 = 89%, 913 KB/s], Decompressed: 7572
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 202 KB/s], Decompressed: 7606
Downloaded: 7648 file(s) [attempted 7648/8459 = 90%, 41 KB/s], Decompressed: 7644
Downloaded: 7692 file(s) [attempted 7692/8459 = 90%, 372 KB/s], Decompressed: 7689
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 140 KB/s], Decompressed: 7733
Downloaded: 7781 file(s) [attempted 7781/8459 = 91%, 314 KB/s], Decompressed: 7774
Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 226 KB/s], Decompressed: 7808
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 2238 KB/s], Decompressed: 7846
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 59 KB/s], Decompressed: 7887
Downloaded: 7935 file(s) [attempted 7935/8459 = 93%, 351 KB/s], Decompressed: 7928
Downloaded: 7969 file(s) [attempted 7969/8459 = 94%, 98 KB/s], Decompressed: 7962
Downloaded: 8003 file(s) [attempted 8003/8459 = 94%, 53 KB/s], Decompressed: 7997
Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 439 KB/s], Decompressed: 8041
Downloaded: 8089 file(s) [attempted 8089/8459 = 95%, 139 KB/s], Decompressed: 8068
Downloaded: 8133 file(s) [attempted 8133/8459 = 96%, 725 KB/s], Decompressed: 8068
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 741 KB/s], Decompressed: 8075
Downloaded: 8205 file(s) [attempted 8205/8459 = 96%, 1581 KB/s], Decompressed: 8198
Downloaded: 8246 file(s) [attempted 8246/8459 = 97%, 794 KB/s], Decompressed: 8243
Downloaded: 8289 file(s) [attempted 8289/8459 = 97%, 305 KB/s], Decompressed: 8277
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 267 KB/s], Decompressed: 8322
Downloaded: 8359 file(s) [attempted 8359/8459 = 98%, 184 KB/s], Decompressed: 8349
Downloaded: 8397 file(s) [attempted 8397/8459 = 99%, 200 KB/s], Decompressed: 8390
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 271 KB/s], Decompressed: 8435
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 271 KB/s], Decompressed: 8455

lean_checker exit 0 duration 5m 10s · created 6/18/2026, 10:12:49 AM

lake build

ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (227s)
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) [0x7278975c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7278975bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7278975bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7278974f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7278974f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7278975caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x727897432923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x727897432b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x727897433827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7278974341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7278975c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x727897215adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7278975c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7278975c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x72789759b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x727897215c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x727892622638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x72789240cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x727891f69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x727891f69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x72788ee4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x72788ee45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x62233a5cc8da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (7.4s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.6s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (35s)
✔ [3414/3416] Built Iut.Basic (2.6s)
✔ [3415/3416] Built Iut (2.4s)
Build completed successfully (3416 jobs).

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

blueprint_build exit 1 duration 3s · created 6/18/2026, 10:12:49 AM

lake build :blueprint

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

semantic_extract exit 0 duration 2h 57m · created 6/18/2026, 10:12:49 AM

./.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":8,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":330959,"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":53,"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":0,"module_index":0,"ok":true,"payload_bytes":738,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":1,"diagnostic_count":0,"duration_ms":57,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":330160,"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":58,"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":1,"module_index":1,"ok":true,"payload_bytes":1330,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":97,"diagnostic_count":15,"duration_ms":7451,"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":340112,"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":387,"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":1887,"diagnostic_count":116,"duration_ms":1541173,"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":340558,"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":1887,"diagnostic_count":116,"duration_ms":8045,"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":66661196,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":42,"module_index":3,"ok":true,"payload_bytes":66661196,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":7663,"diagnostic_count":3067,"duration_ms":6065208,"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":585295,"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":7663,"diagnostic_count":3067,"duration_ms":41962,"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":458047074,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":575,"module_index":4,"ok":true,"payload_bytes":458047074,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":152,"diagnostic_count":23,"duration_ms":28746,"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":925873,"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":442,"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":2,"module_index":5,"ok":true,"payload_bytes":2722873,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":9800,"diagnostic_count":3221,"duration_ms":50544,"module_count":6,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":531558642,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":530,"ok":true,"payload_bytes":531558642,"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":3206}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":366,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":23,"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":3590,"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 27a55ab67425bb7af335b6c6ec2907713f6b0c4e9e3c2e5e062a62117db37c8d
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":10620745,"ok":true}