Verification run

Run 341

promachina/iut-lean branch master triggered via manual
succeeded commit 71ef5dc5e76d toolchain lean-v4-30-0 prover lean took 2h 46m · finished 5w 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

(no log excerpt)

Command runs

git_checkout exit 0 duration 919 ms · created
git fetch --depth 1 origin 71ef5dc5e76d60469a81a05df5dd9473c8c42975
From https://github.com/promachina/iut-lean
 * branch            71ef5dc5e76d60469a81a05df5dd9473c8c42975 -> FETCH_HEAD
semantic_module_facts exit 0 duration 21s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00010)
lean semantic helper: restored compiled static runner cache a9a06e968839d8b8f7e22b6bb42203d7559473912527ed06adfeb9a10487c71a
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
git_clone exit 0 duration 2s · created
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-421-source
Cloning into '/var/lib/apodeixis/repos/job-421-source'...
git_checkout exit 128 duration 4 ms · created
git checkout 71ef5dc5e76d60469a81a05df5dd9473c8c42975
fatal: reference is not a tree: 71ef5dc5e76d60469a81a05df5dd9473c8c42975
git_checkout exit 0 duration 135 ms · created
git checkout 71ef5dc5e76d60469a81a05df5dd9473c8c42975 (after fetch)
Note: switching to '71ef5dc5e76d60469a81a05df5dd9473c8c42975'.

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 71ef5dc Add coordinate scalar valuation hull cover
lake_cache exit 0 duration 40s · 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%, 9 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 9 KB/s], Decompressed: 10
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 15 KB/s], Decompressed: 36
Downloaded: 62 file(s) [attempted 62/8459 = 0%, 352 KB/s], Decompressed: 58
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 186 KB/s], Decompressed: 82
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 255 KB/s], Decompressed: 121
Downloaded: 151 file(s) [attempted 151/8459 = 1%, 87 KB/s], Decompressed: 148
Downloaded: 189 file(s) [attempted 189/8459 = 2%, 566 KB/s], Decompressed: 186
Downloaded: 225 file(s) [attempted 225/8459 = 2%, 779 KB/s], Decompressed: 220
Downloaded: 264 file(s) [attempted 264/8459 = 3%, 144 KB/s], Decompressed: 261
Downloaded: 302 file(s) [attempted 302/8459 = 3%, 670 KB/s], Decompressed: 295
Downloaded: 336 file(s) [attempted 336/8459 = 3%, 131 KB/s], Decompressed: 333
Downloaded: 374 file(s) [attempted 374/8459 = 4%, 101 KB/s], Decompressed: 371
Downloaded: 416 file(s) [attempted 416/8459 = 4%, 227 KB/s], Decompressed: 412
Downloaded: 449 file(s) [attempted 449/8459 = 5%, 75 KB/s], Decompressed: 446
Downloaded: 485 file(s) [attempted 485/8459 = 5%, 78 KB/s], Decompressed: 480
Downloaded: 525 file(s) [attempted 525/8459 = 6%, 607 KB/s], Decompressed: 521
Downloaded: 566 file(s) [attempted 566/8459 = 6%, 164 KB/s], Decompressed: 562
Downloaded: 602 file(s) [attempted 602/8459 = 7%, 241 KB/s], Decompressed: 597
Downloaded: 641 file(s) [attempted 641/8459 = 7%, 86 KB/s], Decompressed: 634
Downloaded: 682 file(s) [attempted 682/8459 = 8%, 87 KB/s], Decompressed: 679
Downloaded: 727 file(s) [attempted 727/8459 = 8%, 75 KB/s], Decompressed: 723
Downloaded: 771 file(s) [attempted 771/8459 = 9%, 836 KB/s], Decompressed: 765
Downloaded: 804 file(s) [attempted 804/8459 = 9%, 117 KB/s], Decompressed: 799
Downloaded: 840 file(s) [attempted 840/8459 = 9%, 493 KB/s], Decompressed: 836
Downloaded: 884 file(s) [attempted 884/8459 = 10%, 37 KB/s], Decompressed: 881
Downloaded: 929 file(s) [attempted 929/8459 = 10%, 131 KB/s], Decompressed: 925
Downloaded: 970 file(s) [attempted 970/8459 = 11%, 284 KB/s], Decompressed: 967
Downloaded: 1004 file(s) [attempted 1004/8459 = 11%, 113 KB/s], Decompressed: 997
Downloaded: 1041 file(s) [attempted 1041/8459 = 12%, 873 KB/s], Decompressed: 1035
Downloaded: 1083 file(s) [attempted 1083/8459 = 12%, 217 KB/s], Decompressed: 1080
Downloaded: 1127 file(s) [attempted 1127/8459 = 13%, 145 KB/s], Decompressed: 1124
Downloaded: 1164 file(s) [attempted 1164/8459 = 13%, 322 KB/s], Decompressed: 1158
Downloaded: 1196 file(s) [attempted 1196/8459 = 14%, 508 KB/s], Decompressed: 1192
Downloaded: 1240 file(s) [attempted 1240/8459 = 14%, 34 KB/s], Decompressed: 1237
Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 522 KB/s], Decompressed: 1278
Downloaded: 1324 file(s) [attempted 1324/8459 = 15%, 358 KB/s], Decompressed: 1319
Downloaded: 1354 file(s) [attempted 1354/8459 = 16%, 148 KB/s], Decompressed: 1350
Downloaded: 1395 file(s) [attempted 1395/8459 = 16%, 44 KB/s], Decompressed: 1391
Downloaded: 1435 file(s) [attempted 1435/8459 = 16%, 480 KB/s], Decompressed: 1432
Downloaded: 1474 file(s) [attempted 1474/8459 = 17%, 581 KB/s], Decompressed: 1470
Downloaded: 1511 file(s) [attempted 1511/8459 = 17%, 133 KB/s], Decompressed: 1505
Downloaded: 1548 file(s) [attempted 1548/8459 = 18%, 168 KB/s], Decompressed: 1542
Downloaded: 1589 file(s) [attempted 1589/8459 = 18%, 401 KB/s], Decompressed: 1586
Downloaded: 1634 file(s) [attempted 1634/8459 = 19%, 244 KB/s], Decompressed: 1631
Downloaded: 1675 file(s) [attempted 1675/8459 = 19%, 110 KB/s], Decompressed: 1668
Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 418 KB/s], Decompressed: 1709
Downloaded: 1754 file(s) [attempted 1754/8459 = 20%, 360 KB/s], Decompressed: 1750
Downloaded: 1795 file(s) [attempted 1795/8459 = 21%, 25 KB/s], Decompressed: 1791
Downloaded: 1834 file(s) [attempted 1834/8459 = 21%, 67 KB/s], Decompressed: 1829
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 270 KB/s], Decompressed: 1863
Downloaded: 1909 file(s) [attempted 1909/8459 = 22%, 514 KB/s], Decompressed: 1904
Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 723 KB/s], Decompressed: 1945
Downloaded: 1990 file(s) [attempted 1990/8459 = 23%, 990 KB/s], Decompressed: 1988
Downloaded: 2021 file(s) [attempted 2021/8459 = 23%, 316 KB/s], Decompressed: 2014
Downloaded: 2062 file(s) [attempted 2062/8459 = 24%, 57 KB/s], Decompressed: 2058
Downloaded: 2103 file(s) [attempted 2103/8459 = 24%, 456 KB/s], Decompressed: 2099
Downloaded: 2147 file(s) [attempted 2147/8459 = 25%, 79 KB/s], Decompressed: 2144
Downloaded: 2192 file(s) [attempted 2192/8459 = 25%, 440 KB/s], Decompressed: 2188
Downloaded: 2224 file(s) [attempted 2224/8459 = 26%, 168 KB/s], Decompressed: 2216
Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 25 KB/s], Decompressed: 2253
Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 910 KB/s], Decompressed: 2291
Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 123 KB/s], Decompressed: 2329
Downloaded: 2371 file(s) [attempted 2371/8459 = 28%, 223 KB/s], Decompressed: 2366
Downloaded: 2407 file(s) [attempted 2407/8459 = 28%, 289 KB/s], Decompressed: 2404
Downloaded: 2445 file(s) [attempted 2445/8459 = 28%, 262 KB/s], Decompressed: 2442
Downloaded: 2486 file(s) [attempted 2486/8459 = 29%, 131 KB/s], Decompressed: 2479
Downloaded: 2520 file(s) [attempted 2520/8459 = 29%, 48 KB/s], Decompressed: 2517
Downloaded: 2561 file(s) [attempted 2561/8459 = 30%, 674 KB/s], Decompressed: 2558
Downloaded: 2603 file(s) [attempted 2603/8459 = 30%, 571 KB/s], Decompressed: 2599
Downloaded: 2646 file(s) [attempted 2646/8459 = 31%, 195 KB/s], Decompressed: 2640
Downloaded: 2685 file(s) [attempted 2685/8459 = 31%, 350 KB/s], Decompressed: 2678
Downloaded: 2717 file(s) [attempted 2717/8459 = 32%, 474 KB/s], Decompressed: 2712
Downloaded: 2753 file(s) [attempted 2753/8459 = 32%, 198 KB/s], Decompressed: 2750
Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 156 KB/s], Decompressed: 2794
Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 248 KB/s], Decompressed: 2832
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 84 KB/s], Decompressed: 2873
Downloaded: 2915 file(s) [attempted 2915/8459 = 34%, 224 KB/s], Decompressed: 2911
Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 917 KB/s], Decompressed: 2948
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 971 KB/s], Decompressed: 2993
Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 145 KB/s], Decompressed: 3030
Downloaded: 3075 file(s) [attempted 3075/8459 = 36%, 211 KB/s], Decompressed: 3071
Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 74 KB/s], Decompressed: 3112
Downloaded: 3154 file(s) [attempted 3154/8459 = 37%, 211 KB/s], Decompressed: 3150
Downloaded: 3188 file(s) [attempted 3188/8459 = 37%, 233 KB/s], Decompressed: 3184
Downloaded: 3225 file(s) [attempted 3225/8459 = 38%, 159 KB/s], Decompressed: 3222
Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 211 KB/s], Decompressed: 3266
Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 116 KB/s], Decompressed: 3314
Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 40 KB/s], Decompressed: 3359
Downloaded: 3403 file(s) [attempted 3403/8459 = 40%, 403 KB/s], Decompressed: 3400
Downloaded: 3439 file(s) [attempted 3439/8459 = 40%, 254 KB/s], Decompressed: 3434
Downloaded: 3479 file(s) [attempted 3479/8459 = 41%, 163 KB/s], Decompressed: 3472
Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 226 KB/s], Decompressed: 3516
Downloaded: 3561 file(s) [attempted 3561/8459 = 42%, 417 KB/s], Decompressed: 3557
Downloaded: 3600 file(s) [attempted 3600/8459 = 42%, 108 KB/s], Decompressed: 3595
Downloaded: 3638 file(s) [attempted 3638/8459 = 43%, 108 KB/s], Decompressed: 3629
Downloaded: 3676 file(s) [attempted 3676/8459 = 43%, 370 KB/s], Decompressed: 3667
Downloaded: 3715 file(s) [attempted 3715/8459 = 43%, 363 KB/s], Decompressed: 3711
Downloaded: 3751 file(s) [attempted 3751/8459 = 44%, 78 KB/s], Decompressed: 3746
Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 170 KB/s], Decompressed: 3787
Downloaded: 3835 file(s) [attempted 3835/8459 = 45%, 201 KB/s], Decompressed: 3831
Downloaded: 3879 file(s) [attempted 3879/8459 = 45%, 117 KB/s], Decompressed: 3876
Downloaded: 3915 file(s) [attempted 3915/8459 = 46%, 2519 KB/s], Decompressed: 3906
Downloaded: 3949 file(s) [attempted 3949/8459 = 46%, 345 KB/s], Decompressed: 3944
Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 574 KB/s], Decompressed: 3989
Downloaded: 4033 file(s) [attempted 4033/8459 = 47%, 951 KB/s], Decompressed: 4026
Downloaded: 4068 file(s) [attempted 4068/8459 = 48%, 271 KB/s], Decompressed: 4060
Downloaded: 4102 file(s) [attempted 4102/8459 = 48%, 458 KB/s], Decompressed: 4098
Downloaded: 4146 file(s) [attempted 4146/8459 = 49%, 807 KB/s], Decompressed: 4143
Downloaded: 4187 file(s) [attempted 4187/8459 = 49%, 337 KB/s], Decompressed: 4180
Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 43 KB/s], Decompressed: 4221
Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 219 KB/s], Decompressed: 4266
Downloaded: 4308 file(s) [attempted 4308/8459 = 50%, 231 KB/s], Decompressed: 4303
Downloaded: 4347 file(s) [attempted 4347/8459 = 51%, 172 KB/s], Decompressed: 4341
Downloaded: 4386 file(s) [attempted 4386/8459 = 51%, 453 KB/s], Decompressed: 4382
Downloaded: 4420 file(s) [attempted 4420/8459 = 52%, 140 KB/s], Decompressed: 4416
Downloaded: 4461 file(s) [attempted 4461/8459 = 52%, 93 KB/s], Decompressed: 4457
Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 304 KB/s], Decompressed: 4499
Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 458 KB/s], Decompressed: 4540
Downloaded: 4585 file(s) [attempted 4585/8459 = 54%, 599 KB/s], Decompressed: 4577
Downloaded: 4618 file(s) [attempted 4618/8459 = 54%, 928 KB/s], Decompressed: 4615
Downloaded: 4656 file(s) [attempted 4656/8459 = 55%, 56 KB/s], Decompressed: 4649
Downloaded: 4697 file(s) [attempted 4697/8459 = 55%, 35 KB/s], Decompressed: 4694
Downloaded: 4742 file(s) [attempted 4742/8459 = 56%, 421 KB/s], Decompressed: 4735
Downloaded: 4779 file(s) [attempted 4779/8459 = 56%, 138 KB/s], Decompressed: 4776
Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 402 KB/s], Decompressed: 4810
Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 62 KB/s], Decompressed: 4851
Downloaded: 4896 file(s) [attempted 4896/8459 = 57%, 838 KB/s], Decompressed: 4892
Downloaded: 4937 file(s) [attempted 4937/8459 = 58%, 23 KB/s], Decompressed: 4933
Downloaded: 4974 file(s) [attempted 4974/8459 = 58%, 499 KB/s], Decompressed: 4971
Downloaded: 5008 file(s) [attempted 5008/8459 = 59%, 60 KB/s], Decompressed: 5005
Downloaded: 5050 file(s) [attempted 5050/8459 = 59%, 464 KB/s], Decompressed: 5046
Downloaded: 5094 file(s) [attempted 5094/8459 = 60%, 928 KB/s], Decompressed: 5091
Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 598 KB/s], Decompressed: 5125
Downloaded: 5169 file(s) [attempted 5169/8459 = 61%, 111 KB/s], Decompressed: 5162
Downloaded: 5204 file(s) [attempted 5204/8459 = 61%, 119 KB/s], Decompressed: 5200
Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 230 KB/s], Decompressed: 5241
Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 273 KB/s], Decompressed: 5279
Downloaded: 5323 file(s) [attempted 5323/8459 = 62%, 63 KB/s], Decompressed: 5320
Downloaded: 5362 file(s) [attempted 5362/8459 = 63%, 444 KB/s], Decompressed: 5359
Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 281 KB/s], Decompressed: 5399
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 466 KB/s], Decompressed: 5436
Downloaded: 5483 file(s) [attempted 5483/8459 = 64%, 299 KB/s], Decompressed: 5477
Downloaded: 5522 file(s) [attempted 5522/8459 = 65%, 161 KB/s], Decompressed: 5518
Downloaded: 5563 file(s) [attempted 5563/8459 = 65%, 80 KB/s], Decompressed: 5559
Downloaded: 5597 file(s) [attempted 5597/8459 = 66%, 646 KB/s], Decompressed: 5594
Downloaded: 5638 file(s) [attempted 5638/8459 = 66%, 141 KB/s], Decompressed: 5635
Downloaded: 5676 file(s) [attempted 5676/8459 = 67%, 58 KB/s], Decompressed: 5669
Downloaded: 5718 file(s) [attempted 5718/8459 = 67%, 169 KB/s], Decompressed: 5713
Downloaded: 5751 file(s) [attempted 5751/8459 = 67%, 306 KB/s], Decompressed: 5750
Downloaded: 5789 file(s) [attempted 5789/8459 = 68%, 235 KB/s], Decompressed: 5785
Downloaded: 5829 file(s) [attempted 5829/8459 = 68%, 1149 KB/s], Decompressed: 5823
Downloaded: 5871 file(s) [attempted 5871/8459 = 69%, 175 KB/s], Decompressed: 5857
Downloaded: 5903 file(s) [attempted 5903/8459 = 69%, 339 KB/s], Decompressed: 5898
Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 822 KB/s], Decompressed: 5936
Downloaded: 5980 file(s) [attempted 5980/8459 = 70%, 1520 KB/s], Decompressed: 5977
Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 76 KB/s], Decompressed: 6021
Downloaded: 6063 file(s) [attempted 6063/8459 = 71%, 1048 KB/s], Decompressed: 6059
Downloaded: 6104 file(s) [attempted 6104/8459 = 72%, 192 KB/s], Decompressed: 6098
Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 68 KB/s], Decompressed: 6138
Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 55 KB/s], Decompressed: 6179
Downloaded: 6221 file(s) [attempted 6221/8459 = 73%, 135 KB/s], Decompressed: 6217
Downloaded: 6262 file(s) [attempted 6262/8459 = 74%, 125 KB/s], Decompressed: 6258
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 2696 KB/s], Decompressed: 6288
Downloaded: 6334 file(s) [attempted 6334/8459 = 74%, 35 KB/s], Decompressed: 6329
Downloaded: 6371 file(s) [attempted 6371/8459 = 75%, 352 KB/s], Decompressed: 6367
Downloaded: 6414 file(s) [attempted 6414/8459 = 75%, 82 KB/s], Decompressed: 6408
Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 751 KB/s], Decompressed: 6446
Downloaded: 6490 file(s) [attempted 6490/8459 = 76%, 161 KB/s], Decompressed: 6487
Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 488 KB/s], Decompressed: 6525
Downloaded: 6569 file(s) [attempted 6569/8459 = 77%, 141 KB/s], Decompressed: 6566
Downloaded: 6611 file(s) [attempted 6611/8459 = 78%, 575 KB/s], Decompressed: 6607
Downloaded: 6651 file(s) [attempted 6651/8459 = 78%, 460 KB/s], Decompressed: 6648
Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 151 KB/s], Decompressed: 6679
Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 163 KB/s], Decompressed: 6723
Downloaded: 6770 file(s) [attempted 6770/8459 = 80%, 1304 KB/s], Decompressed: 6764
Downloaded: 6805 file(s) [attempted 6805/8459 = 80%, 220 KB/s], Decompressed: 6802
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 54 KB/s], Decompressed: 6839
Downloaded: 6881 file(s) [attempted 6881/8459 = 81%, 225 KB/s], Decompressed: 6877
Downloaded: 6922 file(s) [attempted 6922/8459 = 81%, 359 KB/s], Decompressed: 6918
Downloaded: 6963 file(s) [attempted 6963/8459 = 82%, 168 KB/s], Decompressed: 6959
Downloaded: 6993 file(s) [attempted 6993/8459 = 82%, 232 KB/s], Decompressed: 6990
Downloaded: 7038 file(s) [attempted 7038/8459 = 83%, 152 KB/s], Decompressed: 7035
Downloaded: 7078 file(s) [attempted 7078/8459 = 83%, 480 KB/s], Decompressed: 7072
Downloaded: 7114 file(s) [attempted 7114/8459 = 84%, 285 KB/s], Decompressed: 7110
Downloaded: 7152 file(s) [attempted 7152/8459 = 84%, 441 KB/s], Decompressed: 7147
Downloaded: 7192 file(s) [attempted 7192/8459 = 85%, 55 KB/s], Decompressed: 7189
Downloaded: 7233 file(s) [attempted 7233/8459 = 85%, 879 KB/s], Decompressed: 7230
Downloaded: 7267 file(s) [attempted 7267/8459 = 85%, 112 KB/s], Decompressed: 7260
Downloaded: 7308 file(s) [attempted 7308/8459 = 86%, 36 KB/s], Decompressed: 7301
Downloaded: 7353 file(s) [attempted 7353/8459 = 86%, 69 KB/s], Decompressed: 7349
Downloaded: 7394 file(s) [attempted 7394/8459 = 87%, 267 KB/s], Decompressed: 7390
Downloaded: 7438 file(s) [attempted 7438/8459 = 87%, 98 KB/s], Decompressed: 7435
Downloaded: 7470 file(s) [attempted 7470/8459 = 88%, 179 KB/s], Decompressed: 7466
Downloaded: 7505 file(s) [attempted 7505/8459 = 88%, 429 KB/s], Decompressed: 7500
Downloaded: 7551 file(s) [attempted 7551/8459 = 89%, 92 KB/s], Decompressed: 7548
Downloaded: 7599 file(s) [attempted 7599/8459 = 89%, 1044 KB/s], Decompressed: 7596
Downloaded: 7644 file(s) [attempted 7644/8459 = 90%, 855 KB/s], Decompressed: 7640
Downloaded: 7674 file(s) [attempted 7674/8459 = 90%, 348 KB/s], Decompressed: 7671
Downloaded: 7712 file(s) [attempted 7712/8459 = 91%, 453 KB/s], Decompressed: 7709
Downloaded: 7757 file(s) [attempted 7757/8459 = 91%, 114 KB/s], Decompressed: 7753
Downloaded: 7799 file(s) [attempted 7799/8459 = 92%, 159 KB/s], Decompressed: 7794
Downloaded: 7833 file(s) [attempted 7833/8459 = 92%, 703 KB/s], Decompressed: 7825
Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 49 KB/s], Decompressed: 7863
Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 817 KB/s], Decompressed: 7904
Downloaded: 7952 file(s) [attempted 7952/8459 = 94%, 119 KB/s], Decompressed: 7948
Downloaded: 7993 file(s) [attempted 7993/8459 = 94%, 184 KB/s], Decompressed: 7982
Downloaded: 8027 file(s) [attempted 8027/8459 = 94%, 558 KB/s], Decompressed: 8024
Downloaded: 8070 file(s) [attempted 8070/8459 = 95%, 248 KB/s], Decompressed: 8061
Downloaded: 8108 file(s) [attempted 8108/8459 = 95%, 95 KB/s], Decompressed: 8102
Downloaded: 8147 file(s) [attempted 8147/8459 = 96%, 589 KB/s], Decompressed: 8140
Downloaded: 8184 file(s) [attempted 8184/8459 = 96%, 1293 KB/s], Decompressed: 8178
Downloaded: 8222 file(s) [attempted 8222/8459 = 97%, 415 KB/s], Decompressed: 8219
Downloaded: 8261 file(s) [attempted 8261/8459 = 97%, 223 KB/s], Decompressed: 8256
Downloaded: 8301 file(s) [attempted 8301/8459 = 98%, 447 KB/s], Decompressed: 8297
Downloaded: 8338 file(s) [attempted 8338/8459 = 98%, 94 KB/s], Decompressed: 8335
Downloaded: 8374 file(s) [attempted 8374/8459 = 98%, 102 KB/s], Decompressed: 8369
Downloaded: 8417 file(s) [attempted 8417/8459 = 99%, 434 KB/s], Decompressed: 8414
Downloaded: 8450 file(s) [attempted 8450/8459 = 99%, 167 KB/s], Decompressed: 8441
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 249 KB/s], Decompressed: 8448
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 249 KB/s], Decompressed: 8448
lean_checker exit 0 duration 3s · created
lake build
ℹ [3410/3416] Replayed Iut.Stage1.IUTStage1FrobenioidShift
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) [0x7792f29c6785]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7792f29bdb27]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7792f29bdc0b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7792f28f3c62]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7792f28f4439]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7792f29caf99]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7792f2832923]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7792f2832b2b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7792f2833827]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7792f28341b6]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7792f29c9e8b]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7792f2615adb]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7792f29c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7792f29c9fc3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7792f299b1f3]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7792f2615c92]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7792eda22638]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7792ed80cd2e]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7792ed369a82]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7792ed369f0e]
/lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7792ea24524a]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7792ea245305]
/apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5e715c4c08da]
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 915 ms · 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_module_facts exit 0 duration 6m 1s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00000)
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: 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
semantic_module_facts exit 0 duration 5m 42s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00001)
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_module_facts exit 0 duration 2m 1s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00002)
lean semantic helper: restored compiled static runner cache 91173b292067b1a93ea64425cc888039ebce7a3e364765ecea90e7a5cbd3d047
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 2m 3s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00003)
lean semantic helper: restored compiled static runner cache f04752e91581a87c3d8d8a87c9c62d574535d7f0c9532c8f513c6579555ccc6c
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 2m 3s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00004)
lean semantic helper: restored compiled static runner cache e6ad3fd83caa15e625545b87ad41df67e06b9649767ec9f22a1000a9a1e49c7e
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 2m 4s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00005)
lean semantic helper: restored compiled static runner cache 5e719f139e700d3ec36d870eb0df93c69e39d1b25bc64de0e83c7820c297cc88
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 5m 38s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00006)
lean semantic helper: restored compiled static runner cache e925bad531c9c8172209069553d6ef13f8bc4d43ffee8f9f45ce1b2a571648d9
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 2m 6s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00007)
lean semantic helper: restored compiled static runner cache b8207442bfba00511b560efc544d5ce67b0aa813df3d432a1aba6b1f99808bdf
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 1m 59s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00008)
lean semantic helper: restored compiled static runner cache 56cf09ccb3908696b8e5e7742ce037825c061cf4f72cf51826c370ecdd278b63
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 2m 0s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00009)
lean semantic helper: restored compiled static runner cache 82cff17b2a0859360c864be978661e734ea49f8bd78dbf096db8866b58caf113
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 2m 2s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00011)
lean semantic helper: restored compiled static runner cache 6b68dbdfef85a7b6943bcf3aed743bff07bc5a8789269f4969952ccbec066986
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 1m 59s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00012)
lean semantic helper: restored compiled static runner cache 5a5015d089cfb0ec2d9e00c036585dab768f83e5b768c8aa0991818ae117b9aa
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 4m 52s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00013)
lean semantic helper: restored compiled static runner cache 916ea7b0333772c3e6f8e394e031f32699844624a1add271ecbcb781a9f49e93
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 4m 45s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00014)
lean semantic helper: restored compiled static runner cache 2bfcdcefc85e86330c36ad81e41c2ddb7c7e852d7b70484d888f87d3783eb3ee
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 4m 45s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00015)
lean semantic helper: restored compiled static runner cache ac720950978d81db58a9b7127c0c29b52147e5d60a6dd5804497dee52cf190ea
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 5m 29s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00016)
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_module_facts exit 0 duration 5m 37s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00017)
lean semantic helper: restored compiled static runner cache f4d9c003c7452016e42c7fead986b54b7a3d6e7471516ee89e90353366820d66
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 5m 32s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00018)
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_module_facts exit 0 duration 5m 37s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00019)
lean semantic helper: restored compiled static runner cache 0efd485e0463b19f5c2e2a591158e669acbf0d05b6feb20ce1b85cba88b2befe
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 5m 33s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00020)
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_module_facts exit 0 duration 5m 29s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00021)
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_module_facts exit 0 duration 5m 37s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00022)
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_module_facts exit 0 duration 5m 30s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00023)
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_module_facts exit 0 duration 5m 35s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00024)
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_module_facts exit 0 duration 5m 39s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00025)
lean semantic helper: restored compiled static runner cache 361c3a3115683a95ae5a195d9d3288c0f30083b629ae0efa02efc9266225a437
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 5m 35s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00026)
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_module_facts exit 0 duration 5m 28s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00027)
lean semantic helper: restored compiled static runner cache 9c9cf2b3451621905e924ca74e022d2283294e8f723d50f83339e66904461aaf
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 5m 33s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00028)
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_module_facts exit 0 duration 2m 0s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00029)
lean semantic helper: restored compiled static runner cache b278679b96703b88f46c5058abea7a921c64bde7c3009a5f675db878cd3eba6c
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0 duration 4m 45s · created
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00030)
lean semantic helper: restored compiled static runner cache 789c65a0d29891fa409358efae098c665e03a540d880d2a888005d1f8a1e3e15
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 34m 26s · created
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
lean semantic helper: restored compiled static runner cache 361c3a3115683a95ae5a195d9d3288c0f30083b629ae0efa02efc9266225a437
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Keyboard shortcuts