Verification run
Run 353
succeeded commit
858e4497a220 toolchain lean-v4-30-0 prover lean took 3h 2m · 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-464-source
exit_code=Some(0) duration_ms=2455
stderr:
Cloning into '/var/lib/apodeixis/repos/job-464-source'...
$ git checkout 858e4497a220f2dc35f8b590269a44485d8f64e3
exit_code=Some(128) duration_ms=3
stderr:
fatal: reference is not a tree: 858e4497a220f2dc35f8b590269a44485d8f64e3
$ git fetch --depth 1 origin 858e4497a220f2dc35f8b590269a44485d8f64e3
exit_code=Some(0) duration_ms=1045
stderr:
From https://github.com/promachina/iut-lean
* branch 858e4497a220f2dc35f8b590269a44485d8f64e3 -> FETCH_HEAD
$ git checkout 858e4497a220f2dc35f8b590269a44485d8f64e3 (after fetch)
exit_code=Some(0) duration_ms=148
stderr:
Note: switching to '858e4497a220f2dc35f8b590269a44485d8f64e3'.
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 858e449 Derive valuation anchor coordinate transport
Resolved source revision: 858e4497a220f2dc35f8b590269a44485d8f64e3
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=858e4497a220f2dc35f8b590269a44485d8f64e3 provenance={"branch":"master","checked_out_revision":"858e4497a220f2dc35f8b590269a44485d8f64e3","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"858e4497a220f2dc35f8b590269a44485d8f64e3","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: 24/31 module hit(s), 7 miss(es)
Lean semantic module cache: trying stable superset runner for 7 missing module(s) with 31 imported module candidate(s)
Lean semantic module cache: checkpointed 7 module fragment row(s) from stable superset runner
Lean semantic module cache: stable superset runner extracted 7 missing module(s) in one Lean invocation
Lean semantic module cache: extracted 7 missing module(s) in bounded batches; wrote merged semantic response
$ lake exe cache get
exit_code=Some(0) duration_ms=48961
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%, 9 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 1 KB/s], Decompressed: 14
Downloaded: 40 file(s) [attempted 40/8459 = 0%, 14 KB/s], Decompressed: 37
Downloaded: 66 file(s) [attempted 66/8459 = 0%, 52 KB/s], Decompressed: 63
Downloaded: 93 file(s) [attempted 93/8459 = 1%, 492 KB/s], Decompressed: 92
Downloaded: 127 file(s) [attempted 127/8459 = 1%, 33 KB/s], Decompressed: 121
Downloaded: 163 file(s) [attempted 163/8459 = 1%, 75 KB/s], Decompressed: 155
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 509 KB/s], Decompressed: 196
Downloaded: 238 file(s) [attempted 238/8459 = 2%, 259 KB/s], Decompressed: 230
Downloaded: 275 file(s) [attempted 275/8459 = 3%, 249 KB/s], Decompressed: 268
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 159 KB/s], Decompressed: 309
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 23 KB/s], Decompressed: 350
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 54 KB/s], Decompressed: 384
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 903 KB/s], Decompressed: 425
Downloaded: 466 file(s) [attempted 466/8459 = 5%, 855 KB/s], Decompressed: 463
Downloaded: 511 file(s) [attempted 511/8459 = 6%, 67 KB/s], Decompressed: 508
Downloaded: 549 file(s) [attempted 549/8459 = 6%, 287 KB/s], Decompressed: 538
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 46 KB/s], Decompressed: 583
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 73 KB/s], Decompressed: 624
Downloaded: 665 file(s) [attempted 665/8459 = 7%, 43 KB/s], Decompressed: 662
Downloaded: 706 file(s) [attempted 706/8459 = 8%, 255 KB/s], Decompressed: 703
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 231 KB/s], Decompressed: 744
Downloaded: 788 file(s) [attempted 788/8459 = 9%, 363 KB/s], Decompressed: 785
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 479 KB/s], Decompressed: 819
Downloaded: 871 file(s) [attempted 871/8459 = 10%, 41 KB/s], Decompressed: 867
Downloaded: 908 file(s) [attempted 908/8459 = 10%, 60 KB/s], Decompressed: 874
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 400 KB/s], Decompressed: 874
Downloaded: 987 file(s) [attempted 987/8459 = 11%, 256 KB/s], Decompressed: 985
Downloaded: 1025 file(s) [attempted 1025/8459 = 12%, 276 KB/s], Decompressed: 1021
Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 94 KB/s], Decompressed: 1066
Downloaded: 1107 file(s) [attempted 1107/8459 = 13%, 417 KB/s], Decompressed: 1104
Downloaded: 1148 file(s) [attempted 1148/8459 = 13%, 372 KB/s], Decompressed: 1145
Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 946 KB/s], Decompressed: 1186
Downloaded: 1223 file(s) [attempted 1223/8459 = 14%, 190 KB/s], Decompressed: 1220
Downloaded: 1270 file(s) [attempted 1270/8459 = 15%, 259 KB/s], Decompressed: 1264
Downloaded: 1305 file(s) [attempted 1305/8459 = 15%, 592 KB/s], Decompressed: 1299
Downloaded: 1343 file(s) [attempted 1343/8459 = 15%, 132 KB/s], Decompressed: 1340
Downloaded: 1381 file(s) [attempted 1381/8459 = 16%, 255 KB/s], Decompressed: 1377
Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 212 KB/s], Decompressed: 1412
Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 367 KB/s], Decompressed: 1456
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 190 KB/s], Decompressed: 1490
Downloaded: 1537 file(s) [attempted 1537/8459 = 18%, 118 KB/s], Decompressed: 1531
Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 411 KB/s], Decompressed: 1572
Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 550 KB/s], Decompressed: 1607
Downloaded: 1655 file(s) [attempted 1655/8459 = 19%, 960 KB/s], Decompressed: 1651
Downloaded: 1694 file(s) [attempted 1694/8459 = 20%, 428 KB/s], Decompressed: 1689
Downloaded: 1730 file(s) [attempted 1730/8459 = 20%, 248 KB/s], Decompressed: 1726
Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 83 KB/s], Decompressed: 1764
Downloaded: 1809 file(s) [attempted 1809/8459 = 21%, 45 KB/s], Decompressed: 1805
Downloaded: 1853 file(s) [attempted 1853/8459 = 21%, 148 KB/s], Decompressed: 1846
Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 91 KB/s], Decompressed: 1887
Downloaded: 1929 file(s) [attempted 1929/8459 = 22%, 77 KB/s], Decompressed: 1921
Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 917 KB/s], Decompressed: 1956
Downloaded: 2000 file(s) [attempted 2000/8459 = 23%, 48 KB/s], Decompressed: 1997
Downloaded: 2045 file(s) [attempted 2045/8459 = 24%, 188 KB/s], Decompressed: 2041
Downloaded: 2086 file(s) [attempted 2086/8459 = 24%, 311 KB/s], Decompressed: 2082
Downloaded: 2123 file(s) [attempted 2123/8459 = 25%, 1205 KB/s], Decompressed: 2113
Downloaded: 2161 file(s) [attempted 2161/8459 = 25%, 212 KB/s], Decompressed: 2154
Downloaded: 2201 file(s) [attempted 2201/8459 = 26%, 91 KB/s], Decompressed: 2192
Downloaded: 2237 file(s) [attempted 2237/8459 = 26%, 117 KB/s], Decompressed: 2233
Downloaded: 2282 file(s) [attempted 2282/8459 = 26%, 808 KB/s], Decompressed: 2274
Downloaded: 2315 file(s) [attempted 2315/8459 = 27%, 34 KB/s], Decompressed: 2312
Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 845 KB/s], Decompressed: 2349
Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 39 KB/s], Decompressed: 2394
Downloaded: 2438 file(s) [attempted 2438/8459 = 28%, 176 KB/s], Decompressed: 2435
Downloaded: 2479 file(s) [attempted 2479/8459 = 29%, 58 KB/s], Decompressed: 2476
Downloaded: 2523 file(s) [attempted 2523/8459 = 29%, 252 KB/s], Decompressed: 2517
Downloaded: 2561 file(s) [attempted 2561/8459 = 30%, 763 KB/s], Decompressed: 2551
Downloaded: 2593 file(s) [attempted 2593/8459 = 30%, 362 KB/s], Decompressed: 2589
Downloaded: 2637 file(s) [attempted 2637/8459 = 31%, 117 KB/s], Decompressed: 2630
Downloaded: 2674 file(s) [attempted 2674/8459 = 31%, 534 KB/s], Decompressed: 2671
Downloaded: 2719 file(s) [attempted 2719/8459 = 32%, 454 KB/s], Decompressed: 2715
Downloaded: 2763 file(s) [attempted 2763/8459 = 32%, 814 KB/s], Decompressed: 2753
Downloaded: 2795 file(s) [attempted 2795/8459 = 33%, 776 KB/s], Decompressed: 2787
Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 51 KB/s], Decompressed: 2828
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 162 KB/s], Decompressed: 2873
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 79 KB/s], Decompressed: 2914
Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 224 KB/s], Decompressed: 2945
Downloaded: 2993 file(s) [attempted 2993/8459 = 35%, 192 KB/s], Decompressed: 2989
Downloaded: 3035 file(s) [attempted 3035/8459 = 35%, 1101 KB/s], Decompressed: 3027
Downloaded: 3075 file(s) [attempted 3075/8459 = 36%, 226 KB/s], Decompressed: 3068
Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 58 KB/s], Decompressed: 3106
Downloaded: 3150 file(s) [attempted 3150/8459 = 37%, 127 KB/s], Decompressed: 3147
Downloaded: 3190 file(s) [attempted 3190/8459 = 37%, 208 KB/s], Decompressed: 3184
Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 784 KB/s], Decompressed: 3229
Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 215 KB/s], Decompressed: 3266
Downloaded: 3307 file(s) [attempted 3307/8459 = 39%, 611 KB/s], Decompressed: 3304
Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 53 KB/s], Decompressed: 3345
Downloaded: 3390 file(s) [attempted 3390/8459 = 40%, 257 KB/s], Decompressed: 3386
Downloaded: 3431 file(s) [attempted 3431/8459 = 40%, 676 KB/s], Decompressed: 3427
Downloaded: 3468 file(s) [attempted 3468/8459 = 40%, 544 KB/s], Decompressed: 3462
Downloaded: 3506 file(s) [attempted 3506/8459 = 41%, 1642 KB/s], Decompressed: 3503
Downloaded: 3547 file(s) [attempted 3547/8459 = 41%, 462 KB/s], Decompressed: 3537
Downloaded: 3586 file(s) [attempted 3586/8459 = 42%, 544 KB/s], Decompressed: 3581
Downloaded: 3626 file(s) [attempted 3626/8459 = 42%, 625 KB/s], Decompressed: 3619
Downloaded: 3670 file(s) [attempted 3670/8459 = 43%, 112 KB/s], Decompressed: 3663
Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 170 KB/s], Decompressed: 3708
Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 461 KB/s], Decompressed: 3749
Downloaded: 3797 file(s) [attempted 3797/8459 = 44%, 195 KB/s], Decompressed: 3790
Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 127 KB/s], Decompressed: 3828
Downloaded: 3872 file(s) [attempted 3872/8459 = 45%, 258 KB/s], Decompressed: 3865
Downloaded: 3917 file(s) [attempted 3917/8459 = 46%, 57 KB/s], Decompressed: 3910
Downloaded: 3961 file(s) [attempted 3961/8459 = 46%, 31 KB/s], Decompressed: 3954
Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 79 KB/s], Decompressed: 3999
Downloaded: 4047 file(s) [attempted 4047/8459 = 47%, 93 KB/s], Decompressed: 4043
Downloaded: 4078 file(s) [attempted 4078/8459 = 48%, 147 KB/s], Decompressed: 4071
Downloaded: 4119 file(s) [attempted 4119/8459 = 48%, 355 KB/s], Decompressed: 4115
Downloaded: 4164 file(s) [attempted 4164/8459 = 49%, 67 KB/s], Decompressed: 4160
Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 1414 KB/s], Decompressed: 4197
Downloaded: 4242 file(s) [attempted 4242/8459 = 50%, 491 KB/s], Decompressed: 4232
Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 148 KB/s], Decompressed: 4273
Downloaded: 4321 file(s) [attempted 4321/8459 = 51%, 195 KB/s], Decompressed: 4314
Downloaded: 4365 file(s) [attempted 4365/8459 = 51%, 371 KB/s], Decompressed: 4358
Downloaded: 4406 file(s) [attempted 4406/8459 = 52%, 453 KB/s], Decompressed: 4399
Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 46 KB/s], Decompressed: 4440
Downloaded: 4481 file(s) [attempted 4481/8459 = 52%, 336 KB/s], Decompressed: 4471
Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 468 KB/s], Decompressed: 4519
Downloaded: 4567 file(s) [attempted 4567/8459 = 53%, 148 KB/s], Decompressed: 4564
Downloaded: 4611 file(s) [attempted 4611/8459 = 54%, 298 KB/s], Decompressed: 4601
Downloaded: 4646 file(s) [attempted 4646/8459 = 54%, 289 KB/s], Decompressed: 4639
Downloaded: 4683 file(s) [attempted 4683/8459 = 55%, 97 KB/s], Decompressed: 4680
Downloaded: 4724 file(s) [attempted 4724/8459 = 55%, 412 KB/s], Decompressed: 4721
Downloaded: 4765 file(s) [attempted 4765/8459 = 56%, 354 KB/s], Decompressed: 4762
Downloaded: 4804 file(s) [attempted 4804/8459 = 56%, 108 KB/s], Decompressed: 4796
Downloaded: 4840 file(s) [attempted 4840/8459 = 57%, 587 KB/s], Decompressed: 4834
Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 175 KB/s], Decompressed: 4875
Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 263 KB/s], Decompressed: 4916
Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 489 KB/s], Decompressed: 4950
Downloaded: 4995 file(s) [attempted 4995/8459 = 59%, 1166 KB/s], Decompressed: 4988
Downloaded: 5036 file(s) [attempted 5036/8459 = 59%, 113 KB/s], Decompressed: 5029
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 148 KB/s], Decompressed: 5077
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 313 KB/s], Decompressed: 5111
Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 94 KB/s], Decompressed: 5159
Downloaded: 5204 file(s) [attempted 5204/8459 = 61%, 93 KB/s], Decompressed: 5200
Downloaded: 5242 file(s) [attempted 5242/8459 = 61%, 94 KB/s], Decompressed: 5238
Downloaded: 5276 file(s) [attempted 5276/8459 = 62%, 76 KB/s], Decompressed: 5272
Downloaded: 5316 file(s) [attempted 5316/8459 = 62%, 142 KB/s], Decompressed: 5313
Downloaded: 5357 file(s) [attempted 5357/8459 = 63%, 161 KB/s], Decompressed: 5347
Downloaded: 5399 file(s) [attempted 5399/8459 = 63%, 88 KB/s], Decompressed: 5395
Downloaded: 5436 file(s) [attempted 5436/8459 = 64%, 245 KB/s], Decompressed: 5433
Downloaded: 5474 file(s) [attempted 5474/8459 = 64%, 152 KB/s], Decompressed: 5470
Downloaded: 5515 file(s) [attempted 5515/8459 = 65%, 93 KB/s], Decompressed: 5512
Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 1287 KB/s], Decompressed: 5553
Downloaded: 5606 file(s) [attempted 5606/8459 = 66%, 478 KB/s], Decompressed: 5597
Downloaded: 5638 file(s) [attempted 5638/8459 = 66%, 48 KB/s], Decompressed: 5631
Downloaded: 5679 file(s) [attempted 5679/8459 = 67%, 596 KB/s], Decompressed: 5672
Downloaded: 5724 file(s) [attempted 5724/8459 = 67%, 156 KB/s], Decompressed: 5720
Downloaded: 5761 file(s) [attempted 5761/8459 = 68%, 1843 KB/s], Decompressed: 5758
Downloaded: 5799 file(s) [attempted 5799/8459 = 68%, 315 KB/s], Decompressed: 5792
Downloaded: 5837 file(s) [attempted 5837/8459 = 69%, 56 KB/s], Decompressed: 5830
Downloaded: 5874 file(s) [attempted 5874/8459 = 69%, 156 KB/s], Decompressed: 5871
Downloaded: 5912 file(s) [attempted 5912/8459 = 69%, 323 KB/s], Decompressed: 5898
Downloaded: 5953 file(s) [attempted 5953/8459 = 70%, 274 KB/s], Decompressed: 5936
Downloaded: 5980 file(s) [attempted 5980/8459 = 70%, 1581 KB/s], Decompressed: 5977
Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 27 KB/s], Decompressed: 6004
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 159 KB/s], Decompressed: 6049
Downloaded: 6107 file(s) [attempted 6107/8459 = 72%, 307 KB/s], Decompressed: 6083
Downloaded: 6145 file(s) [attempted 6145/8459 = 72%, 1267 KB/s], Decompressed: 6138
Downloaded: 6179 file(s) [attempted 6179/8459 = 73%, 140 KB/s], Decompressed: 6172
Downloaded: 6217 file(s) [attempted 6217/8459 = 73%, 37 KB/s], Decompressed: 6206
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 33 KB/s], Decompressed: 6251
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 58 KB/s], Decompressed: 6288
Downloaded: 6333 file(s) [attempted 6333/8459 = 74%, 461 KB/s], Decompressed: 6326
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 290 KB/s], Decompressed: 6357
Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 42 KB/s], Decompressed: 6401
Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 717 KB/s], Decompressed: 6446
Downloaded: 6487 file(s) [attempted 6487/8459 = 76%, 285 KB/s], Decompressed: 6483
Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 83 KB/s], Decompressed: 6507
Downloaded: 6572 file(s) [attempted 6572/8459 = 77%, 134 KB/s], Decompressed: 6507
Downloaded: 6607 file(s) [attempted 6607/8459 = 78%, 228 KB/s], Decompressed: 6518
Downloaded: 6644 file(s) [attempted 6644/8459 = 78%, 467 KB/s], Decompressed: 6637
Downloaded: 6682 file(s) [attempted 6682/8459 = 78%, 240 KB/s], Decompressed: 6679
Downloaded: 6723 file(s) [attempted 6723/8459 = 79%, 245 KB/s], Decompressed: 6689
Downloaded: 6761 file(s) [attempted 6761/8459 = 79%, 423 KB/s], Decompressed: 6696
Downloaded: 6798 file(s) [attempted 6798/8459 = 80%, 90 KB/s], Decompressed: 6781
Downloaded: 6836 file(s) [attempted 6836/8459 = 80%, 213 KB/s], Decompressed: 6826
Downloaded: 6870 file(s) [attempted 6870/8459 = 81%, 935 KB/s], Decompressed: 6863
Downloaded: 6911 file(s) [attempted 6911/8459 = 81%, 868 KB/s], Decompressed: 6898
Downloaded: 6952 file(s) [attempted 6952/8459 = 82%, 45 KB/s], Decompressed: 6942
Downloaded: 6983 file(s) [attempted 6983/8459 = 82%, 313 KB/s], Decompressed: 6976
Downloaded: 7024 file(s) [attempted 7024/8459 = 83%, 370 KB/s], Decompressed: 7017
Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 1205 KB/s], Decompressed: 7058
Downloaded: 7103 file(s) [attempted 7103/8459 = 83%, 167 KB/s], Decompressed: 7096
Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 108 KB/s], Decompressed: 7141
Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 39 KB/s], Decompressed: 7168
Downloaded: 7216 file(s) [attempted 7216/8459 = 85%, 600 KB/s], Decompressed: 7209
Downloaded: 7257 file(s) [attempted 7257/8459 = 85%, 37 KB/s], Decompressed: 7250
Downloaded: 7301 file(s) [attempted 7301/8459 = 86%, 46 KB/s], Decompressed: 7284
Downloaded: 7333 file(s) [attempted 7333/8459 = 86%, 384 KB/s], Decompressed: 7325
Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 526 KB/s], Decompressed: 7363
Downloaded: 7418 file(s) [attempted 7418/8459 = 87%, 372 KB/s], Decompressed: 7401
Downloaded: 7459 file(s) [attempted 7459/8459 = 88%, 86 KB/s], Decompressed: 7442
Downloaded: 7497 file(s) [attempted 7497/8459 = 88%, 95 KB/s], Decompressed: 7473
Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 2418 KB/s], Decompressed: 7527
Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 251 KB/s], Decompressed: 7565
Downloaded: 7616 file(s) [attempted 7616/8459 = 90%, 33 KB/s], Decompressed: 7609
Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 192 KB/s], Decompressed: 7630
Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 355 KB/s], Decompressed: 7688
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 27 KB/s], Decompressed: 7729
Downloaded: 7777 file(s) [attempted 7777/8459 = 91%, 1587 KB/s], Decompressed: 7757
Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 22 KB/s], Decompressed: 7814
Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 2221 KB/s], Decompressed: 7835
Downloaded: 7883 file(s) [attempted 7883/8459 = 93%, 89 KB/s], Decompressed: 7876
Downloaded: 7928 file(s) [attempted 7928/8459 = 93%, 85 KB/s], Decompressed: 7900
Downloaded: 7972 file(s) [attempted 7972/8459 = 94%, 633 KB/s], Decompressed: 7952
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 123 KB/s], Decompressed: 8000
Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 382 KB/s], Decompressed: 8034
Downloaded: 8082 file(s) [attempted 8082/8459 = 95%, 35 KB/s], Decompressed: 8071
Downloaded: 8123 file(s) [attempted 8123/8459 = 96%, 36 KB/s], Decompressed: 8116
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 718 KB/s], Decompressed: 8164
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 95 KB/s], Decompressed: 8198
Downloaded: 8246 file(s) [attempted 8246/8459 = 97%, 794 KB/s], Decompressed: 8243
Downloaded: 8294 file(s) [attempted 8294/8459 = 98%, 418 KB/s], Decompressed: 8290
Downloaded: 8332 file(s) [attempted 8332/8459 = 98%, 86 KB/s], Decompressed: 8314
Downloaded: 8369 file(s) [attempted 8369/8459 = 98%, 282 KB/s], Decompressed: 8366
Downloaded: 8414 file(s) [attempted 8414/8459 = 99%, 108 KB/s], Decompressed: 8410
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 88 KB/s], Decompressed: 8444
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 88 KB/s], Decompressed: 8451
$ lake build
exit_code=Some(0) duration_ms=715060
stdout:
✔ [3401/3416] Built Iut.Stage1.IUTStage1SourceCore (117s)
✔ [3402/3416] Built Iut.Stage1.IUTStage1Remark312Absorption (78s)
✔ [3403/3416] Built Iut.Stage1.IUTStage1IUTIVAlgebra (12s)
✔ [3404/3416] Built Iut.Stage1.IUTStage1FiniteLabels (5.3s)
✔ [3405/3416] Built Iut.Stage1.IUTStage1StepX (6.3s)
✔ [3406/3416] Built Iut.Stage1.IUTStage1Gaussian (12s)
✔ [3407/3416] Built Iut.Stage1.IUTStage1HodgeSHE (7.4s)
✔ [3408/3416] Built Iut.Stage1.IUTStage1Theorem311 (5.4s)
✔ [3409/3416] Built Iut.Stage1.IUTStage1StepXI (20s)
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (294s)
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) [0x76f1aa1c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x76f1aa1bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x76f1aa1bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x76f1aa0f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x76f1aa0f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x76f1aa1caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x76f1aa032923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x76f1aa032b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x76f1aa033827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x76f1aa0341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x76f1aa1c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x76f1a9e15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x76f1aa1c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x76f1aa1c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x76f1aa19b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x76f1a9e15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x76f1a5222638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x76f1a500cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x76f1a4b69a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x76f1a4b69f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x76f1a1a4524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x76f1a1a45305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x611bdb3aa8da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (66s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (4.8s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (40s)
✔ [3414/3416] Built Iut.Basic (4.6s)
✔ [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=2004
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=9873207
stdout:
apx-semantic-phase {"duration_ms":2,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":12414,"diagnostic_count":4073,"duration_ms":6109855,"ok":true,"phase":"lean_declaration_extraction","target_module_count":7}
apx-semantic-phase {"declaration_count":12414,"dependency_count":134748,"diagnostic_count":162009,"duration_ms":1,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":3619803,"module_count":7,"ok":true,"phase":"lean_module_facts","target_module_count":7}
apx-semantic-phase {"declaration_count":12414,"dependency_count":134748,"diagnostic_count":162009,"duration_ms":22624,"module_count":7,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":3,"ok":true,"payload_bytes":577784048,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1328,"ok":true,"payload_bytes":577784048,"phase":"lean_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":3872}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":330,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":12,"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":27591,"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 934c2d5fe742db50b032ee84cc1b98d2eddf9a599ce8c047d7d565a76c70361c
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":9823041,"ok":true}
Stored Lean workspace build cache
Stored Lean semantic extraction cache
Command runs
git_checkout exit 0
git fetch --depth 1 origin 858e4497a220f2dc35f8b590269a44485d8f64e3
From https://github.com/promachina/iut-lean * branch 858e4497a220f2dc35f8b590269a44485d8f64e3 -> FETCH_HEAD
git_clone exit 0
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-464-source
Cloning into '/var/lib/apodeixis/repos/job-464-source'...
git_checkout exit 128
git checkout 858e4497a220f2dc35f8b590269a44485d8f64e3
fatal: reference is not a tree: 858e4497a220f2dc35f8b590269a44485d8f64e3
git_checkout exit 0
git checkout 858e4497a220f2dc35f8b590269a44485d8f64e3 (after fetch)
Note: switching to '858e4497a220f2dc35f8b590269a44485d8f64e3'. 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 858e449 Derive valuation anchor 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%, 9 KB/s], Decompressed: 0 Downloaded: 15 file(s) [attempted 15/8459 = 0%, 1 KB/s], Decompressed: 14 Downloaded: 40 file(s) [attempted 40/8459 = 0%, 14 KB/s], Decompressed: 37 Downloaded: 66 file(s) [attempted 66/8459 = 0%, 52 KB/s], Decompressed: 63 Downloaded: 93 file(s) [attempted 93/8459 = 1%, 492 KB/s], Decompressed: 92 Downloaded: 127 file(s) [attempted 127/8459 = 1%, 33 KB/s], Decompressed: 121 Downloaded: 163 file(s) [attempted 163/8459 = 1%, 75 KB/s], Decompressed: 155 Downloaded: 199 file(s) [attempted 199/8459 = 2%, 509 KB/s], Decompressed: 196 Downloaded: 238 file(s) [attempted 238/8459 = 2%, 259 KB/s], Decompressed: 230 Downloaded: 275 file(s) [attempted 275/8459 = 3%, 249 KB/s], Decompressed: 268 Downloaded: 312 file(s) [attempted 312/8459 = 3%, 159 KB/s], Decompressed: 309 Downloaded: 353 file(s) [attempted 353/8459 = 4%, 23 KB/s], Decompressed: 350 Downloaded: 388 file(s) [attempted 388/8459 = 4%, 54 KB/s], Decompressed: 384 Downloaded: 432 file(s) [attempted 432/8459 = 5%, 903 KB/s], Decompressed: 425 Downloaded: 466 file(s) [attempted 466/8459 = 5%, 855 KB/s], Decompressed: 463 Downloaded: 511 file(s) [attempted 511/8459 = 6%, 67 KB/s], Decompressed: 508 Downloaded: 549 file(s) [attempted 549/8459 = 6%, 287 KB/s], Decompressed: 538 Downloaded: 586 file(s) [attempted 586/8459 = 6%, 46 KB/s], Decompressed: 583 Downloaded: 627 file(s) [attempted 627/8459 = 7%, 73 KB/s], Decompressed: 624 Downloaded: 665 file(s) [attempted 665/8459 = 7%, 43 KB/s], Decompressed: 662 Downloaded: 706 file(s) [attempted 706/8459 = 8%, 255 KB/s], Decompressed: 703 Downloaded: 747 file(s) [attempted 747/8459 = 8%, 231 KB/s], Decompressed: 744 Downloaded: 788 file(s) [attempted 788/8459 = 9%, 363 KB/s], Decompressed: 785 Downloaded: 826 file(s) [attempted 826/8459 = 9%, 479 KB/s], Decompressed: 819 Downloaded: 871 file(s) [attempted 871/8459 = 10%, 41 KB/s], Decompressed: 867 Downloaded: 908 file(s) [attempted 908/8459 = 10%, 60 KB/s], Decompressed: 874 Downloaded: 949 file(s) [attempted 949/8459 = 11%, 400 KB/s], Decompressed: 874 Downloaded: 987 file(s) [attempted 987/8459 = 11%, 256 KB/s], Decompressed: 985 Downloaded: 1025 file(s) [attempted 1025/8459 = 12%, 276 KB/s], Decompressed: 1021 Downloaded: 1069 file(s) [attempted 1069/8459 = 12%, 94 KB/s], Decompressed: 1066 Downloaded: 1107 file(s) [attempted 1107/8459 = 13%, 417 KB/s], Decompressed: 1104 Downloaded: 1148 file(s) [attempted 1148/8459 = 13%, 372 KB/s], Decompressed: 1145 Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 946 KB/s], Decompressed: 1186 Downloaded: 1223 file(s) [attempted 1223/8459 = 14%, 190 KB/s], Decompressed: 1220 Downloaded: 1270 file(s) [attempted 1270/8459 = 15%, 259 KB/s], Decompressed: 1264 Downloaded: 1305 file(s) [attempted 1305/8459 = 15%, 592 KB/s], Decompressed: 1299 Downloaded: 1343 file(s) [attempted 1343/8459 = 15%, 132 KB/s], Decompressed: 1340 Downloaded: 1381 file(s) [attempted 1381/8459 = 16%, 255 KB/s], Decompressed: 1377 Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 212 KB/s], Decompressed: 1412 Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 367 KB/s], Decompressed: 1456 Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 190 KB/s], Decompressed: 1490 Downloaded: 1537 file(s) [attempted 1537/8459 = 18%, 118 KB/s], Decompressed: 1531 Downloaded: 1576 file(s) [attempted 1576/8459 = 18%, 411 KB/s], Decompressed: 1572 Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 550 KB/s], Decompressed: 1607 Downloaded: 1655 file(s) [attempted 1655/8459 = 19%, 960 KB/s], Decompressed: 1651 Downloaded: 1694 file(s) [attempted 1694/8459 = 20%, 428 KB/s], Decompressed: 1689 Downloaded: 1730 file(s) [attempted 1730/8459 = 20%, 248 KB/s], Decompressed: 1726 Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 83 KB/s], Decompressed: 1764 Downloaded: 1809 file(s) [attempted 1809/8459 = 21%, 45 KB/s], Decompressed: 1805 Downloaded: 1853 file(s) [attempted 1853/8459 = 21%, 148 KB/s], Decompressed: 1846 Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 91 KB/s], Decompressed: 1887 Downloaded: 1929 file(s) [attempted 1929/8459 = 22%, 77 KB/s], Decompressed: 1921 Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 917 KB/s], Decompressed: 1956 Downloaded: 2000 file(s) [attempted 2000/8459 = 23%, 48 KB/s], Decompressed: 1997 Downloaded: 2045 file(s) [attempted 2045/8459 = 24%, 188 KB/s], Decompressed: 2041 Downloaded: 2086 file(s) [attempted 2086/8459 = 24%, 311 KB/s], Decompressed: 2082 Downloaded: 2123 file(s) [attempted 2123/8459 = 25%, 1205 KB/s], Decompressed: 2113 Downloaded: 2161 file(s) [attempted 2161/8459 = 25%, 212 KB/s], Decompressed: 2154 Downloaded: 2201 file(s) [attempted 2201/8459 = 26%, 91 KB/s], Decompressed: 2192 Downloaded: 2237 file(s) [attempted 2237/8459 = 26%, 117 KB/s], Decompressed: 2233 Downloaded: 2282 file(s) [attempted 2282/8459 = 26%, 808 KB/s], Decompressed: 2274 Downloaded: 2315 file(s) [attempted 2315/8459 = 27%, 34 KB/s], Decompressed: 2312 Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 845 KB/s], Decompressed: 2349 Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 39 KB/s], Decompressed: 2394 Downloaded: 2438 file(s) [attempted 2438/8459 = 28%, 176 KB/s], Decompressed: 2435 Downloaded: 2479 file(s) [attempted 2479/8459 = 29%, 58 KB/s], Decompressed: 2476 Downloaded: 2523 file(s) [attempted 2523/8459 = 29%, 252 KB/s], Decompressed: 2517 Downloaded: 2561 file(s) [attempted 2561/8459 = 30%, 763 KB/s], Decompressed: 2551 Downloaded: 2593 file(s) [attempted 2593/8459 = 30%, 362 KB/s], Decompressed: 2589 Downloaded: 2637 file(s) [attempted 2637/8459 = 31%, 117 KB/s], Decompressed: 2630 Downloaded: 2674 file(s) [attempted 2674/8459 = 31%, 534 KB/s], Decompressed: 2671 Downloaded: 2719 file(s) [attempted 2719/8459 = 32%, 454 KB/s], Decompressed: 2715 Downloaded: 2763 file(s) [attempted 2763/8459 = 32%, 814 KB/s], Decompressed: 2753 Downloaded: 2795 file(s) [attempted 2795/8459 = 33%, 776 KB/s], Decompressed: 2787 Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 51 KB/s], Decompressed: 2828 Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 162 KB/s], Decompressed: 2873 Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 79 KB/s], Decompressed: 2914 Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 224 KB/s], Decompressed: 2945 Downloaded: 2993 file(s) [attempted 2993/8459 = 35%, 192 KB/s], Decompressed: 2989 Downloaded: 3035 file(s) [attempted 3035/8459 = 35%, 1101 KB/s], Decompressed: 3027 Downloaded: 3075 file(s) [attempted 3075/8459 = 36%, 226 KB/s], Decompressed: 3068 Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 58 KB/s], Decompressed: 3106 Downloaded: 3150 file(s) [attempted 3150/8459 = 37%, 127 KB/s], Decompressed: 3147 Downloaded: 3190 file(s) [attempted 3190/8459 = 37%, 208 KB/s], Decompressed: 3184 Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 784 KB/s], Decompressed: 3229 Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 215 KB/s], Decompressed: 3266 Downloaded: 3307 file(s) [attempted 3307/8459 = 39%, 611 KB/s], Decompressed: 3304 Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 53 KB/s], Decompressed: 3345 Downloaded: 3390 file(s) [attempted 3390/8459 = 40%, 257 KB/s], Decompressed: 3386 Downloaded: 3431 file(s) [attempted 3431/8459 = 40%, 676 KB/s], Decompressed: 3427 Downloaded: 3468 file(s) [attempted 3468/8459 = 40%, 544 KB/s], Decompressed: 3462 Downloaded: 3506 file(s) [attempted 3506/8459 = 41%, 1642 KB/s], Decompressed: 3503 Downloaded: 3547 file(s) [attempted 3547/8459 = 41%, 462 KB/s], Decompressed: 3537 Downloaded: 3586 file(s) [attempted 3586/8459 = 42%, 544 KB/s], Decompressed: 3581 Downloaded: 3626 file(s) [attempted 3626/8459 = 42%, 625 KB/s], Decompressed: 3619 Downloaded: 3670 file(s) [attempted 3670/8459 = 43%, 112 KB/s], Decompressed: 3663 Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 170 KB/s], Decompressed: 3708 Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 461 KB/s], Decompressed: 3749 Downloaded: 3797 file(s) [attempted 3797/8459 = 44%, 195 KB/s], Decompressed: 3790 Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 127 KB/s], Decompressed: 3828 Downloaded: 3872 file(s) [attempted 3872/8459 = 45%, 258 KB/s], Decompressed: 3865 Downloaded: 3917 file(s) [attempted 3917/8459 = 46%, 57 KB/s], Decompressed: 3910 Downloaded: 3961 file(s) [attempted 3961/8459 = 46%, 31 KB/s], Decompressed: 3954 Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 79 KB/s], Decompressed: 3999 Downloaded: 4047 file(s) [attempted 4047/8459 = 47%, 93 KB/s], Decompressed: 4043 Downloaded: 4078 file(s) [attempted 4078/8459 = 48%, 147 KB/s], Decompressed: 4071 Downloaded: 4119 file(s) [attempted 4119/8459 = 48%, 355 KB/s], Decompressed: 4115 Downloaded: 4164 file(s) [attempted 4164/8459 = 49%, 67 KB/s], Decompressed: 4160 Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 1414 KB/s], Decompressed: 4197 Downloaded: 4242 file(s) [attempted 4242/8459 = 50%, 491 KB/s], Decompressed: 4232 Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 148 KB/s], Decompressed: 4273 Downloaded: 4321 file(s) [attempted 4321/8459 = 51%, 195 KB/s], Decompressed: 4314 Downloaded: 4365 file(s) [attempted 4365/8459 = 51%, 371 KB/s], Decompressed: 4358 Downloaded: 4406 file(s) [attempted 4406/8459 = 52%, 453 KB/s], Decompressed: 4399 Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 46 KB/s], Decompressed: 4440 Downloaded: 4481 file(s) [attempted 4481/8459 = 52%, 336 KB/s], Decompressed: 4471 Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 468 KB/s], Decompressed: 4519 Downloaded: 4567 file(s) [attempted 4567/8459 = 53%, 148 KB/s], Decompressed: 4564 Downloaded: 4611 file(s) [attempted 4611/8459 = 54%, 298 KB/s], Decompressed: 4601 Downloaded: 4646 file(s) [attempted 4646/8459 = 54%, 289 KB/s], Decompressed: 4639 Downloaded: 4683 file(s) [attempted 4683/8459 = 55%, 97 KB/s], Decompressed: 4680 Downloaded: 4724 file(s) [attempted 4724/8459 = 55%, 412 KB/s], Decompressed: 4721 Downloaded: 4765 file(s) [attempted 4765/8459 = 56%, 354 KB/s], Decompressed: 4762 Downloaded: 4804 file(s) [attempted 4804/8459 = 56%, 108 KB/s], Decompressed: 4796 Downloaded: 4840 file(s) [attempted 4840/8459 = 57%, 587 KB/s], Decompressed: 4834 Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 175 KB/s], Decompressed: 4875 Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 263 KB/s], Decompressed: 4916 Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 489 KB/s], Decompressed: 4950 Downloaded: 4995 file(s) [attempted 4995/8459 = 59%, 1166 KB/s], Decompressed: 4988 Downloaded: 5036 file(s) [attempted 5036/8459 = 59%, 113 KB/s], Decompressed: 5029 Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 148 KB/s], Decompressed: 5077 Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 313 KB/s], Decompressed: 5111 Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 94 KB/s], Decompressed: 5159 Downloaded: 5204 file(s) [attempted 5204/8459 = 61%, 93 KB/s], Decompressed: 5200 Downloaded: 5242 file(s) [attempted 5242/8459 = 61%, 94 KB/s], Decompressed: 5238 Downloaded: 5276 file(s) [attempted 5276/8459 = 62%, 76 KB/s], Decompressed: 5272 Downloaded: 5316 file(s) [attempted 5316/8459 = 62%, 142 KB/s], Decompressed: 5313 Downloaded: 5357 file(s) [attempted 5357/8459 = 63%, 161 KB/s], Decompressed: 5347 Downloaded: 5399 file(s) [attempted 5399/8459 = 63%, 88 KB/s], Decompressed: 5395 Downloaded: 5436 file(s) [attempted 5436/8459 = 64%, 245 KB/s], Decompressed: 5433 Downloaded: 5474 file(s) [attempted 5474/8459 = 64%, 152 KB/s], Decompressed: 5470 Downloaded: 5515 file(s) [attempted 5515/8459 = 65%, 93 KB/s], Decompressed: 5512 Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 1287 KB/s], Decompressed: 5553 Downloaded: 5606 file(s) [attempted 5606/8459 = 66%, 478 KB/s], Decompressed: 5597 Downloaded: 5638 file(s) [attempted 5638/8459 = 66%, 48 KB/s], Decompressed: 5631 Downloaded: 5679 file(s) [attempted 5679/8459 = 67%, 596 KB/s], Decompressed: 5672 Downloaded: 5724 file(s) [attempted 5724/8459 = 67%, 156 KB/s], Decompressed: 5720 Downloaded: 5761 file(s) [attempted 5761/8459 = 68%, 1843 KB/s], Decompressed: 5758 Downloaded: 5799 file(s) [attempted 5799/8459 = 68%, 315 KB/s], Decompressed: 5792 Downloaded: 5837 file(s) [attempted 5837/8459 = 69%, 56 KB/s], Decompressed: 5830 Downloaded: 5874 file(s) [attempted 5874/8459 = 69%, 156 KB/s], Decompressed: 5871 Downloaded: 5912 file(s) [attempted 5912/8459 = 69%, 323 KB/s], Decompressed: 5898 Downloaded: 5953 file(s) [attempted 5953/8459 = 70%, 274 KB/s], Decompressed: 5936 Downloaded: 5980 file(s) [attempted 5980/8459 = 70%, 1581 KB/s], Decompressed: 5977 Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 27 KB/s], Decompressed: 6004 Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 159 KB/s], Decompressed: 6049 Downloaded: 6107 file(s) [attempted 6107/8459 = 72%, 307 KB/s], Decompressed: 6083 Downloaded: 6145 file(s) [attempted 6145/8459 = 72%, 1267 KB/s], Decompressed: 6138 Downloaded: 6179 file(s) [attempted 6179/8459 = 73%, 140 KB/s], Decompressed: 6172 Downloaded: 6217 file(s) [attempted 6217/8459 = 73%, 37 KB/s], Decompressed: 6206 Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 33 KB/s], Decompressed: 6251 Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 58 KB/s], Decompressed: 6288 Downloaded: 6333 file(s) [attempted 6333/8459 = 74%, 461 KB/s], Decompressed: 6326 Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 290 KB/s], Decompressed: 6357 Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 42 KB/s], Decompressed: 6401 Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 717 KB/s], Decompressed: 6446 Downloaded: 6487 file(s) [attempted 6487/8459 = 76%, 285 KB/s], Decompressed: 6483 Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 83 KB/s], Decompressed: 6507 Downloaded: 6572 file(s) [attempted 6572/8459 = 77%, 134 KB/s], Decompressed: 6507 Downloaded: 6607 file(s) [attempted 6607/8459 = 78%, 228 KB/s], Decompressed: 6518 Downloaded: 6644 file(s) [attempted 6644/8459 = 78%, 467 KB/s], Decompressed: 6637 Downloaded: 6682 file(s) [attempted 6682/8459 = 78%, 240 KB/s], Decompressed: 6679 Downloaded: 6723 file(s) [attempted 6723/8459 = 79%, 245 KB/s], Decompressed: 6689 Downloaded: 6761 file(s) [attempted 6761/8459 = 79%, 423 KB/s], Decompressed: 6696 Downloaded: 6798 file(s) [attempted 6798/8459 = 80%, 90 KB/s], Decompressed: 6781 Downloaded: 6836 file(s) [attempted 6836/8459 = 80%, 213 KB/s], Decompressed: 6826 Downloaded: 6870 file(s) [attempted 6870/8459 = 81%, 935 KB/s], Decompressed: 6863 Downloaded: 6911 file(s) [attempted 6911/8459 = 81%, 868 KB/s], Decompressed: 6898 Downloaded: 6952 file(s) [attempted 6952/8459 = 82%, 45 KB/s], Decompressed: 6942 Downloaded: 6983 file(s) [attempted 6983/8459 = 82%, 313 KB/s], Decompressed: 6976 Downloaded: 7024 file(s) [attempted 7024/8459 = 83%, 370 KB/s], Decompressed: 7017 Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 1205 KB/s], Decompressed: 7058 Downloaded: 7103 file(s) [attempted 7103/8459 = 83%, 167 KB/s], Decompressed: 7096 Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 108 KB/s], Decompressed: 7141 Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 39 KB/s], Decompressed: 7168 Downloaded: 7216 file(s) [attempted 7216/8459 = 85%, 600 KB/s], Decompressed: 7209 Downloaded: 7257 file(s) [attempted 7257/8459 = 85%, 37 KB/s], Decompressed: 7250 Downloaded: 7301 file(s) [attempted 7301/8459 = 86%, 46 KB/s], Decompressed: 7284 Downloaded: 7333 file(s) [attempted 7333/8459 = 86%, 384 KB/s], Decompressed: 7325 Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 526 KB/s], Decompressed: 7363 Downloaded: 7418 file(s) [attempted 7418/8459 = 87%, 372 KB/s], Decompressed: 7401 Downloaded: 7459 file(s) [attempted 7459/8459 = 88%, 86 KB/s], Decompressed: 7442 Downloaded: 7497 file(s) [attempted 7497/8459 = 88%, 95 KB/s], Decompressed: 7473 Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 2418 KB/s], Decompressed: 7527 Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 251 KB/s], Decompressed: 7565 Downloaded: 7616 file(s) [attempted 7616/8459 = 90%, 33 KB/s], Decompressed: 7609 Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 192 KB/s], Decompressed: 7630 Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 355 KB/s], Decompressed: 7688 Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 27 KB/s], Decompressed: 7729 Downloaded: 7777 file(s) [attempted 7777/8459 = 91%, 1587 KB/s], Decompressed: 7757 Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 22 KB/s], Decompressed: 7814 Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 2221 KB/s], Decompressed: 7835 Downloaded: 7883 file(s) [attempted 7883/8459 = 93%, 89 KB/s], Decompressed: 7876 Downloaded: 7928 file(s) [attempted 7928/8459 = 93%, 85 KB/s], Decompressed: 7900 Downloaded: 7972 file(s) [attempted 7972/8459 = 94%, 633 KB/s], Decompressed: 7952 Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 123 KB/s], Decompressed: 8000 Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 382 KB/s], Decompressed: 8034 Downloaded: 8082 file(s) [attempted 8082/8459 = 95%, 35 KB/s], Decompressed: 8071 Downloaded: 8123 file(s) [attempted 8123/8459 = 96%, 36 KB/s], Decompressed: 8116 Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 718 KB/s], Decompressed: 8164 Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 95 KB/s], Decompressed: 8198 Downloaded: 8246 file(s) [attempted 8246/8459 = 97%, 794 KB/s], Decompressed: 8243 Downloaded: 8294 file(s) [attempted 8294/8459 = 98%, 418 KB/s], Decompressed: 8290 Downloaded: 8332 file(s) [attempted 8332/8459 = 98%, 86 KB/s], Decompressed: 8314 Downloaded: 8369 file(s) [attempted 8369/8459 = 98%, 282 KB/s], Decompressed: 8366 Downloaded: 8414 file(s) [attempted 8414/8459 = 99%, 108 KB/s], Decompressed: 8410 Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 88 KB/s], Decompressed: 8444 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 88 KB/s], Decompressed: 8451
lean_checker exit 0
lake build
✔ [3401/3416] Built Iut.Stage1.IUTStage1SourceCore (117s) ✔ [3402/3416] Built Iut.Stage1.IUTStage1Remark312Absorption (78s) ✔ [3403/3416] Built Iut.Stage1.IUTStage1IUTIVAlgebra (12s) ✔ [3404/3416] Built Iut.Stage1.IUTStage1FiniteLabels (5.3s) ✔ [3405/3416] Built Iut.Stage1.IUTStage1StepX (6.3s) ✔ [3406/3416] Built Iut.Stage1.IUTStage1Gaussian (12s) ✔ [3407/3416] Built Iut.Stage1.IUTStage1HodgeSHE (7.4s) ✔ [3408/3416] Built Iut.Stage1.IUTStage1Theorem311 (5.4s) ✔ [3409/3416] Built Iut.Stage1.IUTStage1StepXI (20s) ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (294s) 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) [0x76f1aa1c6785] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x76f1aa1bdb27] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x76f1aa1bdc0b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x76f1aa0f3c62] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x76f1aa0f4439] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x76f1aa1caf99] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x76f1aa032923] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x76f1aa032b2b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x76f1aa033827] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x76f1aa0341b6] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x76f1aa1c9e8b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x76f1a9e15adb] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x76f1aa1c9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x76f1aa1c9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x76f1aa19b1f3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x76f1a9e15c92] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x76f1a5222638] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x76f1a500cd2e] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x76f1a4b69a82] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x76f1a4b69f0e] /lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x76f1a1a4524a] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x76f1a1a45305] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x611bdb3aa8da] ✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (66s) ✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (4.8s) ✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (40s) ✔ [3414/3416] Built Iut.Basic (4.6s) ✔ [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":2,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":12414,"diagnostic_count":4073,"duration_ms":6109855,"ok":true,"phase":"lean_declaration_extraction","target_module_count":7}
apx-semantic-phase {"declaration_count":12414,"dependency_count":134748,"diagnostic_count":162009,"duration_ms":1,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":3619803,"module_count":7,"ok":true,"phase":"lean_module_facts","target_module_count":7}
apx-semantic-phase {"declaration_count":12414,"dependency_count":134748,"diagnostic_count":162009,"duration_ms":22624,"module_count":7,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":3,"ok":true,"payload_bytes":577784048,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1328,"ok":true,"payload_bytes":577784048,"phase":"lean_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":3872}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":330,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":12,"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":27591,"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 934c2d5fe742db50b032ee84cc1b98d2eddf9a599ce8c047d7d565a76c70361c
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":9823041,"ok":true}