Login

Verification run

Run 359

promachina/iut-lean branch master triggered via github_backfill
succeeded commit 4dbaeefd0b23 toolchain lean-v4-30-0 prover lean took 3h 10m · finished 4w ago
Open project

Package inputs

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

Trust verification

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

(verification not run)

Manifest

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

(manifest not loaded)

Verifier log excerpt

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


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


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


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

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 4dbaeef Project local log factors through product coordinates

Resolved source revision: 4dbaeefd0b2318363be5f0e8efd077d6497c387d

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=4dbaeefd0b2318363be5f0e8efd077d6497c387d provenance={"branch":"master","checked_out_revision":"4dbaeefd0b2318363be5f0e8efd077d6497c387d","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"4dbaeefd0b2318363be5f0e8efd077d6497c387d","used_missing_commit_fetch":true}
Resolved toolchain: lean-v4-30-0 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
Restored Lean workspace build cache
Restored 9 Lean dependency package snapshot(s)
Prepared 9 shared Lean git mirror alias(es)
Lean semantic module cache: computed 31 module hash fact(s) from source and olean files; skipping Lean module-facts probe
Lean semantic module cache: 25/31 module hit(s), 6 miss(es)
Lean semantic module cache: stable superset runner maps 6 missing module(s) to 5 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 6 missing module(s) with 31 imported module candidate(s)
Lean semantic module cache: stable superset runner target set maps to 5 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 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=75965
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%, 14 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 23 KB/s], Decompressed: 13
Downloaded: 42 file(s) [attempted 42/8459 = 0%, 86 KB/s], Decompressed: 41
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 44 KB/s], Decompressed: 61
Downloaded: 100 file(s) [attempted 100/8459 = 1%, 321 KB/s], Decompressed: 75
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 260 KB/s], Decompressed: 75
Downloaded: 169 file(s) [attempted 169/8459 = 1%, 678 KB/s], Decompressed: 162
Downloaded: 206 file(s) [attempted 206/8459 = 2%, 31 KB/s], Decompressed: 186
Downloaded: 247 file(s) [attempted 247/8459 = 2%, 24 KB/s], Decompressed: 186
Downloaded: 292 file(s) [attempted 292/8459 = 3%, 96 KB/s], Decompressed: 288
Downloaded: 329 file(s) [attempted 329/8459 = 3%, 301 KB/s], Decompressed: 326
Downloaded: 371 file(s) [attempted 371/8459 = 4%, 277 KB/s], Decompressed: 367
Downloaded: 408 file(s) [attempted 408/8459 = 4%, 60 KB/s], Decompressed: 405
Downloaded: 443 file(s) [attempted 443/8459 = 5%, 1724 KB/s], Decompressed: 439
Downloaded: 487 file(s) [attempted 487/8459 = 5%, 281 KB/s], Decompressed: 480
Downloaded: 529 file(s) [attempted 529/8459 = 6%, 269 KB/s], Decompressed: 525
Downloaded: 570 file(s) [attempted 570/8459 = 6%, 23 KB/s], Decompressed: 566
Downloaded: 610 file(s) [attempted 610/8459 = 7%, 135 KB/s], Decompressed: 603
Downloaded: 648 file(s) [attempted 648/8459 = 7%, 133 KB/s], Decompressed: 614
Downloaded: 682 file(s) [attempted 682/8459 = 8%, 569 KB/s], Decompressed: 614
Downloaded: 730 file(s) [attempted 730/8459 = 8%, 71 KB/s], Decompressed: 727
Downloaded: 775 file(s) [attempted 775/8459 = 9%, 195 KB/s], Decompressed: 768
Downloaded: 816 file(s) [attempted 816/8459 = 9%, 107 KB/s], Decompressed: 812
Downloaded: 857 file(s) [attempted 857/8459 = 10%, 122 KB/s], Decompressed: 854
Downloaded: 898 file(s) [attempted 898/8459 = 10%, 184 KB/s], Decompressed: 891
Downloaded: 932 file(s) [attempted 932/8459 = 11%, 1001 KB/s], Decompressed: 929
Downloaded: 977 file(s) [attempted 977/8459 = 11%, 753 KB/s], Decompressed: 973
Downloaded: 1018 file(s) [attempted 1018/8459 = 12%, 238 KB/s], Decompressed: 1015
Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 141 KB/s], Decompressed: 1052
Downloaded: 1097 file(s) [attempted 1097/8459 = 12%, 694 KB/s], Decompressed: 1090
Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 70 KB/s], Decompressed: 1127
Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 770 KB/s], Decompressed: 1127
Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 380 KB/s], Decompressed: 1131
Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 204 KB/s], Decompressed: 1240
Downloaded: 1299 file(s) [attempted 1299/8459 = 15%, 214 KB/s], Decompressed: 1295
Downloaded: 1340 file(s) [attempted 1340/8459 = 15%, 1157 KB/s], Decompressed: 1336
Downloaded: 1379 file(s) [attempted 1379/8459 = 16%, 198 KB/s], Decompressed: 1374
Downloaded: 1422 file(s) [attempted 1422/8459 = 16%, 81 KB/s], Decompressed: 1415
Downloaded: 1456 file(s) [attempted 1456/8459 = 17%, 226 KB/s], Decompressed: 1449
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 246 KB/s], Decompressed: 1494
Downloaded: 1542 file(s) [attempted 1542/8459 = 18%, 330 KB/s], Decompressed: 1538
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 141 KB/s], Decompressed: 1579
Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 1701 KB/s], Decompressed: 1613
Downloaded: 1666 file(s) [attempted 1666/8459 = 19%, 451 KB/s], Decompressed: 1651
Downloaded: 1699 file(s) [attempted 1699/8459 = 20%, 468 KB/s], Decompressed: 1696
Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 89 KB/s], Decompressed: 1740
Downloaded: 1788 file(s) [attempted 1788/8459 = 21%, 262 KB/s], Decompressed: 1785
Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 689 KB/s], Decompressed: 1788
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 283 KB/s], Decompressed: 1788
Downloaded: 1901 file(s) [attempted 1901/8459 = 22%, 539 KB/s], Decompressed: 1897
Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 425 KB/s], Decompressed: 1939
Downloaded: 1986 file(s) [attempted 1986/8459 = 23%, 122 KB/s], Decompressed: 1976
Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 51 KB/s], Decompressed: 2021
Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 127 KB/s], Decompressed: 2058
Downloaded: 2106 file(s) [attempted 2106/8459 = 24%, 457 KB/s], Decompressed: 2103
Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 172 KB/s], Decompressed: 2147
Downloaded: 2196 file(s) [attempted 2196/8459 = 25%, 328 KB/s], Decompressed: 2192
Downloaded: 2239 file(s) [attempted 2239/8459 = 26%, 119 KB/s], Decompressed: 2229
Downloaded: 2274 file(s) [attempted 2274/8459 = 26%, 889 KB/s], Decompressed: 2271
Downloaded: 2315 file(s) [attempted 2315/8459 = 27%, 35 KB/s], Decompressed: 2305
Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 334 KB/s], Decompressed: 2349
Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 318 KB/s], Decompressed: 2390
Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 470 KB/s], Decompressed: 2425
Downloaded: 2469 file(s) [attempted 2469/8459 = 29%, 470 KB/s], Decompressed: 2462
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 151 KB/s], Decompressed: 2503
Downloaded: 2551 file(s) [attempted 2551/8459 = 30%, 101 KB/s], Decompressed: 2548
Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 365 KB/s], Decompressed: 2585
Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 23 KB/s], Decompressed: 2623
Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 169 KB/s], Decompressed: 2657
Downloaded: 2705 file(s) [attempted 2705/8459 = 31%, 478 KB/s], Decompressed: 2678
Downloaded: 2750 file(s) [attempted 2750/8459 = 32%, 126 KB/s], Decompressed: 2678
Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 767 KB/s], Decompressed: 2685
Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 560 KB/s], Decompressed: 2685
Downloaded: 2863 file(s) [attempted 2863/8459 = 33%, 243 KB/s], Decompressed: 2685
Downloaded: 2904 file(s) [attempted 2904/8459 = 34%, 929 KB/s], Decompressed: 2685
Downloaded: 2948 file(s) [attempted 2948/8459 = 34%, 2450 KB/s], Decompressed: 2685
Downloaded: 2993 file(s) [attempted 2993/8459 = 35%, 198 KB/s], Decompressed: 2685
Downloaded: 3038 file(s) [attempted 3038/8459 = 35%, 297 KB/s], Decompressed: 2760
Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 229 KB/s], Decompressed: 2760
Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 691 KB/s], Decompressed: 3109
Downloaded: 3153 file(s) [attempted 3153/8459 = 37%, 535 KB/s], Decompressed: 3150
Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 86 KB/s], Decompressed: 3191
Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 194 KB/s], Decompressed: 3229
Downloaded: 3284 file(s) [attempted 3284/8459 = 38%, 222 KB/s], Decompressed: 3273
Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 86 KB/s], Decompressed: 3304
Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 274 KB/s], Decompressed: 3349
Downloaded: 3398 file(s) [attempted 3398/8459 = 40%, 827 KB/s], Decompressed: 3390
Downloaded: 3441 file(s) [attempted 3441/8459 = 40%, 67 KB/s], Decompressed: 3438
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 194 KB/s], Decompressed: 3472
Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 70 KB/s], Decompressed: 3472
Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 706 KB/s], Decompressed: 3482
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 120 KB/s], Decompressed: 3595
Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 205 KB/s], Decompressed: 3595
Downloaded: 3691 file(s) [attempted 3691/8459 = 43%, 196 KB/s], Decompressed: 3598
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 402 KB/s], Decompressed: 3715
Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 636 KB/s], Decompressed: 3756
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 49 KB/s], Decompressed: 3804
Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 419 KB/s], Decompressed: 3841
Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 332 KB/s], Decompressed: 3886
Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 230 KB/s], Decompressed: 3896
Downloaded: 3971 file(s) [attempted 3971/8459 = 46%, 447 KB/s], Decompressed: 3896
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 47 KB/s], Decompressed: 3989
Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 137 KB/s], Decompressed: 4043
Downloaded: 4091 file(s) [attempted 4091/8459 = 48%, 1340 KB/s], Decompressed: 4084
Downloaded: 4136 file(s) [attempted 4136/8459 = 48%, 195 KB/s], Decompressed: 4084
Downloaded: 4173 file(s) [attempted 4173/8459 = 49%, 1131 KB/s], Decompressed: 4084
Downloaded: 4214 file(s) [attempted 4214/8459 = 49%, 925 KB/s], Decompressed: 4091
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 883 KB/s], Decompressed: 4091
Downloaded: 4293 file(s) [attempted 4293/8459 = 50%, 592 KB/s], Decompressed: 4180
Downloaded: 4338 file(s) [attempted 4338/8459 = 51%, 219 KB/s], Decompressed: 4334
Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 845 KB/s], Decompressed: 4379
Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 136 KB/s], Decompressed: 4416
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 112 KB/s], Decompressed: 4461
Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 195 KB/s], Decompressed: 4502
Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 437 KB/s], Decompressed: 4540
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 163 KB/s], Decompressed: 4581
Downloaded: 4626 file(s) [attempted 4626/8459 = 54%, 155 KB/s], Decompressed: 4618
Downloaded: 4663 file(s) [attempted 4663/8459 = 55%, 1210 KB/s], Decompressed: 4652
Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 25 KB/s], Decompressed: 4697
Downloaded: 4748 file(s) [attempted 4748/8459 = 56%, 149 KB/s], Decompressed: 4736
Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 360 KB/s], Decompressed: 4786
Downloaded: 4834 file(s) [attempted 4834/8459 = 57%, 273 KB/s], Decompressed: 4827
Downloaded: 4868 file(s) [attempted 4868/8459 = 57%, 164 KB/s], Decompressed: 4861
Downloaded: 4909 file(s) [attempted 4909/8459 = 58%, 61 KB/s], Decompressed: 4882
Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 456 KB/s], Decompressed: 4947
Downloaded: 4991 file(s) [attempted 4991/8459 = 59%, 1094 KB/s], Decompressed: 4984
Downloaded: 5036 file(s) [attempted 5036/8459 = 59%, 209 KB/s], Decompressed: 5026
Downloaded: 5067 file(s) [attempted 5067/8459 = 59%, 284 KB/s], Decompressed: 5060
Downloaded: 5111 file(s) [attempted 5111/8459 = 60%, 152 KB/s], Decompressed: 5108
Downloaded: 5156 file(s) [attempted 5156/8459 = 60%, 1281 KB/s], Decompressed: 5145
Downloaded: 5193 file(s) [attempted 5193/8459 = 61%, 137 KB/s], Decompressed: 5190
Downloaded: 5238 file(s) [attempted 5238/8459 = 61%, 1642 KB/s], Decompressed: 5231
Downloaded: 5279 file(s) [attempted 5279/8459 = 62%, 304 KB/s], Decompressed: 5272
Downloaded: 5317 file(s) [attempted 5317/8459 = 62%, 1274 KB/s], Decompressed: 5310
Downloaded: 5357 file(s) [attempted 5357/8459 = 63%, 1074 KB/s], Decompressed: 5354
Downloaded: 5396 file(s) [attempted 5396/8459 = 63%, 493 KB/s], Decompressed: 5388
Downloaded: 5436 file(s) [attempted 5436/8459 = 64%, 274 KB/s], Decompressed: 5419
Downloaded: 5477 file(s) [attempted 5477/8459 = 64%, 68 KB/s], Decompressed: 5470
Downloaded: 5518 file(s) [attempted 5518/8459 = 65%, 448 KB/s], Decompressed: 5515
Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 132 KB/s], Decompressed: 5559
Downloaded: 5604 file(s) [attempted 5604/8459 = 66%, 289 KB/s], Decompressed: 5590
Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 548 KB/s], Decompressed: 5638
Downloaded: 5683 file(s) [attempted 5683/8459 = 67%, 133 KB/s], Decompressed: 5672
Downloaded: 5726 file(s) [attempted 5726/8459 = 67%, 485 KB/s], Decompressed: 5717
Downloaded: 5765 file(s) [attempted 5765/8459 = 68%, 762 KB/s], Decompressed: 5754
Downloaded: 5806 file(s) [attempted 5806/8459 = 68%, 119 KB/s], Decompressed: 5802
Downloaded: 5847 file(s) [attempted 5847/8459 = 69%, 133 KB/s], Decompressed: 5833
Downloaded: 5882 file(s) [attempted 5882/8459 = 69%, 51 KB/s], Decompressed: 5878
Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 732 KB/s], Decompressed: 5915
Downloaded: 5967 file(s) [attempted 5967/8459 = 70%, 96 KB/s], Decompressed: 5915
Downloaded: 6005 file(s) [attempted 6005/8459 = 70%, 1126 KB/s], Decompressed: 5915
Downloaded: 6045 file(s) [attempted 6045/8459 = 71%, 106 KB/s], Decompressed: 6035
Downloaded: 6086 file(s) [attempted 6086/8459 = 71%, 317 KB/s], Decompressed: 6076
Downloaded: 6127 file(s) [attempted 6127/8459 = 72%, 159 KB/s], Decompressed: 6121
Downloaded: 6172 file(s) [attempted 6172/8459 = 72%, 121 KB/s], Decompressed: 6162
Downloaded: 6210 file(s) [attempted 6210/8459 = 73%, 723 KB/s], Decompressed: 6206
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 38 KB/s], Decompressed: 6220
Downloaded: 6299 file(s) [attempted 6299/8459 = 74%, 243 KB/s], Decompressed: 6220
Downloaded: 6340 file(s) [attempted 6340/8459 = 74%, 690 KB/s], Decompressed: 6336
Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 125 KB/s], Decompressed: 6379
Downloaded: 6422 file(s) [attempted 6422/8459 = 75%, 280 KB/s], Decompressed: 6408
Downloaded: 6459 file(s) [attempted 6459/8459 = 76%, 1493 KB/s], Decompressed: 6446
Downloaded: 6504 file(s) [attempted 6504/8459 = 76%, 101 KB/s], Decompressed: 6446
Downloaded: 6548 file(s) [attempted 6548/8459 = 77%, 109 KB/s], Decompressed: 6449
Downloaded: 6593 file(s) [attempted 6593/8459 = 77%, 469 KB/s], Decompressed: 6590
Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 374 KB/s], Decompressed: 6631
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 80 KB/s], Decompressed: 6655
Downloaded: 6706 file(s) [attempted 6706/8459 = 79%, 476 KB/s], Decompressed: 6702
Downloaded: 6750 file(s) [attempted 6750/8459 = 79%, 48 KB/s], Decompressed: 6747
Downloaded: 6798 file(s) [attempted 6798/8459 = 80%, 205 KB/s], Decompressed: 6791
Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 545 KB/s], Decompressed: 6815
Downloaded: 6884 file(s) [attempted 6884/8459 = 81%, 2098 KB/s], Decompressed: 6860
Downloaded: 6917 file(s) [attempted 6917/8459 = 81%, 420 KB/s], Decompressed: 6901
Downloaded: 6956 file(s) [attempted 6956/8459 = 82%, 174 KB/s], Decompressed: 6952
Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 1929 KB/s], Decompressed: 6973
Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 1919 KB/s], Decompressed: 6973
Downloaded: 7075 file(s) [attempted 7075/8459 = 83%, 195 KB/s], Decompressed: 6987
Downloaded: 7120 file(s) [attempted 7120/8459 = 84%, 177 KB/s], Decompressed: 7113
Downloaded: 7164 file(s) [attempted 7164/8459 = 84%, 482 KB/s], Decompressed: 7158
Downloaded: 7206 file(s) [attempted 7206/8459 = 85%, 875 KB/s], Decompressed: 7202
Downloaded: 7247 file(s) [attempted 7247/8459 = 85%, 119 KB/s], Decompressed: 7243
Downloaded: 7284 file(s) [attempted 7284/8459 = 86%, 170 KB/s], Decompressed: 7277
Downloaded: 7325 file(s) [attempted 7325/8459 = 86%, 319 KB/s], Decompressed: 7318
Downloaded: 7370 file(s) [attempted 7370/8459 = 87%, 78 KB/s], Decompressed: 7366
Downloaded: 7411 file(s) [attempted 7411/8459 = 87%, 128 KB/s], Decompressed: 7404
Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 111 KB/s], Decompressed: 7442
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 284 KB/s], Decompressed: 7486
Downloaded: 7527 file(s) [attempted 7527/8459 = 88%, 180 KB/s], Decompressed: 7514
Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 462 KB/s], Decompressed: 7514
Downloaded: 7616 file(s) [attempted 7616/8459 = 90%, 33 KB/s], Decompressed: 7609
Downloaded: 7655 file(s) [attempted 7655/8459 = 90%, 431 KB/s], Decompressed: 7650
Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 874 KB/s], Decompressed: 7692
Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 135 KB/s], Decompressed: 7726
Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 88 KB/s], Decompressed: 7767
Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 231 KB/s], Decompressed: 7811
Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 161 KB/s], Decompressed: 7863
Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 224 KB/s], Decompressed: 7900
Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 132 KB/s], Decompressed: 7945
Downloaded: 7993 file(s) [attempted 7993/8459 = 94%, 127 KB/s], Decompressed: 7986
Downloaded: 8024 file(s) [attempted 8024/8459 = 94%, 170 KB/s], Decompressed: 8020
Downloaded: 8071 file(s) [attempted 8071/8459 = 95%, 812 KB/s], Decompressed: 8068
Downloaded: 8116 file(s) [attempted 8116/8459 = 95%, 658 KB/s], Decompressed: 8109
Downloaded: 8153 file(s) [attempted 8153/8459 = 96%, 75 KB/s], Decompressed: 8150
Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 154 KB/s], Decompressed: 8195
Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 239 KB/s], Decompressed: 8215
Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 723 KB/s], Decompressed: 8215
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 684 KB/s], Decompressed: 8321
Downloaded: 8369 file(s) [attempted 8369/8459 = 98%, 468 KB/s], Decompressed: 8362
Downloaded: 8405 file(s) [attempted 8405/8459 = 99%, 596 KB/s], Decompressed: 8396
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 110 KB/s], Decompressed: 8438
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 110 KB/s], Decompressed: 8451


$ lake build
exit_code=Some(0) duration_ms=556383
stdout:
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (433s)
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) [0x74ee3bbc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x74ee3bbbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x74ee3bbbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x74ee3baf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x74ee3baf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x74ee3bbcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x74ee3ba32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x74ee3ba32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x74ee3ba33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x74ee3ba341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x74ee3bbc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x74ee3b815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x74ee3bbc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x74ee3bbc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x74ee3bb9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x74ee3b815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x74ee36c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x74ee36a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x74ee36569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x74ee36569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x74ee3344524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x74ee33445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x62f14a8168da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (28s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.7s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (37s)
✔ [3414/3416] Built Iut.Basic (2.9s)
✔ [3415/3416] Built Iut (2.7s)
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=3706
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=10369145
stdout:
apx-semantic-phase	{"duration_ms":3,"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":359673,"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":94,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":357494,"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":0,"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":7638,"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":358652,"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":3,"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":1890,"diagnostic_count":116,"duration_ms":1556132,"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":369399,"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":1890,"diagnostic_count":116,"duration_ms":111,"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":43182777,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":27,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":43182777,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":7804,"diagnostic_count":3119,"duration_ms":6201167,"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":432359,"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":568,"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":187,"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":19930,"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":687062,"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":28,"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":7,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1647482,"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":3493}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":997,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":21,"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":4303,"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 eb4ab944cd7296b3dd740e7a5c23f2d20af8c66ab56098012314a22d01cf18c9
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":10359244,"ok":true}

Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

git_clone exit 0 duration 3s · created 
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-537-source
Cloning into '/var/lib/apodeixis/repos/job-537-source'...
git_checkout exit 128 duration 4 ms · created 
git checkout 4dbaeefd0b2318363be5f0e8efd077d6497c387d
fatal: reference is not a tree: 4dbaeefd0b2318363be5f0e8efd077d6497c387d
git_checkout exit 0 duration 1s · created 
git fetch --depth 1 origin 4dbaeefd0b2318363be5f0e8efd077d6497c387d
From https://github.com/promachina/iut-lean
 * branch            4dbaeefd0b2318363be5f0e8efd077d6497c387d -> FETCH_HEAD
git_checkout exit 0 duration 140 ms · created 
git checkout 4dbaeefd0b2318363be5f0e8efd077d6497c387d (after fetch)
Note: switching to '4dbaeefd0b2318363be5f0e8efd077d6497c387d'.

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 4dbaeef Project local log factors through product coordinates
lake_cache exit 0 duration 1m 16s · created 
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%, 14 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 23 KB/s], Decompressed: 13
Downloaded: 42 file(s) [attempted 42/8459 = 0%, 86 KB/s], Decompressed: 41
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 44 KB/s], Decompressed: 61
Downloaded: 100 file(s) [attempted 100/8459 = 1%, 321 KB/s], Decompressed: 75
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 260 KB/s], Decompressed: 75
Downloaded: 169 file(s) [attempted 169/8459 = 1%, 678 KB/s], Decompressed: 162
Downloaded: 206 file(s) [attempted 206/8459 = 2%, 31 KB/s], Decompressed: 186
Downloaded: 247 file(s) [attempted 247/8459 = 2%, 24 KB/s], Decompressed: 186
Downloaded: 292 file(s) [attempted 292/8459 = 3%, 96 KB/s], Decompressed: 288
Downloaded: 329 file(s) [attempted 329/8459 = 3%, 301 KB/s], Decompressed: 326
Downloaded: 371 file(s) [attempted 371/8459 = 4%, 277 KB/s], Decompressed: 367
Downloaded: 408 file(s) [attempted 408/8459 = 4%, 60 KB/s], Decompressed: 405
Downloaded: 443 file(s) [attempted 443/8459 = 5%, 1724 KB/s], Decompressed: 439
Downloaded: 487 file(s) [attempted 487/8459 = 5%, 281 KB/s], Decompressed: 480
Downloaded: 529 file(s) [attempted 529/8459 = 6%, 269 KB/s], Decompressed: 525
Downloaded: 570 file(s) [attempted 570/8459 = 6%, 23 KB/s], Decompressed: 566
Downloaded: 610 file(s) [attempted 610/8459 = 7%, 135 KB/s], Decompressed: 603
Downloaded: 648 file(s) [attempted 648/8459 = 7%, 133 KB/s], Decompressed: 614
Downloaded: 682 file(s) [attempted 682/8459 = 8%, 569 KB/s], Decompressed: 614
Downloaded: 730 file(s) [attempted 730/8459 = 8%, 71 KB/s], Decompressed: 727
Downloaded: 775 file(s) [attempted 775/8459 = 9%, 195 KB/s], Decompressed: 768
Downloaded: 816 file(s) [attempted 816/8459 = 9%, 107 KB/s], Decompressed: 812
Downloaded: 857 file(s) [attempted 857/8459 = 10%, 122 KB/s], Decompressed: 854
Downloaded: 898 file(s) [attempted 898/8459 = 10%, 184 KB/s], Decompressed: 891
Downloaded: 932 file(s) [attempted 932/8459 = 11%, 1001 KB/s], Decompressed: 929
Downloaded: 977 file(s) [attempted 977/8459 = 11%, 753 KB/s], Decompressed: 973
Downloaded: 1018 file(s) [attempted 1018/8459 = 12%, 238 KB/s], Decompressed: 1015
Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 141 KB/s], Decompressed: 1052
Downloaded: 1097 file(s) [attempted 1097/8459 = 12%, 694 KB/s], Decompressed: 1090
Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 70 KB/s], Decompressed: 1127
Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 770 KB/s], Decompressed: 1127
Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 380 KB/s], Decompressed: 1131
Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 204 KB/s], Decompressed: 1240
Downloaded: 1299 file(s) [attempted 1299/8459 = 15%, 214 KB/s], Decompressed: 1295
Downloaded: 1340 file(s) [attempted 1340/8459 = 15%, 1157 KB/s], Decompressed: 1336
Downloaded: 1379 file(s) [attempted 1379/8459 = 16%, 198 KB/s], Decompressed: 1374
Downloaded: 1422 file(s) [attempted 1422/8459 = 16%, 81 KB/s], Decompressed: 1415
Downloaded: 1456 file(s) [attempted 1456/8459 = 17%, 226 KB/s], Decompressed: 1449
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 246 KB/s], Decompressed: 1494
Downloaded: 1542 file(s) [attempted 1542/8459 = 18%, 330 KB/s], Decompressed: 1538
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 141 KB/s], Decompressed: 1579
Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 1701 KB/s], Decompressed: 1613
Downloaded: 1666 file(s) [attempted 1666/8459 = 19%, 451 KB/s], Decompressed: 1651
Downloaded: 1699 file(s) [attempted 1699/8459 = 20%, 468 KB/s], Decompressed: 1696
Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 89 KB/s], Decompressed: 1740
Downloaded: 1788 file(s) [attempted 1788/8459 = 21%, 262 KB/s], Decompressed: 1785
Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 689 KB/s], Decompressed: 1788
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 283 KB/s], Decompressed: 1788
Downloaded: 1901 file(s) [attempted 1901/8459 = 22%, 539 KB/s], Decompressed: 1897
Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 425 KB/s], Decompressed: 1939
Downloaded: 1986 file(s) [attempted 1986/8459 = 23%, 122 KB/s], Decompressed: 1976
Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 51 KB/s], Decompressed: 2021
Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 127 KB/s], Decompressed: 2058
Downloaded: 2106 file(s) [attempted 2106/8459 = 24%, 457 KB/s], Decompressed: 2103
Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 172 KB/s], Decompressed: 2147
Downloaded: 2196 file(s) [attempted 2196/8459 = 25%, 328 KB/s], Decompressed: 2192
Downloaded: 2239 file(s) [attempted 2239/8459 = 26%, 119 KB/s], Decompressed: 2229
Downloaded: 2274 file(s) [attempted 2274/8459 = 26%, 889 KB/s], Decompressed: 2271
Downloaded: 2315 file(s) [attempted 2315/8459 = 27%, 35 KB/s], Decompressed: 2305
Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 334 KB/s], Decompressed: 2349
Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 318 KB/s], Decompressed: 2390
Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 470 KB/s], Decompressed: 2425
Downloaded: 2469 file(s) [attempted 2469/8459 = 29%, 470 KB/s], Decompressed: 2462
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 151 KB/s], Decompressed: 2503
Downloaded: 2551 file(s) [attempted 2551/8459 = 30%, 101 KB/s], Decompressed: 2548
Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 365 KB/s], Decompressed: 2585
Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 23 KB/s], Decompressed: 2623
Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 169 KB/s], Decompressed: 2657
Downloaded: 2705 file(s) [attempted 2705/8459 = 31%, 478 KB/s], Decompressed: 2678
Downloaded: 2750 file(s) [attempted 2750/8459 = 32%, 126 KB/s], Decompressed: 2678
Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 767 KB/s], Decompressed: 2685
Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 560 KB/s], Decompressed: 2685
Downloaded: 2863 file(s) [attempted 2863/8459 = 33%, 243 KB/s], Decompressed: 2685
Downloaded: 2904 file(s) [attempted 2904/8459 = 34%, 929 KB/s], Decompressed: 2685
Downloaded: 2948 file(s) [attempted 2948/8459 = 34%, 2450 KB/s], Decompressed: 2685
Downloaded: 2993 file(s) [attempted 2993/8459 = 35%, 198 KB/s], Decompressed: 2685
Downloaded: 3038 file(s) [attempted 3038/8459 = 35%, 297 KB/s], Decompressed: 2760
Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 229 KB/s], Decompressed: 2760
Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 691 KB/s], Decompressed: 3109
Downloaded: 3153 file(s) [attempted 3153/8459 = 37%, 535 KB/s], Decompressed: 3150
Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 86 KB/s], Decompressed: 3191
Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 194 KB/s], Decompressed: 3229
Downloaded: 3284 file(s) [attempted 3284/8459 = 38%, 222 KB/s], Decompressed: 3273
Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 86 KB/s], Decompressed: 3304
Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 274 KB/s], Decompressed: 3349
Downloaded: 3398 file(s) [attempted 3398/8459 = 40%, 827 KB/s], Decompressed: 3390
Downloaded: 3441 file(s) [attempted 3441/8459 = 40%, 67 KB/s], Decompressed: 3438
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 194 KB/s], Decompressed: 3472
Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 70 KB/s], Decompressed: 3472
Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 706 KB/s], Decompressed: 3482
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 120 KB/s], Decompressed: 3595
Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 205 KB/s], Decompressed: 3595
Downloaded: 3691 file(s) [attempted 3691/8459 = 43%, 196 KB/s], Decompressed: 3598
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 402 KB/s], Decompressed: 3715
Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 636 KB/s], Decompressed: 3756
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 49 KB/s], Decompressed: 3804
Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 419 KB/s], Decompressed: 3841
Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 332 KB/s], Decompressed: 3886
Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 230 KB/s], Decompressed: 3896
Downloaded: 3971 file(s) [attempted 3971/8459 = 46%, 447 KB/s], Decompressed: 3896
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 47 KB/s], Decompressed: 3989
Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 137 KB/s], Decompressed: 4043
Downloaded: 4091 file(s) [attempted 4091/8459 = 48%, 1340 KB/s], Decompressed: 4084
Downloaded: 4136 file(s) [attempted 4136/8459 = 48%, 195 KB/s], Decompressed: 4084
Downloaded: 4173 file(s) [attempted 4173/8459 = 49%, 1131 KB/s], Decompressed: 4084
Downloaded: 4214 file(s) [attempted 4214/8459 = 49%, 925 KB/s], Decompressed: 4091
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 883 KB/s], Decompressed: 4091
Downloaded: 4293 file(s) [attempted 4293/8459 = 50%, 592 KB/s], Decompressed: 4180
Downloaded: 4338 file(s) [attempted 4338/8459 = 51%, 219 KB/s], Decompressed: 4334
Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 845 KB/s], Decompressed: 4379
Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 136 KB/s], Decompressed: 4416
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 112 KB/s], Decompressed: 4461
Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 195 KB/s], Decompressed: 4502
Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 437 KB/s], Decompressed: 4540
Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 163 KB/s], Decompressed: 4581
Downloaded: 4626 file(s) [attempted 4626/8459 = 54%, 155 KB/s], Decompressed: 4618
Downloaded: 4663 file(s) [attempted 4663/8459 = 55%, 1210 KB/s], Decompressed: 4652
Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 25 KB/s], Decompressed: 4697
Downloaded: 4748 file(s) [attempted 4748/8459 = 56%, 149 KB/s], Decompressed: 4736
Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 360 KB/s], Decompressed: 4786
Downloaded: 4834 file(s) [attempted 4834/8459 = 57%, 273 KB/s], Decompressed: 4827
Downloaded: 4868 file(s) [attempted 4868/8459 = 57%, 164 KB/s], Decompressed: 4861
Downloaded: 4909 file(s) [attempted 4909/8459 = 58%, 61 KB/s], Decompressed: 4882
Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 456 KB/s], Decompressed: 4947
Downloaded: 4991 file(s) [attempted 4991/8459 = 59%, 1094 KB/s], Decompressed: 4984
Downloaded: 5036 file(s) [attempted 5036/8459 = 59%, 209 KB/s], Decompressed: 5026
Downloaded: 5067 file(s) [attempted 5067/8459 = 59%, 284 KB/s], Decompressed: 5060
Downloaded: 5111 file(s) [attempted 5111/8459 = 60%, 152 KB/s], Decompressed: 5108
Downloaded: 5156 file(s) [attempted 5156/8459 = 60%, 1281 KB/s], Decompressed: 5145
Downloaded: 5193 file(s) [attempted 5193/8459 = 61%, 137 KB/s], Decompressed: 5190
Downloaded: 5238 file(s) [attempted 5238/8459 = 61%, 1642 KB/s], Decompressed: 5231
Downloaded: 5279 file(s) [attempted 5279/8459 = 62%, 304 KB/s], Decompressed: 5272
Downloaded: 5317 file(s) [attempted 5317/8459 = 62%, 1274 KB/s], Decompressed: 5310
Downloaded: 5357 file(s) [attempted 5357/8459 = 63%, 1074 KB/s], Decompressed: 5354
Downloaded: 5396 file(s) [attempted 5396/8459 = 63%, 493 KB/s], Decompressed: 5388
Downloaded: 5436 file(s) [attempted 5436/8459 = 64%, 274 KB/s], Decompressed: 5419
Downloaded: 5477 file(s) [attempted 5477/8459 = 64%, 68 KB/s], Decompressed: 5470
Downloaded: 5518 file(s) [attempted 5518/8459 = 65%, 448 KB/s], Decompressed: 5515
Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 132 KB/s], Decompressed: 5559
Downloaded: 5604 file(s) [attempted 5604/8459 = 66%, 289 KB/s], Decompressed: 5590
Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 548 KB/s], Decompressed: 5638
Downloaded: 5683 file(s) [attempted 5683/8459 = 67%, 133 KB/s], Decompressed: 5672
Downloaded: 5726 file(s) [attempted 5726/8459 = 67%, 485 KB/s], Decompressed: 5717
Downloaded: 5765 file(s) [attempted 5765/8459 = 68%, 762 KB/s], Decompressed: 5754
Downloaded: 5806 file(s) [attempted 5806/8459 = 68%, 119 KB/s], Decompressed: 5802
Downloaded: 5847 file(s) [attempted 5847/8459 = 69%, 133 KB/s], Decompressed: 5833
Downloaded: 5882 file(s) [attempted 5882/8459 = 69%, 51 KB/s], Decompressed: 5878
Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 732 KB/s], Decompressed: 5915
Downloaded: 5967 file(s) [attempted 5967/8459 = 70%, 96 KB/s], Decompressed: 5915
Downloaded: 6005 file(s) [attempted 6005/8459 = 70%, 1126 KB/s], Decompressed: 5915
Downloaded: 6045 file(s) [attempted 6045/8459 = 71%, 106 KB/s], Decompressed: 6035
Downloaded: 6086 file(s) [attempted 6086/8459 = 71%, 317 KB/s], Decompressed: 6076
Downloaded: 6127 file(s) [attempted 6127/8459 = 72%, 159 KB/s], Decompressed: 6121
Downloaded: 6172 file(s) [attempted 6172/8459 = 72%, 121 KB/s], Decompressed: 6162
Downloaded: 6210 file(s) [attempted 6210/8459 = 73%, 723 KB/s], Decompressed: 6206
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 38 KB/s], Decompressed: 6220
Downloaded: 6299 file(s) [attempted 6299/8459 = 74%, 243 KB/s], Decompressed: 6220
Downloaded: 6340 file(s) [attempted 6340/8459 = 74%, 690 KB/s], Decompressed: 6336
Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 125 KB/s], Decompressed: 6379
Downloaded: 6422 file(s) [attempted 6422/8459 = 75%, 280 KB/s], Decompressed: 6408
Downloaded: 6459 file(s) [attempted 6459/8459 = 76%, 1493 KB/s], Decompressed: 6446
Downloaded: 6504 file(s) [attempted 6504/8459 = 76%, 101 KB/s], Decompressed: 6446
Downloaded: 6548 file(s) [attempted 6548/8459 = 77%, 109 KB/s], Decompressed: 6449
Downloaded: 6593 file(s) [attempted 6593/8459 = 77%, 469 KB/s], Decompressed: 6590
Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 374 KB/s], Decompressed: 6631
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 80 KB/s], Decompressed: 6655
Downloaded: 6706 file(s) [attempted 6706/8459 = 79%, 476 KB/s], Decompressed: 6702
Downloaded: 6750 file(s) [attempted 6750/8459 = 79%, 48 KB/s], Decompressed: 6747
Downloaded: 6798 file(s) [attempted 6798/8459 = 80%, 205 KB/s], Decompressed: 6791
Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 545 KB/s], Decompressed: 6815
Downloaded: 6884 file(s) [attempted 6884/8459 = 81%, 2098 KB/s], Decompressed: 6860
Downloaded: 6917 file(s) [attempted 6917/8459 = 81%, 420 KB/s], Decompressed: 6901
Downloaded: 6956 file(s) [attempted 6956/8459 = 82%, 174 KB/s], Decompressed: 6952
Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 1929 KB/s], Decompressed: 6973
Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 1919 KB/s], Decompressed: 6973
Downloaded: 7075 file(s) [attempted 7075/8459 = 83%, 195 KB/s], Decompressed: 6987
Downloaded: 7120 file(s) [attempted 7120/8459 = 84%, 177 KB/s], Decompressed: 7113
Downloaded: 7164 file(s) [attempted 7164/8459 = 84%, 482 KB/s], Decompressed: 7158
Downloaded: 7206 file(s) [attempted 7206/8459 = 85%, 875 KB/s], Decompressed: 7202
Downloaded: 7247 file(s) [attempted 7247/8459 = 85%, 119 KB/s], Decompressed: 7243
Downloaded: 7284 file(s) [attempted 7284/8459 = 86%, 170 KB/s], Decompressed: 7277
Downloaded: 7325 file(s) [attempted 7325/8459 = 86%, 319 KB/s], Decompressed: 7318
Downloaded: 7370 file(s) [attempted 7370/8459 = 87%, 78 KB/s], Decompressed: 7366
Downloaded: 7411 file(s) [attempted 7411/8459 = 87%, 128 KB/s], Decompressed: 7404
Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 111 KB/s], Decompressed: 7442
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 284 KB/s], Decompressed: 7486
Downloaded: 7527 file(s) [attempted 7527/8459 = 88%, 180 KB/s], Decompressed: 7514
Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 462 KB/s], Decompressed: 7514
Downloaded: 7616 file(s) [attempted 7616/8459 = 90%, 33 KB/s], Decompressed: 7609
Downloaded: 7655 file(s) [attempted 7655/8459 = 90%, 431 KB/s], Decompressed: 7650
Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 874 KB/s], Decompressed: 7692
Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 135 KB/s], Decompressed: 7726
Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 88 KB/s], Decompressed: 7767
Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 231 KB/s], Decompressed: 7811
Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 161 KB/s], Decompressed: 7863
Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 224 KB/s], Decompressed: 7900
Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 132 KB/s], Decompressed: 7945
Downloaded: 7993 file(s) [attempted 7993/8459 = 94%, 127 KB/s], Decompressed: 7986
Downloaded: 8024 file(s) [attempted 8024/8459 = 94%, 170 KB/s], Decompressed: 8020
Downloaded: 8071 file(s) [attempted 8071/8459 = 95%, 812 KB/s], Decompressed: 8068
Downloaded: 8116 file(s) [attempted 8116/8459 = 95%, 658 KB/s], Decompressed: 8109
Downloaded: 8153 file(s) [attempted 8153/8459 = 96%, 75 KB/s], Decompressed: 8150
Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 154 KB/s], Decompressed: 8195
Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 239 KB/s], Decompressed: 8215
Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 723 KB/s], Decompressed: 8215
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 684 KB/s], Decompressed: 8321
Downloaded: 8369 file(s) [attempted 8369/8459 = 98%, 468 KB/s], Decompressed: 8362
Downloaded: 8405 file(s) [attempted 8405/8459 = 99%, 596 KB/s], Decompressed: 8396
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 110 KB/s], Decompressed: 8438
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 110 KB/s], Decompressed: 8451
lean_checker exit 0 duration 9m 16s · created 
lake build
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (433s)
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) [0x74ee3bbc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x74ee3bbbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x74ee3bbbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x74ee3baf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x74ee3baf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x74ee3bbcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x74ee3ba32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x74ee3ba32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x74ee3ba33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x74ee3ba341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x74ee3bbc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x74ee3b815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x74ee3bbc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x74ee3bbc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x74ee3bb9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x74ee3b815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x74ee36c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x74ee36a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x74ee36569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x74ee36569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x74ee3344524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x74ee33445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x62f14a8168da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (28s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.7s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (37s)
✔ [3414/3416] Built Iut.Basic (2.9s)
✔ [3415/3416] Built Iut (2.7s)
Build completed successfully (3416 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
blueprint_build exit 1 duration 4s · created 
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 52m · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)
apx-semantic-phase	{"duration_ms":3,"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":359673,"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":94,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":357494,"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":0,"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":7638,"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":358652,"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":3,"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":1890,"diagnostic_count":116,"duration_ms":1556132,"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":369399,"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":1890,"diagnostic_count":116,"duration_ms":111,"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":43182777,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":27,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":43182777,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":7804,"diagnostic_count":3119,"duration_ms":6201167,"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":432359,"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":568,"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":187,"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":19930,"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":687062,"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":28,"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":7,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1647482,"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":3493}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":997,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":21,"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":4303,"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 eb4ab944cd7296b3dd740e7a5c23f2d20af8c66ab56098012314a22d01cf18c9
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":10359244,"ok":true}

Keyboard shortcuts