Verification run
Run 358
succeeded commit
f0fb6f74cd70 toolchain lean-v4-30-0 prover lean took 3h 15m · finished 4w ago
Package inputs
This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.
Trust verification
Recomputes trust checks from the recorded attestations, manifest, and command history.
(verification not run)
Manifest
Loads the published files manifest and location metadata for this job.
(manifest not loaded)
Verifier log excerpt
$ git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-528-source
exit_code=Some(0) duration_ms=2642
stderr:
Cloning into '/var/lib/apodeixis/repos/job-528-source'...
$ git checkout f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda
exit_code=Some(128) duration_ms=2
stderr:
fatal: reference is not a tree: f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda
$ git fetch --depth 1 origin f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda
exit_code=Some(0) duration_ms=1047
stderr:
From https://github.com/promachina/iut-lean
* branch f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda -> FETCH_HEAD
$ git checkout f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda (after fetch)
exit_code=Some(0) duration_ms=137
stderr:
Note: switching to 'f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda'.
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 f0fb6f7 Derive local log landing factorwise
Resolved source revision: f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda provenance={"branch":"master","checked_out_revision":"f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda","used_missing_commit_fetch":true}
Resolved toolchain: lean-v4-30-0 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
Restored Lean workspace build cache
Restored 9 Lean dependency package snapshot(s)
Prepared 9 shared Lean git mirror alias(es)
Lean semantic module cache: computed 31 module hash fact(s) from source and olean files; skipping Lean module-facts probe
Lean semantic module cache: 25/31 module hit(s), 6 miss(es)
Lean semantic module cache: trying stable superset runner for 6 missing module(s) with 31 imported module candidate(s)
Lean semantic module cache: checkpointed 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=48597
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: 13 file(s) [attempted 13/8459 = 0%, 11 KB/s], Decompressed: 10
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 22 KB/s], Decompressed: 38
Downloaded: 69 file(s) [attempted 69/8459 = 0%, 50 KB/s], Decompressed: 64
Downloaded: 100 file(s) [attempted 100/8459 = 1%, 93 KB/s], Decompressed: 95
Downloaded: 136 file(s) [attempted 136/8459 = 1%, 480 KB/s], Decompressed: 127
Downloaded: 159 file(s) [attempted 159/8459 = 1%, 80 KB/s], Decompressed: 155
Downloaded: 192 file(s) [attempted 192/8459 = 2%, 42 KB/s], Decompressed: 189
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 206 KB/s], Decompressed: 230
Downloaded: 275 file(s) [attempted 275/8459 = 3%, 48 KB/s], Decompressed: 271
Downloaded: 316 file(s) [attempted 316/8459 = 3%, 145 KB/s], Decompressed: 309
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 853 KB/s], Decompressed: 343
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 1069 KB/s], Decompressed: 388
Downloaded: 425 file(s) [attempted 425/8459 = 5%, 331 KB/s], Decompressed: 422
Downloaded: 470 file(s) [attempted 470/8459 = 5%, 714 KB/s], Decompressed: 466
Downloaded: 516 file(s) [attempted 516/8459 = 6%, 291 KB/s], Decompressed: 508
Downloaded: 556 file(s) [attempted 556/8459 = 6%, 250 KB/s], Decompressed: 545
Downloaded: 595 file(s) [attempted 595/8459 = 7%, 404 KB/s], Decompressed: 586
Downloaded: 628 file(s) [attempted 628/8459 = 7%, 606 KB/s], Decompressed: 621
Downloaded: 667 file(s) [attempted 667/8459 = 7%, 59 KB/s], Decompressed: 662
Downloaded: 710 file(s) [attempted 710/8459 = 8%, 144 KB/s], Decompressed: 703
Downloaded: 754 file(s) [attempted 754/8459 = 8%, 307 KB/s], Decompressed: 746
Downloaded: 795 file(s) [attempted 795/8459 = 9%, 113 KB/s], Decompressed: 788
Downloaded: 833 file(s) [attempted 833/8459 = 9%, 345 KB/s], Decompressed: 823
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 385 KB/s], Decompressed: 860
Downloaded: 908 file(s) [attempted 908/8459 = 10%, 494 KB/s], Decompressed: 905
Downloaded: 956 file(s) [attempted 956/8459 = 11%, 152 KB/s], Decompressed: 949
Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 305 KB/s], Decompressed: 997
Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 859 KB/s], Decompressed: 1028
Downloaded: 1073 file(s) [attempted 1073/8459 = 12%, 213 KB/s], Decompressed: 1066
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 84 KB/s], Decompressed: 1100
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 352 KB/s], Decompressed: 1148
Downloaded: 1196 file(s) [attempted 1196/8459 = 14%, 500 KB/s], Decompressed: 1189
Downloaded: 1237 file(s) [attempted 1237/8459 = 14%, 95 KB/s], Decompressed: 1230
Downloaded: 1265 file(s) [attempted 1265/8459 = 14%, 28 KB/s], Decompressed: 1258
Downloaded: 1305 file(s) [attempted 1305/8459 = 15%, 631 KB/s], Decompressed: 1299
Downloaded: 1350 file(s) [attempted 1350/8459 = 15%, 52 KB/s], Decompressed: 1346
Downloaded: 1391 file(s) [attempted 1391/8459 = 16%, 32 KB/s], Decompressed: 1388
Downloaded: 1432 file(s) [attempted 1432/8459 = 16%, 1265 KB/s], Decompressed: 1418
Downloaded: 1463 file(s) [attempted 1463/8459 = 17%, 180 KB/s], Decompressed: 1459
Downloaded: 1504 file(s) [attempted 1504/8459 = 17%, 852 KB/s], Decompressed: 1490
Downloaded: 1542 file(s) [attempted 1542/8459 = 18%, 422 KB/s], Decompressed: 1538
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 949 KB/s], Decompressed: 1579
Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 447 KB/s], Decompressed: 1617
Downloaded: 1661 file(s) [attempted 1661/8459 = 19%, 57 KB/s], Decompressed: 1655
Downloaded: 1702 file(s) [attempted 1702/8459 = 20%, 510 KB/s], Decompressed: 1696
Downloaded: 1741 file(s) [attempted 1741/8459 = 20%, 192 KB/s], Decompressed: 1737
Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 68 KB/s], Decompressed: 1781
Downloaded: 1826 file(s) [attempted 1826/8459 = 21%, 211 KB/s], Decompressed: 1819
Downloaded: 1860 file(s) [attempted 1860/8459 = 21%, 30 KB/s], Decompressed: 1853
Downloaded: 1897 file(s) [attempted 1897/8459 = 22%, 763 KB/s], Decompressed: 1894
Downloaded: 1936 file(s) [attempted 1936/8459 = 22%, 334 KB/s], Decompressed: 1928
Downloaded: 1978 file(s) [attempted 1978/8459 = 23%, 48 KB/s], Decompressed: 1969
Downloaded: 2017 file(s) [attempted 2017/8459 = 23%, 291 KB/s], Decompressed: 2010
Downloaded: 2053 file(s) [attempted 2053/8459 = 24%, 666 KB/s], Decompressed: 2045
Downloaded: 2093 file(s) [attempted 2093/8459 = 24%, 254 KB/s], Decompressed: 2089
Downloaded: 2137 file(s) [attempted 2137/8459 = 25%, 668 KB/s], Decompressed: 2130
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 95 KB/s], Decompressed: 2171
Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 329 KB/s], Decompressed: 2212
Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 361 KB/s], Decompressed: 2256
Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 990 KB/s], Decompressed: 2291
Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 85 KB/s], Decompressed: 2329
Downloaded: 2380 file(s) [attempted 2380/8459 = 28%, 986 KB/s], Decompressed: 2377
Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 45 KB/s], Decompressed: 2411
Downloaded: 2455 file(s) [attempted 2455/8459 = 29%, 257 KB/s], Decompressed: 2448
Downloaded: 2496 file(s) [attempted 2496/8459 = 29%, 77 KB/s], Decompressed: 2490
Downloaded: 2541 file(s) [attempted 2541/8459 = 30%, 331 KB/s], Decompressed: 2537
Downloaded: 2582 file(s) [attempted 2582/8459 = 30%, 50 KB/s], Decompressed: 2575
Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 23 KB/s], Decompressed: 2613
Downloaded: 2661 file(s) [attempted 2661/8459 = 31%, 567 KB/s], Decompressed: 2657
Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 489 KB/s], Decompressed: 2698
Downloaded: 2746 file(s) [attempted 2746/8459 = 32%, 44 KB/s], Decompressed: 2739
Downloaded: 2784 file(s) [attempted 2784/8459 = 32%, 832 KB/s], Decompressed: 2777
Downloaded: 2819 file(s) [attempted 2819/8459 = 33%, 233 KB/s], Decompressed: 2815
Downloaded: 2859 file(s) [attempted 2859/8459 = 33%, 308 KB/s], Decompressed: 2856
Downloaded: 2905 file(s) [attempted 2905/8459 = 34%, 1494 KB/s], Decompressed: 2900
Downloaded: 2941 file(s) [attempted 2941/8459 = 34%, 808 KB/s], Decompressed: 2938
Downloaded: 2979 file(s) [attempted 2979/8459 = 35%, 584 KB/s], Decompressed: 2972
Downloaded: 3023 file(s) [attempted 3023/8459 = 35%, 479 KB/s], Decompressed: 3017
Downloaded: 3065 file(s) [attempted 3065/8459 = 36%, 172 KB/s], Decompressed: 3061
Downloaded: 3102 file(s) [attempted 3102/8459 = 36%, 234 KB/s], Decompressed: 3095
Downloaded: 3147 file(s) [attempted 3147/8459 = 37%, 79 KB/s], Decompressed: 3140
Downloaded: 3188 file(s) [attempted 3188/8459 = 37%, 167 KB/s], Decompressed: 3184
Downloaded: 3225 file(s) [attempted 3225/8459 = 38%, 52 KB/s], Decompressed: 3224
Downloaded: 3266 file(s) [attempted 3266/8459 = 38%, 584 KB/s], Decompressed: 3260
Downloaded: 3309 file(s) [attempted 3309/8459 = 39%, 693 KB/s], Decompressed: 3297
Downloaded: 3345 file(s) [attempted 3345/8459 = 39%, 1348 KB/s], Decompressed: 3338
Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 44 KB/s], Decompressed: 3383
Downloaded: 3427 file(s) [attempted 3427/8459 = 40%, 227 KB/s], Decompressed: 3420
Downloaded: 3462 file(s) [attempted 3462/8459 = 40%, 510 KB/s], Decompressed: 3458
Downloaded: 3506 file(s) [attempted 3506/8459 = 41%, 748 KB/s], Decompressed: 3496
Downloaded: 3547 file(s) [attempted 3547/8459 = 41%, 189 KB/s], Decompressed: 3544
Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 170 KB/s], Decompressed: 3581
Downloaded: 3622 file(s) [attempted 3622/8459 = 42%, 1253 KB/s], Decompressed: 3619
Downloaded: 3660 file(s) [attempted 3660/8459 = 43%, 105 KB/s], Decompressed: 3657
Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 1097 KB/s], Decompressed: 3698
Downloaded: 3742 file(s) [attempted 3742/8459 = 44%, 372 KB/s], Decompressed: 3739
Downloaded: 3780 file(s) [attempted 3780/8459 = 44%, 332 KB/s], Decompressed: 3770
Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 221 KB/s], Decompressed: 3807
Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 1487 KB/s], Decompressed: 3852
Downloaded: 3900 file(s) [attempted 3900/8459 = 46%, 194 KB/s], Decompressed: 3896
Downloaded: 3941 file(s) [attempted 3941/8459 = 46%, 476 KB/s], Decompressed: 3934
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 334 KB/s], Decompressed: 3971
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 312 KB/s], Decompressed: 4006
Downloaded: 4054 file(s) [attempted 4054/8459 = 47%, 128 KB/s], Decompressed: 4050
Downloaded: 4091 file(s) [attempted 4091/8459 = 48%, 1460 KB/s], Decompressed: 4088
Downloaded: 4129 file(s) [attempted 4129/8459 = 48%, 612 KB/s], Decompressed: 4125
Downloaded: 4167 file(s) [attempted 4167/8459 = 49%, 633 KB/s], Decompressed: 4163
Downloaded: 4209 file(s) [attempted 4209/8459 = 49%, 58 KB/s], Decompressed: 4204
Downloaded: 4249 file(s) [attempted 4249/8459 = 50%, 207 KB/s], Decompressed: 4245
Downloaded: 4286 file(s) [attempted 4286/8459 = 50%, 57 KB/s], Decompressed: 4279
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 1934 KB/s], Decompressed: 4324
Downloaded: 4372 file(s) [attempted 4372/8459 = 51%, 72 KB/s], Decompressed: 4365
Downloaded: 4406 file(s) [attempted 4406/8459 = 52%, 463 KB/s], Decompressed: 4399
Downloaded: 4447 file(s) [attempted 4447/8459 = 52%, 51 KB/s], Decompressed: 4444
Downloaded: 4490 file(s) [attempted 4490/8459 = 53%, 241 KB/s], Decompressed: 4481
Downloaded: 4526 file(s) [attempted 4526/8459 = 53%, 54 KB/s], Decompressed: 4519
Downloaded: 4564 file(s) [attempted 4564/8459 = 53%, 122 KB/s], Decompressed: 4557
Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 529 KB/s], Decompressed: 4594
Downloaded: 4642 file(s) [attempted 4642/8459 = 54%, 101 KB/s], Decompressed: 4639
Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 362 KB/s], Decompressed: 4680
Downloaded: 4724 file(s) [attempted 4724/8459 = 55%, 675 KB/s], Decompressed: 4721
Downloaded: 4759 file(s) [attempted 4759/8459 = 56%, 127 KB/s], Decompressed: 4755
Downloaded: 4803 file(s) [attempted 4803/8459 = 56%, 165 KB/s], Decompressed: 4796
Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 71 KB/s], Decompressed: 4837
Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 1068 KB/s], Decompressed: 4882
Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 474 KB/s], Decompressed: 4919
Downloaded: 4962 file(s) [attempted 4962/8459 = 58%, 39 KB/s], Decompressed: 4957
Downloaded: 4999 file(s) [attempted 4999/8459 = 59%, 251 KB/s], Decompressed: 4995
Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 185 KB/s], Decompressed: 5039
Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 326 KB/s], Decompressed: 5080
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 514 KB/s], Decompressed: 5115
Downloaded: 5159 file(s) [attempted 5159/8459 = 60%, 139 KB/s], Decompressed: 5152
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 114 KB/s], Decompressed: 5197
Downloaded: 5248 file(s) [attempted 5248/8459 = 62%, 877 KB/s], Decompressed: 5245
Downloaded: 5296 file(s) [attempted 5296/8459 = 62%, 206 KB/s], Decompressed: 5289
Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 196 KB/s], Decompressed: 5330
Downloaded: 5371 file(s) [attempted 5371/8459 = 63%, 179 KB/s], Decompressed: 5364
Downloaded: 5409 file(s) [attempted 5409/8459 = 63%, 493 KB/s], Decompressed: 5405
Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 312 KB/s], Decompressed: 5450
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 588 KB/s], Decompressed: 5494
Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 39 KB/s], Decompressed: 5539
Downloaded: 5583 file(s) [attempted 5583/8459 = 66%, 102 KB/s], Decompressed: 5577
Downloaded: 5614 file(s) [attempted 5614/8459 = 66%, 389 KB/s], Decompressed: 5611
Downloaded: 5656 file(s) [attempted 5656/8459 = 66%, 859 KB/s], Decompressed: 5648
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 118 KB/s], Decompressed: 5693
Downloaded: 5741 file(s) [attempted 5741/8459 = 67%, 261 KB/s], Decompressed: 5737
Downloaded: 5782 file(s) [attempted 5782/8459 = 68%, 80 KB/s], Decompressed: 5778
Downloaded: 5820 file(s) [attempted 5820/8459 = 68%, 109 KB/s], Decompressed: 5813
Downloaded: 5857 file(s) [attempted 5857/8459 = 69%, 461 KB/s], Decompressed: 5854
Downloaded: 5898 file(s) [attempted 5898/8459 = 69%, 700 KB/s], Decompressed: 5891
Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 57 KB/s], Decompressed: 5936
Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 261 KB/s], Decompressed: 5977
Downloaded: 6017 file(s) [attempted 6017/8459 = 71%, 65 KB/s], Decompressed: 6008
Downloaded: 6056 file(s) [attempted 6056/8459 = 71%, 1954 KB/s], Decompressed: 6045
Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 1753 KB/s], Decompressed: 6093
Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 144 KB/s], Decompressed: 6134
Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 58 KB/s], Decompressed: 6179
Downloaded: 6217 file(s) [attempted 6217/8459 = 73%, 40 KB/s], Decompressed: 6213
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 33 KB/s], Decompressed: 6247
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 227 KB/s], Decompressed: 6292
Downloaded: 6337 file(s) [attempted 6337/8459 = 74%, 353 KB/s], Decompressed: 6333
Downloaded: 6381 file(s) [attempted 6381/8459 = 75%, 288 KB/s], Decompressed: 6371
Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 43 KB/s], Decompressed: 6408
Downloaded: 6453 file(s) [attempted 6453/8459 = 76%, 1726 KB/s], Decompressed: 6449
Downloaded: 6490 file(s) [attempted 6490/8459 = 76%, 407 KB/s], Decompressed: 6483
Downloaded: 6535 file(s) [attempted 6535/8459 = 77%, 30 KB/s], Decompressed: 6528
Downloaded: 6572 file(s) [attempted 6572/8459 = 77%, 138 KB/s], Decompressed: 6566
Downloaded: 6607 file(s) [attempted 6607/8459 = 78%, 313 KB/s], Decompressed: 6603
Downloaded: 6649 file(s) [attempted 6649/8459 = 78%, 272 KB/s], Decompressed: 6644
Downloaded: 6687 file(s) [attempted 6687/8459 = 79%, 99 KB/s], Decompressed: 6679
Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 264 KB/s], Decompressed: 6723
Downloaded: 6768 file(s) [attempted 6768/8459 = 80%, 73 KB/s], Decompressed: 6761
Downloaded: 6805 file(s) [attempted 6805/8459 = 80%, 521 KB/s], Decompressed: 6798
Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 58 KB/s], Decompressed: 6839
Downloaded: 6880 file(s) [attempted 6880/8459 = 81%, 67 KB/s], Decompressed: 6877
Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 348 KB/s], Decompressed: 6918
Downloaded: 6969 file(s) [attempted 6969/8459 = 82%, 54 KB/s], Decompressed: 6959
Downloaded: 7005 file(s) [attempted 7005/8459 = 82%, 369 KB/s], Decompressed: 7000
Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 112 KB/s], Decompressed: 7038
Downloaded: 7086 file(s) [attempted 7086/8459 = 83%, 223 KB/s], Decompressed: 7082
Downloaded: 7130 file(s) [attempted 7130/8459 = 84%, 1004 KB/s], Decompressed: 7127
Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 142 KB/s], Decompressed: 7166
Downloaded: 7209 file(s) [attempted 7209/8459 = 85%, 160 KB/s], Decompressed: 7206
Downloaded: 7241 file(s) [attempted 7241/8459 = 85%, 458 KB/s], Decompressed: 7236
Downloaded: 7284 file(s) [attempted 7284/8459 = 86%, 46 KB/s], Decompressed: 7281
Downloaded: 7329 file(s) [attempted 7329/8459 = 86%, 221 KB/s], Decompressed: 7325
Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 1319 KB/s], Decompressed: 7363
Downloaded: 7402 file(s) [attempted 7402/8459 = 87%, 283 KB/s], Decompressed: 7397
Downloaded: 7442 file(s) [attempted 7442/8459 = 87%, 105 KB/s], Decompressed: 7438
Downloaded: 7483 file(s) [attempted 7483/8459 = 88%, 625 KB/s], Decompressed: 7479
Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 119 KB/s], Decompressed: 7524
Downloaded: 7565 file(s) [attempted 7565/8459 = 89%, 233 KB/s], Decompressed: 7562
Downloaded: 7603 file(s) [attempted 7603/8459 = 89%, 290 KB/s], Decompressed: 7599
Downloaded: 7640 file(s) [attempted 7640/8459 = 90%, 1480 KB/s], Decompressed: 7637
Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 49 KB/s], Decompressed: 7681
Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 32 KB/s], Decompressed: 7719
Downloaded: 7764 file(s) [attempted 7764/8459 = 91%, 175 KB/s], Decompressed: 7757
Downloaded: 7804 file(s) [attempted 7804/8459 = 92%, 612 KB/s], Decompressed: 7798
Downloaded: 7846 file(s) [attempted 7846/8459 = 92%, 211 KB/s], Decompressed: 7842
Downloaded: 7883 file(s) [attempted 7883/8459 = 93%, 853 KB/s], Decompressed: 7880
Downloaded: 7924 file(s) [attempted 7924/8459 = 93%, 398 KB/s], Decompressed: 7921
Downloaded: 7958 file(s) [attempted 7958/8459 = 94%, 130 KB/s], Decompressed: 7955
Downloaded: 8000 file(s) [attempted 8000/8459 = 94%, 319 KB/s], Decompressed: 7996
Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 511 KB/s], Decompressed: 8037
Downloaded: 8078 file(s) [attempted 8078/8459 = 95%, 177 KB/s], Decompressed: 8075
Downloaded: 8120 file(s) [attempted 8120/8459 = 95%, 109 KB/s], Decompressed: 8112
Downloaded: 8157 file(s) [attempted 8157/8459 = 96%, 115 KB/s], Decompressed: 8154
Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 128 KB/s], Decompressed: 8195
Downloaded: 8239 file(s) [attempted 8239/8459 = 97%, 52 KB/s], Decompressed: 8232
Downloaded: 8274 file(s) [attempted 8274/8459 = 97%, 143 KB/s], Decompressed: 8270
Downloaded: 8314 file(s) [attempted 8314/8459 = 98%, 52 KB/s], Decompressed: 8308
Downloaded: 8355 file(s) [attempted 8355/8459 = 98%, 407 KB/s], Decompressed: 8352
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 551 KB/s], Decompressed: 8390
Downloaded: 8438 file(s) [attempted 8438/8459 = 99%, 315 KB/s], Decompressed: 8431
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 315 KB/s], Decompressed: 8455
$ lake build
exit_code=Some(0) duration_ms=316934
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) [0x7534635c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7534635bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7534635bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7534634f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7534634f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7534635caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x753463432923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x753463432b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x753463433827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7534634341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7534635c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x753463215adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7534635c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7534635c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x75346359b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x753463215c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x75345e622638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x75345e40cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x75345df69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x75345df69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x75345ae4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x75345ae45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5839161818da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (28s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (4.4s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (38s)
✔ [3414/3416] Built Iut.Basic (4.2s)
✔ [3415/3416] Built Iut (2.8s)
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=3365
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=11110655
stdout:
apx-semantic-phase {"duration_ms":6,"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":389051,"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":81,"module_count":1,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"ok":true,"payload_bytes":738,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":2,"module_index":0,"ok":true,"payload_bytes":738,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":1,"diagnostic_count":0,"duration_ms":326,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":390531,"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":81,"module_count":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"ok":true,"payload_bytes":1330,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"ok":true,"payload_bytes":1330,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":97,"diagnostic_count":15,"duration_ms":8172,"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":370540,"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":416,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"ok":true,"payload_bytes":3002937,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":2,"module_index":2,"ok":true,"payload_bytes":3002937,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":1889,"diagnostic_count":116,"duration_ms":1557014,"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":416284,"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":1889,"diagnostic_count":116,"duration_ms":9086,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"ok":true,"payload_bytes":67044380,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":53,"module_index":3,"ok":true,"payload_bytes":67044380,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":7754,"diagnostic_count":3093,"duration_ms":6296487,"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":555384,"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":7754,"diagnostic_count":3093,"duration_ms":40578,"module_count":1,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":4,"ok":true,"payload_bytes":464123762,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":381,"module_index":4,"ok":true,"payload_bytes":464123762,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":152,"diagnostic_count":23,"duration_ms":29201,"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":1007080,"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":555,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":5,"ok":true,"payload_bytes":2722873,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":12,"module_index":5,"ok":true,"payload_bytes":2722873,"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":4843}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":392,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":30,"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":18019,"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 1e7ffe582ba39c9551655c0d7e38db1c047d5b7a37a348d217240ffb58a3206c
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":11086537,"ok":true}
Stored Lean workspace build cache
Stored Lean semantic extraction cache
Command runs
git_clone exit 0
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-528-source
Cloning into '/var/lib/apodeixis/repos/job-528-source'...
git_checkout exit 128
git checkout f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda
fatal: reference is not a tree: f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda
git_checkout exit 0
git fetch --depth 1 origin f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda
From https://github.com/promachina/iut-lean * branch f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda -> FETCH_HEAD
git_checkout exit 0
git checkout f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda (after fetch)
Note: switching to 'f0fb6f74cd70c59c45e413c8dc79d26bb15e1fda'. 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 f0fb6f7 Derive local log landing factorwise
lake_cache exit 0
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: 13 file(s) [attempted 13/8459 = 0%, 11 KB/s], Decompressed: 10 Downloaded: 39 file(s) [attempted 39/8459 = 0%, 22 KB/s], Decompressed: 38 Downloaded: 69 file(s) [attempted 69/8459 = 0%, 50 KB/s], Decompressed: 64 Downloaded: 100 file(s) [attempted 100/8459 = 1%, 93 KB/s], Decompressed: 95 Downloaded: 136 file(s) [attempted 136/8459 = 1%, 480 KB/s], Decompressed: 127 Downloaded: 159 file(s) [attempted 159/8459 = 1%, 80 KB/s], Decompressed: 155 Downloaded: 192 file(s) [attempted 192/8459 = 2%, 42 KB/s], Decompressed: 189 Downloaded: 234 file(s) [attempted 234/8459 = 2%, 206 KB/s], Decompressed: 230 Downloaded: 275 file(s) [attempted 275/8459 = 3%, 48 KB/s], Decompressed: 271 Downloaded: 316 file(s) [attempted 316/8459 = 3%, 145 KB/s], Decompressed: 309 Downloaded: 353 file(s) [attempted 353/8459 = 4%, 853 KB/s], Decompressed: 343 Downloaded: 391 file(s) [attempted 391/8459 = 4%, 1069 KB/s], Decompressed: 388 Downloaded: 425 file(s) [attempted 425/8459 = 5%, 331 KB/s], Decompressed: 422 Downloaded: 470 file(s) [attempted 470/8459 = 5%, 714 KB/s], Decompressed: 466 Downloaded: 516 file(s) [attempted 516/8459 = 6%, 291 KB/s], Decompressed: 508 Downloaded: 556 file(s) [attempted 556/8459 = 6%, 250 KB/s], Decompressed: 545 Downloaded: 595 file(s) [attempted 595/8459 = 7%, 404 KB/s], Decompressed: 586 Downloaded: 628 file(s) [attempted 628/8459 = 7%, 606 KB/s], Decompressed: 621 Downloaded: 667 file(s) [attempted 667/8459 = 7%, 59 KB/s], Decompressed: 662 Downloaded: 710 file(s) [attempted 710/8459 = 8%, 144 KB/s], Decompressed: 703 Downloaded: 754 file(s) [attempted 754/8459 = 8%, 307 KB/s], Decompressed: 746 Downloaded: 795 file(s) [attempted 795/8459 = 9%, 113 KB/s], Decompressed: 788 Downloaded: 833 file(s) [attempted 833/8459 = 9%, 345 KB/s], Decompressed: 823 Downloaded: 867 file(s) [attempted 867/8459 = 10%, 385 KB/s], Decompressed: 860 Downloaded: 908 file(s) [attempted 908/8459 = 10%, 494 KB/s], Decompressed: 905 Downloaded: 956 file(s) [attempted 956/8459 = 11%, 152 KB/s], Decompressed: 949 Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 305 KB/s], Decompressed: 997 Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 859 KB/s], Decompressed: 1028 Downloaded: 1073 file(s) [attempted 1073/8459 = 12%, 213 KB/s], Decompressed: 1066 Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 84 KB/s], Decompressed: 1100 Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 352 KB/s], Decompressed: 1148 Downloaded: 1196 file(s) [attempted 1196/8459 = 14%, 500 KB/s], Decompressed: 1189 Downloaded: 1237 file(s) [attempted 1237/8459 = 14%, 95 KB/s], Decompressed: 1230 Downloaded: 1265 file(s) [attempted 1265/8459 = 14%, 28 KB/s], Decompressed: 1258 Downloaded: 1305 file(s) [attempted 1305/8459 = 15%, 631 KB/s], Decompressed: 1299 Downloaded: 1350 file(s) [attempted 1350/8459 = 15%, 52 KB/s], Decompressed: 1346 Downloaded: 1391 file(s) [attempted 1391/8459 = 16%, 32 KB/s], Decompressed: 1388 Downloaded: 1432 file(s) [attempted 1432/8459 = 16%, 1265 KB/s], Decompressed: 1418 Downloaded: 1463 file(s) [attempted 1463/8459 = 17%, 180 KB/s], Decompressed: 1459 Downloaded: 1504 file(s) [attempted 1504/8459 = 17%, 852 KB/s], Decompressed: 1490 Downloaded: 1542 file(s) [attempted 1542/8459 = 18%, 422 KB/s], Decompressed: 1538 Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 949 KB/s], Decompressed: 1579 Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 447 KB/s], Decompressed: 1617 Downloaded: 1661 file(s) [attempted 1661/8459 = 19%, 57 KB/s], Decompressed: 1655 Downloaded: 1702 file(s) [attempted 1702/8459 = 20%, 510 KB/s], Decompressed: 1696 Downloaded: 1741 file(s) [attempted 1741/8459 = 20%, 192 KB/s], Decompressed: 1737 Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 68 KB/s], Decompressed: 1781 Downloaded: 1826 file(s) [attempted 1826/8459 = 21%, 211 KB/s], Decompressed: 1819 Downloaded: 1860 file(s) [attempted 1860/8459 = 21%, 30 KB/s], Decompressed: 1853 Downloaded: 1897 file(s) [attempted 1897/8459 = 22%, 763 KB/s], Decompressed: 1894 Downloaded: 1936 file(s) [attempted 1936/8459 = 22%, 334 KB/s], Decompressed: 1928 Downloaded: 1978 file(s) [attempted 1978/8459 = 23%, 48 KB/s], Decompressed: 1969 Downloaded: 2017 file(s) [attempted 2017/8459 = 23%, 291 KB/s], Decompressed: 2010 Downloaded: 2053 file(s) [attempted 2053/8459 = 24%, 666 KB/s], Decompressed: 2045 Downloaded: 2093 file(s) [attempted 2093/8459 = 24%, 254 KB/s], Decompressed: 2089 Downloaded: 2137 file(s) [attempted 2137/8459 = 25%, 668 KB/s], Decompressed: 2130 Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 95 KB/s], Decompressed: 2171 Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 329 KB/s], Decompressed: 2212 Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 361 KB/s], Decompressed: 2256 Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 990 KB/s], Decompressed: 2291 Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 85 KB/s], Decompressed: 2329 Downloaded: 2380 file(s) [attempted 2380/8459 = 28%, 986 KB/s], Decompressed: 2377 Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 45 KB/s], Decompressed: 2411 Downloaded: 2455 file(s) [attempted 2455/8459 = 29%, 257 KB/s], Decompressed: 2448 Downloaded: 2496 file(s) [attempted 2496/8459 = 29%, 77 KB/s], Decompressed: 2490 Downloaded: 2541 file(s) [attempted 2541/8459 = 30%, 331 KB/s], Decompressed: 2537 Downloaded: 2582 file(s) [attempted 2582/8459 = 30%, 50 KB/s], Decompressed: 2575 Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 23 KB/s], Decompressed: 2613 Downloaded: 2661 file(s) [attempted 2661/8459 = 31%, 567 KB/s], Decompressed: 2657 Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 489 KB/s], Decompressed: 2698 Downloaded: 2746 file(s) [attempted 2746/8459 = 32%, 44 KB/s], Decompressed: 2739 Downloaded: 2784 file(s) [attempted 2784/8459 = 32%, 832 KB/s], Decompressed: 2777 Downloaded: 2819 file(s) [attempted 2819/8459 = 33%, 233 KB/s], Decompressed: 2815 Downloaded: 2859 file(s) [attempted 2859/8459 = 33%, 308 KB/s], Decompressed: 2856 Downloaded: 2905 file(s) [attempted 2905/8459 = 34%, 1494 KB/s], Decompressed: 2900 Downloaded: 2941 file(s) [attempted 2941/8459 = 34%, 808 KB/s], Decompressed: 2938 Downloaded: 2979 file(s) [attempted 2979/8459 = 35%, 584 KB/s], Decompressed: 2972 Downloaded: 3023 file(s) [attempted 3023/8459 = 35%, 479 KB/s], Decompressed: 3017 Downloaded: 3065 file(s) [attempted 3065/8459 = 36%, 172 KB/s], Decompressed: 3061 Downloaded: 3102 file(s) [attempted 3102/8459 = 36%, 234 KB/s], Decompressed: 3095 Downloaded: 3147 file(s) [attempted 3147/8459 = 37%, 79 KB/s], Decompressed: 3140 Downloaded: 3188 file(s) [attempted 3188/8459 = 37%, 167 KB/s], Decompressed: 3184 Downloaded: 3225 file(s) [attempted 3225/8459 = 38%, 52 KB/s], Decompressed: 3224 Downloaded: 3266 file(s) [attempted 3266/8459 = 38%, 584 KB/s], Decompressed: 3260 Downloaded: 3309 file(s) [attempted 3309/8459 = 39%, 693 KB/s], Decompressed: 3297 Downloaded: 3345 file(s) [attempted 3345/8459 = 39%, 1348 KB/s], Decompressed: 3338 Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 44 KB/s], Decompressed: 3383 Downloaded: 3427 file(s) [attempted 3427/8459 = 40%, 227 KB/s], Decompressed: 3420 Downloaded: 3462 file(s) [attempted 3462/8459 = 40%, 510 KB/s], Decompressed: 3458 Downloaded: 3506 file(s) [attempted 3506/8459 = 41%, 748 KB/s], Decompressed: 3496 Downloaded: 3547 file(s) [attempted 3547/8459 = 41%, 189 KB/s], Decompressed: 3544 Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 170 KB/s], Decompressed: 3581 Downloaded: 3622 file(s) [attempted 3622/8459 = 42%, 1253 KB/s], Decompressed: 3619 Downloaded: 3660 file(s) [attempted 3660/8459 = 43%, 105 KB/s], Decompressed: 3657 Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 1097 KB/s], Decompressed: 3698 Downloaded: 3742 file(s) [attempted 3742/8459 = 44%, 372 KB/s], Decompressed: 3739 Downloaded: 3780 file(s) [attempted 3780/8459 = 44%, 332 KB/s], Decompressed: 3770 Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 221 KB/s], Decompressed: 3807 Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 1487 KB/s], Decompressed: 3852 Downloaded: 3900 file(s) [attempted 3900/8459 = 46%, 194 KB/s], Decompressed: 3896 Downloaded: 3941 file(s) [attempted 3941/8459 = 46%, 476 KB/s], Decompressed: 3934 Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 334 KB/s], Decompressed: 3971 Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 312 KB/s], Decompressed: 4006 Downloaded: 4054 file(s) [attempted 4054/8459 = 47%, 128 KB/s], Decompressed: 4050 Downloaded: 4091 file(s) [attempted 4091/8459 = 48%, 1460 KB/s], Decompressed: 4088 Downloaded: 4129 file(s) [attempted 4129/8459 = 48%, 612 KB/s], Decompressed: 4125 Downloaded: 4167 file(s) [attempted 4167/8459 = 49%, 633 KB/s], Decompressed: 4163 Downloaded: 4209 file(s) [attempted 4209/8459 = 49%, 58 KB/s], Decompressed: 4204 Downloaded: 4249 file(s) [attempted 4249/8459 = 50%, 207 KB/s], Decompressed: 4245 Downloaded: 4286 file(s) [attempted 4286/8459 = 50%, 57 KB/s], Decompressed: 4279 Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 1934 KB/s], Decompressed: 4324 Downloaded: 4372 file(s) [attempted 4372/8459 = 51%, 72 KB/s], Decompressed: 4365 Downloaded: 4406 file(s) [attempted 4406/8459 = 52%, 463 KB/s], Decompressed: 4399 Downloaded: 4447 file(s) [attempted 4447/8459 = 52%, 51 KB/s], Decompressed: 4444 Downloaded: 4490 file(s) [attempted 4490/8459 = 53%, 241 KB/s], Decompressed: 4481 Downloaded: 4526 file(s) [attempted 4526/8459 = 53%, 54 KB/s], Decompressed: 4519 Downloaded: 4564 file(s) [attempted 4564/8459 = 53%, 122 KB/s], Decompressed: 4557 Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 529 KB/s], Decompressed: 4594 Downloaded: 4642 file(s) [attempted 4642/8459 = 54%, 101 KB/s], Decompressed: 4639 Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 362 KB/s], Decompressed: 4680 Downloaded: 4724 file(s) [attempted 4724/8459 = 55%, 675 KB/s], Decompressed: 4721 Downloaded: 4759 file(s) [attempted 4759/8459 = 56%, 127 KB/s], Decompressed: 4755 Downloaded: 4803 file(s) [attempted 4803/8459 = 56%, 165 KB/s], Decompressed: 4796 Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 71 KB/s], Decompressed: 4837 Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 1068 KB/s], Decompressed: 4882 Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 474 KB/s], Decompressed: 4919 Downloaded: 4962 file(s) [attempted 4962/8459 = 58%, 39 KB/s], Decompressed: 4957 Downloaded: 4999 file(s) [attempted 4999/8459 = 59%, 251 KB/s], Decompressed: 4995 Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 185 KB/s], Decompressed: 5039 Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 326 KB/s], Decompressed: 5080 Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 514 KB/s], Decompressed: 5115 Downloaded: 5159 file(s) [attempted 5159/8459 = 60%, 139 KB/s], Decompressed: 5152 Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 114 KB/s], Decompressed: 5197 Downloaded: 5248 file(s) [attempted 5248/8459 = 62%, 877 KB/s], Decompressed: 5245 Downloaded: 5296 file(s) [attempted 5296/8459 = 62%, 206 KB/s], Decompressed: 5289 Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 196 KB/s], Decompressed: 5330 Downloaded: 5371 file(s) [attempted 5371/8459 = 63%, 179 KB/s], Decompressed: 5364 Downloaded: 5409 file(s) [attempted 5409/8459 = 63%, 493 KB/s], Decompressed: 5405 Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 312 KB/s], Decompressed: 5450 Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 588 KB/s], Decompressed: 5494 Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 39 KB/s], Decompressed: 5539 Downloaded: 5583 file(s) [attempted 5583/8459 = 66%, 102 KB/s], Decompressed: 5577 Downloaded: 5614 file(s) [attempted 5614/8459 = 66%, 389 KB/s], Decompressed: 5611 Downloaded: 5656 file(s) [attempted 5656/8459 = 66%, 859 KB/s], Decompressed: 5648 Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 118 KB/s], Decompressed: 5693 Downloaded: 5741 file(s) [attempted 5741/8459 = 67%, 261 KB/s], Decompressed: 5737 Downloaded: 5782 file(s) [attempted 5782/8459 = 68%, 80 KB/s], Decompressed: 5778 Downloaded: 5820 file(s) [attempted 5820/8459 = 68%, 109 KB/s], Decompressed: 5813 Downloaded: 5857 file(s) [attempted 5857/8459 = 69%, 461 KB/s], Decompressed: 5854 Downloaded: 5898 file(s) [attempted 5898/8459 = 69%, 700 KB/s], Decompressed: 5891 Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 57 KB/s], Decompressed: 5936 Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 261 KB/s], Decompressed: 5977 Downloaded: 6017 file(s) [attempted 6017/8459 = 71%, 65 KB/s], Decompressed: 6008 Downloaded: 6056 file(s) [attempted 6056/8459 = 71%, 1954 KB/s], Decompressed: 6045 Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 1753 KB/s], Decompressed: 6093 Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 144 KB/s], Decompressed: 6134 Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 58 KB/s], Decompressed: 6179 Downloaded: 6217 file(s) [attempted 6217/8459 = 73%, 40 KB/s], Decompressed: 6213 Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 33 KB/s], Decompressed: 6247 Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 227 KB/s], Decompressed: 6292 Downloaded: 6337 file(s) [attempted 6337/8459 = 74%, 353 KB/s], Decompressed: 6333 Downloaded: 6381 file(s) [attempted 6381/8459 = 75%, 288 KB/s], Decompressed: 6371 Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 43 KB/s], Decompressed: 6408 Downloaded: 6453 file(s) [attempted 6453/8459 = 76%, 1726 KB/s], Decompressed: 6449 Downloaded: 6490 file(s) [attempted 6490/8459 = 76%, 407 KB/s], Decompressed: 6483 Downloaded: 6535 file(s) [attempted 6535/8459 = 77%, 30 KB/s], Decompressed: 6528 Downloaded: 6572 file(s) [attempted 6572/8459 = 77%, 138 KB/s], Decompressed: 6566 Downloaded: 6607 file(s) [attempted 6607/8459 = 78%, 313 KB/s], Decompressed: 6603 Downloaded: 6649 file(s) [attempted 6649/8459 = 78%, 272 KB/s], Decompressed: 6644 Downloaded: 6687 file(s) [attempted 6687/8459 = 79%, 99 KB/s], Decompressed: 6679 Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 264 KB/s], Decompressed: 6723 Downloaded: 6768 file(s) [attempted 6768/8459 = 80%, 73 KB/s], Decompressed: 6761 Downloaded: 6805 file(s) [attempted 6805/8459 = 80%, 521 KB/s], Decompressed: 6798 Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 58 KB/s], Decompressed: 6839 Downloaded: 6880 file(s) [attempted 6880/8459 = 81%, 67 KB/s], Decompressed: 6877 Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 348 KB/s], Decompressed: 6918 Downloaded: 6969 file(s) [attempted 6969/8459 = 82%, 54 KB/s], Decompressed: 6959 Downloaded: 7005 file(s) [attempted 7005/8459 = 82%, 369 KB/s], Decompressed: 7000 Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 112 KB/s], Decompressed: 7038 Downloaded: 7086 file(s) [attempted 7086/8459 = 83%, 223 KB/s], Decompressed: 7082 Downloaded: 7130 file(s) [attempted 7130/8459 = 84%, 1004 KB/s], Decompressed: 7127 Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 142 KB/s], Decompressed: 7166 Downloaded: 7209 file(s) [attempted 7209/8459 = 85%, 160 KB/s], Decompressed: 7206 Downloaded: 7241 file(s) [attempted 7241/8459 = 85%, 458 KB/s], Decompressed: 7236 Downloaded: 7284 file(s) [attempted 7284/8459 = 86%, 46 KB/s], Decompressed: 7281 Downloaded: 7329 file(s) [attempted 7329/8459 = 86%, 221 KB/s], Decompressed: 7325 Downloaded: 7366 file(s) [attempted 7366/8459 = 87%, 1319 KB/s], Decompressed: 7363 Downloaded: 7402 file(s) [attempted 7402/8459 = 87%, 283 KB/s], Decompressed: 7397 Downloaded: 7442 file(s) [attempted 7442/8459 = 87%, 105 KB/s], Decompressed: 7438 Downloaded: 7483 file(s) [attempted 7483/8459 = 88%, 625 KB/s], Decompressed: 7479 Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 119 KB/s], Decompressed: 7524 Downloaded: 7565 file(s) [attempted 7565/8459 = 89%, 233 KB/s], Decompressed: 7562 Downloaded: 7603 file(s) [attempted 7603/8459 = 89%, 290 KB/s], Decompressed: 7599 Downloaded: 7640 file(s) [attempted 7640/8459 = 90%, 1480 KB/s], Decompressed: 7637 Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 49 KB/s], Decompressed: 7681 Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 32 KB/s], Decompressed: 7719 Downloaded: 7764 file(s) [attempted 7764/8459 = 91%, 175 KB/s], Decompressed: 7757 Downloaded: 7804 file(s) [attempted 7804/8459 = 92%, 612 KB/s], Decompressed: 7798 Downloaded: 7846 file(s) [attempted 7846/8459 = 92%, 211 KB/s], Decompressed: 7842 Downloaded: 7883 file(s) [attempted 7883/8459 = 93%, 853 KB/s], Decompressed: 7880 Downloaded: 7924 file(s) [attempted 7924/8459 = 93%, 398 KB/s], Decompressed: 7921 Downloaded: 7958 file(s) [attempted 7958/8459 = 94%, 130 KB/s], Decompressed: 7955 Downloaded: 8000 file(s) [attempted 8000/8459 = 94%, 319 KB/s], Decompressed: 7996 Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 511 KB/s], Decompressed: 8037 Downloaded: 8078 file(s) [attempted 8078/8459 = 95%, 177 KB/s], Decompressed: 8075 Downloaded: 8120 file(s) [attempted 8120/8459 = 95%, 109 KB/s], Decompressed: 8112 Downloaded: 8157 file(s) [attempted 8157/8459 = 96%, 115 KB/s], Decompressed: 8154 Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 128 KB/s], Decompressed: 8195 Downloaded: 8239 file(s) [attempted 8239/8459 = 97%, 52 KB/s], Decompressed: 8232 Downloaded: 8274 file(s) [attempted 8274/8459 = 97%, 143 KB/s], Decompressed: 8270 Downloaded: 8314 file(s) [attempted 8314/8459 = 98%, 52 KB/s], Decompressed: 8308 Downloaded: 8355 file(s) [attempted 8355/8459 = 98%, 407 KB/s], Decompressed: 8352 Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 551 KB/s], Decompressed: 8390 Downloaded: 8438 file(s) [attempted 8438/8459 = 99%, 315 KB/s], Decompressed: 8431 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 315 KB/s], Decompressed: 8455
lean_checker exit 0
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) [0x7534635c6785] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7534635bdb27] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7534635bdc0b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7534634f3c62] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7534634f4439] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7534635caf99] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x753463432923] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x753463432b2b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x753463433827] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7534634341b6] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7534635c9e8b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x753463215adb] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7534635c9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7534635c9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x75346359b1f3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x753463215c92] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x75345e622638] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x75345e40cd2e] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x75345df69a82] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x75345df69f0e] /lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x75345ae4524a] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x75345ae45305] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5839161818da] ✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (28s) ✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (4.4s) ✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (38s) ✔ [3414/3416] Built Iut.Basic (4.2s) ✔ [3415/3416] Built Iut (2.8s) Build completed successfully (3416 jobs).
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
blueprint_build exit 1
lake build :blueprint
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes error: unknown package facet `blueprint`
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)
apx-semantic-phase {"duration_ms":6,"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":389051,"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":81,"module_count":1,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"ok":true,"payload_bytes":738,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":2,"module_index":0,"ok":true,"payload_bytes":738,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":1,"diagnostic_count":0,"duration_ms":326,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":390531,"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":81,"module_count":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"ok":true,"payload_bytes":1330,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"ok":true,"payload_bytes":1330,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":97,"diagnostic_count":15,"duration_ms":8172,"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":370540,"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":416,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"ok":true,"payload_bytes":3002937,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":2,"module_index":2,"ok":true,"payload_bytes":3002937,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":1889,"diagnostic_count":116,"duration_ms":1557014,"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":416284,"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":1889,"diagnostic_count":116,"duration_ms":9086,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"ok":true,"payload_bytes":67044380,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":53,"module_index":3,"ok":true,"payload_bytes":67044380,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":7754,"diagnostic_count":3093,"duration_ms":6296487,"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":555384,"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":7754,"diagnostic_count":3093,"duration_ms":40578,"module_count":1,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":4,"ok":true,"payload_bytes":464123762,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":381,"module_index":4,"ok":true,"payload_bytes":464123762,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":152,"diagnostic_count":23,"duration_ms":29201,"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":1007080,"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":555,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":5,"ok":true,"payload_bytes":2722873,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":12,"module_index":5,"ok":true,"payload_bytes":2722873,"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":4843}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":392,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":30,"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":18019,"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 1e7ffe582ba39c9551655c0d7e38db1c047d5b7a37a348d217240ffb58a3206c
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":11086537,"ok":true}