Run 363

Package inputs

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

Verifier log excerpt

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


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


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


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

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 a94d412 Project arbitrary q measure calibration from source

Resolved source revision: a94d4121a752df1afe89d3ed087a101ba25e5e76

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=a94d4121a752df1afe89d3ed087a101ba25e5e76 provenance={"branch":"master","checked_out_revision":"a94d4121a752df1afe89d3ed087a101ba25e5e76","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"a94d4121a752df1afe89d3ed087a101ba25e5e76","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=50975
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%, 3 KB/s], Decompressed: 11
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 17 KB/s], Decompressed: 36
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 97 KB/s], Decompressed: 61
Downloaded: 90 file(s) [attempted 90/8459 = 1%, 355 KB/s], Decompressed: 86
Downloaded: 128 file(s) [attempted 128/8459 = 1%, 280 KB/s], Decompressed: 121
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 856 KB/s], Decompressed: 151
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 125 KB/s], Decompressed: 192
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 219 KB/s], Decompressed: 223
Downloaded: 264 file(s) [attempted 264/8459 = 3%, 855 KB/s], Decompressed: 261
Downloaded: 309 file(s) [attempted 309/8459 = 3%, 812 KB/s], Decompressed: 302
Downloaded: 343 file(s) [attempted 343/8459 = 4%, 28 KB/s], Decompressed: 340
Downloaded: 383 file(s) [attempted 383/8459 = 4%, 214 KB/s], Decompressed: 374
Downloaded: 416 file(s) [attempted 416/8459 = 4%, 164 KB/s], Decompressed: 412
Downloaded: 456 file(s) [attempted 456/8459 = 5%, 289 KB/s], Decompressed: 449
Downloaded: 489 file(s) [attempted 489/8459 = 5%, 77 KB/s], Decompressed: 466
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 668 KB/s], Decompressed: 521
Downloaded: 566 file(s) [attempted 566/8459 = 6%, 445 KB/s], Decompressed: 562
Downloaded: 607 file(s) [attempted 607/8459 = 7%, 129 KB/s], Decompressed: 604
Downloaded: 648 file(s) [attempted 648/8459 = 7%, 143 KB/s], Decompressed: 645
Downloaded: 686 file(s) [attempted 686/8459 = 8%, 696 KB/s], Decompressed: 672
Downloaded: 720 file(s) [attempted 720/8459 = 8%, 46 KB/s], Decompressed: 713
Downloaded: 761 file(s) [attempted 761/8459 = 8%, 165 KB/s], Decompressed: 754
Downloaded: 802 file(s) [attempted 802/8459 = 9%, 943 KB/s], Decompressed: 771
Downloaded: 847 file(s) [attempted 847/8459 = 10%, 36 KB/s], Decompressed: 812
Downloaded: 891 file(s) [attempted 891/8459 = 10%, 75 KB/s], Decompressed: 884
Downloaded: 919 file(s) [attempted 919/8459 = 10%, 146 KB/s], Decompressed: 915
Downloaded: 960 file(s) [attempted 960/8459 = 11%, 129 KB/s], Decompressed: 953
Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 25 KB/s], Decompressed: 997
Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 573 KB/s], Decompressed: 1042
Downloaded: 1090 file(s) [attempted 1090/8459 = 12%, 62 KB/s], Decompressed: 1076
Downloaded: 1124 file(s) [attempted 1124/8459 = 13%, 326 KB/s], Decompressed: 1117
Downloaded: 1158 file(s) [attempted 1158/8459 = 13%, 141 KB/s], Decompressed: 1155
Downloaded: 1199 file(s) [attempted 1199/8459 = 14%, 2377 KB/s], Decompressed: 1196
Downloaded: 1240 file(s) [attempted 1240/8459 = 14%, 147 KB/s], Decompressed: 1237
Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 191 KB/s], Decompressed: 1278
Downloaded: 1326 file(s) [attempted 1326/8459 = 15%, 364 KB/s], Decompressed: 1319
Downloaded: 1364 file(s) [attempted 1364/8459 = 16%, 215 KB/s], Decompressed: 1347
Downloaded: 1398 file(s) [attempted 1398/8459 = 16%, 105 KB/s], Decompressed: 1394
Downloaded: 1442 file(s) [attempted 1442/8459 = 17%, 237 KB/s], Decompressed: 1439
Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 408 KB/s], Decompressed: 1477
Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 196 KB/s], Decompressed: 1511
Downloaded: 1567 file(s) [attempted 1567/8459 = 18%, 992 KB/s], Decompressed: 1559
Downloaded: 1597 file(s) [attempted 1597/8459 = 18%, 170 KB/s], Decompressed: 1593
Downloaded: 1634 file(s) [attempted 1634/8459 = 19%, 241 KB/s], Decompressed: 1631
Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 120 KB/s], Decompressed: 1668
Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 164 KB/s], Decompressed: 1709
Downloaded: 1750 file(s) [attempted 1750/8459 = 20%, 199 KB/s], Decompressed: 1740
Downloaded: 1788 file(s) [attempted 1788/8459 = 21%, 272 KB/s], Decompressed: 1781
Downloaded: 1826 file(s) [attempted 1826/8459 = 21%, 72 KB/s], Decompressed: 1819
Downloaded: 1863 file(s) [attempted 1863/8459 = 22%, 1696 KB/s], Decompressed: 1860
Downloaded: 1901 file(s) [attempted 1901/8459 = 22%, 149 KB/s], Decompressed: 1898
Downloaded: 1936 file(s) [attempted 1936/8459 = 22%, 67 KB/s], Decompressed: 1932
Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 382 KB/s], Decompressed: 1973
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 124 KB/s], Decompressed: 2000
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 181 KB/s], Decompressed: 2045
Downloaded: 2089 file(s) [attempted 2089/8459 = 24%, 73 KB/s], Decompressed: 2086
Downloaded: 2123 file(s) [attempted 2123/8459 = 25%, 272 KB/s], Decompressed: 2106
Downloaded: 2161 file(s) [attempted 2161/8459 = 25%, 202 KB/s], Decompressed: 2154
Downloaded: 2199 file(s) [attempted 2199/8459 = 25%, 91 KB/s], Decompressed: 2192
Downloaded: 2240 file(s) [attempted 2240/8459 = 26%, 111 KB/s], Decompressed: 2236
Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 210 KB/s], Decompressed: 2277
Downloaded: 2318 file(s) [attempted 2318/8459 = 27%, 391 KB/s], Decompressed: 2315
Downloaded: 2358 file(s) [attempted 2358/8459 = 27%, 72 KB/s], Decompressed: 2349
Downloaded: 2395 file(s) [attempted 2395/8459 = 28%, 35 KB/s], Decompressed: 2390
Downloaded: 2435 file(s) [attempted 2435/8459 = 28%, 75 KB/s], Decompressed: 2431
Downloaded: 2476 file(s) [attempted 2476/8459 = 29%, 356 KB/s], Decompressed: 2462
Downloaded: 2514 file(s) [attempted 2514/8459 = 29%, 127 KB/s], Decompressed: 2510
Downloaded: 2548 file(s) [attempted 2548/8459 = 30%, 85 KB/s], Decompressed: 2537
Downloaded: 2585 file(s) [attempted 2585/8459 = 30%, 279 KB/s], Decompressed: 2579
Downloaded: 2626 file(s) [attempted 2626/8459 = 31%, 397 KB/s], Decompressed: 2623
Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 676 KB/s], Decompressed: 2661
Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 901 KB/s], Decompressed: 2698
Downloaded: 2736 file(s) [attempted 2736/8459 = 32%, 571 KB/s], Decompressed: 2733
Downloaded: 2781 file(s) [attempted 2781/8459 = 32%, 52 KB/s], Decompressed: 2777
Downloaded: 2818 file(s) [attempted 2818/8459 = 33%, 93 KB/s], Decompressed: 2815
Downloaded: 2856 file(s) [attempted 2856/8459 = 33%, 32 KB/s], Decompressed: 2852
Downloaded: 2893 file(s) [attempted 2893/8459 = 34%, 455 KB/s], Decompressed: 2887
Downloaded: 2931 file(s) [attempted 2931/8459 = 34%, 615 KB/s], Decompressed: 2924
Downloaded: 2976 file(s) [attempted 2976/8459 = 35%, 597 KB/s], Decompressed: 2972
Downloaded: 3017 file(s) [attempted 3017/8459 = 35%, 614 KB/s], Decompressed: 3010
Downloaded: 3051 file(s) [attempted 3051/8459 = 36%, 318 KB/s], Decompressed: 3044
Downloaded: 3092 file(s) [attempted 3092/8459 = 36%, 365 KB/s], Decompressed: 3088
Downloaded: 3133 file(s) [attempted 3133/8459 = 37%, 1005 KB/s], Decompressed: 3126
Downloaded: 3171 file(s) [attempted 3171/8459 = 37%, 68 KB/s], Decompressed: 3167
Downloaded: 3213 file(s) [attempted 3213/8459 = 37%, 122 KB/s], Decompressed: 3210
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 243 KB/s], Decompressed: 3242
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 82 KB/s], Decompressed: 3280
Downloaded: 3332 file(s) [attempted 3332/8459 = 39%, 385 KB/s], Decompressed: 3318
Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 119 KB/s], Decompressed: 3359
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 199 KB/s], Decompressed: 3403
Downloaded: 3451 file(s) [attempted 3451/8459 = 40%, 86 KB/s], Decompressed: 3448
Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 186 KB/s], Decompressed: 3485
Downloaded: 3533 file(s) [attempted 3533/8459 = 41%, 142 KB/s], Decompressed: 3509
Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 395 KB/s], Decompressed: 3561
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 36 KB/s], Decompressed: 3604
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 123 KB/s], Decompressed: 3646
Downloaded: 3705 file(s) [attempted 3705/8459 = 43%, 1764 KB/s], Decompressed: 3694
Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 195 KB/s], Decompressed: 3749
Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 50 KB/s], Decompressed: 3787
Downloaded: 3828 file(s) [attempted 3828/8459 = 45%, 454 KB/s], Decompressed: 3817
Downloaded: 3864 file(s) [attempted 3864/8459 = 45%, 1267 KB/s], Decompressed: 3859
Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 64 KB/s], Decompressed: 3903
Downloaded: 3951 file(s) [attempted 3951/8459 = 46%, 350 KB/s], Decompressed: 3944
Downloaded: 3984 file(s) [attempted 3984/8459 = 47%, 1591 KB/s], Decompressed: 3978
Downloaded: 4018 file(s) [attempted 4018/8459 = 47%, 1743 KB/s], Decompressed: 4013
Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 386 KB/s], Decompressed: 4057
Downloaded: 4103 file(s) [attempted 4103/8459 = 48%, 40 KB/s], Decompressed: 4102
Downloaded: 4143 file(s) [attempted 4143/8459 = 48%, 959 KB/s], Decompressed: 4132
Downloaded: 4177 file(s) [attempted 4177/8459 = 49%, 59 KB/s], Decompressed: 4167
Downloaded: 4214 file(s) [attempted 4214/8459 = 49%, 69 KB/s], Decompressed: 4211
Downloaded: 4259 file(s) [attempted 4259/8459 = 50%, 394 KB/s], Decompressed: 4256
Downloaded: 4297 file(s) [attempted 4297/8459 = 50%, 889 KB/s], Decompressed: 4293
Downloaded: 4334 file(s) [attempted 4334/8459 = 51%, 309 KB/s], Decompressed: 4331
Downloaded: 4372 file(s) [attempted 4372/8459 = 51%, 276 KB/s], Decompressed: 4365
Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 103 KB/s], Decompressed: 4413
Downloaded: 4457 file(s) [attempted 4457/8459 = 52%, 36 KB/s], Decompressed: 4454
Downloaded: 4495 file(s) [attempted 4495/8459 = 53%, 244 KB/s], Decompressed: 4492
Downloaded: 4536 file(s) [attempted 4536/8459 = 53%, 1027 KB/s], Decompressed: 4533
Downloaded: 4572 file(s) [attempted 4572/8459 = 54%, 81 KB/s], Decompressed: 4564
Downloaded: 4615 file(s) [attempted 4615/8459 = 54%, 691 KB/s], Decompressed: 4605
Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 489 KB/s], Decompressed: 4646
Downloaded: 4690 file(s) [attempted 4690/8459 = 55%, 94 KB/s], Decompressed: 4687
Downloaded: 4733 file(s) [attempted 4733/8459 = 55%, 562 KB/s], Decompressed: 4718
Downloaded: 4771 file(s) [attempted 4771/8459 = 56%, 35 KB/s], Decompressed: 4748
Downloaded: 4808 file(s) [attempted 4808/8459 = 56%, 119 KB/s], Decompressed: 4803
Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 98 KB/s], Decompressed: 4841
Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 1056 KB/s], Decompressed: 4882
Downloaded: 4928 file(s) [attempted 4928/8459 = 58%, 134 KB/s], Decompressed: 4919
Downloaded: 4964 file(s) [attempted 4964/8459 = 58%, 84 KB/s], Decompressed: 4961
Downloaded: 4999 file(s) [attempted 4999/8459 = 59%, 235 KB/s], Decompressed: 4995
Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 184 KB/s], Decompressed: 5039
Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 138 KB/s], Decompressed: 5080
Downloaded: 5125 file(s) [attempted 5125/8459 = 60%, 44 KB/s], Decompressed: 5118
Downloaded: 5159 file(s) [attempted 5159/8459 = 60%, 60 KB/s], Decompressed: 5152
Downloaded: 5197 file(s) [attempted 5197/8459 = 61%, 37 KB/s], Decompressed: 5193
Downloaded: 5241 file(s) [attempted 5241/8459 = 61%, 98 KB/s], Decompressed: 5234
Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 1146 KB/s], Decompressed: 5279
Downloaded: 5327 file(s) [attempted 5327/8459 = 62%, 46 KB/s], Decompressed: 5320
Downloaded: 5361 file(s) [attempted 5361/8459 = 63%, 21 KB/s], Decompressed: 5358
Downloaded: 5399 file(s) [attempted 5399/8459 = 63%, 88 KB/s], Decompressed: 5395
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 974 KB/s], Decompressed: 5440
Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 157 KB/s], Decompressed: 5477
Downloaded: 5525 file(s) [attempted 5525/8459 = 65%, 499 KB/s], Decompressed: 5522
Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 78 KB/s], Decompressed: 5556
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 21 KB/s], Decompressed: 5597
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 28 KB/s], Decompressed: 5638
Downloaded: 5679 file(s) [attempted 5679/8459 = 67%, 604 KB/s], Decompressed: 5676
Downloaded: 5724 file(s) [attempted 5724/8459 = 67%, 162 KB/s], Decompressed: 5707
Downloaded: 5758 file(s) [attempted 5758/8459 = 68%, 204 KB/s], Decompressed: 5755
Downloaded: 5799 file(s) [attempted 5799/8459 = 68%, 108 KB/s], Decompressed: 5796
Downloaded: 5841 file(s) [attempted 5841/8459 = 69%, 142 KB/s], Decompressed: 5833
Downloaded: 5878 file(s) [attempted 5878/8459 = 69%, 151 KB/s], Decompressed: 5874
Downloaded: 5919 file(s) [attempted 5919/8459 = 69%, 75 KB/s], Decompressed: 5909
Downloaded: 5956 file(s) [attempted 5956/8459 = 70%, 487 KB/s], Decompressed: 5946
Downloaded: 5994 file(s) [attempted 5994/8459 = 70%, 243 KB/s], Decompressed: 5991
Downloaded: 6032 file(s) [attempted 6032/8459 = 71%, 80 KB/s], Decompressed: 6028
Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 242 KB/s], Decompressed: 6066
Downloaded: 6110 file(s) [attempted 6110/8459 = 72%, 287 KB/s], Decompressed: 6107
Downloaded: 6148 file(s) [attempted 6148/8459 = 72%, 44 KB/s], Decompressed: 6141
Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 203 KB/s], Decompressed: 6182
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 211 KB/s], Decompressed: 6223
Downloaded: 6271 file(s) [attempted 6271/8459 = 74%, 236 KB/s], Decompressed: 6264
Downloaded: 6312 file(s) [attempted 6312/8459 = 74%, 1142 KB/s], Decompressed: 6309
Downloaded: 6350 file(s) [attempted 6350/8459 = 75%, 316 KB/s], Decompressed: 6347
Downloaded: 6387 file(s) [attempted 6387/8459 = 75%, 434 KB/s], Decompressed: 6377
Downloaded: 6425 file(s) [attempted 6425/8459 = 75%, 146 KB/s], Decompressed: 6422
Downloaded: 6470 file(s) [attempted 6470/8459 = 76%, 186 KB/s], Decompressed: 6466
Downloaded: 6507 file(s) [attempted 6507/8459 = 76%, 434 KB/s], Decompressed: 6504
Downloaded: 6542 file(s) [attempted 6542/8459 = 77%, 647 KB/s], Decompressed: 6535
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 339 KB/s], Decompressed: 6569
Downloaded: 6622 file(s) [attempted 6622/8459 = 78%, 395 KB/s], Decompressed: 6617
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 79 KB/s], Decompressed: 6658
Downloaded: 6700 file(s) [attempted 6700/8459 = 79%, 119 KB/s], Decompressed: 6692
Downloaded: 6733 file(s) [attempted 6733/8459 = 79%, 304 KB/s], Decompressed: 6730
Downloaded: 6778 file(s) [attempted 6778/8459 = 80%, 38 KB/s], Decompressed: 6774
Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 119 KB/s], Decompressed: 6812
Downloaded: 6860 file(s) [attempted 6860/8459 = 81%, 583 KB/s], Decompressed: 6857
Downloaded: 6901 file(s) [attempted 6901/8459 = 81%, 438 KB/s], Decompressed: 6898
Downloaded: 6935 file(s) [attempted 6935/8459 = 81%, 72 KB/s], Decompressed: 6932
Downloaded: 6976 file(s) [attempted 6976/8459 = 82%, 112 KB/s], Decompressed: 6973
Downloaded: 7016 file(s) [attempted 7016/8459 = 82%, 62 KB/s], Decompressed: 7007
Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 100 KB/s], Decompressed: 7055
Downloaded: 7100 file(s) [attempted 7100/8459 = 83%, 68 KB/s], Decompressed: 7096
Downloaded: 7130 file(s) [attempted 7130/8459 = 84%, 966 KB/s], Decompressed: 7127
Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 970 KB/s], Decompressed: 7165
Downloaded: 7212 file(s) [attempted 7212/8459 = 85%, 23 KB/s], Decompressed: 7206
Downloaded: 7257 file(s) [attempted 7257/8459 = 85%, 358 KB/s], Decompressed: 7250
Downloaded: 7295 file(s) [attempted 7295/8459 = 86%, 35 KB/s], Decompressed: 7287
Downloaded: 7329 file(s) [attempted 7329/8459 = 86%, 452 KB/s], Decompressed: 7325
Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 120 KB/s], Decompressed: 7363
Downloaded: 7411 file(s) [attempted 7411/8459 = 87%, 77 KB/s], Decompressed: 7408
Downloaded: 7455 file(s) [attempted 7455/8459 = 88%, 232 KB/s], Decompressed: 7445
Downloaded: 7493 file(s) [attempted 7493/8459 = 88%, 310 KB/s], Decompressed: 7486
Downloaded: 7527 file(s) [attempted 7527/8459 = 88%, 177 KB/s], Decompressed: 7524
Downloaded: 7568 file(s) [attempted 7568/8459 = 89%, 444 KB/s], Decompressed: 7558
Downloaded: 7609 file(s) [attempted 7609/8459 = 89%, 221 KB/s], Decompressed: 7606
Downloaded: 7651 file(s) [attempted 7651/8459 = 90%, 252 KB/s], Decompressed: 7644
Downloaded: 7692 file(s) [attempted 7692/8459 = 90%, 45 KB/s], Decompressed: 7688
Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 592 KB/s], Decompressed: 7722
Downloaded: 7765 file(s) [attempted 7765/8459 = 91%, 97 KB/s], Decompressed: 7757
Downloaded: 7808 file(s) [attempted 7808/8459 = 92%, 34 KB/s], Decompressed: 7801
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 315 KB/s], Decompressed: 7846
Downloaded: 7887 file(s) [attempted 7887/8459 = 93%, 58 KB/s], Decompressed: 7876
Downloaded: 7924 file(s) [attempted 7924/8459 = 93%, 613 KB/s], Decompressed: 7921
Downloaded: 7959 file(s) [attempted 7959/8459 = 94%, 787 KB/s], Decompressed: 7955
Downloaded: 7997 file(s) [attempted 7997/8459 = 94%, 109 KB/s], Decompressed: 7993
Downloaded: 8041 file(s) [attempted 8041/8459 = 95%, 788 KB/s], Decompressed: 8037
Downloaded: 8082 file(s) [attempted 8082/8459 = 95%, 114 KB/s], Decompressed: 8078
Downloaded: 8116 file(s) [attempted 8116/8459 = 95%, 75 KB/s], Decompressed: 8102
Downloaded: 8150 file(s) [attempted 8150/8459 = 96%, 769 KB/s], Decompressed: 8147
Downloaded: 8195 file(s) [attempted 8195/8459 = 96%, 356 KB/s], Decompressed: 8191
Downloaded: 8239 file(s) [attempted 8239/8459 = 97%, 190 KB/s], Decompressed: 8236
Downloaded: 8277 file(s) [attempted 8277/8459 = 97%, 142 KB/s], Decompressed: 8273
Downloaded: 8314 file(s) [attempted 8314/8459 = 98%, 161 KB/s], Decompressed: 8304
Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 264 KB/s], Decompressed: 8349
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 88 KB/s], Decompressed: 8390
Downloaded: 8438 file(s) [attempted 8438/8459 = 99%, 309 KB/s], Decompressed: 8431
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 162 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 162 KB/s], Decompressed: 8455


$ lake build
exit_code=Some(0) duration_ms=308834
stdout:
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (212s)
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) [0x77bcfdbc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x77bcfdbbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x77bcfdbbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x77bcfdaf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x77bcfdaf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x77bcfdbcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x77bcfda32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x77bcfda32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x77bcfda33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x77bcfda341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x77bcfdbc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x77bcfd815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x77bcfdbc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x77bcfdbc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x77bcfdb9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x77bcfd815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x77bcf8c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x77bcf8a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x77bcf8569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x77bcf8569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x77bcf544524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x77bcf5445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x59b03cb278da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (23s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.2s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (37s)
✔ [3414/3416] Built Iut.Basic (2.6s)
✔ [3415/3416] Built Iut (2.5s)
Build completed successfully (3416 jobs).

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


$ lake build :blueprint
exit_code=Some(1) duration_ms=3016
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=10432898
stdout:
apx-semantic-phase	{"duration_ms":3,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":10,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":326408,"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":1,"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":79,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":329534,"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":7094,"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":336179,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":97,"diagnostic_count":15,"duration_ms":7,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1216278,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1216278,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":1893,"diagnostic_count":116,"duration_ms":1563337,"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":339142,"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":1893,"diagnostic_count":116,"duration_ms":90,"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":43443040,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":29,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":43443040,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":7806,"diagnostic_count":3119,"duration_ms":6343769,"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":429067,"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":7806,"diagnostic_count":3119,"duration_ms":564,"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":266799327,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":224,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":266799327,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":152,"diagnostic_count":23,"duration_ms":19744,"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":720278,"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":129,"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":8,"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":3349}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":757,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3523,"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 cfb976988920a519775ad4b1e69c4ad36c75af40648a2f7b96c005a6accda9d7
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":10424492,"ok":true}

Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

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

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

git checkout a94d4121a752df1afe89d3ed087a101ba25e5e76

fatal: reference is not a tree: a94d4121a752df1afe89d3ed087a101ba25e5e76

git fetch --depth 1 origin a94d4121a752df1afe89d3ed087a101ba25e5e76

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

git checkout a94d4121a752df1afe89d3ed087a101ba25e5e76 (after fetch)

Note: switching to 'a94d4121a752df1afe89d3ed087a101ba25e5e76'.

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 a94d412 Project arbitrary q measure calibration from source

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%, 3 KB/s], Decompressed: 11
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 17 KB/s], Decompressed: 36
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 97 KB/s], Decompressed: 61
Downloaded: 90 file(s) [attempted 90/8459 = 1%, 355 KB/s], Decompressed: 86
Downloaded: 128 file(s) [attempted 128/8459 = 1%, 280 KB/s], Decompressed: 121
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 856 KB/s], Decompressed: 151
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 125 KB/s], Decompressed: 192
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 219 KB/s], Decompressed: 223
Downloaded: 264 file(s) [attempted 264/8459 = 3%, 855 KB/s], Decompressed: 261
Downloaded: 309 file(s) [attempted 309/8459 = 3%, 812 KB/s], Decompressed: 302
Downloaded: 343 file(s) [attempted 343/8459 = 4%, 28 KB/s], Decompressed: 340
Downloaded: 383 file(s) [attempted 383/8459 = 4%, 214 KB/s], Decompressed: 374
Downloaded: 416 file(s) [attempted 416/8459 = 4%, 164 KB/s], Decompressed: 412
Downloaded: 456 file(s) [attempted 456/8459 = 5%, 289 KB/s], Decompressed: 449
Downloaded: 489 file(s) [attempted 489/8459 = 5%, 77 KB/s], Decompressed: 466
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 668 KB/s], Decompressed: 521
Downloaded: 566 file(s) [attempted 566/8459 = 6%, 445 KB/s], Decompressed: 562
Downloaded: 607 file(s) [attempted 607/8459 = 7%, 129 KB/s], Decompressed: 604
Downloaded: 648 file(s) [attempted 648/8459 = 7%, 143 KB/s], Decompressed: 645
Downloaded: 686 file(s) [attempted 686/8459 = 8%, 696 KB/s], Decompressed: 672
Downloaded: 720 file(s) [attempted 720/8459 = 8%, 46 KB/s], Decompressed: 713
Downloaded: 761 file(s) [attempted 761/8459 = 8%, 165 KB/s], Decompressed: 754
Downloaded: 802 file(s) [attempted 802/8459 = 9%, 943 KB/s], Decompressed: 771
Downloaded: 847 file(s) [attempted 847/8459 = 10%, 36 KB/s], Decompressed: 812
Downloaded: 891 file(s) [attempted 891/8459 = 10%, 75 KB/s], Decompressed: 884
Downloaded: 919 file(s) [attempted 919/8459 = 10%, 146 KB/s], Decompressed: 915
Downloaded: 960 file(s) [attempted 960/8459 = 11%, 129 KB/s], Decompressed: 953
Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 25 KB/s], Decompressed: 997
Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 573 KB/s], Decompressed: 1042
Downloaded: 1090 file(s) [attempted 1090/8459 = 12%, 62 KB/s], Decompressed: 1076
Downloaded: 1124 file(s) [attempted 1124/8459 = 13%, 326 KB/s], Decompressed: 1117
Downloaded: 1158 file(s) [attempted 1158/8459 = 13%, 141 KB/s], Decompressed: 1155
Downloaded: 1199 file(s) [attempted 1199/8459 = 14%, 2377 KB/s], Decompressed: 1196
Downloaded: 1240 file(s) [attempted 1240/8459 = 14%, 147 KB/s], Decompressed: 1237
Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 191 KB/s], Decompressed: 1278
Downloaded: 1326 file(s) [attempted 1326/8459 = 15%, 364 KB/s], Decompressed: 1319
Downloaded: 1364 file(s) [attempted 1364/8459 = 16%, 215 KB/s], Decompressed: 1347
Downloaded: 1398 file(s) [attempted 1398/8459 = 16%, 105 KB/s], Decompressed: 1394
Downloaded: 1442 file(s) [attempted 1442/8459 = 17%, 237 KB/s], Decompressed: 1439
Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 408 KB/s], Decompressed: 1477
Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 196 KB/s], Decompressed: 1511
Downloaded: 1567 file(s) [attempted 1567/8459 = 18%, 992 KB/s], Decompressed: 1559
Downloaded: 1597 file(s) [attempted 1597/8459 = 18%, 170 KB/s], Decompressed: 1593
Downloaded: 1634 file(s) [attempted 1634/8459 = 19%, 241 KB/s], Decompressed: 1631
Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 120 KB/s], Decompressed: 1668
Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 164 KB/s], Decompressed: 1709
Downloaded: 1750 file(s) [attempted 1750/8459 = 20%, 199 KB/s], Decompressed: 1740
Downloaded: 1788 file(s) [attempted 1788/8459 = 21%, 272 KB/s], Decompressed: 1781
Downloaded: 1826 file(s) [attempted 1826/8459 = 21%, 72 KB/s], Decompressed: 1819
Downloaded: 1863 file(s) [attempted 1863/8459 = 22%, 1696 KB/s], Decompressed: 1860
Downloaded: 1901 file(s) [attempted 1901/8459 = 22%, 149 KB/s], Decompressed: 1898
Downloaded: 1936 file(s) [attempted 1936/8459 = 22%, 67 KB/s], Decompressed: 1932
Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 382 KB/s], Decompressed: 1973
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 124 KB/s], Decompressed: 2000
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 181 KB/s], Decompressed: 2045
Downloaded: 2089 file(s) [attempted 2089/8459 = 24%, 73 KB/s], Decompressed: 2086
Downloaded: 2123 file(s) [attempted 2123/8459 = 25%, 272 KB/s], Decompressed: 2106
Downloaded: 2161 file(s) [attempted 2161/8459 = 25%, 202 KB/s], Decompressed: 2154
Downloaded: 2199 file(s) [attempted 2199/8459 = 25%, 91 KB/s], Decompressed: 2192
Downloaded: 2240 file(s) [attempted 2240/8459 = 26%, 111 KB/s], Decompressed: 2236
Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 210 KB/s], Decompressed: 2277
Downloaded: 2318 file(s) [attempted 2318/8459 = 27%, 391 KB/s], Decompressed: 2315
Downloaded: 2358 file(s) [attempted 2358/8459 = 27%, 72 KB/s], Decompressed: 2349
Downloaded: 2395 file(s) [attempted 2395/8459 = 28%, 35 KB/s], Decompressed: 2390
Downloaded: 2435 file(s) [attempted 2435/8459 = 28%, 75 KB/s], Decompressed: 2431
Downloaded: 2476 file(s) [attempted 2476/8459 = 29%, 356 KB/s], Decompressed: 2462
Downloaded: 2514 file(s) [attempted 2514/8459 = 29%, 127 KB/s], Decompressed: 2510
Downloaded: 2548 file(s) [attempted 2548/8459 = 30%, 85 KB/s], Decompressed: 2537
Downloaded: 2585 file(s) [attempted 2585/8459 = 30%, 279 KB/s], Decompressed: 2579
Downloaded: 2626 file(s) [attempted 2626/8459 = 31%, 397 KB/s], Decompressed: 2623
Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 676 KB/s], Decompressed: 2661
Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 901 KB/s], Decompressed: 2698
Downloaded: 2736 file(s) [attempted 2736/8459 = 32%, 571 KB/s], Decompressed: 2733
Downloaded: 2781 file(s) [attempted 2781/8459 = 32%, 52 KB/s], Decompressed: 2777
Downloaded: 2818 file(s) [attempted 2818/8459 = 33%, 93 KB/s], Decompressed: 2815
Downloaded: 2856 file(s) [attempted 2856/8459 = 33%, 32 KB/s], Decompressed: 2852
Downloaded: 2893 file(s) [attempted 2893/8459 = 34%, 455 KB/s], Decompressed: 2887
Downloaded: 2931 file(s) [attempted 2931/8459 = 34%, 615 KB/s], Decompressed: 2924
Downloaded: 2976 file(s) [attempted 2976/8459 = 35%, 597 KB/s], Decompressed: 2972
Downloaded: 3017 file(s) [attempted 3017/8459 = 35%, 614 KB/s], Decompressed: 3010
Downloaded: 3051 file(s) [attempted 3051/8459 = 36%, 318 KB/s], Decompressed: 3044
Downloaded: 3092 file(s) [attempted 3092/8459 = 36%, 365 KB/s], Decompressed: 3088
Downloaded: 3133 file(s) [attempted 3133/8459 = 37%, 1005 KB/s], Decompressed: 3126
Downloaded: 3171 file(s) [attempted 3171/8459 = 37%, 68 KB/s], Decompressed: 3167
Downloaded: 3213 file(s) [attempted 3213/8459 = 37%, 122 KB/s], Decompressed: 3210
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 243 KB/s], Decompressed: 3242
Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 82 KB/s], Decompressed: 3280
Downloaded: 3332 file(s) [attempted 3332/8459 = 39%, 385 KB/s], Decompressed: 3318
Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 119 KB/s], Decompressed: 3359
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 199 KB/s], Decompressed: 3403
Downloaded: 3451 file(s) [attempted 3451/8459 = 40%, 86 KB/s], Decompressed: 3448
Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 186 KB/s], Decompressed: 3485
Downloaded: 3533 file(s) [attempted 3533/8459 = 41%, 142 KB/s], Decompressed: 3509
Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 395 KB/s], Decompressed: 3561
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 36 KB/s], Decompressed: 3604
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 123 KB/s], Decompressed: 3646
Downloaded: 3705 file(s) [attempted 3705/8459 = 43%, 1764 KB/s], Decompressed: 3694
Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 195 KB/s], Decompressed: 3749
Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 50 KB/s], Decompressed: 3787
Downloaded: 3828 file(s) [attempted 3828/8459 = 45%, 454 KB/s], Decompressed: 3817
Downloaded: 3864 file(s) [attempted 3864/8459 = 45%, 1267 KB/s], Decompressed: 3859
Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 64 KB/s], Decompressed: 3903
Downloaded: 3951 file(s) [attempted 3951/8459 = 46%, 350 KB/s], Decompressed: 3944
Downloaded: 3984 file(s) [attempted 3984/8459 = 47%, 1591 KB/s], Decompressed: 3978
Downloaded: 4018 file(s) [attempted 4018/8459 = 47%, 1743 KB/s], Decompressed: 4013
Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 386 KB/s], Decompressed: 4057
Downloaded: 4103 file(s) [attempted 4103/8459 = 48%, 40 KB/s], Decompressed: 4102
Downloaded: 4143 file(s) [attempted 4143/8459 = 48%, 959 KB/s], Decompressed: 4132
Downloaded: 4177 file(s) [attempted 4177/8459 = 49%, 59 KB/s], Decompressed: 4167
Downloaded: 4214 file(s) [attempted 4214/8459 = 49%, 69 KB/s], Decompressed: 4211
Downloaded: 4259 file(s) [attempted 4259/8459 = 50%, 394 KB/s], Decompressed: 4256
Downloaded: 4297 file(s) [attempted 4297/8459 = 50%, 889 KB/s], Decompressed: 4293
Downloaded: 4334 file(s) [attempted 4334/8459 = 51%, 309 KB/s], Decompressed: 4331
Downloaded: 4372 file(s) [attempted 4372/8459 = 51%, 276 KB/s], Decompressed: 4365
Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 103 KB/s], Decompressed: 4413
Downloaded: 4457 file(s) [attempted 4457/8459 = 52%, 36 KB/s], Decompressed: 4454
Downloaded: 4495 file(s) [attempted 4495/8459 = 53%, 244 KB/s], Decompressed: 4492
Downloaded: 4536 file(s) [attempted 4536/8459 = 53%, 1027 KB/s], Decompressed: 4533
Downloaded: 4572 file(s) [attempted 4572/8459 = 54%, 81 KB/s], Decompressed: 4564
Downloaded: 4615 file(s) [attempted 4615/8459 = 54%, 691 KB/s], Decompressed: 4605
Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 489 KB/s], Decompressed: 4646
Downloaded: 4690 file(s) [attempted 4690/8459 = 55%, 94 KB/s], Decompressed: 4687
Downloaded: 4733 file(s) [attempted 4733/8459 = 55%, 562 KB/s], Decompressed: 4718
Downloaded: 4771 file(s) [attempted 4771/8459 = 56%, 35 KB/s], Decompressed: 4748
Downloaded: 4808 file(s) [attempted 4808/8459 = 56%, 119 KB/s], Decompressed: 4803
Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 98 KB/s], Decompressed: 4841
Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 1056 KB/s], Decompressed: 4882
Downloaded: 4928 file(s) [attempted 4928/8459 = 58%, 134 KB/s], Decompressed: 4919
Downloaded: 4964 file(s) [attempted 4964/8459 = 58%, 84 KB/s], Decompressed: 4961
Downloaded: 4999 file(s) [attempted 4999/8459 = 59%, 235 KB/s], Decompressed: 4995
Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 184 KB/s], Decompressed: 5039
Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 138 KB/s], Decompressed: 5080
Downloaded: 5125 file(s) [attempted 5125/8459 = 60%, 44 KB/s], Decompressed: 5118
Downloaded: 5159 file(s) [attempted 5159/8459 = 60%, 60 KB/s], Decompressed: 5152
Downloaded: 5197 file(s) [attempted 5197/8459 = 61%, 37 KB/s], Decompressed: 5193
Downloaded: 5241 file(s) [attempted 5241/8459 = 61%, 98 KB/s], Decompressed: 5234
Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 1146 KB/s], Decompressed: 5279
Downloaded: 5327 file(s) [attempted 5327/8459 = 62%, 46 KB/s], Decompressed: 5320
Downloaded: 5361 file(s) [attempted 5361/8459 = 63%, 21 KB/s], Decompressed: 5358
Downloaded: 5399 file(s) [attempted 5399/8459 = 63%, 88 KB/s], Decompressed: 5395
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 974 KB/s], Decompressed: 5440
Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 157 KB/s], Decompressed: 5477
Downloaded: 5525 file(s) [attempted 5525/8459 = 65%, 499 KB/s], Decompressed: 5522
Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 78 KB/s], Decompressed: 5556
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 21 KB/s], Decompressed: 5597
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 28 KB/s], Decompressed: 5638
Downloaded: 5679 file(s) [attempted 5679/8459 = 67%, 604 KB/s], Decompressed: 5676
Downloaded: 5724 file(s) [attempted 5724/8459 = 67%, 162 KB/s], Decompressed: 5707
Downloaded: 5758 file(s) [attempted 5758/8459 = 68%, 204 KB/s], Decompressed: 5755
Downloaded: 5799 file(s) [attempted 5799/8459 = 68%, 108 KB/s], Decompressed: 5796
Downloaded: 5841 file(s) [attempted 5841/8459 = 69%, 142 KB/s], Decompressed: 5833
Downloaded: 5878 file(s) [attempted 5878/8459 = 69%, 151 KB/s], Decompressed: 5874
Downloaded: 5919 file(s) [attempted 5919/8459 = 69%, 75 KB/s], Decompressed: 5909
Downloaded: 5956 file(s) [attempted 5956/8459 = 70%, 487 KB/s], Decompressed: 5946
Downloaded: 5994 file(s) [attempted 5994/8459 = 70%, 243 KB/s], Decompressed: 5991
Downloaded: 6032 file(s) [attempted 6032/8459 = 71%, 80 KB/s], Decompressed: 6028
Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 242 KB/s], Decompressed: 6066
Downloaded: 6110 file(s) [attempted 6110/8459 = 72%, 287 KB/s], Decompressed: 6107
Downloaded: 6148 file(s) [attempted 6148/8459 = 72%, 44 KB/s], Decompressed: 6141
Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 203 KB/s], Decompressed: 6182
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 211 KB/s], Decompressed: 6223
Downloaded: 6271 file(s) [attempted 6271/8459 = 74%, 236 KB/s], Decompressed: 6264
Downloaded: 6312 file(s) [attempted 6312/8459 = 74%, 1142 KB/s], Decompressed: 6309
Downloaded: 6350 file(s) [attempted 6350/8459 = 75%, 316 KB/s], Decompressed: 6347
Downloaded: 6387 file(s) [attempted 6387/8459 = 75%, 434 KB/s], Decompressed: 6377
Downloaded: 6425 file(s) [attempted 6425/8459 = 75%, 146 KB/s], Decompressed: 6422
Downloaded: 6470 file(s) [attempted 6470/8459 = 76%, 186 KB/s], Decompressed: 6466
Downloaded: 6507 file(s) [attempted 6507/8459 = 76%, 434 KB/s], Decompressed: 6504
Downloaded: 6542 file(s) [attempted 6542/8459 = 77%, 647 KB/s], Decompressed: 6535
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 339 KB/s], Decompressed: 6569
Downloaded: 6622 file(s) [attempted 6622/8459 = 78%, 395 KB/s], Decompressed: 6617
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 79 KB/s], Decompressed: 6658
Downloaded: 6700 file(s) [attempted 6700/8459 = 79%, 119 KB/s], Decompressed: 6692
Downloaded: 6733 file(s) [attempted 6733/8459 = 79%, 304 KB/s], Decompressed: 6730
Downloaded: 6778 file(s) [attempted 6778/8459 = 80%, 38 KB/s], Decompressed: 6774
Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 119 KB/s], Decompressed: 6812
Downloaded: 6860 file(s) [attempted 6860/8459 = 81%, 583 KB/s], Decompressed: 6857
Downloaded: 6901 file(s) [attempted 6901/8459 = 81%, 438 KB/s], Decompressed: 6898
Downloaded: 6935 file(s) [attempted 6935/8459 = 81%, 72 KB/s], Decompressed: 6932
Downloaded: 6976 file(s) [attempted 6976/8459 = 82%, 112 KB/s], Decompressed: 6973
Downloaded: 7016 file(s) [attempted 7016/8459 = 82%, 62 KB/s], Decompressed: 7007
Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 100 KB/s], Decompressed: 7055
Downloaded: 7100 file(s) [attempted 7100/8459 = 83%, 68 KB/s], Decompressed: 7096
Downloaded: 7130 file(s) [attempted 7130/8459 = 84%, 966 KB/s], Decompressed: 7127
Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 970 KB/s], Decompressed: 7165
Downloaded: 7212 file(s) [attempted 7212/8459 = 85%, 23 KB/s], Decompressed: 7206
Downloaded: 7257 file(s) [attempted 7257/8459 = 85%, 358 KB/s], Decompressed: 7250
Downloaded: 7295 file(s) [attempted 7295/8459 = 86%, 35 KB/s], Decompressed: 7287
Downloaded: 7329 file(s) [attempted 7329/8459 = 86%, 452 KB/s], Decompressed: 7325
Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 120 KB/s], Decompressed: 7363
Downloaded: 7411 file(s) [attempted 7411/8459 = 87%, 77 KB/s], Decompressed: 7408
Downloaded: 7455 file(s) [attempted 7455/8459 = 88%, 232 KB/s], Decompressed: 7445
Downloaded: 7493 file(s) [attempted 7493/8459 = 88%, 310 KB/s], Decompressed: 7486
Downloaded: 7527 file(s) [attempted 7527/8459 = 88%, 177 KB/s], Decompressed: 7524
Downloaded: 7568 file(s) [attempted 7568/8459 = 89%, 444 KB/s], Decompressed: 7558
Downloaded: 7609 file(s) [attempted 7609/8459 = 89%, 221 KB/s], Decompressed: 7606
Downloaded: 7651 file(s) [attempted 7651/8459 = 90%, 252 KB/s], Decompressed: 7644
Downloaded: 7692 file(s) [attempted 7692/8459 = 90%, 45 KB/s], Decompressed: 7688
Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 592 KB/s], Decompressed: 7722
Downloaded: 7765 file(s) [attempted 7765/8459 = 91%, 97 KB/s], Decompressed: 7757
Downloaded: 7808 file(s) [attempted 7808/8459 = 92%, 34 KB/s], Decompressed: 7801
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 315 KB/s], Decompressed: 7846
Downloaded: 7887 file(s) [attempted 7887/8459 = 93%, 58 KB/s], Decompressed: 7876
Downloaded: 7924 file(s) [attempted 7924/8459 = 93%, 613 KB/s], Decompressed: 7921
Downloaded: 7959 file(s) [attempted 7959/8459 = 94%, 787 KB/s], Decompressed: 7955
Downloaded: 7997 file(s) [attempted 7997/8459 = 94%, 109 KB/s], Decompressed: 7993
Downloaded: 8041 file(s) [attempted 8041/8459 = 95%, 788 KB/s], Decompressed: 8037
Downloaded: 8082 file(s) [attempted 8082/8459 = 95%, 114 KB/s], Decompressed: 8078
Downloaded: 8116 file(s) [attempted 8116/8459 = 95%, 75 KB/s], Decompressed: 8102
Downloaded: 8150 file(s) [attempted 8150/8459 = 96%, 769 KB/s], Decompressed: 8147
Downloaded: 8195 file(s) [attempted 8195/8459 = 96%, 356 KB/s], Decompressed: 8191
Downloaded: 8239 file(s) [attempted 8239/8459 = 97%, 190 KB/s], Decompressed: 8236
Downloaded: 8277 file(s) [attempted 8277/8459 = 97%, 142 KB/s], Decompressed: 8273
Downloaded: 8314 file(s) [attempted 8314/8459 = 98%, 161 KB/s], Decompressed: 8304
Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 264 KB/s], Decompressed: 8349
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 88 KB/s], Decompressed: 8390
Downloaded: 8438 file(s) [attempted 8438/8459 = 99%, 309 KB/s], Decompressed: 8431
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 162 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 162 KB/s], Decompressed: 8455

lake build

ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (212s)
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) [0x77bcfdbc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x77bcfdbbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x77bcfdbbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x77bcfdaf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x77bcfdaf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x77bcfdbcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x77bcfda32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x77bcfda32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x77bcfda33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x77bcfda341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x77bcfdbc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x77bcfd815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x77bcfdbc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x77bcfdbc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x77bcfdb9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x77bcfd815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x77bcf8c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x77bcf8a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x77bcf8569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x77bcf8569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x77bcf544524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x77bcf5445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x59b03cb278da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (23s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.2s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (37s)
✔ [3414/3416] Built Iut.Basic (2.6s)
✔ [3415/3416] Built Iut (2.5s)
Build completed successfully (3416 jobs).

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

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`

./.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":10,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":326408,"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":1,"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":79,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":329534,"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":7094,"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":336179,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":97,"diagnostic_count":15,"duration_ms":7,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1216278,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1216278,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":1893,"diagnostic_count":116,"duration_ms":1563337,"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":339142,"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":1893,"diagnostic_count":116,"duration_ms":90,"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":43443040,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":29,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":43443040,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":7806,"diagnostic_count":3119,"duration_ms":6343769,"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":429067,"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":7806,"diagnostic_count":3119,"duration_ms":564,"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":266799327,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":224,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":266799327,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":152,"diagnostic_count":23,"duration_ms":19744,"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":720278,"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":129,"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":8,"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":3349}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":757,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3523,"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 cfb976988920a519775ad4b1e69c4ad36c75af40648a2f7b96c005a6accda9d7
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":10424492,"ok":true}