Verification run
Run 354
succeeded commit
f04a12a826f5 toolchain lean-v4-30-0 prover lean took 4h 16m · 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-502-source
exit_code=Some(0) duration_ms=2296
stderr:
Cloning into '/var/lib/apodeixis/repos/job-502-source'...
$ git checkout f04a12a826f5f3ad48d99a52fe90aaf585a9c371
exit_code=Some(128) duration_ms=1
stderr:
fatal: reference is not a tree: f04a12a826f5f3ad48d99a52fe90aaf585a9c371
$ git fetch --depth 1 origin f04a12a826f5f3ad48d99a52fe90aaf585a9c371
exit_code=Some(0) duration_ms=1142
stderr:
From https://github.com/promachina/iut-lean
* branch f04a12a826f5f3ad48d99a52fe90aaf585a9c371 -> FETCH_HEAD
$ git checkout f04a12a826f5f3ad48d99a52fe90aaf585a9c371 (after fetch)
exit_code=Some(0) duration_ms=191
stderr:
Note: switching to 'f04a12a826f5f3ad48d99a52fe90aaf585a9c371'.
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 f04a12a Assemble finite local log coordinate transport
Resolved source revision: f04a12a826f5f3ad48d99a52fe90aaf585a9c371
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=f04a12a826f5f3ad48d99a52fe90aaf585a9c371 provenance={"branch":"master","checked_out_revision":"f04a12a826f5f3ad48d99a52fe90aaf585a9c371","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"f04a12a826f5f3ad48d99a52fe90aaf585a9c371","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: stable superset runner failed with import_failure; falling back
Lean semantic module cache: stable superset runner fell back to exact-module batches
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=47581
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%, 8 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 1 KB/s], Decompressed: 14
Downloaded: 43 file(s) [attempted 43/8459 = 0%, 24 KB/s], Decompressed: 38
Downloaded: 69 file(s) [attempted 69/8459 = 0%, 26 KB/s], Decompressed: 65
Downloaded: 100 file(s) [attempted 100/8459 = 1%, 73 KB/s], Decompressed: 96
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 83 KB/s], Decompressed: 127
Downloaded: 165 file(s) [attempted 165/8459 = 1%, 58 KB/s], Decompressed: 158
Downloaded: 203 file(s) [attempted 203/8459 = 2%, 76 KB/s], Decompressed: 196
Downloaded: 240 file(s) [attempted 240/8459 = 2%, 174 KB/s], Decompressed: 237
Downloaded: 282 file(s) [attempted 282/8459 = 3%, 1011 KB/s], Decompressed: 278
Downloaded: 321 file(s) [attempted 321/8459 = 3%, 1652 KB/s], Decompressed: 312
Downloaded: 360 file(s) [attempted 360/8459 = 4%, 436 KB/s], Decompressed: 357
Downloaded: 401 file(s) [attempted 401/8459 = 4%, 112 KB/s], Decompressed: 395
Downloaded: 439 file(s) [attempted 439/8459 = 5%, 417 KB/s], Decompressed: 436
Downloaded: 478 file(s) [attempted 478/8459 = 5%, 337 KB/s], Decompressed: 473
Downloaded: 521 file(s) [attempted 521/8459 = 6%, 624 KB/s], Decompressed: 514
Downloaded: 559 file(s) [attempted 559/8459 = 6%, 357 KB/s], Decompressed: 553
Downloaded: 594 file(s) [attempted 594/8459 = 7%, 871 KB/s], Decompressed: 590
Downloaded: 634 file(s) [attempted 634/8459 = 7%, 35 KB/s], Decompressed: 621
Downloaded: 675 file(s) [attempted 675/8459 = 7%, 242 KB/s], Decompressed: 672
Downloaded: 718 file(s) [attempted 718/8459 = 8%, 155 KB/s], Decompressed: 713
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 205 KB/s], Decompressed: 747
Downloaded: 790 file(s) [attempted 790/8459 = 9%, 62 KB/s], Decompressed: 785
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 138 KB/s], Decompressed: 819
Downloaded: 864 file(s) [attempted 864/8459 = 10%, 38 KB/s], Decompressed: 857
Downloaded: 904 file(s) [attempted 904/8459 = 10%, 45 KB/s], Decompressed: 898
Downloaded: 943 file(s) [attempted 943/8459 = 11%, 143 KB/s], Decompressed: 939
Downloaded: 987 file(s) [attempted 987/8459 = 11%, 388 KB/s], Decompressed: 984
Downloaded: 1029 file(s) [attempted 1029/8459 = 12%, 740 KB/s], Decompressed: 1024
Downloaded: 1066 file(s) [attempted 1066/8459 = 12%, 182 KB/s], Decompressed: 1062
Downloaded: 1104 file(s) [attempted 1104/8459 = 13%, 61 KB/s], Decompressed: 1100
Downloaded: 1141 file(s) [attempted 1141/8459 = 13%, 118 KB/s], Decompressed: 1138
Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 941 KB/s], Decompressed: 1186
Downloaded: 1233 file(s) [attempted 1233/8459 = 14%, 205 KB/s], Decompressed: 1223
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 275 KB/s], Decompressed: 1268
Downloaded: 1309 file(s) [attempted 1309/8459 = 15%, 265 KB/s], Decompressed: 1302
Downloaded: 1346 file(s) [attempted 1346/8459 = 15%, 215 KB/s], Decompressed: 1343
Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 447 KB/s], Decompressed: 1384
Downloaded: 1432 file(s) [attempted 1432/8459 = 16%, 1286 KB/s], Decompressed: 1429
Downloaded: 1471 file(s) [attempted 1471/8459 = 17%, 623 KB/s], Decompressed: 1463
Downloaded: 1511 file(s) [attempted 1511/8459 = 17%, 153 KB/s], Decompressed: 1507
Downloaded: 1549 file(s) [attempted 1549/8459 = 18%, 186 KB/s], Decompressed: 1545
Downloaded: 1593 file(s) [attempted 1593/8459 = 18%, 134 KB/s], Decompressed: 1589
Downloaded: 1634 file(s) [attempted 1634/8459 = 19%, 55 KB/s], Decompressed: 1631
Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 122 KB/s], Decompressed: 1665
Downloaded: 1711 file(s) [attempted 1711/8459 = 20%, 346 KB/s], Decompressed: 1702
Downloaded: 1747 file(s) [attempted 1747/8459 = 20%, 992 KB/s], Decompressed: 1743
Downloaded: 1791 file(s) [attempted 1791/8459 = 21%, 936 KB/s], Decompressed: 1788
Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 73 KB/s], Decompressed: 1822
Downloaded: 1870 file(s) [attempted 1870/8459 = 22%, 277 KB/s], Decompressed: 1867
Downloaded: 1906 file(s) [attempted 1906/8459 = 22%, 533 KB/s], Decompressed: 1901
Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 426 KB/s], Decompressed: 1939
Downloaded: 1982 file(s) [attempted 1982/8459 = 23%, 77 KB/s], Decompressed: 1977
Downloaded: 2020 file(s) [attempted 2020/8459 = 23%, 397 KB/s], Decompressed: 2010
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 414 KB/s], Decompressed: 2055
Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 1076 KB/s], Decompressed: 2093
Downloaded: 2137 file(s) [attempted 2137/8459 = 25%, 672 KB/s], Decompressed: 2130
Downloaded: 2175 file(s) [attempted 2175/8459 = 25%, 97 KB/s], Decompressed: 2171
Downloaded: 2216 file(s) [attempted 2216/8459 = 26%, 117 KB/s], Decompressed: 2206
Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 576 KB/s], Decompressed: 2206
Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 263 KB/s], Decompressed: 2209
Downloaded: 2339 file(s) [attempted 2339/8459 = 27%, 115 KB/s], Decompressed: 2209
Downloaded: 2377 file(s) [attempted 2377/8459 = 28%, 789 KB/s], Decompressed: 2209
Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 36 KB/s], Decompressed: 2209
Downloaded: 2459 file(s) [attempted 2459/8459 = 29%, 177 KB/s], Decompressed: 2209
Downloaded: 2496 file(s) [attempted 2496/8459 = 29%, 416 KB/s], Decompressed: 2209
Downloaded: 2537 file(s) [attempted 2537/8459 = 29%, 316 KB/s], Decompressed: 2288
Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 64 KB/s], Decompressed: 2537
Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 77 KB/s], Decompressed: 2616
Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 175 KB/s], Decompressed: 2661
Downloaded: 2705 file(s) [attempted 2705/8459 = 31%, 1002 KB/s], Decompressed: 2702
Downloaded: 2739 file(s) [attempted 2739/8459 = 32%, 38 KB/s], Decompressed: 2736
Downloaded: 2777 file(s) [attempted 2777/8459 = 32%, 322 KB/s], Decompressed: 2774
Downloaded: 2819 file(s) [attempted 2819/8459 = 33%, 83 KB/s], Decompressed: 2815
Downloaded: 2863 file(s) [attempted 2863/8459 = 33%, 52 KB/s], Decompressed: 2859
Downloaded: 2900 file(s) [attempted 2900/8459 = 34%, 122 KB/s], Decompressed: 2897
Downloaded: 2941 file(s) [attempted 2941/8459 = 34%, 40 KB/s], Decompressed: 2934
Downloaded: 2979 file(s) [attempted 2979/8459 = 35%, 351 KB/s], Decompressed: 2972
Downloaded: 3017 file(s) [attempted 3017/8459 = 35%, 466 KB/s], Decompressed: 3013
Downloaded: 3061 file(s) [attempted 3061/8459 = 36%, 111 KB/s], Decompressed: 3058
Downloaded: 3104 file(s) [attempted 3104/8459 = 36%, 412 KB/s], Decompressed: 3095
Downloaded: 3147 file(s) [attempted 3147/8459 = 37%, 309 KB/s], Decompressed: 3143
Downloaded: 3184 file(s) [attempted 3184/8459 = 37%, 176 KB/s], Decompressed: 3181
Downloaded: 3225 file(s) [attempted 3225/8459 = 38%, 52 KB/s], Decompressed: 3222
Downloaded: 3263 file(s) [attempted 3263/8459 = 38%, 1089 KB/s], Decompressed: 3256
Downloaded: 3306 file(s) [attempted 3306/8459 = 39%, 245 KB/s], Decompressed: 3301
Downloaded: 3351 file(s) [attempted 3351/8459 = 39%, 720 KB/s], Decompressed: 3342
Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 45 KB/s], Decompressed: 3379
Downloaded: 3421 file(s) [attempted 3421/8459 = 40%, 411 KB/s], Decompressed: 3417
Downloaded: 3463 file(s) [attempted 3463/8459 = 40%, 306 KB/s], Decompressed: 3458
Downloaded: 3499 file(s) [attempted 3499/8459 = 41%, 171 KB/s], Decompressed: 3496
Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 71 KB/s], Decompressed: 3533
Downloaded: 3573 file(s) [attempted 3573/8459 = 42%, 747 KB/s], Decompressed: 3568
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 177 KB/s], Decompressed: 3602
Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 202 KB/s], Decompressed: 3646
Downloaded: 3693 file(s) [attempted 3693/8459 = 43%, 72 KB/s], Decompressed: 3687
Downloaded: 3733 file(s) [attempted 3733/8459 = 44%, 93 KB/s], Decompressed: 3725
Downloaded: 3768 file(s) [attempted 3768/8459 = 44%, 1076 KB/s], Decompressed: 3759
Downloaded: 3804 file(s) [attempted 3804/8459 = 44%, 367 KB/s], Decompressed: 3797
Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 714 KB/s], Decompressed: 3847
Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 248 KB/s], Decompressed: 3886
Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 41 KB/s], Decompressed: 3930
Downloaded: 3975 file(s) [attempted 3975/8459 = 46%, 354 KB/s], Decompressed: 3965
Downloaded: 4007 file(s) [attempted 4007/8459 = 47%, 284 KB/s], Decompressed: 4002
Downloaded: 4047 file(s) [attempted 4047/8459 = 47%, 74 KB/s], Decompressed: 4043
Downloaded: 4084 file(s) [attempted 4084/8459 = 48%, 234 KB/s], Decompressed: 4081
Downloaded: 4127 file(s) [attempted 4127/8459 = 48%, 146 KB/s], Decompressed: 4115
Downloaded: 4163 file(s) [attempted 4163/8459 = 49%, 207 KB/s], Decompressed: 4160
Downloaded: 4202 file(s) [attempted 4202/8459 = 49%, 1419 KB/s], Decompressed: 4194
Downloaded: 4238 file(s) [attempted 4238/8459 = 50%, 340 KB/s], Decompressed: 4235
Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 228 KB/s], Decompressed: 4276
Downloaded: 4324 file(s) [attempted 4324/8459 = 51%, 332 KB/s], Decompressed: 4317
Downloaded: 4362 file(s) [attempted 4362/8459 = 51%, 100 KB/s], Decompressed: 4355
Downloaded: 4405 file(s) [attempted 4405/8459 = 52%, 653 KB/s], Decompressed: 4396
Downloaded: 4433 file(s) [attempted 4433/8459 = 52%, 127 KB/s], Decompressed: 4430
Downloaded: 4475 file(s) [attempted 4475/8459 = 52%, 422 KB/s], Decompressed: 4471
Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 113 KB/s], Decompressed: 4512
Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 327 KB/s], Decompressed: 4546
Downloaded: 4598 file(s) [attempted 4598/8459 = 54%, 36 KB/s], Decompressed: 4587
Downloaded: 4632 file(s) [attempted 4632/8459 = 54%, 546 KB/s], Decompressed: 4622
Downloaded: 4673 file(s) [attempted 4673/8459 = 55%, 404 KB/s], Decompressed: 4622
Downloaded: 4714 file(s) [attempted 4714/8459 = 55%, 193 KB/s], Decompressed: 4625
Downloaded: 4755 file(s) [attempted 4755/8459 = 56%, 808 KB/s], Decompressed: 4752
Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 291 KB/s], Decompressed: 4789
Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 197 KB/s], Decompressed: 4830
Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 88 KB/s], Decompressed: 4875
Downloaded: 4923 file(s) [attempted 4923/8459 = 58%, 398 KB/s], Decompressed: 4919
Downloaded: 4966 file(s) [attempted 4966/8459 = 58%, 38 KB/s], Decompressed: 4957
Downloaded: 4995 file(s) [attempted 4995/8459 = 59%, 998 KB/s], Decompressed: 4991
Downloaded: 5038 file(s) [attempted 5038/8459 = 59%, 107 KB/s], Decompressed: 5032
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 148 KB/s], Decompressed: 5077
Downloaded: 5125 file(s) [attempted 5125/8459 = 60%, 647 KB/s], Decompressed: 5121
Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 54 KB/s], Decompressed: 5156
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 27 KB/s], Decompressed: 5197
Downloaded: 5241 file(s) [attempted 5241/8459 = 61%, 273 KB/s], Decompressed: 5238
Downloaded: 5286 file(s) [attempted 5286/8459 = 62%, 362 KB/s], Decompressed: 5282
Downloaded: 5330 file(s) [attempted 5330/8459 = 63%, 422 KB/s], Decompressed: 5323
Downloaded: 5368 file(s) [attempted 5368/8459 = 63%, 124 KB/s], Decompressed: 5361
Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 59 KB/s], Decompressed: 5399
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 507 KB/s], Decompressed: 5440
Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 150 KB/s], Decompressed: 5481
Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 955 KB/s], Decompressed: 5525
Downloaded: 5573 file(s) [attempted 5573/8459 = 65%, 120 KB/s], Decompressed: 5570
Downloaded: 5611 file(s) [attempted 5611/8459 = 66%, 96 KB/s], Decompressed: 5607
Downloaded: 5648 file(s) [attempted 5648/8459 = 66%, 186 KB/s], Decompressed: 5645
Downloaded: 5693 file(s) [attempted 5693/8459 = 67%, 289 KB/s], Decompressed: 5689
Downloaded: 5734 file(s) [attempted 5734/8459 = 67%, 103 KB/s], Decompressed: 5727
Downloaded: 5775 file(s) [attempted 5775/8459 = 68%, 577 KB/s], Decompressed: 5768
Downloaded: 5813 file(s) [attempted 5813/8459 = 68%, 65 KB/s], Decompressed: 5807
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 627 KB/s], Decompressed: 5843
Downloaded: 5888 file(s) [attempted 5888/8459 = 69%, 449 KB/s], Decompressed: 5885
Downloaded: 5936 file(s) [attempted 5936/8459 = 70%, 143 KB/s], Decompressed: 5932
Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 72 KB/s], Decompressed: 5980
Downloaded: 6028 file(s) [attempted 6028/8459 = 71%, 26 KB/s], Decompressed: 6021
Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 885 KB/s], Decompressed: 6066
Downloaded: 6107 file(s) [attempted 6107/8459 = 72%, 304 KB/s], Decompressed: 6097
Downloaded: 6142 file(s) [attempted 6142/8459 = 72%, 226 KB/s], Decompressed: 6138
Downloaded: 6186 file(s) [attempted 6186/8459 = 73%, 685 KB/s], Decompressed: 6182
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 197 KB/s], Decompressed: 6227
Downloaded: 6271 file(s) [attempted 6271/8459 = 74%, 239 KB/s], Decompressed: 6266
Downloaded: 6306 file(s) [attempted 6306/8459 = 74%, 1016 KB/s], Decompressed: 6302
Downloaded: 6343 file(s) [attempted 6343/8459 = 74%, 1083 KB/s], Decompressed: 6340
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 703 KB/s], Decompressed: 6388
Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 224 KB/s], Decompressed: 6429
Downloaded: 6473 file(s) [attempted 6473/8459 = 76%, 275 KB/s], Decompressed: 6466
Downloaded: 6511 file(s) [attempted 6511/8459 = 76%, 114 KB/s], Decompressed: 6504
Downloaded: 6548 file(s) [attempted 6548/8459 = 77%, 53 KB/s], Decompressed: 6545
Downloaded: 6593 file(s) [attempted 6593/8459 = 77%, 122 KB/s], Decompressed: 6590
Downloaded: 6637 file(s) [attempted 6637/8459 = 78%, 33 KB/s], Decompressed: 6631
Downloaded: 6675 file(s) [attempted 6675/8459 = 78%, 57 KB/s], Decompressed: 6672
Downloaded: 6713 file(s) [attempted 6713/8459 = 79%, 26 KB/s], Decompressed: 6709
Downloaded: 6757 file(s) [attempted 6757/8459 = 79%, 469 KB/s], Decompressed: 6750
Downloaded: 6798 file(s) [attempted 6798/8459 = 80%, 81 KB/s], Decompressed: 6791
Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 233 KB/s], Decompressed: 6839
Downloaded: 6887 file(s) [attempted 6887/8459 = 81%, 151 KB/s], Decompressed: 6884
Downloaded: 6922 file(s) [attempted 6922/8459 = 81%, 180 KB/s], Decompressed: 6915
Downloaded: 6963 file(s) [attempted 6963/8459 = 82%, 118 KB/s], Decompressed: 6952
Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 380 KB/s], Decompressed: 6993
Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 22 KB/s], Decompressed: 7038
Downloaded: 7086 file(s) [attempted 7086/8459 = 83%, 316 KB/s], Decompressed: 7080
Downloaded: 7123 file(s) [attempted 7123/8459 = 84%, 209 KB/s], Decompressed: 7120
Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 38 KB/s], Decompressed: 7168
Downloaded: 7212 file(s) [attempted 7212/8459 = 85%, 23 KB/s], Decompressed: 7209
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 304 KB/s], Decompressed: 7240
Downloaded: 7291 file(s) [attempted 7291/8459 = 86%, 277 KB/s], Decompressed: 7284
Downloaded: 7332 file(s) [attempted 7332/8459 = 86%, 24 KB/s], Decompressed: 7325
Downloaded: 7373 file(s) [attempted 7373/8459 = 87%, 65 KB/s], Decompressed: 7370
Downloaded: 7415 file(s) [attempted 7415/8459 = 87%, 118 KB/s], Decompressed: 7408
Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 319 KB/s], Decompressed: 7442
Downloaded: 7492 file(s) [attempted 7492/8459 = 88%, 136 KB/s], Decompressed: 7486
Downloaded: 7527 file(s) [attempted 7527/8459 = 88%, 114 KB/s], Decompressed: 7520
Downloaded: 7568 file(s) [attempted 7568/8459 = 89%, 472 KB/s], Decompressed: 7565
Downloaded: 7611 file(s) [attempted 7611/8459 = 89%, 350 KB/s], Decompressed: 7599
Downloaded: 7647 file(s) [attempted 7647/8459 = 90%, 175 KB/s], Decompressed: 7640
Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 1007 KB/s], Decompressed: 7685
Downloaded: 7730 file(s) [attempted 7730/8459 = 91%, 993 KB/s], Decompressed: 7722
Downloaded: 7767 file(s) [attempted 7767/8459 = 91%, 586 KB/s], Decompressed: 7757
Downloaded: 7808 file(s) [attempted 7808/8459 = 92%, 964 KB/s], Decompressed: 7804
Downloaded: 7846 file(s) [attempted 7846/8459 = 92%, 154 KB/s], Decompressed: 7842
Downloaded: 7889 file(s) [attempted 7889/8459 = 93%, 309 KB/s], Decompressed: 7880
Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 653 KB/s], Decompressed: 7930
Downloaded: 7972 file(s) [attempted 7972/8459 = 94%, 374 KB/s], Decompressed: 7969
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 153 KB/s], Decompressed: 8010
Downloaded: 8051 file(s) [attempted 8051/8459 = 95%, 435 KB/s], Decompressed: 8047
Downloaded: 8090 file(s) [attempted 8090/8459 = 95%, 326 KB/s], Decompressed: 8085
Downloaded: 8130 file(s) [attempted 8130/8459 = 96%, 283 KB/s], Decompressed: 8126
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 748 KB/s], Decompressed: 8164
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 87 KB/s], Decompressed: 8212
Downloaded: 8253 file(s) [attempted 8253/8459 = 97%, 1584 KB/s], Decompressed: 8249
Downloaded: 8290 file(s) [attempted 8290/8459 = 98%, 517 KB/s], Decompressed: 8284
Downloaded: 8331 file(s) [attempted 8331/8459 = 98%, 83 KB/s], Decompressed: 8325
Downloaded: 8373 file(s) [attempted 8373/8459 = 98%, 92 KB/s], Decompressed: 8369
Downloaded: 8414 file(s) [attempted 8414/8459 = 99%, 605 KB/s], Decompressed: 8410
Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 204 KB/s], Decompressed: 8444
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 204 KB/s], Decompressed: 8451
$ lake build
exit_code=Some(0) duration_ms=414195
stdout:
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (253s)
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) [0x73c265bc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x73c265bbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x73c265bbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x73c265af3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x73c265af4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x73c265bcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x73c265a32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x73c265a32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x73c265a33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x73c265a341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x73c265bc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x73c265815adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73c265bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73c265bc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x73c265b9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x73c265815c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x73c260c22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x73c260a0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x73c260569a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x73c260569f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x73c25d44524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x73c25d445305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5da312ac48da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (66s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.0s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (38s)
✔ [3414/3416] Built Iut.Basic (3.3s)
✔ [3415/3416] Built Iut (9.5s)
Build completed successfully (3416 jobs).
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
$ lake build :blueprint
exit_code=Some(1) duration_ms=2130
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=6570049
stdout:
apx-semantic-phase {"duration_ms":5,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":7592,"diagnostic_count":3037,"duration_ms":5905163,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":7592,"dependency_count":73323,"diagnostic_count":134256,"duration_ms":1,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":532650,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":7592,"dependency_count":73323,"diagnostic_count":134256,"duration_ms":10186,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":453516949,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":997,"ok":true,"payload_bytes":453516949,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":18}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":693,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":19,"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":62267,"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 8543c918f29ec02fbe854b9f99cf4ce914898c81cc06fadb720100009a7ef83e
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":6495138,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
exit_code=Some(0) duration_ms=479685
stdout:
apx-semantic-phase {"duration_ms":7,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":97,"diagnostic_count":15,"duration_ms":6948,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":97,"dependency_count":189,"diagnostic_count":2058,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":374956,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":97,"dependency_count":189,"diagnostic_count":2058,"duration_ms":269,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":2,"ok":true,"payload_bytes":3002937,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":14,"ok":true,"payload_bytes":3002937,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":346,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache c5d00d79bfc98fa70cdec4b614d7e759f078085d8cc1d30933d856891591a0a2
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":39,"runner_cache_hit":true}
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":478654,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
exit_code=Some(0) duration_ms=497539
stdout:
apx-semantic-phase {"duration_ms":9,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":152,"diagnostic_count":23,"duration_ms":12701,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":152,"dependency_count":468,"diagnostic_count":1820,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":376285,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":152,"dependency_count":468,"diagnostic_count":1820,"duration_ms":193,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":2722873,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":10,"ok":true,"payload_bytes":2722873,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":329,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 4aee9bac4a0df9b38a9b35781b33cc39661cad08c376cdc832c218cc4f3678c0
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":43,"runner_cache_hit":true}
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":496370,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)
exit_code=Some(0) duration_ms=2118657
stdout:
apx-semantic-phase {"duration_ms":180,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":1885,"diagnostic_count":116,"duration_ms":1581003,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":1885,"dependency_count":2619,"diagnostic_count":33439,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":415444,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":1885,"dependency_count":2619,"diagnostic_count":33439,"duration_ms":1760,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":66295081,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":65,"ok":true,"payload_bytes":66295081,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":436,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":103511,"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 62bff9e19e2f0fb064b5be968a31116d5e750cf0a316b7426f9d1ac2b091e2da
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":2011585,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)
exit_code=Some(0) duration_ms=430025
stdout:
apx-semantic-phase {"duration_ms":8,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":1,"diagnostic_count":0,"duration_ms":97,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":1,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":357590,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":1,"dependency_count":0,"diagnostic_count":0,"duration_ms":56,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1330,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":6,"ok":true,"payload_bytes":1330,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":20}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":428,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 1d35f17e8a5e2a4f7eb2e38812720399852ea8f1a139b919203fe67b11f92c80
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":42,"runner_cache_hit":true}
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":429040,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)
exit_code=Some(0) duration_ms=366063
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":6,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":357761,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":90,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":2,"ok":true,"payload_bytes":738,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":6,"ok":true,"payload_bytes":738,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":11}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":94,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 1efb022e29a187ab0ac03706f29926a53fd827a39730c76c52602cb79bfbc075
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":32,"runner_cache_hit":true}
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":365542,"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-502-source
Cloning into '/var/lib/apodeixis/repos/job-502-source'...
git_checkout exit 128
git checkout f04a12a826f5f3ad48d99a52fe90aaf585a9c371
fatal: reference is not a tree: f04a12a826f5f3ad48d99a52fe90aaf585a9c371
git_checkout exit 0
git fetch --depth 1 origin f04a12a826f5f3ad48d99a52fe90aaf585a9c371
From https://github.com/promachina/iut-lean * branch f04a12a826f5f3ad48d99a52fe90aaf585a9c371 -> FETCH_HEAD
git_checkout exit 0
git checkout f04a12a826f5f3ad48d99a52fe90aaf585a9c371 (after fetch)
Note: switching to 'f04a12a826f5f3ad48d99a52fe90aaf585a9c371'. 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 f04a12a Assemble finite local log coordinate transport
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%, 8 KB/s], Decompressed: 0 Downloaded: 16 file(s) [attempted 16/8459 = 0%, 1 KB/s], Decompressed: 14 Downloaded: 43 file(s) [attempted 43/8459 = 0%, 24 KB/s], Decompressed: 38 Downloaded: 69 file(s) [attempted 69/8459 = 0%, 26 KB/s], Decompressed: 65 Downloaded: 100 file(s) [attempted 100/8459 = 1%, 73 KB/s], Decompressed: 96 Downloaded: 134 file(s) [attempted 134/8459 = 1%, 83 KB/s], Decompressed: 127 Downloaded: 165 file(s) [attempted 165/8459 = 1%, 58 KB/s], Decompressed: 158 Downloaded: 203 file(s) [attempted 203/8459 = 2%, 76 KB/s], Decompressed: 196 Downloaded: 240 file(s) [attempted 240/8459 = 2%, 174 KB/s], Decompressed: 237 Downloaded: 282 file(s) [attempted 282/8459 = 3%, 1011 KB/s], Decompressed: 278 Downloaded: 321 file(s) [attempted 321/8459 = 3%, 1652 KB/s], Decompressed: 312 Downloaded: 360 file(s) [attempted 360/8459 = 4%, 436 KB/s], Decompressed: 357 Downloaded: 401 file(s) [attempted 401/8459 = 4%, 112 KB/s], Decompressed: 395 Downloaded: 439 file(s) [attempted 439/8459 = 5%, 417 KB/s], Decompressed: 436 Downloaded: 478 file(s) [attempted 478/8459 = 5%, 337 KB/s], Decompressed: 473 Downloaded: 521 file(s) [attempted 521/8459 = 6%, 624 KB/s], Decompressed: 514 Downloaded: 559 file(s) [attempted 559/8459 = 6%, 357 KB/s], Decompressed: 553 Downloaded: 594 file(s) [attempted 594/8459 = 7%, 871 KB/s], Decompressed: 590 Downloaded: 634 file(s) [attempted 634/8459 = 7%, 35 KB/s], Decompressed: 621 Downloaded: 675 file(s) [attempted 675/8459 = 7%, 242 KB/s], Decompressed: 672 Downloaded: 718 file(s) [attempted 718/8459 = 8%, 155 KB/s], Decompressed: 713 Downloaded: 751 file(s) [attempted 751/8459 = 8%, 205 KB/s], Decompressed: 747 Downloaded: 790 file(s) [attempted 790/8459 = 9%, 62 KB/s], Decompressed: 785 Downloaded: 826 file(s) [attempted 826/8459 = 9%, 138 KB/s], Decompressed: 819 Downloaded: 864 file(s) [attempted 864/8459 = 10%, 38 KB/s], Decompressed: 857 Downloaded: 904 file(s) [attempted 904/8459 = 10%, 45 KB/s], Decompressed: 898 Downloaded: 943 file(s) [attempted 943/8459 = 11%, 143 KB/s], Decompressed: 939 Downloaded: 987 file(s) [attempted 987/8459 = 11%, 388 KB/s], Decompressed: 984 Downloaded: 1029 file(s) [attempted 1029/8459 = 12%, 740 KB/s], Decompressed: 1024 Downloaded: 1066 file(s) [attempted 1066/8459 = 12%, 182 KB/s], Decompressed: 1062 Downloaded: 1104 file(s) [attempted 1104/8459 = 13%, 61 KB/s], Decompressed: 1100 Downloaded: 1141 file(s) [attempted 1141/8459 = 13%, 118 KB/s], Decompressed: 1138 Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 941 KB/s], Decompressed: 1186 Downloaded: 1233 file(s) [attempted 1233/8459 = 14%, 205 KB/s], Decompressed: 1223 Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 275 KB/s], Decompressed: 1268 Downloaded: 1309 file(s) [attempted 1309/8459 = 15%, 265 KB/s], Decompressed: 1302 Downloaded: 1346 file(s) [attempted 1346/8459 = 15%, 215 KB/s], Decompressed: 1343 Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 447 KB/s], Decompressed: 1384 Downloaded: 1432 file(s) [attempted 1432/8459 = 16%, 1286 KB/s], Decompressed: 1429 Downloaded: 1471 file(s) [attempted 1471/8459 = 17%, 623 KB/s], Decompressed: 1463 Downloaded: 1511 file(s) [attempted 1511/8459 = 17%, 153 KB/s], Decompressed: 1507 Downloaded: 1549 file(s) [attempted 1549/8459 = 18%, 186 KB/s], Decompressed: 1545 Downloaded: 1593 file(s) [attempted 1593/8459 = 18%, 134 KB/s], Decompressed: 1589 Downloaded: 1634 file(s) [attempted 1634/8459 = 19%, 55 KB/s], Decompressed: 1631 Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 122 KB/s], Decompressed: 1665 Downloaded: 1711 file(s) [attempted 1711/8459 = 20%, 346 KB/s], Decompressed: 1702 Downloaded: 1747 file(s) [attempted 1747/8459 = 20%, 992 KB/s], Decompressed: 1743 Downloaded: 1791 file(s) [attempted 1791/8459 = 21%, 936 KB/s], Decompressed: 1788 Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 73 KB/s], Decompressed: 1822 Downloaded: 1870 file(s) [attempted 1870/8459 = 22%, 277 KB/s], Decompressed: 1867 Downloaded: 1906 file(s) [attempted 1906/8459 = 22%, 533 KB/s], Decompressed: 1901 Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 426 KB/s], Decompressed: 1939 Downloaded: 1982 file(s) [attempted 1982/8459 = 23%, 77 KB/s], Decompressed: 1977 Downloaded: 2020 file(s) [attempted 2020/8459 = 23%, 397 KB/s], Decompressed: 2010 Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 414 KB/s], Decompressed: 2055 Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 1076 KB/s], Decompressed: 2093 Downloaded: 2137 file(s) [attempted 2137/8459 = 25%, 672 KB/s], Decompressed: 2130 Downloaded: 2175 file(s) [attempted 2175/8459 = 25%, 97 KB/s], Decompressed: 2171 Downloaded: 2216 file(s) [attempted 2216/8459 = 26%, 117 KB/s], Decompressed: 2206 Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 576 KB/s], Decompressed: 2206 Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 263 KB/s], Decompressed: 2209 Downloaded: 2339 file(s) [attempted 2339/8459 = 27%, 115 KB/s], Decompressed: 2209 Downloaded: 2377 file(s) [attempted 2377/8459 = 28%, 789 KB/s], Decompressed: 2209 Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 36 KB/s], Decompressed: 2209 Downloaded: 2459 file(s) [attempted 2459/8459 = 29%, 177 KB/s], Decompressed: 2209 Downloaded: 2496 file(s) [attempted 2496/8459 = 29%, 416 KB/s], Decompressed: 2209 Downloaded: 2537 file(s) [attempted 2537/8459 = 29%, 316 KB/s], Decompressed: 2288 Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 64 KB/s], Decompressed: 2537 Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 77 KB/s], Decompressed: 2616 Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 175 KB/s], Decompressed: 2661 Downloaded: 2705 file(s) [attempted 2705/8459 = 31%, 1002 KB/s], Decompressed: 2702 Downloaded: 2739 file(s) [attempted 2739/8459 = 32%, 38 KB/s], Decompressed: 2736 Downloaded: 2777 file(s) [attempted 2777/8459 = 32%, 322 KB/s], Decompressed: 2774 Downloaded: 2819 file(s) [attempted 2819/8459 = 33%, 83 KB/s], Decompressed: 2815 Downloaded: 2863 file(s) [attempted 2863/8459 = 33%, 52 KB/s], Decompressed: 2859 Downloaded: 2900 file(s) [attempted 2900/8459 = 34%, 122 KB/s], Decompressed: 2897 Downloaded: 2941 file(s) [attempted 2941/8459 = 34%, 40 KB/s], Decompressed: 2934 Downloaded: 2979 file(s) [attempted 2979/8459 = 35%, 351 KB/s], Decompressed: 2972 Downloaded: 3017 file(s) [attempted 3017/8459 = 35%, 466 KB/s], Decompressed: 3013 Downloaded: 3061 file(s) [attempted 3061/8459 = 36%, 111 KB/s], Decompressed: 3058 Downloaded: 3104 file(s) [attempted 3104/8459 = 36%, 412 KB/s], Decompressed: 3095 Downloaded: 3147 file(s) [attempted 3147/8459 = 37%, 309 KB/s], Decompressed: 3143 Downloaded: 3184 file(s) [attempted 3184/8459 = 37%, 176 KB/s], Decompressed: 3181 Downloaded: 3225 file(s) [attempted 3225/8459 = 38%, 52 KB/s], Decompressed: 3222 Downloaded: 3263 file(s) [attempted 3263/8459 = 38%, 1089 KB/s], Decompressed: 3256 Downloaded: 3306 file(s) [attempted 3306/8459 = 39%, 245 KB/s], Decompressed: 3301 Downloaded: 3351 file(s) [attempted 3351/8459 = 39%, 720 KB/s], Decompressed: 3342 Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 45 KB/s], Decompressed: 3379 Downloaded: 3421 file(s) [attempted 3421/8459 = 40%, 411 KB/s], Decompressed: 3417 Downloaded: 3463 file(s) [attempted 3463/8459 = 40%, 306 KB/s], Decompressed: 3458 Downloaded: 3499 file(s) [attempted 3499/8459 = 41%, 171 KB/s], Decompressed: 3496 Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 71 KB/s], Decompressed: 3533 Downloaded: 3573 file(s) [attempted 3573/8459 = 42%, 747 KB/s], Decompressed: 3568 Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 177 KB/s], Decompressed: 3602 Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 202 KB/s], Decompressed: 3646 Downloaded: 3693 file(s) [attempted 3693/8459 = 43%, 72 KB/s], Decompressed: 3687 Downloaded: 3733 file(s) [attempted 3733/8459 = 44%, 93 KB/s], Decompressed: 3725 Downloaded: 3768 file(s) [attempted 3768/8459 = 44%, 1076 KB/s], Decompressed: 3759 Downloaded: 3804 file(s) [attempted 3804/8459 = 44%, 367 KB/s], Decompressed: 3797 Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 714 KB/s], Decompressed: 3847 Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 248 KB/s], Decompressed: 3886 Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 41 KB/s], Decompressed: 3930 Downloaded: 3975 file(s) [attempted 3975/8459 = 46%, 354 KB/s], Decompressed: 3965 Downloaded: 4007 file(s) [attempted 4007/8459 = 47%, 284 KB/s], Decompressed: 4002 Downloaded: 4047 file(s) [attempted 4047/8459 = 47%, 74 KB/s], Decompressed: 4043 Downloaded: 4084 file(s) [attempted 4084/8459 = 48%, 234 KB/s], Decompressed: 4081 Downloaded: 4127 file(s) [attempted 4127/8459 = 48%, 146 KB/s], Decompressed: 4115 Downloaded: 4163 file(s) [attempted 4163/8459 = 49%, 207 KB/s], Decompressed: 4160 Downloaded: 4202 file(s) [attempted 4202/8459 = 49%, 1419 KB/s], Decompressed: 4194 Downloaded: 4238 file(s) [attempted 4238/8459 = 50%, 340 KB/s], Decompressed: 4235 Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 228 KB/s], Decompressed: 4276 Downloaded: 4324 file(s) [attempted 4324/8459 = 51%, 332 KB/s], Decompressed: 4317 Downloaded: 4362 file(s) [attempted 4362/8459 = 51%, 100 KB/s], Decompressed: 4355 Downloaded: 4405 file(s) [attempted 4405/8459 = 52%, 653 KB/s], Decompressed: 4396 Downloaded: 4433 file(s) [attempted 4433/8459 = 52%, 127 KB/s], Decompressed: 4430 Downloaded: 4475 file(s) [attempted 4475/8459 = 52%, 422 KB/s], Decompressed: 4471 Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 113 KB/s], Decompressed: 4512 Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 327 KB/s], Decompressed: 4546 Downloaded: 4598 file(s) [attempted 4598/8459 = 54%, 36 KB/s], Decompressed: 4587 Downloaded: 4632 file(s) [attempted 4632/8459 = 54%, 546 KB/s], Decompressed: 4622 Downloaded: 4673 file(s) [attempted 4673/8459 = 55%, 404 KB/s], Decompressed: 4622 Downloaded: 4714 file(s) [attempted 4714/8459 = 55%, 193 KB/s], Decompressed: 4625 Downloaded: 4755 file(s) [attempted 4755/8459 = 56%, 808 KB/s], Decompressed: 4752 Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 291 KB/s], Decompressed: 4789 Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 197 KB/s], Decompressed: 4830 Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 88 KB/s], Decompressed: 4875 Downloaded: 4923 file(s) [attempted 4923/8459 = 58%, 398 KB/s], Decompressed: 4919 Downloaded: 4966 file(s) [attempted 4966/8459 = 58%, 38 KB/s], Decompressed: 4957 Downloaded: 4995 file(s) [attempted 4995/8459 = 59%, 998 KB/s], Decompressed: 4991 Downloaded: 5038 file(s) [attempted 5038/8459 = 59%, 107 KB/s], Decompressed: 5032 Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 148 KB/s], Decompressed: 5077 Downloaded: 5125 file(s) [attempted 5125/8459 = 60%, 647 KB/s], Decompressed: 5121 Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 54 KB/s], Decompressed: 5156 Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 27 KB/s], Decompressed: 5197 Downloaded: 5241 file(s) [attempted 5241/8459 = 61%, 273 KB/s], Decompressed: 5238 Downloaded: 5286 file(s) [attempted 5286/8459 = 62%, 362 KB/s], Decompressed: 5282 Downloaded: 5330 file(s) [attempted 5330/8459 = 63%, 422 KB/s], Decompressed: 5323 Downloaded: 5368 file(s) [attempted 5368/8459 = 63%, 124 KB/s], Decompressed: 5361 Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 59 KB/s], Decompressed: 5399 Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 507 KB/s], Decompressed: 5440 Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 150 KB/s], Decompressed: 5481 Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 955 KB/s], Decompressed: 5525 Downloaded: 5573 file(s) [attempted 5573/8459 = 65%, 120 KB/s], Decompressed: 5570 Downloaded: 5611 file(s) [attempted 5611/8459 = 66%, 96 KB/s], Decompressed: 5607 Downloaded: 5648 file(s) [attempted 5648/8459 = 66%, 186 KB/s], Decompressed: 5645 Downloaded: 5693 file(s) [attempted 5693/8459 = 67%, 289 KB/s], Decompressed: 5689 Downloaded: 5734 file(s) [attempted 5734/8459 = 67%, 103 KB/s], Decompressed: 5727 Downloaded: 5775 file(s) [attempted 5775/8459 = 68%, 577 KB/s], Decompressed: 5768 Downloaded: 5813 file(s) [attempted 5813/8459 = 68%, 65 KB/s], Decompressed: 5807 Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 627 KB/s], Decompressed: 5843 Downloaded: 5888 file(s) [attempted 5888/8459 = 69%, 449 KB/s], Decompressed: 5885 Downloaded: 5936 file(s) [attempted 5936/8459 = 70%, 143 KB/s], Decompressed: 5932 Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 72 KB/s], Decompressed: 5980 Downloaded: 6028 file(s) [attempted 6028/8459 = 71%, 26 KB/s], Decompressed: 6021 Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 885 KB/s], Decompressed: 6066 Downloaded: 6107 file(s) [attempted 6107/8459 = 72%, 304 KB/s], Decompressed: 6097 Downloaded: 6142 file(s) [attempted 6142/8459 = 72%, 226 KB/s], Decompressed: 6138 Downloaded: 6186 file(s) [attempted 6186/8459 = 73%, 685 KB/s], Decompressed: 6182 Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 197 KB/s], Decompressed: 6227 Downloaded: 6271 file(s) [attempted 6271/8459 = 74%, 239 KB/s], Decompressed: 6266 Downloaded: 6306 file(s) [attempted 6306/8459 = 74%, 1016 KB/s], Decompressed: 6302 Downloaded: 6343 file(s) [attempted 6343/8459 = 74%, 1083 KB/s], Decompressed: 6340 Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 703 KB/s], Decompressed: 6388 Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 224 KB/s], Decompressed: 6429 Downloaded: 6473 file(s) [attempted 6473/8459 = 76%, 275 KB/s], Decompressed: 6466 Downloaded: 6511 file(s) [attempted 6511/8459 = 76%, 114 KB/s], Decompressed: 6504 Downloaded: 6548 file(s) [attempted 6548/8459 = 77%, 53 KB/s], Decompressed: 6545 Downloaded: 6593 file(s) [attempted 6593/8459 = 77%, 122 KB/s], Decompressed: 6590 Downloaded: 6637 file(s) [attempted 6637/8459 = 78%, 33 KB/s], Decompressed: 6631 Downloaded: 6675 file(s) [attempted 6675/8459 = 78%, 57 KB/s], Decompressed: 6672 Downloaded: 6713 file(s) [attempted 6713/8459 = 79%, 26 KB/s], Decompressed: 6709 Downloaded: 6757 file(s) [attempted 6757/8459 = 79%, 469 KB/s], Decompressed: 6750 Downloaded: 6798 file(s) [attempted 6798/8459 = 80%, 81 KB/s], Decompressed: 6791 Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 233 KB/s], Decompressed: 6839 Downloaded: 6887 file(s) [attempted 6887/8459 = 81%, 151 KB/s], Decompressed: 6884 Downloaded: 6922 file(s) [attempted 6922/8459 = 81%, 180 KB/s], Decompressed: 6915 Downloaded: 6963 file(s) [attempted 6963/8459 = 82%, 118 KB/s], Decompressed: 6952 Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 380 KB/s], Decompressed: 6993 Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 22 KB/s], Decompressed: 7038 Downloaded: 7086 file(s) [attempted 7086/8459 = 83%, 316 KB/s], Decompressed: 7080 Downloaded: 7123 file(s) [attempted 7123/8459 = 84%, 209 KB/s], Decompressed: 7120 Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 38 KB/s], Decompressed: 7168 Downloaded: 7212 file(s) [attempted 7212/8459 = 85%, 23 KB/s], Decompressed: 7209 Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 304 KB/s], Decompressed: 7240 Downloaded: 7291 file(s) [attempted 7291/8459 = 86%, 277 KB/s], Decompressed: 7284 Downloaded: 7332 file(s) [attempted 7332/8459 = 86%, 24 KB/s], Decompressed: 7325 Downloaded: 7373 file(s) [attempted 7373/8459 = 87%, 65 KB/s], Decompressed: 7370 Downloaded: 7415 file(s) [attempted 7415/8459 = 87%, 118 KB/s], Decompressed: 7408 Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 319 KB/s], Decompressed: 7442 Downloaded: 7492 file(s) [attempted 7492/8459 = 88%, 136 KB/s], Decompressed: 7486 Downloaded: 7527 file(s) [attempted 7527/8459 = 88%, 114 KB/s], Decompressed: 7520 Downloaded: 7568 file(s) [attempted 7568/8459 = 89%, 472 KB/s], Decompressed: 7565 Downloaded: 7611 file(s) [attempted 7611/8459 = 89%, 350 KB/s], Decompressed: 7599 Downloaded: 7647 file(s) [attempted 7647/8459 = 90%, 175 KB/s], Decompressed: 7640 Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 1007 KB/s], Decompressed: 7685 Downloaded: 7730 file(s) [attempted 7730/8459 = 91%, 993 KB/s], Decompressed: 7722 Downloaded: 7767 file(s) [attempted 7767/8459 = 91%, 586 KB/s], Decompressed: 7757 Downloaded: 7808 file(s) [attempted 7808/8459 = 92%, 964 KB/s], Decompressed: 7804 Downloaded: 7846 file(s) [attempted 7846/8459 = 92%, 154 KB/s], Decompressed: 7842 Downloaded: 7889 file(s) [attempted 7889/8459 = 93%, 309 KB/s], Decompressed: 7880 Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 653 KB/s], Decompressed: 7930 Downloaded: 7972 file(s) [attempted 7972/8459 = 94%, 374 KB/s], Decompressed: 7969 Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 153 KB/s], Decompressed: 8010 Downloaded: 8051 file(s) [attempted 8051/8459 = 95%, 435 KB/s], Decompressed: 8047 Downloaded: 8090 file(s) [attempted 8090/8459 = 95%, 326 KB/s], Decompressed: 8085 Downloaded: 8130 file(s) [attempted 8130/8459 = 96%, 283 KB/s], Decompressed: 8126 Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 748 KB/s], Decompressed: 8164 Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 87 KB/s], Decompressed: 8212 Downloaded: 8253 file(s) [attempted 8253/8459 = 97%, 1584 KB/s], Decompressed: 8249 Downloaded: 8290 file(s) [attempted 8290/8459 = 98%, 517 KB/s], Decompressed: 8284 Downloaded: 8331 file(s) [attempted 8331/8459 = 98%, 83 KB/s], Decompressed: 8325 Downloaded: 8373 file(s) [attempted 8373/8459 = 98%, 92 KB/s], Decompressed: 8369 Downloaded: 8414 file(s) [attempted 8414/8459 = 99%, 605 KB/s], Decompressed: 8410 Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 204 KB/s], Decompressed: 8444 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 204 KB/s], Decompressed: 8451
lean_checker exit 0
lake build
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (253s) 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) [0x73c265bc6785] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x73c265bbdb27] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x73c265bbdc0b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x73c265af3c62] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x73c265af4439] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x73c265bcaf99] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x73c265a32923] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x73c265a32b2b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x73c265a33827] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x73c265a341b6] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x73c265bc9e8b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x73c265815adb] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73c265bc9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73c265bc9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x73c265b9b1f3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x73c265815c92] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x73c260c22638] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x73c260a0cd2e] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x73c260569a82] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x73c260569f0e] /lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x73c25d44524a] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x73c25d445305] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5da312ac48da] ✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (66s) ✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.0s) ✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (38s) ✔ [3414/3416] Built Iut.Basic (3.3s) ✔ [3415/3416] Built Iut (9.5s) Build completed successfully (3416 jobs).
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
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-batch-00000)
apx-semantic-phase {"duration_ms":5,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":7592,"diagnostic_count":3037,"duration_ms":5905163,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":7592,"dependency_count":73323,"diagnostic_count":134256,"duration_ms":1,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":532650,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":7592,"dependency_count":73323,"diagnostic_count":134256,"duration_ms":10186,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":453516949,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":997,"ok":true,"payload_bytes":453516949,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":18}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":693,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":19,"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":62267,"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 8543c918f29ec02fbe854b9f99cf4ce914898c81cc06fadb720100009a7ef83e
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":6495138,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
apx-semantic-phase {"duration_ms":7,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":97,"diagnostic_count":15,"duration_ms":6948,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":97,"dependency_count":189,"diagnostic_count":2058,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":374956,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":97,"dependency_count":189,"diagnostic_count":2058,"duration_ms":269,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":2,"ok":true,"payload_bytes":3002937,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":14,"ok":true,"payload_bytes":3002937,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":346,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache c5d00d79bfc98fa70cdec4b614d7e759f078085d8cc1d30933d856891591a0a2
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":39,"runner_cache_hit":true}
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":478654,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
apx-semantic-phase {"duration_ms":9,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":152,"diagnostic_count":23,"duration_ms":12701,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":152,"dependency_count":468,"diagnostic_count":1820,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":376285,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":152,"dependency_count":468,"diagnostic_count":1820,"duration_ms":193,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":2722873,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":10,"ok":true,"payload_bytes":2722873,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":329,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 4aee9bac4a0df9b38a9b35781b33cc39661cad08c376cdc832c218cc4f3678c0
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":43,"runner_cache_hit":true}
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":496370,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)
apx-semantic-phase {"duration_ms":180,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":1885,"diagnostic_count":116,"duration_ms":1581003,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":1885,"dependency_count":2619,"diagnostic_count":33439,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":415444,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":1885,"dependency_count":2619,"diagnostic_count":33439,"duration_ms":1760,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":66295081,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":65,"ok":true,"payload_bytes":66295081,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":436,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":103511,"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 62bff9e19e2f0fb064b5be968a31116d5e750cf0a316b7426f9d1ac2b091e2da
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":2011585,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)
apx-semantic-phase {"duration_ms":8,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":1,"diagnostic_count":0,"duration_ms":97,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":1,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":357590,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":1,"dependency_count":0,"diagnostic_count":0,"duration_ms":56,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1330,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":6,"ok":true,"payload_bytes":1330,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":20}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":428,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 1d35f17e8a5e2a4f7eb2e38812720399852ea8f1a139b919203fe67b11f92c80
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":42,"runner_cache_hit":true}
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":429040,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":6,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":357761,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":90,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":2,"ok":true,"payload_bytes":738,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":6,"ok":true,"payload_bytes":738,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":11}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":94,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 1efb022e29a187ab0ac03706f29926a53fd827a39730c76c52602cb79bfbc075
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":32,"runner_cache_hit":true}
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":365542,"ok":true}