Login

Verification run

Run 348

promachina/iut-lean branch master triggered via github_backfill
succeeded commit b110bf270c4b toolchain lean-v4-30-0 prover lean took 4h 25m · finished 4w ago
Open project

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


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


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


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

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 b110bf2 Reduce valuation unit ball transport payload

Resolved source revision: b110bf270c4bd71585cbb11b610c329e80681f46

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=b110bf270c4bd71585cbb11b610c329e80681f46 provenance={"branch":"master","checked_out_revision":"b110bf270c4bd71585cbb11b610c329e80681f46","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"none","local_clone":false,"requested_commit_sha":"b110bf270c4bd71585cbb11b610c329e80681f46","used_missing_commit_fetch":true}
Resolved toolchain: lean-v4-30-0 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
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: 16/31 module hit(s), 15 miss(es)
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00000
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00001
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00002
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00003
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00004
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00005
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00006
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00007
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00008
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00009
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00010
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00011
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00012
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00013
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00014
Lean semantic module cache: extracted 15 missing module(s) in bounded batches; wrote merged semantic response

$ lake exe cache get
exit_code=Some(0) duration_ms=46501
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%, 14 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 4 KB/s], Decompressed: 14
Downloaded: 36 file(s) [attempted 36/8459 = 0%, 28 KB/s], Decompressed: 34
Downloaded: 64 file(s) [attempted 64/8459 = 0%, 300 KB/s], Decompressed: 62
Downloaded: 93 file(s) [attempted 93/8459 = 1%, 731 KB/s], Decompressed: 90
Downloaded: 127 file(s) [attempted 127/8459 = 1%, 400 KB/s], Decompressed: 124
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 359 KB/s], Decompressed: 155
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 160 KB/s], Decompressed: 196
Downloaded: 244 file(s) [attempted 244/8459 = 2%, 26 KB/s], Decompressed: 240
Downloaded: 282 file(s) [attempted 282/8459 = 3%, 315 KB/s], Decompressed: 271
Downloaded: 316 file(s) [attempted 316/8459 = 3%, 155 KB/s], Decompressed: 312
Downloaded: 357 file(s) [attempted 357/8459 = 4%, 217 KB/s], Decompressed: 350
Downloaded: 395 file(s) [attempted 395/8459 = 4%, 125 KB/s], Decompressed: 391
Downloaded: 443 file(s) [attempted 443/8459 = 5%, 530 KB/s], Decompressed: 439
Downloaded: 487 file(s) [attempted 487/8459 = 5%, 1505 KB/s], Decompressed: 480
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 185 KB/s], Decompressed: 525
Downloaded: 562 file(s) [attempted 562/8459 = 6%, 581 KB/s], Decompressed: 556
Downloaded: 603 file(s) [attempted 603/8459 = 7%, 165 KB/s], Decompressed: 600
Downloaded: 645 file(s) [attempted 645/8459 = 7%, 185 KB/s], Decompressed: 641
Downloaded: 689 file(s) [attempted 689/8459 = 8%, 157 KB/s], Decompressed: 686
Downloaded: 734 file(s) [attempted 734/8459 = 8%, 782 KB/s], Decompressed: 730
Downloaded: 775 file(s) [attempted 775/8459 = 9%, 1863 KB/s], Decompressed: 771
Downloaded: 816 file(s) [attempted 816/8459 = 9%, 93 KB/s], Decompressed: 812
Downloaded: 860 file(s) [attempted 860/8459 = 10%, 158 KB/s], Decompressed: 854
Downloaded: 898 file(s) [attempted 898/8459 = 10%, 85 KB/s], Decompressed: 891
Downloaded: 939 file(s) [attempted 939/8459 = 11%, 262 KB/s], Decompressed: 922
Downloaded: 975 file(s) [attempted 975/8459 = 11%, 542 KB/s], Decompressed: 963
Downloaded: 1011 file(s) [attempted 1011/8459 = 11%, 174 KB/s], Decompressed: 1008
Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 149 KB/s], Decompressed: 1053
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 1780 KB/s], Decompressed: 1100
Downloaded: 1158 file(s) [attempted 1158/8459 = 13%, 458 KB/s], Decompressed: 1151
Downloaded: 1203 file(s) [attempted 1203/8459 = 14%, 185 KB/s], Decompressed: 1199
Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 1125 KB/s], Decompressed: 1234
Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 94 KB/s], Decompressed: 1271
Downloaded: 1319 file(s) [attempted 1319/8459 = 15%, 135 KB/s], Decompressed: 1316
Downloaded: 1360 file(s) [attempted 1360/8459 = 16%, 142 KB/s], Decompressed: 1357
Downloaded: 1405 file(s) [attempted 1405/8459 = 16%, 138 KB/s], Decompressed: 1401
Downloaded: 1446 file(s) [attempted 1446/8459 = 17%, 1112 KB/s], Decompressed: 1439
Downloaded: 1487 file(s) [attempted 1487/8459 = 17%, 411 KB/s], Decompressed: 1483
Downloaded: 1528 file(s) [attempted 1528/8459 = 18%, 336 KB/s], Decompressed: 1514
Downloaded: 1569 file(s) [attempted 1569/8459 = 18%, 118 KB/s], Decompressed: 1559
Downloaded: 1607 file(s) [attempted 1607/8459 = 18%, 34 KB/s], Decompressed: 1603
Downloaded: 1648 file(s) [attempted 1648/8459 = 19%, 157 KB/s], Decompressed: 1641
Downloaded: 1689 file(s) [attempted 1689/8459 = 19%, 304 KB/s], Decompressed: 1678
Downloaded: 1730 file(s) [attempted 1730/8459 = 20%, 258 KB/s], Decompressed: 1726
Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 85 KB/s], Decompressed: 1764
Downloaded: 1810 file(s) [attempted 1810/8459 = 21%, 65 KB/s], Decompressed: 1805
Downloaded: 1853 file(s) [attempted 1853/8459 = 21%, 514 KB/s], Decompressed: 1846
Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 95 KB/s], Decompressed: 1880
Downloaded: 1932 file(s) [attempted 1932/8459 = 22%, 718 KB/s], Decompressed: 1928
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 116 KB/s], Decompressed: 1963
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 138 KB/s], Decompressed: 2007
Downloaded: 2055 file(s) [attempted 2055/8459 = 24%, 93 KB/s], Decompressed: 2048
Downloaded: 2096 file(s) [attempted 2096/8459 = 24%, 69 KB/s], Decompressed: 2093
Downloaded: 2134 file(s) [attempted 2134/8459 = 25%, 104 KB/s], Decompressed: 2130
Downloaded: 2175 file(s) [attempted 2175/8459 = 25%, 1285 KB/s], Decompressed: 2164
Downloaded: 2216 file(s) [attempted 2216/8459 = 26%, 376 KB/s], Decompressed: 2212
Downloaded: 2260 file(s) [attempted 2260/8459 = 26%, 334 KB/s], Decompressed: 2253
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 297 KB/s], Decompressed: 2294
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 112 KB/s], Decompressed: 2339
Downloaded: 2383 file(s) [attempted 2383/8459 = 28%, 666 KB/s], Decompressed: 2380
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 938 KB/s], Decompressed: 2414
Downloaded: 2462 file(s) [attempted 2462/8459 = 29%, 344 KB/s], Decompressed: 2459
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 179 KB/s], Decompressed: 2500
Downloaded: 2544 file(s) [attempted 2544/8459 = 30%, 96 KB/s], Decompressed: 2537
Downloaded: 2585 file(s) [attempted 2585/8459 = 30%, 237 KB/s], Decompressed: 2579
Downloaded: 2623 file(s) [attempted 2623/8459 = 31%, 518 KB/s], Decompressed: 2620
Downloaded: 2668 file(s) [attempted 2668/8459 = 31%, 180 KB/s], Decompressed: 2661
Downloaded: 2712 file(s) [attempted 2712/8459 = 32%, 336 KB/s], Decompressed: 2709
Downloaded: 2753 file(s) [attempted 2753/8459 = 32%, 199 KB/s], Decompressed: 2746
Downloaded: 2791 file(s) [attempted 2791/8459 = 32%, 116 KB/s], Decompressed: 2787
Downloaded: 2830 file(s) [attempted 2830/8459 = 33%, 1724 KB/s], Decompressed: 2822
Downloaded: 2873 file(s) [attempted 2873/8459 = 33%, 1063 KB/s], Decompressed: 2869
Downloaded: 2914 file(s) [attempted 2914/8459 = 34%, 268 KB/s], Decompressed: 2900
Downloaded: 2952 file(s) [attempted 2952/8459 = 34%, 206 KB/s], Decompressed: 2948
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 186 KB/s], Decompressed: 2994
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 116 KB/s], Decompressed: 3030
Downloaded: 3075 file(s) [attempted 3075/8459 = 36%, 831 KB/s], Decompressed: 3068
Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 171 KB/s], Decompressed: 3112
Downloaded: 3156 file(s) [attempted 3156/8459 = 37%, 192 KB/s], Decompressed: 3147
Downloaded: 3196 file(s) [attempted 3196/8459 = 37%, 294 KB/s], Decompressed: 3192
Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 215 KB/s], Decompressed: 3232
Downloaded: 3277 file(s) [attempted 3277/8459 = 38%, 263 KB/s], Decompressed: 3273
Downloaded: 3314 file(s) [attempted 3314/8459 = 39%, 282 KB/s], Decompressed: 3311
Downloaded: 3352 file(s) [attempted 3352/8459 = 39%, 56 KB/s], Decompressed: 3349
Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 49 KB/s], Decompressed: 3393
Downloaded: 3438 file(s) [attempted 3438/8459 = 40%, 200 KB/s], Decompressed: 3434
Downloaded: 3479 file(s) [attempted 3479/8459 = 41%, 638 KB/s], Decompressed: 3472
Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 101 KB/s], Decompressed: 3509
Downloaded: 3559 file(s) [attempted 3559/8459 = 42%, 86 KB/s], Decompressed: 3550
Downloaded: 3598 file(s) [attempted 3598/8459 = 42%, 210 KB/s], Decompressed: 3595
Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 197 KB/s], Decompressed: 3633
Downloaded: 3684 file(s) [attempted 3684/8459 = 43%, 352 KB/s], Decompressed: 3677
Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 288 KB/s], Decompressed: 3711
Downloaded: 3763 file(s) [attempted 3763/8459 = 44%, 576 KB/s], Decompressed: 3758
Downloaded: 3804 file(s) [attempted 3804/8459 = 44%, 57 KB/s], Decompressed: 3800
Downloaded: 3845 file(s) [attempted 3845/8459 = 45%, 459 KB/s], Decompressed: 3835
Downloaded: 3882 file(s) [attempted 3882/8459 = 45%, 104 KB/s], Decompressed: 3879
Downloaded: 3920 file(s) [attempted 3920/8459 = 46%, 357 KB/s], Decompressed: 3917
Downloaded: 3961 file(s) [attempted 3961/8459 = 46%, 289 KB/s], Decompressed: 3958
Downloaded: 4006 file(s) [attempted 4006/8459 = 47%, 303 KB/s], Decompressed: 4004
Downloaded: 4051 file(s) [attempted 4051/8459 = 47%, 563 KB/s], Decompressed: 4045
Downloaded: 4084 file(s) [attempted 4084/8459 = 48%, 244 KB/s], Decompressed: 4078
Downloaded: 4125 file(s) [attempted 4125/8459 = 48%, 95 KB/s], Decompressed: 4115
Downloaded: 4163 file(s) [attempted 4163/8459 = 49%, 174 KB/s], Decompressed: 4160
Downloaded: 4208 file(s) [attempted 4208/8459 = 49%, 184 KB/s], Decompressed: 4204
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 190 KB/s], Decompressed: 4245
Downloaded: 4295 file(s) [attempted 4295/8459 = 50%, 286 KB/s], Decompressed: 4286
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 197 KB/s], Decompressed: 4320
Downloaded: 4368 file(s) [attempted 4368/8459 = 51%, 425 KB/s], Decompressed: 4362
Downloaded: 4409 file(s) [attempted 4409/8459 = 52%, 77 KB/s], Decompressed: 4403
Downloaded: 4449 file(s) [attempted 4449/8459 = 52%, 193 KB/s], Decompressed: 4444
Downloaded: 4492 file(s) [attempted 4492/8459 = 53%, 252 KB/s], Decompressed: 4490
Downloaded: 4529 file(s) [attempted 4529/8459 = 53%, 58 KB/s], Decompressed: 4526
Downloaded: 4574 file(s) [attempted 4574/8459 = 54%, 246 KB/s], Decompressed: 4567
Downloaded: 4619 file(s) [attempted 4619/8459 = 54%, 725 KB/s], Decompressed: 4611
Downloaded: 4659 file(s) [attempted 4659/8459 = 55%, 35 KB/s], Decompressed: 4656
Downloaded: 4702 file(s) [attempted 4702/8459 = 55%, 235 KB/s], Decompressed: 4694
Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 246 KB/s], Decompressed: 4731
Downloaded: 4779 file(s) [attempted 4779/8459 = 56%, 148 KB/s], Decompressed: 4772
Downloaded: 4824 file(s) [attempted 4824/8459 = 57%, 286 KB/s], Decompressed: 4820
Downloaded: 4868 file(s) [attempted 4868/8459 = 57%, 189 KB/s], Decompressed: 4865
Downloaded: 4910 file(s) [attempted 4910/8459 = 58%, 211 KB/s], Decompressed: 4902
Downloaded: 4954 file(s) [attempted 4954/8459 = 58%, 142 KB/s], Decompressed: 4947
Downloaded: 4991 file(s) [attempted 4991/8459 = 59%, 51 KB/s], Decompressed: 4984
Downloaded: 5032 file(s) [attempted 5032/8459 = 59%, 359 KB/s], Decompressed: 5029
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 524 KB/s], Decompressed: 5073
Downloaded: 5124 file(s) [attempted 5124/8459 = 60%, 111 KB/s], Decompressed: 5118
Downloaded: 5163 file(s) [attempted 5163/8459 = 61%, 101 KB/s], Decompressed: 5159
Downloaded: 5203 file(s) [attempted 5203/8459 = 61%, 25 KB/s], Decompressed: 5200
Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 242 KB/s], Decompressed: 5241
Downloaded: 5289 file(s) [attempted 5289/8459 = 62%, 135 KB/s], Decompressed: 5286
Downloaded: 5330 file(s) [attempted 5330/8459 = 63%, 522 KB/s], Decompressed: 5323
Downloaded: 5368 file(s) [attempted 5368/8459 = 63%, 177 KB/s], Decompressed: 5364
Downloaded: 5409 file(s) [attempted 5409/8459 = 63%, 508 KB/s], Decompressed: 5405
Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 347 KB/s], Decompressed: 5450
Downloaded: 5491 file(s) [attempted 5491/8459 = 64%, 193 KB/s], Decompressed: 5488
Downloaded: 5535 file(s) [attempted 5535/8459 = 65%, 601 KB/s], Decompressed: 5525
Downloaded: 5577 file(s) [attempted 5577/8459 = 65%, 41 KB/s], Decompressed: 5570
Downloaded: 5618 file(s) [attempted 5618/8459 = 66%, 352 KB/s], Decompressed: 5611
Downloaded: 5659 file(s) [attempted 5659/8459 = 66%, 201 KB/s], Decompressed: 5648
Downloaded: 5693 file(s) [attempted 5693/8459 = 67%, 128 KB/s], Decompressed: 5689
Downloaded: 5737 file(s) [attempted 5737/8459 = 67%, 106 KB/s], Decompressed: 5734
Downloaded: 5778 file(s) [attempted 5778/8459 = 68%, 63 KB/s], Decompressed: 5775
Downloaded: 5819 file(s) [attempted 5819/8459 = 68%, 111 KB/s], Decompressed: 5816
Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 333 KB/s], Decompressed: 5857
Downloaded: 5902 file(s) [attempted 5902/8459 = 69%, 47 KB/s], Decompressed: 5898
Downloaded: 5943 file(s) [attempted 5943/8459 = 70%, 690 KB/s], Decompressed: 5939
Downloaded: 5981 file(s) [attempted 5981/8459 = 70%, 1547 KB/s], Decompressed: 5977
Downloaded: 6021 file(s) [attempted 6021/8459 = 71%, 65 KB/s], Decompressed: 6015
Downloaded: 6066 file(s) [attempted 6066/8459 = 71%, 1022 KB/s], Decompressed: 6059
Downloaded: 6104 file(s) [attempted 6104/8459 = 72%, 340 KB/s], Decompressed: 6100
Downloaded: 6148 file(s) [attempted 6148/8459 = 72%, 837 KB/s], Decompressed: 6145
Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 210 KB/s], Decompressed: 6182
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 1048 KB/s], Decompressed: 6223
Downloaded: 6273 file(s) [attempted 6273/8459 = 74%, 49 KB/s], Decompressed: 6264
Downloaded: 6309 file(s) [attempted 6309/8459 = 74%, 1199 KB/s], Decompressed: 6302
Downloaded: 6347 file(s) [attempted 6347/8459 = 75%, 835 KB/s], Decompressed: 6343
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 417 KB/s], Decompressed: 6384
Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 71 KB/s], Decompressed: 6429
Downloaded: 6477 file(s) [attempted 6477/8459 = 76%, 245 KB/s], Decompressed: 6473
Downloaded: 6514 file(s) [attempted 6514/8459 = 77%, 145 KB/s], Decompressed: 6507
Downloaded: 6555 file(s) [attempted 6555/8459 = 77%, 529 KB/s], Decompressed: 6552
Downloaded: 6594 file(s) [attempted 6594/8459 = 77%, 387 KB/s], Decompressed: 6589
Downloaded: 6637 file(s) [attempted 6637/8459 = 78%, 1152 KB/s], Decompressed: 6634
Downloaded: 6682 file(s) [attempted 6682/8459 = 78%, 99 KB/s], Decompressed: 6678
Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 259 KB/s], Decompressed: 6716
Downloaded: 6764 file(s) [attempted 6764/8459 = 79%, 148 KB/s], Decompressed: 6761
Downloaded: 6802 file(s) [attempted 6802/8459 = 80%, 150 KB/s], Decompressed: 6795
Downloaded: 6840 file(s) [attempted 6840/8459 = 80%, 220 KB/s], Decompressed: 6836
Downloaded: 6887 file(s) [attempted 6887/8459 = 81%, 183 KB/s], Decompressed: 6884
Downloaded: 6932 file(s) [attempted 6932/8459 = 81%, 193 KB/s], Decompressed: 6928
Downloaded: 6970 file(s) [attempted 6970/8459 = 82%, 30 KB/s], Decompressed: 6966
Downloaded: 7011 file(s) [attempted 7011/8459 = 82%, 462 KB/s], Decompressed: 7004
Downloaded: 7045 file(s) [attempted 7045/8459 = 83%, 1921 KB/s], Decompressed: 7041
Downloaded: 7090 file(s) [attempted 7090/8459 = 83%, 309 KB/s], Decompressed: 7086
Downloaded: 7130 file(s) [attempted 7130/8459 = 84%, 1021 KB/s], Decompressed: 7123
Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 38 KB/s], Decompressed: 7168
Downloaded: 7215 file(s) [attempted 7215/8459 = 85%, 684 KB/s], Decompressed: 7206
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 70 KB/s], Decompressed: 7247
Downloaded: 7294 file(s) [attempted 7294/8459 = 86%, 107 KB/s], Decompressed: 7288
Downloaded: 7336 file(s) [attempted 7336/8459 = 86%, 387 KB/s], Decompressed: 7332
Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 43 KB/s], Decompressed: 7373
Downloaded: 7418 file(s) [attempted 7418/8459 = 87%, 320 KB/s], Decompressed: 7411
Downloaded: 7459 file(s) [attempted 7459/8459 = 88%, 88 KB/s], Decompressed: 7452
Downloaded: 7496 file(s) [attempted 7496/8459 = 88%, 28 KB/s], Decompressed: 7493
Downloaded: 7541 file(s) [attempted 7541/8459 = 89%, 162 KB/s], Decompressed: 7537
Downloaded: 7585 file(s) [attempted 7585/8459 = 89%, 88 KB/s], Decompressed: 7582
Downloaded: 7626 file(s) [attempted 7626/8459 = 90%, 1044 KB/s], Decompressed: 7623
Downloaded: 7666 file(s) [attempted 7666/8459 = 90%, 203 KB/s], Decompressed: 7661
Downloaded: 7704 file(s) [attempted 7704/8459 = 91%, 1082 KB/s], Decompressed: 7698
Downloaded: 7746 file(s) [attempted 7746/8459 = 91%, 185 KB/s], Decompressed: 7743
Downloaded: 7792 file(s) [attempted 7792/8459 = 92%, 41 KB/s], Decompressed: 7784
Downloaded: 7832 file(s) [attempted 7832/8459 = 92%, 333 KB/s], Decompressed: 7828
Downloaded: 7873 file(s) [attempted 7873/8459 = 93%, 395 KB/s], Decompressed: 7869
Downloaded: 7914 file(s) [attempted 7914/8459 = 93%, 100 KB/s], Decompressed: 7907
Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 793 KB/s], Decompressed: 7945
Downloaded: 7989 file(s) [attempted 7989/8459 = 94%, 1637 KB/s], Decompressed: 7986
Downloaded: 8034 file(s) [attempted 8034/8459 = 94%, 453 KB/s], Decompressed: 8030
Downloaded: 8073 file(s) [attempted 8073/8459 = 95%, 242 KB/s], Decompressed: 8062
Downloaded: 8109 file(s) [attempted 8109/8459 = 95%, 160 KB/s], Decompressed: 8098
Downloaded: 8150 file(s) [attempted 8150/8459 = 96%, 66 KB/s], Decompressed: 8143
Downloaded: 8191 file(s) [attempted 8191/8459 = 96%, 37 KB/s], Decompressed: 8188
Downloaded: 8232 file(s) [attempted 8232/8459 = 97%, 516 KB/s], Decompressed: 8225
Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 718 KB/s], Decompressed: 8273
Downloaded: 8330 file(s) [attempted 8330/8459 = 98%, 537 KB/s], Decompressed: 8314
Downloaded: 8366 file(s) [attempted 8366/8459 = 98%, 205 KB/s], Decompressed: 8359
Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 65 KB/s], Decompressed: 8396
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 498 KB/s], Decompressed: 8438
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 498 KB/s], Decompressed: 8451


$ lake build
exit_code=Some(0) duration_ms=400760
stdout:
✔ [1/14] Built Iut.Foundations.Species (667ms)
✔ [753/764] Built Iut.Foundations.RealLineCopy (16s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.6s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/772] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3382/3392] Built Iut.Foundations.AlgorithmicOutput (1.6s)
✔ [3384/3393] Built Iut.Stage1.PilotComparison (1.6s)
✔ [3385/3393] Built Iut.Foundations.AlgorithmicBridge (2.6s)
✔ [3388/3393] Built Iut.Stage1.CorollarySchema (33s)
✔ [3389/3398] Built Iut.Foundations.InitialThetaData (23s)
✔ [3390/3398] Built Iut.Stage1.SourceObligations (3.2s)
✔ [3392/3415] Built Iut.Stage1.IUTSourceScaffold (2.6s)
✔ [3395/3416] Built Iut.Stage1.IUTStage1Data (3.1s)
✔ [3401/3416] Built Iut.Stage1.IUTStage1SourceCore (33s)
✔ [3402/3416] Built Iut.Stage1.IUTStage1Remark312Absorption (2.9s)
✔ [3403/3416] Built Iut.Stage1.IUTStage1IUTIVAlgebra (9.9s)
✔ [3404/3416] Built Iut.Stage1.IUTStage1FiniteLabels (4.4s)
✔ [3405/3416] Built Iut.Stage1.IUTStage1StepX (5.1s)
✔ [3406/3416] Built Iut.Stage1.IUTStage1Gaussian (9.2s)
✔ [3407/3416] Built Iut.Stage1.IUTStage1HodgeSHE (5.4s)
✔ [3408/3416] Built Iut.Stage1.IUTStage1Theorem311 (4.8s)
✔ [3409/3416] Built Iut.Stage1.IUTStage1StepXI (17s)
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (130s)
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) [0x73ff11dc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x73ff11dbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x73ff11dbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x73ff11cf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x73ff11cf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x73ff11dcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x73ff11c32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x73ff11c32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x73ff11c33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x73ff11c341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x73ff11dc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x73ff11a15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73ff11dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73ff11dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x73ff11d9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x73ff11a15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x73ff0ce22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x73ff0cc0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x73ff0c769a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x73ff0c769f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x73ff0964524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x73ff09645305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x63034e99c8da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (4.0s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.1s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (36s)
✔ [3414/3416] Built Iut.Basic (2.4s)
✔ [3415/3416] Built Iut (2.3s)
Build completed successfully (3416 jobs).

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


$ lake build :blueprint
exit_code=Some(1) duration_ms=1789
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=2010715
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 2ac9cf74b29e38ccaba829a5368016604647e7e0b1c1509cac0a741ae794a888
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


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


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


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


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


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


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


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


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


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


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


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


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


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


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

Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

git_clone exit 0 duration 5s · created 
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-437-source
Cloning into '/var/lib/apodeixis/repos/job-437-source'...
git_checkout exit 128 duration 1 ms · created 
git checkout b110bf270c4bd71585cbb11b610c329e80681f46
fatal: reference is not a tree: b110bf270c4bd71585cbb11b610c329e80681f46
git_checkout exit 0 duration 1s · created 
git fetch --depth 1 origin b110bf270c4bd71585cbb11b610c329e80681f46
From https://github.com/promachina/iut-lean
 * branch            b110bf270c4bd71585cbb11b610c329e80681f46 -> FETCH_HEAD
git_checkout exit 0 duration 145 ms · created 
git checkout b110bf270c4bd71585cbb11b610c329e80681f46 (after fetch)
Note: switching to 'b110bf270c4bd71585cbb11b610c329e80681f46'.

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 b110bf2 Reduce valuation unit ball transport payload
lake_cache exit 0 duration 47s · created 
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%, 14 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 4 KB/s], Decompressed: 14
Downloaded: 36 file(s) [attempted 36/8459 = 0%, 28 KB/s], Decompressed: 34
Downloaded: 64 file(s) [attempted 64/8459 = 0%, 300 KB/s], Decompressed: 62
Downloaded: 93 file(s) [attempted 93/8459 = 1%, 731 KB/s], Decompressed: 90
Downloaded: 127 file(s) [attempted 127/8459 = 1%, 400 KB/s], Decompressed: 124
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 359 KB/s], Decompressed: 155
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 160 KB/s], Decompressed: 196
Downloaded: 244 file(s) [attempted 244/8459 = 2%, 26 KB/s], Decompressed: 240
Downloaded: 282 file(s) [attempted 282/8459 = 3%, 315 KB/s], Decompressed: 271
Downloaded: 316 file(s) [attempted 316/8459 = 3%, 155 KB/s], Decompressed: 312
Downloaded: 357 file(s) [attempted 357/8459 = 4%, 217 KB/s], Decompressed: 350
Downloaded: 395 file(s) [attempted 395/8459 = 4%, 125 KB/s], Decompressed: 391
Downloaded: 443 file(s) [attempted 443/8459 = 5%, 530 KB/s], Decompressed: 439
Downloaded: 487 file(s) [attempted 487/8459 = 5%, 1505 KB/s], Decompressed: 480
Downloaded: 528 file(s) [attempted 528/8459 = 6%, 185 KB/s], Decompressed: 525
Downloaded: 562 file(s) [attempted 562/8459 = 6%, 581 KB/s], Decompressed: 556
Downloaded: 603 file(s) [attempted 603/8459 = 7%, 165 KB/s], Decompressed: 600
Downloaded: 645 file(s) [attempted 645/8459 = 7%, 185 KB/s], Decompressed: 641
Downloaded: 689 file(s) [attempted 689/8459 = 8%, 157 KB/s], Decompressed: 686
Downloaded: 734 file(s) [attempted 734/8459 = 8%, 782 KB/s], Decompressed: 730
Downloaded: 775 file(s) [attempted 775/8459 = 9%, 1863 KB/s], Decompressed: 771
Downloaded: 816 file(s) [attempted 816/8459 = 9%, 93 KB/s], Decompressed: 812
Downloaded: 860 file(s) [attempted 860/8459 = 10%, 158 KB/s], Decompressed: 854
Downloaded: 898 file(s) [attempted 898/8459 = 10%, 85 KB/s], Decompressed: 891
Downloaded: 939 file(s) [attempted 939/8459 = 11%, 262 KB/s], Decompressed: 922
Downloaded: 975 file(s) [attempted 975/8459 = 11%, 542 KB/s], Decompressed: 963
Downloaded: 1011 file(s) [attempted 1011/8459 = 11%, 174 KB/s], Decompressed: 1008
Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 149 KB/s], Decompressed: 1053
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 1780 KB/s], Decompressed: 1100
Downloaded: 1158 file(s) [attempted 1158/8459 = 13%, 458 KB/s], Decompressed: 1151
Downloaded: 1203 file(s) [attempted 1203/8459 = 14%, 185 KB/s], Decompressed: 1199
Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 1125 KB/s], Decompressed: 1234
Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 94 KB/s], Decompressed: 1271
Downloaded: 1319 file(s) [attempted 1319/8459 = 15%, 135 KB/s], Decompressed: 1316
Downloaded: 1360 file(s) [attempted 1360/8459 = 16%, 142 KB/s], Decompressed: 1357
Downloaded: 1405 file(s) [attempted 1405/8459 = 16%, 138 KB/s], Decompressed: 1401
Downloaded: 1446 file(s) [attempted 1446/8459 = 17%, 1112 KB/s], Decompressed: 1439
Downloaded: 1487 file(s) [attempted 1487/8459 = 17%, 411 KB/s], Decompressed: 1483
Downloaded: 1528 file(s) [attempted 1528/8459 = 18%, 336 KB/s], Decompressed: 1514
Downloaded: 1569 file(s) [attempted 1569/8459 = 18%, 118 KB/s], Decompressed: 1559
Downloaded: 1607 file(s) [attempted 1607/8459 = 18%, 34 KB/s], Decompressed: 1603
Downloaded: 1648 file(s) [attempted 1648/8459 = 19%, 157 KB/s], Decompressed: 1641
Downloaded: 1689 file(s) [attempted 1689/8459 = 19%, 304 KB/s], Decompressed: 1678
Downloaded: 1730 file(s) [attempted 1730/8459 = 20%, 258 KB/s], Decompressed: 1726
Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 85 KB/s], Decompressed: 1764
Downloaded: 1810 file(s) [attempted 1810/8459 = 21%, 65 KB/s], Decompressed: 1805
Downloaded: 1853 file(s) [attempted 1853/8459 = 21%, 514 KB/s], Decompressed: 1846
Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 95 KB/s], Decompressed: 1880
Downloaded: 1932 file(s) [attempted 1932/8459 = 22%, 718 KB/s], Decompressed: 1928
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 116 KB/s], Decompressed: 1963
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 138 KB/s], Decompressed: 2007
Downloaded: 2055 file(s) [attempted 2055/8459 = 24%, 93 KB/s], Decompressed: 2048
Downloaded: 2096 file(s) [attempted 2096/8459 = 24%, 69 KB/s], Decompressed: 2093
Downloaded: 2134 file(s) [attempted 2134/8459 = 25%, 104 KB/s], Decompressed: 2130
Downloaded: 2175 file(s) [attempted 2175/8459 = 25%, 1285 KB/s], Decompressed: 2164
Downloaded: 2216 file(s) [attempted 2216/8459 = 26%, 376 KB/s], Decompressed: 2212
Downloaded: 2260 file(s) [attempted 2260/8459 = 26%, 334 KB/s], Decompressed: 2253
Downloaded: 2301 file(s) [attempted 2301/8459 = 27%, 297 KB/s], Decompressed: 2294
Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 112 KB/s], Decompressed: 2339
Downloaded: 2383 file(s) [attempted 2383/8459 = 28%, 666 KB/s], Decompressed: 2380
Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 938 KB/s], Decompressed: 2414
Downloaded: 2462 file(s) [attempted 2462/8459 = 29%, 344 KB/s], Decompressed: 2459
Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 179 KB/s], Decompressed: 2500
Downloaded: 2544 file(s) [attempted 2544/8459 = 30%, 96 KB/s], Decompressed: 2537
Downloaded: 2585 file(s) [attempted 2585/8459 = 30%, 237 KB/s], Decompressed: 2579
Downloaded: 2623 file(s) [attempted 2623/8459 = 31%, 518 KB/s], Decompressed: 2620
Downloaded: 2668 file(s) [attempted 2668/8459 = 31%, 180 KB/s], Decompressed: 2661
Downloaded: 2712 file(s) [attempted 2712/8459 = 32%, 336 KB/s], Decompressed: 2709
Downloaded: 2753 file(s) [attempted 2753/8459 = 32%, 199 KB/s], Decompressed: 2746
Downloaded: 2791 file(s) [attempted 2791/8459 = 32%, 116 KB/s], Decompressed: 2787
Downloaded: 2830 file(s) [attempted 2830/8459 = 33%, 1724 KB/s], Decompressed: 2822
Downloaded: 2873 file(s) [attempted 2873/8459 = 33%, 1063 KB/s], Decompressed: 2869
Downloaded: 2914 file(s) [attempted 2914/8459 = 34%, 268 KB/s], Decompressed: 2900
Downloaded: 2952 file(s) [attempted 2952/8459 = 34%, 206 KB/s], Decompressed: 2948
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 186 KB/s], Decompressed: 2994
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 116 KB/s], Decompressed: 3030
Downloaded: 3075 file(s) [attempted 3075/8459 = 36%, 831 KB/s], Decompressed: 3068
Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 171 KB/s], Decompressed: 3112
Downloaded: 3156 file(s) [attempted 3156/8459 = 37%, 192 KB/s], Decompressed: 3147
Downloaded: 3196 file(s) [attempted 3196/8459 = 37%, 294 KB/s], Decompressed: 3192
Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 215 KB/s], Decompressed: 3232
Downloaded: 3277 file(s) [attempted 3277/8459 = 38%, 263 KB/s], Decompressed: 3273
Downloaded: 3314 file(s) [attempted 3314/8459 = 39%, 282 KB/s], Decompressed: 3311
Downloaded: 3352 file(s) [attempted 3352/8459 = 39%, 56 KB/s], Decompressed: 3349
Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 49 KB/s], Decompressed: 3393
Downloaded: 3438 file(s) [attempted 3438/8459 = 40%, 200 KB/s], Decompressed: 3434
Downloaded: 3479 file(s) [attempted 3479/8459 = 41%, 638 KB/s], Decompressed: 3472
Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 101 KB/s], Decompressed: 3509
Downloaded: 3559 file(s) [attempted 3559/8459 = 42%, 86 KB/s], Decompressed: 3550
Downloaded: 3598 file(s) [attempted 3598/8459 = 42%, 210 KB/s], Decompressed: 3595
Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 197 KB/s], Decompressed: 3633
Downloaded: 3684 file(s) [attempted 3684/8459 = 43%, 352 KB/s], Decompressed: 3677
Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 288 KB/s], Decompressed: 3711
Downloaded: 3763 file(s) [attempted 3763/8459 = 44%, 576 KB/s], Decompressed: 3758
Downloaded: 3804 file(s) [attempted 3804/8459 = 44%, 57 KB/s], Decompressed: 3800
Downloaded: 3845 file(s) [attempted 3845/8459 = 45%, 459 KB/s], Decompressed: 3835
Downloaded: 3882 file(s) [attempted 3882/8459 = 45%, 104 KB/s], Decompressed: 3879
Downloaded: 3920 file(s) [attempted 3920/8459 = 46%, 357 KB/s], Decompressed: 3917
Downloaded: 3961 file(s) [attempted 3961/8459 = 46%, 289 KB/s], Decompressed: 3958
Downloaded: 4006 file(s) [attempted 4006/8459 = 47%, 303 KB/s], Decompressed: 4004
Downloaded: 4051 file(s) [attempted 4051/8459 = 47%, 563 KB/s], Decompressed: 4045
Downloaded: 4084 file(s) [attempted 4084/8459 = 48%, 244 KB/s], Decompressed: 4078
Downloaded: 4125 file(s) [attempted 4125/8459 = 48%, 95 KB/s], Decompressed: 4115
Downloaded: 4163 file(s) [attempted 4163/8459 = 49%, 174 KB/s], Decompressed: 4160
Downloaded: 4208 file(s) [attempted 4208/8459 = 49%, 184 KB/s], Decompressed: 4204
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 190 KB/s], Decompressed: 4245
Downloaded: 4295 file(s) [attempted 4295/8459 = 50%, 286 KB/s], Decompressed: 4286
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 197 KB/s], Decompressed: 4320
Downloaded: 4368 file(s) [attempted 4368/8459 = 51%, 425 KB/s], Decompressed: 4362
Downloaded: 4409 file(s) [attempted 4409/8459 = 52%, 77 KB/s], Decompressed: 4403
Downloaded: 4449 file(s) [attempted 4449/8459 = 52%, 193 KB/s], Decompressed: 4444
Downloaded: 4492 file(s) [attempted 4492/8459 = 53%, 252 KB/s], Decompressed: 4490
Downloaded: 4529 file(s) [attempted 4529/8459 = 53%, 58 KB/s], Decompressed: 4526
Downloaded: 4574 file(s) [attempted 4574/8459 = 54%, 246 KB/s], Decompressed: 4567
Downloaded: 4619 file(s) [attempted 4619/8459 = 54%, 725 KB/s], Decompressed: 4611
Downloaded: 4659 file(s) [attempted 4659/8459 = 55%, 35 KB/s], Decompressed: 4656
Downloaded: 4702 file(s) [attempted 4702/8459 = 55%, 235 KB/s], Decompressed: 4694
Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 246 KB/s], Decompressed: 4731
Downloaded: 4779 file(s) [attempted 4779/8459 = 56%, 148 KB/s], Decompressed: 4772
Downloaded: 4824 file(s) [attempted 4824/8459 = 57%, 286 KB/s], Decompressed: 4820
Downloaded: 4868 file(s) [attempted 4868/8459 = 57%, 189 KB/s], Decompressed: 4865
Downloaded: 4910 file(s) [attempted 4910/8459 = 58%, 211 KB/s], Decompressed: 4902
Downloaded: 4954 file(s) [attempted 4954/8459 = 58%, 142 KB/s], Decompressed: 4947
Downloaded: 4991 file(s) [attempted 4991/8459 = 59%, 51 KB/s], Decompressed: 4984
Downloaded: 5032 file(s) [attempted 5032/8459 = 59%, 359 KB/s], Decompressed: 5029
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 524 KB/s], Decompressed: 5073
Downloaded: 5124 file(s) [attempted 5124/8459 = 60%, 111 KB/s], Decompressed: 5118
Downloaded: 5163 file(s) [attempted 5163/8459 = 61%, 101 KB/s], Decompressed: 5159
Downloaded: 5203 file(s) [attempted 5203/8459 = 61%, 25 KB/s], Decompressed: 5200
Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 242 KB/s], Decompressed: 5241
Downloaded: 5289 file(s) [attempted 5289/8459 = 62%, 135 KB/s], Decompressed: 5286
Downloaded: 5330 file(s) [attempted 5330/8459 = 63%, 522 KB/s], Decompressed: 5323
Downloaded: 5368 file(s) [attempted 5368/8459 = 63%, 177 KB/s], Decompressed: 5364
Downloaded: 5409 file(s) [attempted 5409/8459 = 63%, 508 KB/s], Decompressed: 5405
Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 347 KB/s], Decompressed: 5450
Downloaded: 5491 file(s) [attempted 5491/8459 = 64%, 193 KB/s], Decompressed: 5488
Downloaded: 5535 file(s) [attempted 5535/8459 = 65%, 601 KB/s], Decompressed: 5525
Downloaded: 5577 file(s) [attempted 5577/8459 = 65%, 41 KB/s], Decompressed: 5570
Downloaded: 5618 file(s) [attempted 5618/8459 = 66%, 352 KB/s], Decompressed: 5611
Downloaded: 5659 file(s) [attempted 5659/8459 = 66%, 201 KB/s], Decompressed: 5648
Downloaded: 5693 file(s) [attempted 5693/8459 = 67%, 128 KB/s], Decompressed: 5689
Downloaded: 5737 file(s) [attempted 5737/8459 = 67%, 106 KB/s], Decompressed: 5734
Downloaded: 5778 file(s) [attempted 5778/8459 = 68%, 63 KB/s], Decompressed: 5775
Downloaded: 5819 file(s) [attempted 5819/8459 = 68%, 111 KB/s], Decompressed: 5816
Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 333 KB/s], Decompressed: 5857
Downloaded: 5902 file(s) [attempted 5902/8459 = 69%, 47 KB/s], Decompressed: 5898
Downloaded: 5943 file(s) [attempted 5943/8459 = 70%, 690 KB/s], Decompressed: 5939
Downloaded: 5981 file(s) [attempted 5981/8459 = 70%, 1547 KB/s], Decompressed: 5977
Downloaded: 6021 file(s) [attempted 6021/8459 = 71%, 65 KB/s], Decompressed: 6015
Downloaded: 6066 file(s) [attempted 6066/8459 = 71%, 1022 KB/s], Decompressed: 6059
Downloaded: 6104 file(s) [attempted 6104/8459 = 72%, 340 KB/s], Decompressed: 6100
Downloaded: 6148 file(s) [attempted 6148/8459 = 72%, 837 KB/s], Decompressed: 6145
Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 210 KB/s], Decompressed: 6182
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 1048 KB/s], Decompressed: 6223
Downloaded: 6273 file(s) [attempted 6273/8459 = 74%, 49 KB/s], Decompressed: 6264
Downloaded: 6309 file(s) [attempted 6309/8459 = 74%, 1199 KB/s], Decompressed: 6302
Downloaded: 6347 file(s) [attempted 6347/8459 = 75%, 835 KB/s], Decompressed: 6343
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 417 KB/s], Decompressed: 6384
Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 71 KB/s], Decompressed: 6429
Downloaded: 6477 file(s) [attempted 6477/8459 = 76%, 245 KB/s], Decompressed: 6473
Downloaded: 6514 file(s) [attempted 6514/8459 = 77%, 145 KB/s], Decompressed: 6507
Downloaded: 6555 file(s) [attempted 6555/8459 = 77%, 529 KB/s], Decompressed: 6552
Downloaded: 6594 file(s) [attempted 6594/8459 = 77%, 387 KB/s], Decompressed: 6589
Downloaded: 6637 file(s) [attempted 6637/8459 = 78%, 1152 KB/s], Decompressed: 6634
Downloaded: 6682 file(s) [attempted 6682/8459 = 78%, 99 KB/s], Decompressed: 6678
Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 259 KB/s], Decompressed: 6716
Downloaded: 6764 file(s) [attempted 6764/8459 = 79%, 148 KB/s], Decompressed: 6761
Downloaded: 6802 file(s) [attempted 6802/8459 = 80%, 150 KB/s], Decompressed: 6795
Downloaded: 6840 file(s) [attempted 6840/8459 = 80%, 220 KB/s], Decompressed: 6836
Downloaded: 6887 file(s) [attempted 6887/8459 = 81%, 183 KB/s], Decompressed: 6884
Downloaded: 6932 file(s) [attempted 6932/8459 = 81%, 193 KB/s], Decompressed: 6928
Downloaded: 6970 file(s) [attempted 6970/8459 = 82%, 30 KB/s], Decompressed: 6966
Downloaded: 7011 file(s) [attempted 7011/8459 = 82%, 462 KB/s], Decompressed: 7004
Downloaded: 7045 file(s) [attempted 7045/8459 = 83%, 1921 KB/s], Decompressed: 7041
Downloaded: 7090 file(s) [attempted 7090/8459 = 83%, 309 KB/s], Decompressed: 7086
Downloaded: 7130 file(s) [attempted 7130/8459 = 84%, 1021 KB/s], Decompressed: 7123
Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 38 KB/s], Decompressed: 7168
Downloaded: 7215 file(s) [attempted 7215/8459 = 85%, 684 KB/s], Decompressed: 7206
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 70 KB/s], Decompressed: 7247
Downloaded: 7294 file(s) [attempted 7294/8459 = 86%, 107 KB/s], Decompressed: 7288
Downloaded: 7336 file(s) [attempted 7336/8459 = 86%, 387 KB/s], Decompressed: 7332
Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 43 KB/s], Decompressed: 7373
Downloaded: 7418 file(s) [attempted 7418/8459 = 87%, 320 KB/s], Decompressed: 7411
Downloaded: 7459 file(s) [attempted 7459/8459 = 88%, 88 KB/s], Decompressed: 7452
Downloaded: 7496 file(s) [attempted 7496/8459 = 88%, 28 KB/s], Decompressed: 7493
Downloaded: 7541 file(s) [attempted 7541/8459 = 89%, 162 KB/s], Decompressed: 7537
Downloaded: 7585 file(s) [attempted 7585/8459 = 89%, 88 KB/s], Decompressed: 7582
Downloaded: 7626 file(s) [attempted 7626/8459 = 90%, 1044 KB/s], Decompressed: 7623
Downloaded: 7666 file(s) [attempted 7666/8459 = 90%, 203 KB/s], Decompressed: 7661
Downloaded: 7704 file(s) [attempted 7704/8459 = 91%, 1082 KB/s], Decompressed: 7698
Downloaded: 7746 file(s) [attempted 7746/8459 = 91%, 185 KB/s], Decompressed: 7743
Downloaded: 7792 file(s) [attempted 7792/8459 = 92%, 41 KB/s], Decompressed: 7784
Downloaded: 7832 file(s) [attempted 7832/8459 = 92%, 333 KB/s], Decompressed: 7828
Downloaded: 7873 file(s) [attempted 7873/8459 = 93%, 395 KB/s], Decompressed: 7869
Downloaded: 7914 file(s) [attempted 7914/8459 = 93%, 100 KB/s], Decompressed: 7907
Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 793 KB/s], Decompressed: 7945
Downloaded: 7989 file(s) [attempted 7989/8459 = 94%, 1637 KB/s], Decompressed: 7986
Downloaded: 8034 file(s) [attempted 8034/8459 = 94%, 453 KB/s], Decompressed: 8030
Downloaded: 8073 file(s) [attempted 8073/8459 = 95%, 242 KB/s], Decompressed: 8062
Downloaded: 8109 file(s) [attempted 8109/8459 = 95%, 160 KB/s], Decompressed: 8098
Downloaded: 8150 file(s) [attempted 8150/8459 = 96%, 66 KB/s], Decompressed: 8143
Downloaded: 8191 file(s) [attempted 8191/8459 = 96%, 37 KB/s], Decompressed: 8188
Downloaded: 8232 file(s) [attempted 8232/8459 = 97%, 516 KB/s], Decompressed: 8225
Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 718 KB/s], Decompressed: 8273
Downloaded: 8330 file(s) [attempted 8330/8459 = 98%, 537 KB/s], Decompressed: 8314
Downloaded: 8366 file(s) [attempted 8366/8459 = 98%, 205 KB/s], Decompressed: 8359
Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 65 KB/s], Decompressed: 8396
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 498 KB/s], Decompressed: 8438
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 498 KB/s], Decompressed: 8451
lean_checker exit 0 duration 6m 41s · created 
lake build
✔ [1/14] Built Iut.Foundations.Species (667ms)
✔ [753/764] Built Iut.Foundations.RealLineCopy (16s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.7s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.6s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/772] Built Iut.Foundations.QualitativeData (1.9s)
✔ [3382/3392] Built Iut.Foundations.AlgorithmicOutput (1.6s)
✔ [3384/3393] Built Iut.Stage1.PilotComparison (1.6s)
✔ [3385/3393] Built Iut.Foundations.AlgorithmicBridge (2.6s)
✔ [3388/3393] Built Iut.Stage1.CorollarySchema (33s)
✔ [3389/3398] Built Iut.Foundations.InitialThetaData (23s)
✔ [3390/3398] Built Iut.Stage1.SourceObligations (3.2s)
✔ [3392/3415] Built Iut.Stage1.IUTSourceScaffold (2.6s)
✔ [3395/3416] Built Iut.Stage1.IUTStage1Data (3.1s)
✔ [3401/3416] Built Iut.Stage1.IUTStage1SourceCore (33s)
✔ [3402/3416] Built Iut.Stage1.IUTStage1Remark312Absorption (2.9s)
✔ [3403/3416] Built Iut.Stage1.IUTStage1IUTIVAlgebra (9.9s)
✔ [3404/3416] Built Iut.Stage1.IUTStage1FiniteLabels (4.4s)
✔ [3405/3416] Built Iut.Stage1.IUTStage1StepX (5.1s)
✔ [3406/3416] Built Iut.Stage1.IUTStage1Gaussian (9.2s)
✔ [3407/3416] Built Iut.Stage1.IUTStage1HodgeSHE (5.4s)
✔ [3408/3416] Built Iut.Stage1.IUTStage1Theorem311 (4.8s)
✔ [3409/3416] Built Iut.Stage1.IUTStage1StepXI (17s)
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (130s)
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) [0x73ff11dc6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x73ff11dbdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x73ff11dbdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x73ff11cf3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x73ff11cf4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x73ff11dcaf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x73ff11c32923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x73ff11c32b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x73ff11c33827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x73ff11c341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x73ff11dc9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x73ff11a15adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73ff11dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x73ff11dc9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x73ff11d9b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x73ff11a15c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x73ff0ce22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x73ff0cc0cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x73ff0c769a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x73ff0c769f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x73ff0964524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x73ff09645305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x63034e99c8da]
✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (4.0s)
✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.1s)
✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (36s)
✔ [3414/3416] Built Iut.Basic (2.4s)
✔ [3415/3416] Built Iut (2.3s)
Build completed successfully (3416 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
blueprint_build exit 1 duration 2s · created 
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 duration 33m 31s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 2ac9cf74b29e38ccaba829a5368016604647e7e0b1c1509cac0a741ae794a888
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 5m 25s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
lean semantic helper: restored compiled static runner cache b0ddeaaa2553229aaff1dc72c131add56ca5eaf65331b57c95c4ac371fadb91f
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 6m 54s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
lean semantic helper: restored compiled static runner cache e538f0251f041ef0b337d3bd2b02e2800bdae1a864fbf6b2380b52ffeb000535
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 5m 56s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)
lean semantic helper: restored compiled static runner cache 75b5977bf3c3f7790c74f7fcdf61319b52a6563d7e4b9f6920235cee9e6766b3
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 6m 4s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)
lean semantic helper: restored compiled static runner cache b1361ddd4d800407fee97079d7c69334e9fa98f8d8138ea91735fd01a42f86a2
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 6m 26s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)
lean semantic helper: restored compiled static runner cache 03585dcb70610534a4ce74449195125e05e01fddbca11f3263fb9006bd27c14e
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 7m 22s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006)
lean semantic helper: restored compiled static runner cache 08877232589cf9db425b8187c7f232d1869e5ec11e14304e9a4a61a9b73231aa
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 6m 32s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007)
lean semantic helper: restored compiled static runner cache e73538885b586c3d3ade36b614bd08578304e5f0d861b518f22c5a691c41fbd9
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 18m 16s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00008)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 2a0d9b1759608dd0839ed14e6eb12641720673a8d70f159823fcbef8f7aaf986
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 1h 40m · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00009)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 70eef4f33133c7580bac3525074e20bc9c50b8f59dcfca0fea5bd8ef86905f10
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 6m 57s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00010)
lean semantic helper: restored compiled static runner cache 8ce5ff6c967baef3842b8fb460ab7dc29b28a04bbb424be955c4371e23608184
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 5m 49s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00011)
lean semantic helper: restored compiled static runner cache 6247def1945279a6946b34517b575ac426a9bd22cc4c3ceb7a79dc06ef4083db
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 31m 38s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00012)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 9f443dd4847774d8f8b98d82ad89000c793023e3d9d91cd61f02b1b72cf933a0
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 5m 33s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00013)
lean semantic helper: restored compiled static runner cache 60b5e07f9f538c271c74b7f6a814efcb4304463fa74b69c58466604298c0acfe
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0 duration 5m 23s · created 
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00014)
lean semantic helper: restored compiled static runner cache e103fd3939aed645f6a64b867308ee472e79eb2af9586b744c189d70ac5f91ea
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Keyboard shortcuts