Run 349

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-457-source
exit_code=Some(0) duration_ms=2409
stderr:
Cloning into '/var/lib/apodeixis/repos/job-457-source'...


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


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


$ git checkout 5d7fe098c63e2c7af131a16914ed639ef020f286 (after fetch)
exit_code=Some(0) duration_ms=83
stderr:
Note: switching to '5d7fe098c63e2c7af131a16914ed639ef020f286'.

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 5d7fe09 Chart valuation unit ball carrier transport

Resolved source revision: 5d7fe098c63e2c7af131a16914ed639ef020f286

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=5d7fe098c63e2c7af131a16914ed639ef020f286 provenance={"branch":"master","checked_out_revision":"5d7fe098c63e2c7af131a16914ed639ef020f286","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"5d7fe098c63e2c7af131a16914ed639ef020f286","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: checkpointed 1 module fragment row(s) from batch extract-batch-00000
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00001
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00002
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00003
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00004
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00005
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=37482
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: 14 file(s) [attempted 14/8459 = 0%, 6 KB/s], Decompressed: 12
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 15 KB/s], Decompressed: 35
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 56 KB/s], Decompressed: 61
Downloaded: 92 file(s) [attempted 92/8459 = 1%, 60 KB/s], Decompressed: 85
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 23 KB/s], Decompressed: 121
Downloaded: 165 file(s) [attempted 165/8459 = 1%, 198 KB/s], Decompressed: 158
Downloaded: 205 file(s) [attempted 205/8459 = 2%, 32 KB/s], Decompressed: 199
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 256 KB/s], Decompressed: 230
Downloaded: 274 file(s) [attempted 274/8459 = 3%, 1026 KB/s], Decompressed: 268
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 530 KB/s], Decompressed: 306
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 50 KB/s], Decompressed: 350
Downloaded: 393 file(s) [attempted 393/8459 = 4%, 208 KB/s], Decompressed: 384
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 28 KB/s], Decompressed: 425
Downloaded: 473 file(s) [attempted 473/8459 = 5%, 77 KB/s], Decompressed: 470
Downloaded: 511 file(s) [attempted 511/8459 = 6%, 749 KB/s], Decompressed: 508
Downloaded: 552 file(s) [attempted 552/8459 = 6%, 148 KB/s], Decompressed: 545
Downloaded: 593 file(s) [attempted 593/8459 = 7%, 269 KB/s], Decompressed: 591
Downloaded: 631 file(s) [attempted 631/8459 = 7%, 142 KB/s], Decompressed: 624
Downloaded: 669 file(s) [attempted 669/8459 = 7%, 25 KB/s], Decompressed: 665
Downloaded: 710 file(s) [attempted 710/8459 = 8%, 26 KB/s], Decompressed: 703
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 81 KB/s], Decompressed: 747
Downloaded: 788 file(s) [attempted 788/8459 = 9%, 325 KB/s], Decompressed: 785
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 114 KB/s], Decompressed: 823
Downloaded: 864 file(s) [attempted 864/8459 = 10%, 145 KB/s], Decompressed: 860
Downloaded: 907 file(s) [attempted 907/8459 = 10%, 623 KB/s], Decompressed: 902
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 180 KB/s], Decompressed: 943
Downloaded: 991 file(s) [attempted 991/8459 = 11%, 246 KB/s], Decompressed: 987
Downloaded: 1028 file(s) [attempted 1028/8459 = 12%, 157 KB/s], Decompressed: 1025
Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 224 KB/s], Decompressed: 1062
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 1710 KB/s], Decompressed: 1107
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 153 KB/s], Decompressed: 1145
Downloaded: 1192 file(s) [attempted 1192/8459 = 14%, 865 KB/s], Decompressed: 1189
Downloaded: 1234 file(s) [attempted 1234/8459 = 14%, 1165 KB/s], Decompressed: 1227
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 265 KB/s], Decompressed: 1268
Downloaded: 1312 file(s) [attempted 1312/8459 = 15%, 179 KB/s], Decompressed: 1305
Downloaded: 1346 file(s) [attempted 1346/8459 = 15%, 209 KB/s], Decompressed: 1343
Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 376 KB/s], Decompressed: 1384
Downloaded: 1429 file(s) [attempted 1429/8459 = 16%, 88 KB/s], Decompressed: 1425
Downloaded: 1470 file(s) [attempted 1470/8459 = 17%, 206 KB/s], Decompressed: 1463
Downloaded: 1500 file(s) [attempted 1500/8459 = 17%, 165 KB/s], Decompressed: 1497
Downloaded: 1542 file(s) [attempted 1542/8459 = 18%, 84 KB/s], Decompressed: 1535
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 409 KB/s], Decompressed: 1579
Downloaded: 1631 file(s) [attempted 1631/8459 = 19%, 682 KB/s], Decompressed: 1627
Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 581 KB/s], Decompressed: 1658
Downloaded: 1706 file(s) [attempted 1706/8459 = 20%, 504 KB/s], Decompressed: 1700
Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 229 KB/s], Decompressed: 1741
Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 437 KB/s], Decompressed: 1781
Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 1071 KB/s], Decompressed: 1822
Downloaded: 1863 file(s) [attempted 1863/8459 = 22%, 1247 KB/s], Decompressed: 1856
Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 79 KB/s], Decompressed: 1901
Downloaded: 1939 file(s) [attempted 1939/8459 = 22%, 151 KB/s], Decompressed: 1932
Downloaded: 1978 file(s) [attempted 1978/8459 = 23%, 482 KB/s], Decompressed: 1973
Downloaded: 2021 file(s) [attempted 2021/8459 = 23%, 173 KB/s], Decompressed: 2014
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 413 KB/s], Decompressed: 2055
Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 121 KB/s], Decompressed: 2089
Downloaded: 2132 file(s) [attempted 2132/8459 = 25%, 1442 KB/s], Decompressed: 2127
Downloaded: 2170 file(s) [attempted 2170/8459 = 25%, 54 KB/s], Decompressed: 2164
Downloaded: 2212 file(s) [attempted 2212/8459 = 26%, 290 KB/s], Decompressed: 2209
Downloaded: 2253 file(s) [attempted 2253/8459 = 26%, 675 KB/s], Decompressed: 2250
Downloaded: 2295 file(s) [attempted 2295/8459 = 27%, 504 KB/s], Decompressed: 2291
Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 49 KB/s], Decompressed: 2329
Downloaded: 2367 file(s) [attempted 2367/8459 = 27%, 98 KB/s], Decompressed: 2363
Downloaded: 2407 file(s) [attempted 2407/8459 = 28%, 283 KB/s], Decompressed: 2404
Downloaded: 2448 file(s) [attempted 2448/8459 = 28%, 243 KB/s], Decompressed: 2445
Downloaded: 2493 file(s) [attempted 2493/8459 = 29%, 49 KB/s], Decompressed: 2486
Downloaded: 2529 file(s) [attempted 2529/8459 = 29%, 1102 KB/s], Decompressed: 2520
Downloaded: 2565 file(s) [attempted 2565/8459 = 30%, 731 KB/s], Decompressed: 2558
Downloaded: 2603 file(s) [attempted 2603/8459 = 30%, 598 KB/s], Decompressed: 2599
Downloaded: 2647 file(s) [attempted 2647/8459 = 31%, 23 KB/s], Decompressed: 2637
Downloaded: 2691 file(s) [attempted 2691/8459 = 31%, 398 KB/s], Decompressed: 2688
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 272 KB/s], Decompressed: 2722
Downloaded: 2763 file(s) [attempted 2763/8459 = 32%, 55 KB/s], Decompressed: 2760
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 478 KB/s], Decompressed: 2801
Downloaded: 2845 file(s) [attempted 2845/8459 = 33%, 101 KB/s], Decompressed: 2842
Downloaded: 2890 file(s) [attempted 2890/8459 = 34%, 30 KB/s], Decompressed: 2883
Downloaded: 2934 file(s) [attempted 2934/8459 = 34%, 648 KB/s], Decompressed: 2924
Downloaded: 2965 file(s) [attempted 2965/8459 = 35%, 155 KB/s], Decompressed: 2958
Downloaded: 3006 file(s) [attempted 3006/8459 = 35%, 381 KB/s], Decompressed: 3003
Downloaded: 3045 file(s) [attempted 3045/8459 = 35%, 1393 KB/s], Decompressed: 3041
Downloaded: 3088 file(s) [attempted 3088/8459 = 36%, 1725 KB/s], Decompressed: 3085
Downloaded: 3126 file(s) [attempted 3126/8459 = 36%, 54 KB/s], Decompressed: 3119
Downloaded: 3161 file(s) [attempted 3161/8459 = 37%, 1587 KB/s], Decompressed: 3157
Downloaded: 3205 file(s) [attempted 3205/8459 = 37%, 484 KB/s], Decompressed: 3201
Downloaded: 3242 file(s) [attempted 3242/8459 = 38%, 251 KB/s], Decompressed: 3239
Downloaded: 3281 file(s) [attempted 3281/8459 = 38%, 400 KB/s], Decompressed: 3273
Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 856 KB/s], Decompressed: 3318
Downloaded: 3359 file(s) [attempted 3359/8459 = 39%, 76 KB/s], Decompressed: 3355
Downloaded: 3397 file(s) [attempted 3397/8459 = 40%, 780 KB/s], Decompressed: 3393
Downloaded: 3435 file(s) [attempted 3435/8459 = 40%, 108 KB/s], Decompressed: 3427
Downloaded: 3475 file(s) [attempted 3475/8459 = 41%, 344 KB/s], Decompressed: 3472
Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 239 KB/s], Decompressed: 3516
Downloaded: 3557 file(s) [attempted 3557/8459 = 42%, 208 KB/s], Decompressed: 3554
Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 256 KB/s], Decompressed: 3588
Downloaded: 3633 file(s) [attempted 3633/8459 = 42%, 59 KB/s], Decompressed: 3629
Downloaded: 3677 file(s) [attempted 3677/8459 = 43%, 346 KB/s], Decompressed: 3674
Downloaded: 3718 file(s) [attempted 3718/8459 = 43%, 146 KB/s], Decompressed: 3711
Downloaded: 3756 file(s) [attempted 3756/8459 = 44%, 49 KB/s], Decompressed: 3746
Downloaded: 3793 file(s) [attempted 3793/8459 = 44%, 352 KB/s], Decompressed: 3790
Downloaded: 3835 file(s) [attempted 3835/8459 = 45%, 125 KB/s], Decompressed: 3831
Downloaded: 3879 file(s) [attempted 3879/8459 = 45%, 200 KB/s], Decompressed: 3872
Downloaded: 3920 file(s) [attempted 3920/8459 = 46%, 113 KB/s], Decompressed: 3917
Downloaded: 3961 file(s) [attempted 3961/8459 = 46%, 79 KB/s], Decompressed: 3954
Downloaded: 3996 file(s) [attempted 3996/8459 = 47%, 189 KB/s], Decompressed: 3989
Downloaded: 4036 file(s) [attempted 4036/8459 = 47%, 70 KB/s], Decompressed: 4033
Downloaded: 4081 file(s) [attempted 4081/8459 = 48%, 165 KB/s], Decompressed: 4078
Downloaded: 4119 file(s) [attempted 4119/8459 = 48%, 1182 KB/s], Decompressed: 4108
Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 240 KB/s], Decompressed: 4153
Downloaded: 4201 file(s) [attempted 4201/8459 = 49%, 393 KB/s], Decompressed: 4197
Downloaded: 4245 file(s) [attempted 4245/8459 = 50%, 77 KB/s], Decompressed: 4238
Downloaded: 4287 file(s) [attempted 4287/8459 = 50%, 121 KB/s], Decompressed: 4283
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 1896 KB/s], Decompressed: 4324
Downloaded: 4362 file(s) [attempted 4362/8459 = 51%, 125 KB/s], Decompressed: 4355
Downloaded: 4399 file(s) [attempted 4399/8459 = 52%, 32 KB/s], Decompressed: 4396
Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 544 KB/s], Decompressed: 4437
Downloaded: 4485 file(s) [attempted 4485/8459 = 53%, 601 KB/s], Decompressed: 4475
Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 109 KB/s], Decompressed: 4516
Downloaded: 4560 file(s) [attempted 4560/8459 = 53%, 492 KB/s], Decompressed: 4553
Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 1338 KB/s], Decompressed: 4598
Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 182 KB/s], Decompressed: 4646
Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 162 KB/s], Decompressed: 4683
Downloaded: 4725 file(s) [attempted 4725/8459 = 55%, 1561 KB/s], Decompressed: 4721
Downloaded: 4762 file(s) [attempted 4762/8459 = 56%, 623 KB/s], Decompressed: 4759
Downloaded: 4800 file(s) [attempted 4800/8459 = 56%, 117 KB/s], Decompressed: 4796
Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 97 KB/s], Decompressed: 4837
Downloaded: 4882 file(s) [attempted 4882/8459 = 57%, 115 KB/s], Decompressed: 4878
Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 31 KB/s], Decompressed: 4916
Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 1306 KB/s], Decompressed: 4954
Downloaded: 4999 file(s) [attempted 4999/8459 = 59%, 70 KB/s], Decompressed: 4995
Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 99 KB/s], Decompressed: 5032
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 143 KB/s], Decompressed: 5073
Downloaded: 5118 file(s) [attempted 5118/8459 = 60%, 71 KB/s], Decompressed: 5115
Downloaded: 5161 file(s) [attempted 5161/8459 = 61%, 445 KB/s], Decompressed: 5152
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 451 KB/s], Decompressed: 5197
Downloaded: 5241 file(s) [attempted 5241/8459 = 61%, 45 KB/s], Decompressed: 5238
Downloaded: 5280 file(s) [attempted 5280/8459 = 62%, 714 KB/s], Decompressed: 5269
Downloaded: 5316 file(s) [attempted 5316/8459 = 62%, 144 KB/s], Decompressed: 5313
Downloaded: 5354 file(s) [attempted 5354/8459 = 63%, 613 KB/s], Decompressed: 5351
Downloaded: 5397 file(s) [attempted 5397/8459 = 63%, 489 KB/s], Decompressed: 5392
Downloaded: 5436 file(s) [attempted 5436/8459 = 64%, 263 KB/s], Decompressed: 5433
Downloaded: 5474 file(s) [attempted 5474/8459 = 64%, 152 KB/s], Decompressed: 5470
Downloaded: 5514 file(s) [attempted 5514/8459 = 65%, 211 KB/s], Decompressed: 5508
Downloaded: 5553 file(s) [attempted 5553/8459 = 65%, 48 KB/s], Decompressed: 5542
Downloaded: 5594 file(s) [attempted 5594/8459 = 66%, 250 KB/s], Decompressed: 5587
Downloaded: 5629 file(s) [attempted 5629/8459 = 66%, 1328 KB/s], Decompressed: 5624
Downloaded: 5672 file(s) [attempted 5672/8459 = 67%, 69 KB/s], Decompressed: 5669
Downloaded: 5713 file(s) [attempted 5713/8459 = 67%, 191 KB/s], Decompressed: 5710
Downloaded: 5755 file(s) [attempted 5755/8459 = 68%, 90 KB/s], Decompressed: 5748
Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 60 KB/s], Decompressed: 5789
Downloaded: 5827 file(s) [attempted 5827/8459 = 68%, 165 KB/s], Decompressed: 5823
Downloaded: 5871 file(s) [attempted 5871/8459 = 69%, 178 KB/s], Decompressed: 5867
Downloaded: 5914 file(s) [attempted 5914/8459 = 69%, 49 KB/s], Decompressed: 5909
Downloaded: 5950 file(s) [attempted 5950/8459 = 70%, 89 KB/s], Decompressed: 5946
Downloaded: 5989 file(s) [attempted 5989/8459 = 70%, 1528 KB/s], Decompressed: 5984
Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 27 KB/s], Decompressed: 6021
Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 355 KB/s], Decompressed: 6066
Downloaded: 6114 file(s) [attempted 6114/8459 = 72%, 3171 KB/s], Decompressed: 6104
Downloaded: 6151 file(s) [attempted 6151/8459 = 72%, 370 KB/s], Decompressed: 6148
Downloaded: 6196 file(s) [attempted 6196/8459 = 73%, 319 KB/s], Decompressed: 6189
Downloaded: 6234 file(s) [attempted 6234/8459 = 73%, 655 KB/s], Decompressed: 6230
Downloaded: 6268 file(s) [attempted 6268/8459 = 74%, 104 KB/s], Decompressed: 6262
Downloaded: 6308 file(s) [attempted 6308/8459 = 74%, 144 KB/s], Decompressed: 6302
Downloaded: 6347 file(s) [attempted 6347/8459 = 75%, 56 KB/s], Decompressed: 6343
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 60 KB/s], Decompressed: 6388
Downloaded: 6429 file(s) [attempted 6429/8459 = 76%, 85 KB/s], Decompressed: 6418
Downloaded: 6460 file(s) [attempted 6460/8459 = 76%, 884 KB/s], Decompressed: 6456
Downloaded: 6507 file(s) [attempted 6507/8459 = 76%, 80 KB/s], Decompressed: 6504
Downloaded: 6552 file(s) [attempted 6552/8459 = 77%, 98 KB/s], Decompressed: 6548
Downloaded: 6592 file(s) [attempted 6592/8459 = 77%, 123 KB/s], Decompressed: 6586
Downloaded: 6626 file(s) [attempted 6626/8459 = 78%, 313 KB/s], Decompressed: 6617
Downloaded: 6663 file(s) [attempted 6663/8459 = 78%, 322 KB/s], Decompressed: 6658
Downloaded: 6709 file(s) [attempted 6709/8459 = 79%, 439 KB/s], Decompressed: 6702
Downloaded: 6757 file(s) [attempted 6757/8459 = 79%, 283 KB/s], Decompressed: 6740
Downloaded: 6802 file(s) [attempted 6802/8459 = 80%, 140 KB/s], Decompressed: 6798
Downloaded: 6839 file(s) [attempted 6839/8459 = 80%, 95 KB/s], Decompressed: 6836
Downloaded: 6871 file(s) [attempted 6871/8459 = 81%, 780 KB/s], Decompressed: 6867
Downloaded: 6915 file(s) [attempted 6915/8459 = 81%, 419 KB/s], Decompressed: 6911
Downloaded: 6956 file(s) [attempted 6956/8459 = 82%, 172 KB/s], Decompressed: 6952
Downloaded: 6993 file(s) [attempted 6993/8459 = 82%, 1311 KB/s], Decompressed: 6976
Downloaded: 7031 file(s) [attempted 7031/8459 = 83%, 1790 KB/s], Decompressed: 7024
Downloaded: 7072 file(s) [attempted 7072/8459 = 83%, 288 KB/s], Decompressed: 7069
Downloaded: 7117 file(s) [attempted 7117/8459 = 84%, 81 KB/s], Decompressed: 7113
Downloaded: 7154 file(s) [attempted 7154/8459 = 84%, 99 KB/s], Decompressed: 7151
Downloaded: 7192 file(s) [attempted 7192/8459 = 85%, 55 KB/s], Decompressed: 7182
Downloaded: 7226 file(s) [attempted 7226/8459 = 85%, 152 KB/s], Decompressed: 7223
Downloaded: 7271 file(s) [attempted 7271/8459 = 85%, 78 KB/s], Decompressed: 7267
Downloaded: 7315 file(s) [attempted 7315/8459 = 86%, 197 KB/s], Decompressed: 7308
Downloaded: 7349 file(s) [attempted 7349/8459 = 86%, 46 KB/s], Decompressed: 7348
Downloaded: 7387 file(s) [attempted 7387/8459 = 87%, 91 KB/s], Decompressed: 7384
Downloaded: 7428 file(s) [attempted 7428/8459 = 87%, 105 KB/s], Decompressed: 7421
Downloaded: 7473 file(s) [attempted 7473/8459 = 88%, 353 KB/s], Decompressed: 7469
Downloaded: 7510 file(s) [attempted 7510/8459 = 88%, 216 KB/s], Decompressed: 7503
Downloaded: 7541 file(s) [attempted 7541/8459 = 89%, 198 KB/s], Decompressed: 7534
Downloaded: 7585 file(s) [attempted 7585/8459 = 89%, 153 KB/s], Decompressed: 7582
Downloaded: 7627 file(s) [attempted 7627/8459 = 90%, 131 KB/s], Decompressed: 7623
Downloaded: 7670 file(s) [attempted 7670/8459 = 90%, 39 KB/s], Decompressed: 7661
Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 69 KB/s], Decompressed: 7698
Downloaded: 7739 file(s) [attempted 7739/8459 = 91%, 782 KB/s], Decompressed: 7736
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 31 KB/s], Decompressed: 7781
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 443 KB/s], Decompressed: 7815
Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 34 KB/s], Decompressed: 7856
Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 237 KB/s], Decompressed: 7880
Downloaded: 7941 file(s) [attempted 7941/8459 = 93%, 314 KB/s], Decompressed: 7938
Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 825 KB/s], Decompressed: 7969
Downloaded: 8017 file(s) [attempted 8017/8459 = 94%, 116 KB/s], Decompressed: 8013
Downloaded: 8058 file(s) [attempted 8058/8459 = 95%, 479 KB/s], Decompressed: 8054
Downloaded: 8099 file(s) [attempted 8099/8459 = 95%, 355 KB/s], Decompressed: 8095
Downloaded: 8138 file(s) [attempted 8138/8459 = 96%, 299 KB/s], Decompressed: 8131
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 1094 KB/s], Decompressed: 8164
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 104 KB/s], Decompressed: 8212
Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 112 KB/s], Decompressed: 8256
Downloaded: 8302 file(s) [attempted 8302/8459 = 98%, 87 KB/s], Decompressed: 8294
Downloaded: 8342 file(s) [attempted 8342/8459 = 98%, 782 KB/s], Decompressed: 8338
Downloaded: 8379 file(s) [attempted 8379/8459 = 99%, 125 KB/s], Decompressed: 8373
Downloaded: 8417 file(s) [attempted 8417/8459 = 99%, 110 KB/s], Decompressed: 8414
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 499 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 499 KB/s], Decompressed: 8455


$ lake build
exit_code=Some(0) duration_ms=265849
stdout:
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (188s)
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) [0x75c5863c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x75c5863bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x75c5863bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x75c5862f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x75c5862f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x75c5863caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x75c586232923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x75c586232b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x75c586233827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x75c5862341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x75c5863c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x75c586015adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x75c5863c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x75c5863c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x75c58639b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x75c586015c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x75c581422638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x75c58120cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x75c580d69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x75c580d69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x75c57dc4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x75c57dc45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5cb7f03ea8da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (5.9s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.1s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (36s)
✔ [3414/3416] Built Iut.Basic (2.6s)
✔ [3415/3416] Built Iut (2.3s)
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=1822
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-batch-00000)
exit_code=Some(0) duration_ms=6016037
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache f4d8a5a71ef92e1eca529c90b5502827db3b1734353de1d3795d9937d061cd59
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
exit_code=Some(0) duration_ms=428006
stderr:
lean semantic helper: restored compiled static runner cache 8ce5ff6c967baef3842b8fb460ab7dc29b28a04bbb424be955c4371e23608184
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
exit_code=Some(0) duration_ms=360602
stderr:
lean semantic helper: restored compiled static runner cache 6247def1945279a6946b34517b575ac426a9bd22cc4c3ceb7a79dc06ef4083db
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)
exit_code=Some(0) duration_ms=1910497
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 1743058e355c2c9d0a14ee7f999dc06a3d68424d26bfda2428b61a1002396ce8
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)
exit_code=Some(0) duration_ms=328283
stderr:
lean semantic helper: restored compiled static runner cache 60b5e07f9f538c271c74b7f6a814efcb4304463fa74b69c58466604298c0acfe
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)
exit_code=Some(0) duration_ms=336837
stderr:
lean semantic helper: restored compiled static runner cache e103fd3939aed645f6a64b867308ee472e79eb2af9586b744c189d70ac5f91ea
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)

lean semantic helper: restored compiled static runner cache 60b5e07f9f538c271c74b7f6a814efcb4304463fa74b69c58466604298c0acfe
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

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

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

git checkout 5d7fe098c63e2c7af131a16914ed639ef020f286

fatal: reference is not a tree: 5d7fe098c63e2c7af131a16914ed639ef020f286

git fetch --depth 1 origin 5d7fe098c63e2c7af131a16914ed639ef020f286

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

git checkout 5d7fe098c63e2c7af131a16914ed639ef020f286 (after fetch)

Note: switching to '5d7fe098c63e2c7af131a16914ed639ef020f286'.

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 5d7fe09 Chart valuation unit ball carrier transport

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: 14 file(s) [attempted 14/8459 = 0%, 6 KB/s], Decompressed: 12
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 15 KB/s], Decompressed: 35
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 56 KB/s], Decompressed: 61
Downloaded: 92 file(s) [attempted 92/8459 = 1%, 60 KB/s], Decompressed: 85
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 23 KB/s], Decompressed: 121
Downloaded: 165 file(s) [attempted 165/8459 = 1%, 198 KB/s], Decompressed: 158
Downloaded: 205 file(s) [attempted 205/8459 = 2%, 32 KB/s], Decompressed: 199
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 256 KB/s], Decompressed: 230
Downloaded: 274 file(s) [attempted 274/8459 = 3%, 1026 KB/s], Decompressed: 268
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 530 KB/s], Decompressed: 306
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 50 KB/s], Decompressed: 350
Downloaded: 393 file(s) [attempted 393/8459 = 4%, 208 KB/s], Decompressed: 384
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 28 KB/s], Decompressed: 425
Downloaded: 473 file(s) [attempted 473/8459 = 5%, 77 KB/s], Decompressed: 470
Downloaded: 511 file(s) [attempted 511/8459 = 6%, 749 KB/s], Decompressed: 508
Downloaded: 552 file(s) [attempted 552/8459 = 6%, 148 KB/s], Decompressed: 545
Downloaded: 593 file(s) [attempted 593/8459 = 7%, 269 KB/s], Decompressed: 591
Downloaded: 631 file(s) [attempted 631/8459 = 7%, 142 KB/s], Decompressed: 624
Downloaded: 669 file(s) [attempted 669/8459 = 7%, 25 KB/s], Decompressed: 665
Downloaded: 710 file(s) [attempted 710/8459 = 8%, 26 KB/s], Decompressed: 703
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 81 KB/s], Decompressed: 747
Downloaded: 788 file(s) [attempted 788/8459 = 9%, 325 KB/s], Decompressed: 785
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 114 KB/s], Decompressed: 823
Downloaded: 864 file(s) [attempted 864/8459 = 10%, 145 KB/s], Decompressed: 860
Downloaded: 907 file(s) [attempted 907/8459 = 10%, 623 KB/s], Decompressed: 902
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 180 KB/s], Decompressed: 943
Downloaded: 991 file(s) [attempted 991/8459 = 11%, 246 KB/s], Decompressed: 987
Downloaded: 1028 file(s) [attempted 1028/8459 = 12%, 157 KB/s], Decompressed: 1025
Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 224 KB/s], Decompressed: 1062
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 1710 KB/s], Decompressed: 1107
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 153 KB/s], Decompressed: 1145
Downloaded: 1192 file(s) [attempted 1192/8459 = 14%, 865 KB/s], Decompressed: 1189
Downloaded: 1234 file(s) [attempted 1234/8459 = 14%, 1165 KB/s], Decompressed: 1227
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 265 KB/s], Decompressed: 1268
Downloaded: 1312 file(s) [attempted 1312/8459 = 15%, 179 KB/s], Decompressed: 1305
Downloaded: 1346 file(s) [attempted 1346/8459 = 15%, 209 KB/s], Decompressed: 1343
Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 376 KB/s], Decompressed: 1384
Downloaded: 1429 file(s) [attempted 1429/8459 = 16%, 88 KB/s], Decompressed: 1425
Downloaded: 1470 file(s) [attempted 1470/8459 = 17%, 206 KB/s], Decompressed: 1463
Downloaded: 1500 file(s) [attempted 1500/8459 = 17%, 165 KB/s], Decompressed: 1497
Downloaded: 1542 file(s) [attempted 1542/8459 = 18%, 84 KB/s], Decompressed: 1535
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 409 KB/s], Decompressed: 1579
Downloaded: 1631 file(s) [attempted 1631/8459 = 19%, 682 KB/s], Decompressed: 1627
Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 581 KB/s], Decompressed: 1658
Downloaded: 1706 file(s) [attempted 1706/8459 = 20%, 504 KB/s], Decompressed: 1700
Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 229 KB/s], Decompressed: 1741
Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 437 KB/s], Decompressed: 1781
Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 1071 KB/s], Decompressed: 1822
Downloaded: 1863 file(s) [attempted 1863/8459 = 22%, 1247 KB/s], Decompressed: 1856
Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 79 KB/s], Decompressed: 1901
Downloaded: 1939 file(s) [attempted 1939/8459 = 22%, 151 KB/s], Decompressed: 1932
Downloaded: 1978 file(s) [attempted 1978/8459 = 23%, 482 KB/s], Decompressed: 1973
Downloaded: 2021 file(s) [attempted 2021/8459 = 23%, 173 KB/s], Decompressed: 2014
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 413 KB/s], Decompressed: 2055
Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 121 KB/s], Decompressed: 2089
Downloaded: 2132 file(s) [attempted 2132/8459 = 25%, 1442 KB/s], Decompressed: 2127
Downloaded: 2170 file(s) [attempted 2170/8459 = 25%, 54 KB/s], Decompressed: 2164
Downloaded: 2212 file(s) [attempted 2212/8459 = 26%, 290 KB/s], Decompressed: 2209
Downloaded: 2253 file(s) [attempted 2253/8459 = 26%, 675 KB/s], Decompressed: 2250
Downloaded: 2295 file(s) [attempted 2295/8459 = 27%, 504 KB/s], Decompressed: 2291
Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 49 KB/s], Decompressed: 2329
Downloaded: 2367 file(s) [attempted 2367/8459 = 27%, 98 KB/s], Decompressed: 2363
Downloaded: 2407 file(s) [attempted 2407/8459 = 28%, 283 KB/s], Decompressed: 2404
Downloaded: 2448 file(s) [attempted 2448/8459 = 28%, 243 KB/s], Decompressed: 2445
Downloaded: 2493 file(s) [attempted 2493/8459 = 29%, 49 KB/s], Decompressed: 2486
Downloaded: 2529 file(s) [attempted 2529/8459 = 29%, 1102 KB/s], Decompressed: 2520
Downloaded: 2565 file(s) [attempted 2565/8459 = 30%, 731 KB/s], Decompressed: 2558
Downloaded: 2603 file(s) [attempted 2603/8459 = 30%, 598 KB/s], Decompressed: 2599
Downloaded: 2647 file(s) [attempted 2647/8459 = 31%, 23 KB/s], Decompressed: 2637
Downloaded: 2691 file(s) [attempted 2691/8459 = 31%, 398 KB/s], Decompressed: 2688
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 272 KB/s], Decompressed: 2722
Downloaded: 2763 file(s) [attempted 2763/8459 = 32%, 55 KB/s], Decompressed: 2760
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 478 KB/s], Decompressed: 2801
Downloaded: 2845 file(s) [attempted 2845/8459 = 33%, 101 KB/s], Decompressed: 2842
Downloaded: 2890 file(s) [attempted 2890/8459 = 34%, 30 KB/s], Decompressed: 2883
Downloaded: 2934 file(s) [attempted 2934/8459 = 34%, 648 KB/s], Decompressed: 2924
Downloaded: 2965 file(s) [attempted 2965/8459 = 35%, 155 KB/s], Decompressed: 2958
Downloaded: 3006 file(s) [attempted 3006/8459 = 35%, 381 KB/s], Decompressed: 3003
Downloaded: 3045 file(s) [attempted 3045/8459 = 35%, 1393 KB/s], Decompressed: 3041
Downloaded: 3088 file(s) [attempted 3088/8459 = 36%, 1725 KB/s], Decompressed: 3085
Downloaded: 3126 file(s) [attempted 3126/8459 = 36%, 54 KB/s], Decompressed: 3119
Downloaded: 3161 file(s) [attempted 3161/8459 = 37%, 1587 KB/s], Decompressed: 3157
Downloaded: 3205 file(s) [attempted 3205/8459 = 37%, 484 KB/s], Decompressed: 3201
Downloaded: 3242 file(s) [attempted 3242/8459 = 38%, 251 KB/s], Decompressed: 3239
Downloaded: 3281 file(s) [attempted 3281/8459 = 38%, 400 KB/s], Decompressed: 3273
Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 856 KB/s], Decompressed: 3318
Downloaded: 3359 file(s) [attempted 3359/8459 = 39%, 76 KB/s], Decompressed: 3355
Downloaded: 3397 file(s) [attempted 3397/8459 = 40%, 780 KB/s], Decompressed: 3393
Downloaded: 3435 file(s) [attempted 3435/8459 = 40%, 108 KB/s], Decompressed: 3427
Downloaded: 3475 file(s) [attempted 3475/8459 = 41%, 344 KB/s], Decompressed: 3472
Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 239 KB/s], Decompressed: 3516
Downloaded: 3557 file(s) [attempted 3557/8459 = 42%, 208 KB/s], Decompressed: 3554
Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 256 KB/s], Decompressed: 3588
Downloaded: 3633 file(s) [attempted 3633/8459 = 42%, 59 KB/s], Decompressed: 3629
Downloaded: 3677 file(s) [attempted 3677/8459 = 43%, 346 KB/s], Decompressed: 3674
Downloaded: 3718 file(s) [attempted 3718/8459 = 43%, 146 KB/s], Decompressed: 3711
Downloaded: 3756 file(s) [attempted 3756/8459 = 44%, 49 KB/s], Decompressed: 3746
Downloaded: 3793 file(s) [attempted 3793/8459 = 44%, 352 KB/s], Decompressed: 3790
Downloaded: 3835 file(s) [attempted 3835/8459 = 45%, 125 KB/s], Decompressed: 3831
Downloaded: 3879 file(s) [attempted 3879/8459 = 45%, 200 KB/s], Decompressed: 3872
Downloaded: 3920 file(s) [attempted 3920/8459 = 46%, 113 KB/s], Decompressed: 3917
Downloaded: 3961 file(s) [attempted 3961/8459 = 46%, 79 KB/s], Decompressed: 3954
Downloaded: 3996 file(s) [attempted 3996/8459 = 47%, 189 KB/s], Decompressed: 3989
Downloaded: 4036 file(s) [attempted 4036/8459 = 47%, 70 KB/s], Decompressed: 4033
Downloaded: 4081 file(s) [attempted 4081/8459 = 48%, 165 KB/s], Decompressed: 4078
Downloaded: 4119 file(s) [attempted 4119/8459 = 48%, 1182 KB/s], Decompressed: 4108
Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 240 KB/s], Decompressed: 4153
Downloaded: 4201 file(s) [attempted 4201/8459 = 49%, 393 KB/s], Decompressed: 4197
Downloaded: 4245 file(s) [attempted 4245/8459 = 50%, 77 KB/s], Decompressed: 4238
Downloaded: 4287 file(s) [attempted 4287/8459 = 50%, 121 KB/s], Decompressed: 4283
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 1896 KB/s], Decompressed: 4324
Downloaded: 4362 file(s) [attempted 4362/8459 = 51%, 125 KB/s], Decompressed: 4355
Downloaded: 4399 file(s) [attempted 4399/8459 = 52%, 32 KB/s], Decompressed: 4396
Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 544 KB/s], Decompressed: 4437
Downloaded: 4485 file(s) [attempted 4485/8459 = 53%, 601 KB/s], Decompressed: 4475
Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 109 KB/s], Decompressed: 4516
Downloaded: 4560 file(s) [attempted 4560/8459 = 53%, 492 KB/s], Decompressed: 4553
Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 1338 KB/s], Decompressed: 4598
Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 182 KB/s], Decompressed: 4646
Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 162 KB/s], Decompressed: 4683
Downloaded: 4725 file(s) [attempted 4725/8459 = 55%, 1561 KB/s], Decompressed: 4721
Downloaded: 4762 file(s) [attempted 4762/8459 = 56%, 623 KB/s], Decompressed: 4759
Downloaded: 4800 file(s) [attempted 4800/8459 = 56%, 117 KB/s], Decompressed: 4796
Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 97 KB/s], Decompressed: 4837
Downloaded: 4882 file(s) [attempted 4882/8459 = 57%, 115 KB/s], Decompressed: 4878
Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 31 KB/s], Decompressed: 4916
Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 1306 KB/s], Decompressed: 4954
Downloaded: 4999 file(s) [attempted 4999/8459 = 59%, 70 KB/s], Decompressed: 4995
Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 99 KB/s], Decompressed: 5032
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 143 KB/s], Decompressed: 5073
Downloaded: 5118 file(s) [attempted 5118/8459 = 60%, 71 KB/s], Decompressed: 5115
Downloaded: 5161 file(s) [attempted 5161/8459 = 61%, 445 KB/s], Decompressed: 5152
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 451 KB/s], Decompressed: 5197
Downloaded: 5241 file(s) [attempted 5241/8459 = 61%, 45 KB/s], Decompressed: 5238
Downloaded: 5280 file(s) [attempted 5280/8459 = 62%, 714 KB/s], Decompressed: 5269
Downloaded: 5316 file(s) [attempted 5316/8459 = 62%, 144 KB/s], Decompressed: 5313
Downloaded: 5354 file(s) [attempted 5354/8459 = 63%, 613 KB/s], Decompressed: 5351
Downloaded: 5397 file(s) [attempted 5397/8459 = 63%, 489 KB/s], Decompressed: 5392
Downloaded: 5436 file(s) [attempted 5436/8459 = 64%, 263 KB/s], Decompressed: 5433
Downloaded: 5474 file(s) [attempted 5474/8459 = 64%, 152 KB/s], Decompressed: 5470
Downloaded: 5514 file(s) [attempted 5514/8459 = 65%, 211 KB/s], Decompressed: 5508
Downloaded: 5553 file(s) [attempted 5553/8459 = 65%, 48 KB/s], Decompressed: 5542
Downloaded: 5594 file(s) [attempted 5594/8459 = 66%, 250 KB/s], Decompressed: 5587
Downloaded: 5629 file(s) [attempted 5629/8459 = 66%, 1328 KB/s], Decompressed: 5624
Downloaded: 5672 file(s) [attempted 5672/8459 = 67%, 69 KB/s], Decompressed: 5669
Downloaded: 5713 file(s) [attempted 5713/8459 = 67%, 191 KB/s], Decompressed: 5710
Downloaded: 5755 file(s) [attempted 5755/8459 = 68%, 90 KB/s], Decompressed: 5748
Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 60 KB/s], Decompressed: 5789
Downloaded: 5827 file(s) [attempted 5827/8459 = 68%, 165 KB/s], Decompressed: 5823
Downloaded: 5871 file(s) [attempted 5871/8459 = 69%, 178 KB/s], Decompressed: 5867
Downloaded: 5914 file(s) [attempted 5914/8459 = 69%, 49 KB/s], Decompressed: 5909
Downloaded: 5950 file(s) [attempted 5950/8459 = 70%, 89 KB/s], Decompressed: 5946
Downloaded: 5989 file(s) [attempted 5989/8459 = 70%, 1528 KB/s], Decompressed: 5984
Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 27 KB/s], Decompressed: 6021
Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 355 KB/s], Decompressed: 6066
Downloaded: 6114 file(s) [attempted 6114/8459 = 72%, 3171 KB/s], Decompressed: 6104
Downloaded: 6151 file(s) [attempted 6151/8459 = 72%, 370 KB/s], Decompressed: 6148
Downloaded: 6196 file(s) [attempted 6196/8459 = 73%, 319 KB/s], Decompressed: 6189
Downloaded: 6234 file(s) [attempted 6234/8459 = 73%, 655 KB/s], Decompressed: 6230
Downloaded: 6268 file(s) [attempted 6268/8459 = 74%, 104 KB/s], Decompressed: 6262
Downloaded: 6308 file(s) [attempted 6308/8459 = 74%, 144 KB/s], Decompressed: 6302
Downloaded: 6347 file(s) [attempted 6347/8459 = 75%, 56 KB/s], Decompressed: 6343
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 60 KB/s], Decompressed: 6388
Downloaded: 6429 file(s) [attempted 6429/8459 = 76%, 85 KB/s], Decompressed: 6418
Downloaded: 6460 file(s) [attempted 6460/8459 = 76%, 884 KB/s], Decompressed: 6456
Downloaded: 6507 file(s) [attempted 6507/8459 = 76%, 80 KB/s], Decompressed: 6504
Downloaded: 6552 file(s) [attempted 6552/8459 = 77%, 98 KB/s], Decompressed: 6548
Downloaded: 6592 file(s) [attempted 6592/8459 = 77%, 123 KB/s], Decompressed: 6586
Downloaded: 6626 file(s) [attempted 6626/8459 = 78%, 313 KB/s], Decompressed: 6617
Downloaded: 6663 file(s) [attempted 6663/8459 = 78%, 322 KB/s], Decompressed: 6658
Downloaded: 6709 file(s) [attempted 6709/8459 = 79%, 439 KB/s], Decompressed: 6702
Downloaded: 6757 file(s) [attempted 6757/8459 = 79%, 283 KB/s], Decompressed: 6740
Downloaded: 6802 file(s) [attempted 6802/8459 = 80%, 140 KB/s], Decompressed: 6798
Downloaded: 6839 file(s) [attempted 6839/8459 = 80%, 95 KB/s], Decompressed: 6836
Downloaded: 6871 file(s) [attempted 6871/8459 = 81%, 780 KB/s], Decompressed: 6867
Downloaded: 6915 file(s) [attempted 6915/8459 = 81%, 419 KB/s], Decompressed: 6911
Downloaded: 6956 file(s) [attempted 6956/8459 = 82%, 172 KB/s], Decompressed: 6952
Downloaded: 6993 file(s) [attempted 6993/8459 = 82%, 1311 KB/s], Decompressed: 6976
Downloaded: 7031 file(s) [attempted 7031/8459 = 83%, 1790 KB/s], Decompressed: 7024
Downloaded: 7072 file(s) [attempted 7072/8459 = 83%, 288 KB/s], Decompressed: 7069
Downloaded: 7117 file(s) [attempted 7117/8459 = 84%, 81 KB/s], Decompressed: 7113
Downloaded: 7154 file(s) [attempted 7154/8459 = 84%, 99 KB/s], Decompressed: 7151
Downloaded: 7192 file(s) [attempted 7192/8459 = 85%, 55 KB/s], Decompressed: 7182
Downloaded: 7226 file(s) [attempted 7226/8459 = 85%, 152 KB/s], Decompressed: 7223
Downloaded: 7271 file(s) [attempted 7271/8459 = 85%, 78 KB/s], Decompressed: 7267
Downloaded: 7315 file(s) [attempted 7315/8459 = 86%, 197 KB/s], Decompressed: 7308
Downloaded: 7349 file(s) [attempted 7349/8459 = 86%, 46 KB/s], Decompressed: 7348
Downloaded: 7387 file(s) [attempted 7387/8459 = 87%, 91 KB/s], Decompressed: 7384
Downloaded: 7428 file(s) [attempted 7428/8459 = 87%, 105 KB/s], Decompressed: 7421
Downloaded: 7473 file(s) [attempted 7473/8459 = 88%, 353 KB/s], Decompressed: 7469
Downloaded: 7510 file(s) [attempted 7510/8459 = 88%, 216 KB/s], Decompressed: 7503
Downloaded: 7541 file(s) [attempted 7541/8459 = 89%, 198 KB/s], Decompressed: 7534
Downloaded: 7585 file(s) [attempted 7585/8459 = 89%, 153 KB/s], Decompressed: 7582
Downloaded: 7627 file(s) [attempted 7627/8459 = 90%, 131 KB/s], Decompressed: 7623
Downloaded: 7670 file(s) [attempted 7670/8459 = 90%, 39 KB/s], Decompressed: 7661
Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 69 KB/s], Decompressed: 7698
Downloaded: 7739 file(s) [attempted 7739/8459 = 91%, 782 KB/s], Decompressed: 7736
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 31 KB/s], Decompressed: 7781
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 443 KB/s], Decompressed: 7815
Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 34 KB/s], Decompressed: 7856
Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 237 KB/s], Decompressed: 7880
Downloaded: 7941 file(s) [attempted 7941/8459 = 93%, 314 KB/s], Decompressed: 7938
Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 825 KB/s], Decompressed: 7969
Downloaded: 8017 file(s) [attempted 8017/8459 = 94%, 116 KB/s], Decompressed: 8013
Downloaded: 8058 file(s) [attempted 8058/8459 = 95%, 479 KB/s], Decompressed: 8054
Downloaded: 8099 file(s) [attempted 8099/8459 = 95%, 355 KB/s], Decompressed: 8095
Downloaded: 8138 file(s) [attempted 8138/8459 = 96%, 299 KB/s], Decompressed: 8131
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 1094 KB/s], Decompressed: 8164
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 104 KB/s], Decompressed: 8212
Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 112 KB/s], Decompressed: 8256
Downloaded: 8302 file(s) [attempted 8302/8459 = 98%, 87 KB/s], Decompressed: 8294
Downloaded: 8342 file(s) [attempted 8342/8459 = 98%, 782 KB/s], Decompressed: 8338
Downloaded: 8379 file(s) [attempted 8379/8459 = 99%, 125 KB/s], Decompressed: 8373
Downloaded: 8417 file(s) [attempted 8417/8459 = 99%, 110 KB/s], Decompressed: 8414
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 499 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 499 KB/s], Decompressed: 8455

lake build

ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (188s)
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) [0x75c5863c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x75c5863bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x75c5863bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x75c5862f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x75c5862f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x75c5863caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x75c586232923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x75c586232b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x75c586233827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x75c5862341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x75c5863c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x75c586015adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x75c5863c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x75c5863c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x75c58639b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x75c586015c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x75c581422638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x75c58120cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x75c580d69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x75c580d69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x75c57dc4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x75c57dc45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5cb7f03ea8da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (5.9s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.1s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (36s)
✔ [3414/3416] Built Iut.Basic (2.6s)
✔ [3415/3416] Built Iut (2.3s)
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-batch-00000)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache f4d8a5a71ef92e1eca529c90b5502827db3b1734353de1d3795d9937d061cd59
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)

lean semantic helper: restored compiled static runner cache 8ce5ff6c967baef3842b8fb460ab7dc29b28a04bbb424be955c4371e23608184
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)

lean semantic helper: restored compiled static runner cache 6247def1945279a6946b34517b575ac426a9bd22cc4c3ceb7a79dc06ef4083db
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 1743058e355c2c9d0a14ee7f999dc06a3d68424d26bfda2428b61a1002396ce8
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)

lean semantic helper: restored compiled static runner cache e103fd3939aed645f6a64b867308ee472e79eb2af9586b744c189d70ac5f91ea
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes