Verification run
Run 6
succeeded commit
c4d4c2e83231 toolchain lean-v4-31-0-rc1 prover lean took 18m 39s · finished 6w ago
Package inputs
This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.
Trust verification
Recomputes trust checks from the recorded attestations, manifest, and command history.
(verification not run)
Manifest
Loads the published files manifest and location metadata for this job.
(manifest not loaded)
Verifier log excerpt
(no log excerpt)
Command runs
git_checkout exit 0
git remote set-url origin [clone-url]
git_checkout exit 0
git fetch --prune --depth 1 origin main
From https://github.com/ImperialCollegeLondon/FLT * branch main -> FETCH_HEAD
git_checkout exit 0
git checkout -B main FETCH_HEAD
Your branch is up to date with 'origin/main'.
Switched to and reset branch 'main'
git_checkout exit 0
git checkout c4d4c2e8323150cb677ad6d771dcad039079dfe2
Note: switching to 'c4d4c2e8323150cb677ad6d771dcad039079dfe2'. 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 c4d4c2e chore: bump mathlib to 405bba7, fix breaking changes (#995)
lake_cache exit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8477 file(s) from leanprover-community/mathlib4 cache Decompressed 8477 file(s) Already decompressed 8477 file(s)
Downloaded: 1 file(s) [attempted 1/8477 = 0%, 12 KB/s], Decompressed: 0 Downloaded: 15 file(s) [attempted 15/8477 = 0%, 10 KB/s], Decompressed: 14 Downloaded: 38 file(s) [attempted 38/8477 = 0%, 21 KB/s], Decompressed: 36 Downloaded: 63 file(s) [attempted 63/8477 = 0%, 30 KB/s], Decompressed: 61 Downloaded: 87 file(s) [attempted 87/8477 = 1%, 433 KB/s], Decompressed: 83 Downloaded: 121 file(s) [attempted 121/8477 = 1%, 330 KB/s], Decompressed: 117 Downloaded: 158 file(s) [attempted 158/8477 = 1%, 84 KB/s], Decompressed: 155 Downloaded: 193 file(s) [attempted 193/8477 = 2%, 41 KB/s], Decompressed: 189 Downloaded: 227 file(s) [attempted 227/8477 = 2%, 57 KB/s], Decompressed: 223 Downloaded: 264 file(s) [attempted 264/8477 = 3%, 320 KB/s], Decompressed: 261 Downloaded: 302 file(s) [attempted 302/8477 = 3%, 828 KB/s], Decompressed: 299 Downloaded: 343 file(s) [attempted 343/8477 = 4%, 29 KB/s], Decompressed: 340 Downloaded: 384 file(s) [attempted 384/8477 = 4%, 43 KB/s], Decompressed: 381 Downloaded: 423 file(s) [attempted 423/8477 = 4%, 128 KB/s], Decompressed: 419 Downloaded: 462 file(s) [attempted 462/8477 = 5%, 270 KB/s], Decompressed: 453 Downloaded: 504 file(s) [attempted 504/8477 = 5%, 177 KB/s], Decompressed: 501 Downloaded: 545 file(s) [attempted 545/8477 = 6%, 35 KB/s], Decompressed: 538 Downloaded: 582 file(s) [attempted 582/8477 = 6%, 32 KB/s], Decompressed: 576 Downloaded: 624 file(s) [attempted 624/8477 = 7%, 209 KB/s], Decompressed: 617 Downloaded: 662 file(s) [attempted 662/8477 = 7%, 151 KB/s], Decompressed: 658 Downloaded: 700 file(s) [attempted 700/8477 = 8%, 205 KB/s], Decompressed: 696 Downloaded: 741 file(s) [attempted 741/8477 = 8%, 294 KB/s], Decompressed: 737 Downloaded: 778 file(s) [attempted 778/8477 = 9%, 416 KB/s], Decompressed: 775 Downloaded: 819 file(s) [attempted 819/8477 = 9%, 1938 KB/s], Decompressed: 816 Downloaded: 867 file(s) [attempted 867/8477 = 10%, 460 KB/s], Decompressed: 864 Downloaded: 915 file(s) [attempted 915/8477 = 10%, 582 KB/s], Decompressed: 912 Downloaded: 960 file(s) [attempted 960/8477 = 11%, 232 KB/s], Decompressed: 956 Downloaded: 995 file(s) [attempted 995/8477 = 11%, 836 KB/s], Decompressed: 987 Downloaded: 1028 file(s) [attempted 1028/8477 = 12%, 461 KB/s], Decompressed: 1021 Downloaded: 1068 file(s) [attempted 1068/8477 = 12%, 61 KB/s], Decompressed: 1062 Downloaded: 1104 file(s) [attempted 1104/8477 = 13%, 126 KB/s], Decompressed: 1100 Downloaded: 1138 file(s) [attempted 1138/8477 = 13%, 443 KB/s], Decompressed: 1134 Downloaded: 1169 file(s) [attempted 1169/8477 = 13%, 628 KB/s], Decompressed: 1165 Downloaded: 1210 file(s) [attempted 1210/8477 = 14%, 216 KB/s], Decompressed: 1206 Downloaded: 1254 file(s) [attempted 1254/8477 = 14%, 609 KB/s], Decompressed: 1247 Downloaded: 1289 file(s) [attempted 1289/8477 = 15%, 145 KB/s], Decompressed: 1281 Downloaded: 1329 file(s) [attempted 1329/8477 = 15%, 47 KB/s], Decompressed: 1326 Downloaded: 1370 file(s) [attempted 1370/8477 = 16%, 316 KB/s], Decompressed: 1367 Downloaded: 1412 file(s) [attempted 1412/8477 = 16%, 330 KB/s], Decompressed: 1408 Downloaded: 1456 file(s) [attempted 1456/8477 = 17%, 114 KB/s], Decompressed: 1449 Downloaded: 1497 file(s) [attempted 1497/8477 = 17%, 203 KB/s], Decompressed: 1490 Downloaded: 1535 file(s) [attempted 1535/8477 = 18%, 122 KB/s], Decompressed: 1531 Downloaded: 1578 file(s) [attempted 1578/8477 = 18%, 112 KB/s], Decompressed: 1566 Downloaded: 1610 file(s) [attempted 1610/8477 = 18%, 1027 KB/s], Decompressed: 1607 Downloaded: 1655 file(s) [attempted 1655/8477 = 19%, 22 KB/s], Decompressed: 1648 Downloaded: 1696 file(s) [attempted 1696/8477 = 20%, 293 KB/s], Decompressed: 1692 Downloaded: 1740 file(s) [attempted 1740/8477 = 20%, 366 KB/s], Decompressed: 1737 Downloaded: 1775 file(s) [attempted 1775/8477 = 20%, 466 KB/s], Decompressed: 1771 Downloaded: 1819 file(s) [attempted 1819/8477 = 21%, 170 KB/s], Decompressed: 1815 Downloaded: 1857 file(s) [attempted 1857/8477 = 21%, 318 KB/s], Decompressed: 1853 Downloaded: 1894 file(s) [attempted 1894/8477 = 22%, 799 KB/s], Decompressed: 1891 Downloaded: 1932 file(s) [attempted 1932/8477 = 22%, 295 KB/s], Decompressed: 1928 Downloaded: 1965 file(s) [attempted 1965/8477 = 23%, 909 KB/s], Decompressed: 1959 Downloaded: 1997 file(s) [attempted 1997/8477 = 23%, 383 KB/s], Decompressed: 1993 Downloaded: 2028 file(s) [attempted 2028/8477 = 23%, 205 KB/s], Decompressed: 2024 Downloaded: 2052 file(s) [attempted 2052/8477 = 24%, 362 KB/s], Decompressed: 2048 Downloaded: 2096 file(s) [attempted 2096/8477 = 24%, 94 KB/s], Decompressed: 2093 Downloaded: 2140 file(s) [attempted 2140/8477 = 25%, 143 KB/s], Decompressed: 2137 Downloaded: 2185 file(s) [attempted 2185/8477 = 25%, 443 KB/s], Decompressed: 2182 Downloaded: 2226 file(s) [attempted 2226/8477 = 26%, 115 KB/s], Decompressed: 2220 Downloaded: 2260 file(s) [attempted 2260/8477 = 26%, 49 KB/s], Decompressed: 2257 Downloaded: 2301 file(s) [attempted 2301/8477 = 27%, 654 KB/s], Decompressed: 2298 Downloaded: 2336 file(s) [attempted 2336/8477 = 27%, 87 KB/s], Decompressed: 2332 Downloaded: 2380 file(s) [attempted 2380/8477 = 28%, 231 KB/s], Decompressed: 2377 Downloaded: 2421 file(s) [attempted 2421/8477 = 28%, 421 KB/s], Decompressed: 2411 Downloaded: 2452 file(s) [attempted 2452/8477 = 28%, 69 KB/s], Decompressed: 2448 Downloaded: 2496 file(s) [attempted 2496/8477 = 29%, 307 KB/s], Decompressed: 2493 Downloaded: 2541 file(s) [attempted 2541/8477 = 29%, 608 KB/s], Decompressed: 2537 Downloaded: 2582 file(s) [attempted 2582/8477 = 30%, 1532 KB/s], Decompressed: 2575 Downloaded: 2622 file(s) [attempted 2622/8477 = 30%, 285 KB/s], Decompressed: 2616 Downloaded: 2657 file(s) [attempted 2657/8477 = 31%, 335 KB/s], Decompressed: 2650 Downloaded: 2698 file(s) [attempted 2698/8477 = 31%, 58 KB/s], Decompressed: 2688 Downloaded: 2736 file(s) [attempted 2736/8477 = 32%, 159 KB/s], Decompressed: 2733 Downloaded: 2784 file(s) [attempted 2784/8477 = 32%, 159 KB/s], Decompressed: 2777 Downloaded: 2828 file(s) [attempted 2828/8477 = 33%, 96 KB/s], Decompressed: 2822 Downloaded: 2863 file(s) [attempted 2863/8477 = 33%, 292 KB/s], Decompressed: 2859 Downloaded: 2904 file(s) [attempted 2904/8477 = 34%, 183 KB/s], Decompressed: 2897 Downloaded: 2948 file(s) [attempted 2948/8477 = 34%, 41 KB/s], Decompressed: 2947 Downloaded: 2989 file(s) [attempted 2989/8477 = 35%, 25 KB/s], Decompressed: 2986 Downloaded: 3030 file(s) [attempted 3030/8477 = 35%, 404 KB/s], Decompressed: 3027 Downloaded: 3069 file(s) [attempted 3069/8477 = 36%, 1081 KB/s], Decompressed: 3061 Downloaded: 3102 file(s) [attempted 3102/8477 = 36%, 191 KB/s], Decompressed: 3099 Downloaded: 3150 file(s) [attempted 3150/8477 = 37%, 84 KB/s], Decompressed: 3143 Downloaded: 3195 file(s) [attempted 3195/8477 = 37%, 221 KB/s], Decompressed: 3191 Downloaded: 3230 file(s) [attempted 3230/8477 = 38%, 168 KB/s], Decompressed: 3225 Downloaded: 3270 file(s) [attempted 3270/8477 = 38%, 1096 KB/s], Decompressed: 3266 Downloaded: 3311 file(s) [attempted 3311/8477 = 39%, 311 KB/s], Decompressed: 3307 Downloaded: 3352 file(s) [attempted 3352/8477 = 39%, 1440 KB/s], Decompressed: 3345 Downloaded: 3396 file(s) [attempted 3396/8477 = 40%, 1490 KB/s], Decompressed: 3393 Downloaded: 3434 file(s) [attempted 3434/8477 = 40%, 24 KB/s], Decompressed: 3431 Downloaded: 3472 file(s) [attempted 3472/8477 = 40%, 533 KB/s], Decompressed: 3468 Downloaded: 3510 file(s) [attempted 3510/8477 = 41%, 796 KB/s], Decompressed: 3506 Downloaded: 3550 file(s) [attempted 3550/8477 = 41%, 1139 KB/s], Decompressed: 3547 Downloaded: 3588 file(s) [attempted 3588/8477 = 42%, 583 KB/s], Decompressed: 3585 Downloaded: 3633 file(s) [attempted 3633/8477 = 42%, 804 KB/s], Decompressed: 3626 Downloaded: 3670 file(s) [attempted 3670/8477 = 43%, 333 KB/s], Decompressed: 3667 Downloaded: 3711 file(s) [attempted 3711/8477 = 43%, 488 KB/s], Decompressed: 3701 Downloaded: 3749 file(s) [attempted 3749/8477 = 44%, 193 KB/s], Decompressed: 3746 Downloaded: 3790 file(s) [attempted 3790/8477 = 44%, 103 KB/s], Decompressed: 3787 Downloaded: 3835 file(s) [attempted 3835/8477 = 45%, 741 KB/s], Decompressed: 3831 Downloaded: 3872 file(s) [attempted 3872/8477 = 45%, 56 KB/s], Decompressed: 3865 Downloaded: 3913 file(s) [attempted 3913/8477 = 46%, 244 KB/s], Decompressed: 3906 Downloaded: 3958 file(s) [attempted 3958/8477 = 46%, 261 KB/s], Decompressed: 3954 Downloaded: 3995 file(s) [attempted 3995/8477 = 47%, 685 KB/s], Decompressed: 3992 Downloaded: 4036 file(s) [attempted 4036/8477 = 47%, 106 KB/s], Decompressed: 4030 Downloaded: 4074 file(s) [attempted 4074/8477 = 48%, 237 KB/s], Decompressed: 4071 Downloaded: 4112 file(s) [attempted 4112/8477 = 48%, 105 KB/s], Decompressed: 4108 Downloaded: 4152 file(s) [attempted 4152/8477 = 48%, 79 KB/s], Decompressed: 4146 Downloaded: 4190 file(s) [attempted 4190/8477 = 49%, 59 KB/s], Decompressed: 4187 Downloaded: 4235 file(s) [attempted 4235/8477 = 49%, 289 KB/s], Decompressed: 4232 Downloaded: 4279 file(s) [attempted 4279/8477 = 50%, 391 KB/s], Decompressed: 4276 Downloaded: 4310 file(s) [attempted 4310/8477 = 50%, 1251 KB/s], Decompressed: 4303 Downloaded: 4351 file(s) [attempted 4351/8477 = 51%, 231 KB/s], Decompressed: 4344 Downloaded: 4392 file(s) [attempted 4392/8477 = 51%, 504 KB/s], Decompressed: 4389 Downloaded: 4440 file(s) [attempted 4440/8477 = 52%, 557 KB/s], Decompressed: 4437 Downloaded: 4486 file(s) [attempted 4486/8477 = 52%, 201 KB/s], Decompressed: 4481 Downloaded: 4526 file(s) [attempted 4526/8477 = 53%, 107 KB/s], Decompressed: 4522 Downloaded: 4564 file(s) [attempted 4564/8477 = 53%, 40 KB/s], Decompressed: 4557 Downloaded: 4600 file(s) [attempted 4600/8477 = 54%, 535 KB/s], Decompressed: 4594 Downloaded: 4639 file(s) [attempted 4639/8477 = 54%, 101 KB/s], Decompressed: 4635 Downloaded: 4682 file(s) [attempted 4682/8477 = 55%, 729 KB/s], Decompressed: 4676 Downloaded: 4724 file(s) [attempted 4724/8477 = 55%, 146 KB/s], Decompressed: 4721 Downloaded: 4762 file(s) [attempted 4762/8477 = 56%, 273 KB/s], Decompressed: 4755 Downloaded: 4800 file(s) [attempted 4800/8477 = 56%, 723 KB/s], Decompressed: 4789 Downloaded: 4837 file(s) [attempted 4837/8477 = 57%, 412 KB/s], Decompressed: 4834 Downloaded: 4882 file(s) [attempted 4882/8477 = 57%, 628 KB/s], Decompressed: 4878 Downloaded: 4926 file(s) [attempted 4926/8477 = 58%, 251 KB/s], Decompressed: 4919 Downloaded: 4958 file(s) [attempted 4958/8477 = 58%, 54 KB/s], Decompressed: 4954 Downloaded: 4998 file(s) [attempted 4998/8477 = 58%, 294 KB/s], Decompressed: 4991 Downloaded: 5039 file(s) [attempted 5039/8477 = 59%, 36 KB/s], Decompressed: 5036 Downloaded: 5080 file(s) [attempted 5080/8477 = 59%, 61 KB/s], Decompressed: 5077 Downloaded: 5121 file(s) [attempted 5121/8477 = 60%, 1963 KB/s], Decompressed: 5115 Downloaded: 5162 file(s) [attempted 5162/8477 = 60%, 481 KB/s], Decompressed: 5156 Downloaded: 5203 file(s) [attempted 5203/8477 = 61%, 106 KB/s], Decompressed: 5200 Downloaded: 5243 file(s) [attempted 5243/8477 = 61%, 301 KB/s], Decompressed: 5238 Downloaded: 5281 file(s) [attempted 5281/8477 = 62%, 507 KB/s], Decompressed: 5275 Downloaded: 5321 file(s) [attempted 5321/8477 = 62%, 369 KB/s], Decompressed: 5316 Downloaded: 5364 file(s) [attempted 5364/8477 = 63%, 667 KB/s], Decompressed: 5361 Downloaded: 5405 file(s) [attempted 5405/8477 = 63%, 464 KB/s], Decompressed: 5402 Downloaded: 5443 file(s) [attempted 5443/8477 = 64%, 257 KB/s], Decompressed: 5440 Downloaded: 5484 file(s) [attempted 5484/8477 = 64%, 22 KB/s], Decompressed: 5477 Downloaded: 5518 file(s) [attempted 5518/8477 = 65%, 301 KB/s], Decompressed: 5515 Downloaded: 5556 file(s) [attempted 5556/8477 = 65%, 107 KB/s], Decompressed: 5549 Downloaded: 5590 file(s) [attempted 5590/8477 = 65%, 332 KB/s], Decompressed: 5583 Downloaded: 5628 file(s) [attempted 5628/8477 = 66%, 673 KB/s], Decompressed: 5624 Downloaded: 5669 file(s) [attempted 5669/8477 = 66%, 18 KB/s], Decompressed: 5652 Downloaded: 5696 file(s) [attempted 5696/8477 = 67%, 899 KB/s], Decompressed: 5689 Downloaded: 5741 file(s) [attempted 5741/8477 = 67%, 314 KB/s], Decompressed: 5737 Downloaded: 5785 file(s) [attempted 5785/8477 = 68%, 364 KB/s], Decompressed: 5782 Downloaded: 5830 file(s) [attempted 5830/8477 = 68%, 119 KB/s], Decompressed: 5826 Downloaded: 5872 file(s) [attempted 5872/8477 = 69%, 362 KB/s], Decompressed: 5867 Downloaded: 5912 file(s) [attempted 5912/8477 = 69%, 1048 KB/s], Decompressed: 5908 Downloaded: 5948 file(s) [attempted 5948/8477 = 70%, 1204 KB/s], Decompressed: 5943 Downloaded: 5987 file(s) [attempted 5987/8477 = 70%, 228 KB/s], Decompressed: 5984 Downloaded: 6028 file(s) [attempted 6028/8477 = 71%, 611 KB/s], Decompressed: 6025 Downloaded: 6069 file(s) [attempted 6069/8477 = 71%, 343 KB/s], Decompressed: 6066 Downloaded: 6114 file(s) [attempted 6114/8477 = 72%, 535 KB/s], Decompressed: 6110 Downloaded: 6158 file(s) [attempted 6158/8477 = 72%, 70 KB/s], Decompressed: 6155 Downloaded: 6199 file(s) [attempted 6199/8477 = 73%, 58 KB/s], Decompressed: 6189 Downloaded: 6237 file(s) [attempted 6237/8477 = 73%, 144 KB/s], Decompressed: 6234 Downloaded: 6278 file(s) [attempted 6278/8477 = 74%, 51 KB/s], Decompressed: 6275 Downloaded: 6317 file(s) [attempted 6317/8477 = 74%, 1113 KB/s], Decompressed: 6312 Downloaded: 6358 file(s) [attempted 6358/8477 = 75%, 210 KB/s], Decompressed: 6354 Downloaded: 6398 file(s) [attempted 6398/8477 = 75%, 147 KB/s], Decompressed: 6394 Downloaded: 6432 file(s) [attempted 6432/8477 = 75%, 49 KB/s], Decompressed: 6425 Downloaded: 6473 file(s) [attempted 6473/8477 = 76%, 147 KB/s], Decompressed: 6466 Downloaded: 6514 file(s) [attempted 6514/8477 = 76%, 410 KB/s], Decompressed: 6511 Downloaded: 6555 file(s) [attempted 6555/8477 = 77%, 201 KB/s], Decompressed: 6552 Downloaded: 6600 file(s) [attempted 6600/8477 = 77%, 482 KB/s], Decompressed: 6596 Downloaded: 6637 file(s) [attempted 6637/8477 = 78%, 840 KB/s], Decompressed: 6627 Downloaded: 6679 file(s) [attempted 6679/8477 = 78%, 1090 KB/s], Decompressed: 6675 Downloaded: 6714 file(s) [attempted 6714/8477 = 79%, 1484 KB/s], Decompressed: 6709 Downloaded: 6755 file(s) [attempted 6755/8477 = 79%, 772 KB/s], Decompressed: 6750 Downloaded: 6795 file(s) [attempted 6795/8477 = 80%, 445 KB/s], Decompressed: 6791 Downloaded: 6838 file(s) [attempted 6838/8477 = 80%, 121 KB/s], Decompressed: 6833 Downloaded: 6871 file(s) [attempted 6871/8477 = 81%, 304 KB/s], Decompressed: 6867 Downloaded: 6911 file(s) [attempted 6911/8477 = 81%, 210 KB/s], Decompressed: 6908 Downloaded: 6952 file(s) [attempted 6952/8477 = 82%, 302 KB/s], Decompressed: 6945 Downloaded: 6997 file(s) [attempted 6997/8477 = 82%, 669 KB/s], Decompressed: 6993 Downloaded: 7038 file(s) [attempted 7038/8477 = 83%, 80 KB/s], Decompressed: 7034 Downloaded: 7079 file(s) [attempted 7079/8477 = 83%, 619 KB/s], Decompressed: 7072 Downloaded: 7117 file(s) [attempted 7117/8477 = 83%, 192 KB/s], Decompressed: 7110 Downloaded: 7155 file(s) [attempted 7155/8477 = 84%, 77 KB/s], Decompressed: 7147 Downloaded: 7196 file(s) [attempted 7196/8477 = 84%, 39 KB/s], Decompressed: 7192 Downloaded: 7236 file(s) [attempted 7236/8477 = 85%, 290 KB/s], Decompressed: 7233 Downloaded: 7274 file(s) [attempted 7274/8477 = 85%, 37 KB/s], Decompressed: 7267 Downloaded: 7315 file(s) [attempted 7315/8477 = 86%, 553 KB/s], Decompressed: 7312 Downloaded: 7353 file(s) [attempted 7353/8477 = 86%, 390 KB/s], Decompressed: 7349 Downloaded: 7394 file(s) [attempted 7394/8477 = 87%, 41 KB/s], Decompressed: 7390 Downloaded: 7435 file(s) [attempted 7435/8477 = 87%, 118 KB/s], Decompressed: 7428 Downloaded: 7470 file(s) [attempted 7470/8477 = 88%, 129 KB/s], Decompressed: 7466 Downloaded: 7510 file(s) [attempted 7510/8477 = 88%, 458 KB/s], Decompressed: 7507 Downloaded: 7551 file(s) [attempted 7551/8477 = 89%, 128 KB/s], Decompressed: 7544 Downloaded: 7592 file(s) [attempted 7592/8477 = 89%, 126 KB/s], Decompressed: 7589 Downloaded: 7634 file(s) [attempted 7634/8477 = 90%, 33 KB/s], Decompressed: 7626 Downloaded: 7668 file(s) [attempted 7668/8477 = 90%, 108 KB/s], Decompressed: 7664 Downloaded: 7712 file(s) [attempted 7712/8477 = 90%, 993 KB/s], Decompressed: 7705 Downloaded: 7750 file(s) [attempted 7750/8477 = 91%, 132 KB/s], Decompressed: 7746 Downloaded: 7791 file(s) [attempted 7791/8477 = 91%, 296 KB/s], Decompressed: 7787 Downloaded: 7835 file(s) [attempted 7835/8477 = 92%, 235 KB/s], Decompressed: 7828 Downloaded: 7876 file(s) [attempted 7876/8477 = 92%, 486 KB/s], Decompressed: 7873 Downloaded: 7917 file(s) [attempted 7917/8477 = 93%, 249 KB/s], Decompressed: 7914 Downloaded: 7956 file(s) [attempted 7956/8477 = 93%, 261 KB/s], Decompressed: 7952 Downloaded: 7996 file(s) [attempted 7996/8477 = 94%, 147 KB/s], Decompressed: 7993 Downloaded: 8037 file(s) [attempted 8037/8477 = 94%, 691 KB/s], Decompressed: 8034 Downloaded: 8075 file(s) [attempted 8075/8477 = 95%, 734 KB/s], Decompressed: 8068 Downloaded: 8109 file(s) [attempted 8109/8477 = 95%, 139 KB/s], Decompressed: 8103 Downloaded: 8154 file(s) [attempted 8154/8477 = 96%, 1019 KB/s], Decompressed: 8147 Downloaded: 8195 file(s) [attempted 8195/8477 = 96%, 49 KB/s], Decompressed: 8191 Downloaded: 8239 file(s) [attempted 8239/8477 = 97%, 458 KB/s], Decompressed: 8236 Downloaded: 8273 file(s) [attempted 8273/8477 = 97%, 396 KB/s], Decompressed: 8266 Downloaded: 8311 file(s) [attempted 8311/8477 = 98%, 560 KB/s], Decompressed: 8308 Downloaded: 8352 file(s) [attempted 8352/8477 = 98%, 81 KB/s], Decompressed: 8349 Downloaded: 8396 file(s) [attempted 8396/8477 = 99%, 203 KB/s], Decompressed: 8393 Downloaded: 8441 file(s) [attempted 8441/8477 = 99%, 220 KB/s], Decompressed: 8434 Downloaded: 8475 file(s) [attempted 8475/8477 = 99%, 78 KB/s], Decompressed: 8472 Downloaded: 8477 file(s) [attempted 8477/8477 = 100%, 78 KB/s], Decompressed: 8472
lean_checker exit 0
lake build
Build completed successfully (4009 jobs).
blueprint_build exit 1
lake build :blueprint
error: unknown package facet `blueprint`
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh
lean semantic helper: reusing cached response at .apodeixis/semantic-extraction.json