Verification run
Run 346
succeeded commit
4445261e2486 toolchain lean-v4-30-0 prover lean took 2m 15s · finished 5w 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
lake_cache exit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache Decompressed 8459 file(s) Already decompressed 8459 file(s)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes Downloaded: 1 file(s) [attempted 1/8459 = 0%, 9 KB/s], Decompressed: 0 Downloaded: 16 file(s) [attempted 16/8459 = 0%, 4 KB/s], Decompressed: 14 Downloaded: 39 file(s) [attempted 39/8459 = 0%, 28 KB/s], Decompressed: 36 Downloaded: 67 file(s) [attempted 67/8459 = 0%, 44 KB/s], Decompressed: 63 Downloaded: 90 file(s) [attempted 90/8459 = 1%, 299 KB/s], Decompressed: 86 Downloaded: 127 file(s) [attempted 127/8459 = 1%, 265 KB/s], Decompressed: 121 Downloaded: 162 file(s) [attempted 162/8459 = 1%, 126 KB/s], Decompressed: 158 Downloaded: 200 file(s) [attempted 200/8459 = 2%, 488 KB/s], Decompressed: 196 Downloaded: 240 file(s) [attempted 240/8459 = 2%, 993 KB/s], Decompressed: 234 Downloaded: 282 file(s) [attempted 282/8459 = 3%, 181 KB/s], Decompressed: 271 Downloaded: 319 file(s) [attempted 319/8459 = 3%, 467 KB/s], Decompressed: 312 Downloaded: 360 file(s) [attempted 360/8459 = 4%, 430 KB/s], Decompressed: 353 Downloaded: 401 file(s) [attempted 401/8459 = 4%, 110 KB/s], Decompressed: 395 Downloaded: 443 file(s) [attempted 443/8459 = 5%, 253 KB/s], Decompressed: 439 Downloaded: 486 file(s) [attempted 486/8459 = 5%, 401 KB/s], Decompressed: 477 Downloaded: 518 file(s) [attempted 518/8459 = 6%, 1526 KB/s], Decompressed: 511 Downloaded: 559 file(s) [attempted 559/8459 = 6%, 243 KB/s], Decompressed: 556 Downloaded: 604 file(s) [attempted 604/8459 = 7%, 27 KB/s], Decompressed: 597 Downloaded: 645 file(s) [attempted 645/8459 = 7%, 154 KB/s], Decompressed: 641 Downloaded: 689 file(s) [attempted 689/8459 = 8%, 250 KB/s], Decompressed: 686 Downloaded: 732 file(s) [attempted 732/8459 = 8%, 458 KB/s], Decompressed: 723 Downloaded: 771 file(s) [attempted 771/8459 = 9%, 357 KB/s], Decompressed: 765 Downloaded: 809 file(s) [attempted 809/8459 = 9%, 306 KB/s], Decompressed: 802 Downloaded: 850 file(s) [attempted 850/8459 = 10%, 112 KB/s], Decompressed: 847 Downloaded: 893 file(s) [attempted 893/8459 = 10%, 77 KB/s], Decompressed: 888 Downloaded: 934 file(s) [attempted 934/8459 = 11%, 79 KB/s], Decompressed: 929 Downloaded: 970 file(s) [attempted 970/8459 = 11%, 61 KB/s], Decompressed: 968 Downloaded: 1011 file(s) [attempted 1011/8459 = 11%, 905 KB/s], Decompressed: 1008 Downloaded: 1052 file(s) [attempted 1052/8459 = 12%, 626 KB/s], Decompressed: 1049 Downloaded: 1093 file(s) [attempted 1093/8459 = 12%, 604 KB/s], Decompressed: 1090 Downloaded: 1141 file(s) [attempted 1141/8459 = 13%, 120 KB/s], Decompressed: 1134 Downloaded: 1182 file(s) [attempted 1182/8459 = 13%, 126 KB/s], Decompressed: 1179 Downloaded: 1217 file(s) [attempted 1217/8459 = 14%, 141 KB/s], Decompressed: 1213 Downloaded: 1261 file(s) [attempted 1261/8459 = 14%, 285 KB/s], Decompressed: 1258 Downloaded: 1299 file(s) [attempted 1299/8459 = 15%, 451 KB/s], Decompressed: 1295 Downloaded: 1346 file(s) [attempted 1346/8459 = 15%, 169 KB/s], Decompressed: 1343 Downloaded: 1391 file(s) [attempted 1391/8459 = 16%, 401 KB/s], Decompressed: 1384 Downloaded: 1426 file(s) [attempted 1426/8459 = 16%, 181 KB/s], Decompressed: 1418 Downloaded: 1466 file(s) [attempted 1466/8459 = 17%, 76 KB/s], Decompressed: 1463 Downloaded: 1507 file(s) [attempted 1507/8459 = 17%, 2676 KB/s], Decompressed: 1500 Downloaded: 1549 file(s) [attempted 1549/8459 = 18%, 61 KB/s], Decompressed: 1545 Downloaded: 1589 file(s) [attempted 1589/8459 = 18%, 34 KB/s], Decompressed: 1586 Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 201 KB/s], Decompressed: 1624 Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 442 KB/s], Decompressed: 1665 Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 202 KB/s], Decompressed: 1709 Downloaded: 1754 file(s) [attempted 1754/8459 = 20%, 276 KB/s], Decompressed: 1750 Downloaded: 1798 file(s) [attempted 1798/8459 = 21%, 36 KB/s], Decompressed: 1795 Downloaded: 1836 file(s) [attempted 1836/8459 = 21%, 322 KB/s], Decompressed: 1832 Downloaded: 1874 file(s) [attempted 1874/8459 = 22%, 280 KB/s], Decompressed: 1870 Downloaded: 1918 file(s) [attempted 1918/8459 = 22%, 5410 KB/s], Decompressed: 1915 Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 130 KB/s], Decompressed: 1956 Downloaded: 2000 file(s) [attempted 2000/8459 = 23%, 521 KB/s], Decompressed: 1997 Downloaded: 2038 file(s) [attempted 2038/8459 = 24%, 35 KB/s], Decompressed: 2034 Downloaded: 2072 file(s) [attempted 2072/8459 = 24%, 116 KB/s], Decompressed: 2069 Downloaded: 2110 file(s) [attempted 2110/8459 = 24%, 364 KB/s], Decompressed: 2106 Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 510 KB/s], Decompressed: 2151 Downloaded: 2202 file(s) [attempted 2202/8459 = 26%, 451 KB/s], Decompressed: 2199 Downloaded: 2250 file(s) [attempted 2250/8459 = 26%, 711 KB/s], Decompressed: 2247 Downloaded: 2295 file(s) [attempted 2295/8459 = 27%, 154 KB/s], Decompressed: 2291 Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 289 KB/s], Decompressed: 2329 Downloaded: 2366 file(s) [attempted 2366/8459 = 27%, 83 KB/s], Decompressed: 2363 Downloaded: 2407 file(s) [attempted 2407/8459 = 28%, 128 KB/s], Decompressed: 2404 Downloaded: 2448 file(s) [attempted 2448/8459 = 28%, 65 KB/s], Decompressed: 2445 Downloaded: 2493 file(s) [attempted 2493/8459 = 29%, 82 KB/s], Decompressed: 2490 Downloaded: 2528 file(s) [attempted 2528/8459 = 29%, 99 KB/s], Decompressed: 2524 Downloaded: 2566 file(s) [attempted 2566/8459 = 30%, 333 KB/s], Decompressed: 2561 Downloaded: 2606 file(s) [attempted 2606/8459 = 30%, 2294 KB/s], Decompressed: 2602 Downloaded: 2647 file(s) [attempted 2647/8459 = 31%, 610 KB/s], Decompressed: 2644 Downloaded: 2691 file(s) [attempted 2691/8459 = 31%, 57 KB/s], Decompressed: 2685 Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 301 KB/s], Decompressed: 2726 Downloaded: 2763 file(s) [attempted 2763/8459 = 32%, 156 KB/s], Decompressed: 2760 Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 69 KB/s], Decompressed: 2801 Downloaded: 2845 file(s) [attempted 2845/8459 = 33%, 524 KB/s], Decompressed: 2839 Downloaded: 2887 file(s) [attempted 2887/8459 = 34%, 322 KB/s], Decompressed: 2880 Downloaded: 2922 file(s) [attempted 2922/8459 = 34%, 33 KB/s], Decompressed: 2917 Downloaded: 2965 file(s) [attempted 2965/8459 = 35%, 193 KB/s], Decompressed: 2962 Downloaded: 3013 file(s) [attempted 3013/8459 = 35%, 1188 KB/s], Decompressed: 3010 Downloaded: 3061 file(s) [attempted 3061/8459 = 36%, 215 KB/s], Decompressed: 3055 Downloaded: 3099 file(s) [attempted 3099/8459 = 36%, 115 KB/s], Decompressed: 3095 Downloaded: 3142 file(s) [attempted 3142/8459 = 37%, 58 KB/s], Decompressed: 3136 Downloaded: 3179 file(s) [attempted 3179/8459 = 37%, 368 KB/s], Decompressed: 3174 Downloaded: 3220 file(s) [attempted 3220/8459 = 38%, 443 KB/s], Decompressed: 3215 Downloaded: 3260 file(s) [attempted 3260/8459 = 38%, 414 KB/s], Decompressed: 3256 Downloaded: 3304 file(s) [attempted 3304/8459 = 39%, 780 KB/s], Decompressed: 3301 Downloaded: 3346 file(s) [attempted 3346/8459 = 39%, 370 KB/s], Decompressed: 3342 Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 98 KB/s], Decompressed: 3379 Downloaded: 3424 file(s) [attempted 3424/8459 = 40%, 314 KB/s], Decompressed: 3417 Downloaded: 3465 file(s) [attempted 3465/8459 = 40%, 609 KB/s], Decompressed: 3461 Downloaded: 3507 file(s) [attempted 3507/8459 = 41%, 164 KB/s], Decompressed: 3499 Downloaded: 3547 file(s) [attempted 3547/8459 = 41%, 24 KB/s], Decompressed: 3540 Downloaded: 3585 file(s) [attempted 3585/8459 = 42%, 827 KB/s], Decompressed: 3581 Downloaded: 3622 file(s) [attempted 3622/8459 = 42%, 780 KB/s], Decompressed: 3615 Downloaded: 3667 file(s) [attempted 3667/8459 = 43%, 595 KB/s], Decompressed: 3663 Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 171 KB/s], Decompressed: 3704 Downloaded: 3753 file(s) [attempted 3753/8459 = 44%, 462 KB/s], Decompressed: 3749 Downloaded: 3796 file(s) [attempted 3796/8459 = 44%, 307 KB/s], Decompressed: 3790 Downloaded: 3832 file(s) [attempted 3832/8459 = 45%, 25 KB/s], Decompressed: 3828 Downloaded: 3872 file(s) [attempted 3872/8459 = 45%, 1252 KB/s], Decompressed: 3869 Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 120 KB/s], Decompressed: 3910 Downloaded: 3955 file(s) [attempted 3955/8459 = 46%, 338 KB/s], Decompressed: 3953 Downloaded: 3995 file(s) [attempted 3995/8459 = 47%, 125 KB/s], Decompressed: 3992 Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 779 KB/s], Decompressed: 4036 Downloaded: 4074 file(s) [attempted 4074/8459 = 48%, 457 KB/s], Decompressed: 4071 Downloaded: 4115 file(s) [attempted 4115/8459 = 48%, 36 KB/s], Decompressed: 4108 Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 255 KB/s], Decompressed: 4153 Downloaded: 4201 file(s) [attempted 4201/8459 = 49%, 624 KB/s], Decompressed: 4197 Downloaded: 4239 file(s) [attempted 4239/8459 = 50%, 379 KB/s], Decompressed: 4235 Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 337 KB/s], Decompressed: 4273 Downloaded: 4314 file(s) [attempted 4314/8459 = 50%, 448 KB/s], Decompressed: 4310 Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 1163 KB/s], Decompressed: 4356 Downloaded: 4399 file(s) [attempted 4399/8459 = 52%, 182 KB/s], Decompressed: 4392 Downloaded: 4440 file(s) [attempted 4440/8459 = 52%, 270 KB/s], Decompressed: 4433 Downloaded: 4481 file(s) [attempted 4481/8459 = 52%, 671 KB/s], Decompressed: 4474 Downloaded: 4519 file(s) [attempted 4519/8459 = 53%, 560 KB/s], Decompressed: 4516 Downloaded: 4563 file(s) [attempted 4563/8459 = 53%, 332 KB/s], Decompressed: 4560 Downloaded: 4608 file(s) [attempted 4608/8459 = 54%, 116 KB/s], Decompressed: 4605 Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 61 KB/s], Decompressed: 4642 Downloaded: 4690 file(s) [attempted 4690/8459 = 55%, 98 KB/s], Decompressed: 4683 Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 95 KB/s], Decompressed: 4728 Downloaded: 4772 file(s) [attempted 4772/8459 = 56%, 331 KB/s], Decompressed: 4769 Downloaded: 4814 file(s) [attempted 4814/8459 = 56%, 210 KB/s], Decompressed: 4810 Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 63 KB/s], Decompressed: 4851 Downloaded: 4896 file(s) [attempted 4896/8459 = 57%, 90 KB/s], Decompressed: 4892 Downloaded: 4937 file(s) [attempted 4937/8459 = 58%, 24 KB/s], Decompressed: 4933 Downloaded: 4979 file(s) [attempted 4979/8459 = 58%, 124 KB/s], Decompressed: 4974 Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 132 KB/s], Decompressed: 5015 Downloaded: 5063 file(s) [attempted 5063/8459 = 59%, 397 KB/s], Decompressed: 5060 Downloaded: 5104 file(s) [attempted 5104/8459 = 60%, 746 KB/s], Decompressed: 5101 Downloaded: 5145 file(s) [attempted 5145/8459 = 60%, 126 KB/s], Decompressed: 5138 Downloaded: 5184 file(s) [attempted 5184/8459 = 61%, 69 KB/s], Decompressed: 5176 Downloaded: 5224 file(s) [attempted 5224/8459 = 61%, 47 KB/s], Decompressed: 5221 Downloaded: 5265 file(s) [attempted 5265/8459 = 62%, 444 KB/s], Decompressed: 5258 Downloaded: 5306 file(s) [attempted 5306/8459 = 62%, 382 KB/s], Decompressed: 5303 Downloaded: 5351 file(s) [attempted 5351/8459 = 63%, 138 KB/s], Decompressed: 5344 Downloaded: 5388 file(s) [attempted 5388/8459 = 63%, 227 KB/s], Decompressed: 5385 Downloaded: 5423 file(s) [attempted 5423/8459 = 64%, 654 KB/s], Decompressed: 5419 Downloaded: 5465 file(s) [attempted 5465/8459 = 64%, 137 KB/s], Decompressed: 5460 Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 1249 KB/s], Decompressed: 5498 Downloaded: 5546 file(s) [attempted 5546/8459 = 65%, 229 KB/s], Decompressed: 5542 Downloaded: 5580 file(s) [attempted 5580/8459 = 65%, 110 KB/s], Decompressed: 5573 Downloaded: 5621 file(s) [attempted 5621/8459 = 66%, 202 KB/s], Decompressed: 5618 Downloaded: 5662 file(s) [attempted 5662/8459 = 66%, 166 KB/s], Decompressed: 5659 Downloaded: 5703 file(s) [attempted 5703/8459 = 67%, 68 KB/s], Decompressed: 5700 Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 39 KB/s], Decompressed: 5741 Downloaded: 5779 file(s) [attempted 5779/8459 = 68%, 61 KB/s], Decompressed: 5775 Downloaded: 5820 file(s) [attempted 5820/8459 = 68%, 213 KB/s], Decompressed: 5816 Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 114 KB/s], Decompressed: 5863 Downloaded: 5905 file(s) [attempted 5905/8459 = 69%, 611 KB/s], Decompressed: 5902 Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 103 KB/s], Decompressed: 5939 Downloaded: 5982 file(s) [attempted 5982/8459 = 70%, 1540 KB/s], Decompressed: 5977 Downloaded: 6022 file(s) [attempted 6022/8459 = 71%, 221 KB/s], Decompressed: 6018 Downloaded: 6066 file(s) [attempted 6066/8459 = 71%, 399 KB/s], Decompressed: 6059 Downloaded: 6107 file(s) [attempted 6107/8459 = 72%, 312 KB/s], Decompressed: 6104 Downloaded: 6151 file(s) [attempted 6151/8459 = 72%, 392 KB/s], Decompressed: 6141 Downloaded: 6193 file(s) [attempted 6193/8459 = 73%, 801 KB/s], Decompressed: 6189 Downloaded: 6231 file(s) [attempted 6231/8459 = 73%, 1002 KB/s], Decompressed: 6227 Downloaded: 6273 file(s) [attempted 6273/8459 = 74%, 167 KB/s], Decompressed: 6268 Downloaded: 6309 file(s) [attempted 6309/8459 = 74%, 166 KB/s], Decompressed: 6305 Downloaded: 6347 file(s) [attempted 6347/8459 = 75%, 30 KB/s], Decompressed: 6340 Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 830 KB/s], Decompressed: 6384 Downloaded: 6432 file(s) [attempted 6432/8459 = 76%, 154 KB/s], Decompressed: 6429 Downloaded: 6477 file(s) [attempted 6477/8459 = 76%, 95 KB/s], Decompressed: 6473 Downloaded: 6524 file(s) [attempted 6524/8459 = 77%, 114 KB/s], Decompressed: 6518 Downloaded: 6562 file(s) [attempted 6562/8459 = 77%, 734 KB/s], Decompressed: 6559 Downloaded: 6603 file(s) [attempted 6603/8459 = 78%, 71 KB/s], Decompressed: 6596 Downloaded: 6644 file(s) [attempted 6644/8459 = 78%, 134 KB/s], Decompressed: 6641 Downloaded: 6682 file(s) [attempted 6682/8459 = 78%, 344 KB/s], Decompressed: 6678 Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 154 KB/s], Decompressed: 6720 Downloaded: 6771 file(s) [attempted 6771/8459 = 80%, 318 KB/s], Decompressed: 6761 Downloaded: 6805 file(s) [attempted 6805/8459 = 80%, 532 KB/s], Decompressed: 6802 Downloaded: 6844 file(s) [attempted 6844/8459 = 80%, 238 KB/s], Decompressed: 6839 Downloaded: 6884 file(s) [attempted 6884/8459 = 81%, 674 KB/s], Decompressed: 6880 Downloaded: 6928 file(s) [attempted 6928/8459 = 81%, 92 KB/s], Decompressed: 6925 Downloaded: 6967 file(s) [attempted 6967/8459 = 82%, 189 KB/s], Decompressed: 6959 Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 369 KB/s], Decompressed: 7000 Downloaded: 7045 file(s) [attempted 7045/8459 = 83%, 184 KB/s], Decompressed: 7041 Downloaded: 7089 file(s) [attempted 7089/8459 = 83%, 576 KB/s], Decompressed: 7086 Downloaded: 7134 file(s) [attempted 7134/8459 = 84%, 145 KB/s], Decompressed: 7130 Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 32 KB/s], Decompressed: 7171 Downloaded: 7219 file(s) [attempted 7219/8459 = 85%, 193 KB/s], Decompressed: 7212 Downloaded: 7257 file(s) [attempted 7257/8459 = 85%, 379 KB/s], Decompressed: 7247 Downloaded: 7295 file(s) [attempted 7295/8459 = 86%, 37 KB/s], Decompressed: 7291 Downloaded: 7336 file(s) [attempted 7336/8459 = 86%, 384 KB/s], Decompressed: 7332 Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 646 KB/s], Decompressed: 7379 Downloaded: 7426 file(s) [attempted 7426/8459 = 87%, 957 KB/s], Decompressed: 7418 Downloaded: 7459 file(s) [attempted 7459/8459 = 88%, 815 KB/s], Decompressed: 7455 Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 295 KB/s], Decompressed: 7497 Downloaded: 7538 file(s) [attempted 7538/8459 = 89%, 534 KB/s], Decompressed: 7534 Downloaded: 7582 file(s) [attempted 7582/8459 = 89%, 30 KB/s], Decompressed: 7579 Downloaded: 7625 file(s) [attempted 7625/8459 = 90%, 1047 KB/s], Decompressed: 7616 Downloaded: 7659 file(s) [attempted 7659/8459 = 90%, 478 KB/s], Decompressed: 7650 Downloaded: 7698 file(s) [attempted 7698/8459 = 91%, 61 KB/s], Decompressed: 7695 Downloaded: 7743 file(s) [attempted 7743/8459 = 91%, 194 KB/s], Decompressed: 7739 Downloaded: 7787 file(s) [attempted 7787/8459 = 92%, 249 KB/s], Decompressed: 7780 Downloaded: 7828 file(s) [attempted 7828/8459 = 92%, 720 KB/s], Decompressed: 7825 Downloaded: 7869 file(s) [attempted 7869/8459 = 93%, 1829 KB/s], Decompressed: 7866 Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 826 KB/s], Decompressed: 7904 Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 1001 KB/s], Decompressed: 7945 Downloaded: 7989 file(s) [attempted 7989/8459 = 94%, 230 KB/s], Decompressed: 7982 Downloaded: 8034 file(s) [attempted 8034/8459 = 94%, 154 KB/s], Decompressed: 8030 Downloaded: 8078 file(s) [attempted 8078/8459 = 95%, 881 KB/s], Decompressed: 8071 Downloaded: 8112 file(s) [attempted 8112/8459 = 95%, 297 KB/s], Decompressed: 8109 Downloaded: 8153 file(s) [attempted 8153/8459 = 96%, 205 KB/s], Decompressed: 8151 Downloaded: 8195 file(s) [attempted 8195/8459 = 96%, 372 KB/s], Decompressed: 8191 Downloaded: 8239 file(s) [attempted 8239/8459 = 97%, 54 KB/s], Decompressed: 8232 Downloaded: 8277 file(s) [attempted 8277/8459 = 97%, 745 KB/s], Decompressed: 8266 Downloaded: 8314 file(s) [attempted 8314/8459 = 98%, 54 KB/s], Decompressed: 8311 Downloaded: 8355 file(s) [attempted 8355/8459 = 98%, 446 KB/s], Decompressed: 8352 Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 133 KB/s], Decompressed: 8393 Downloaded: 8435 file(s) [attempted 8435/8459 = 99%, 730 KB/s], Decompressed: 8427 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 500 KB/s], Decompressed: 8455 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 500 KB/s], Decompressed: 8455
git_clone exit 0
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-434-source
Cloning into '/var/lib/apodeixis/repos/job-434-source'...
git_checkout exit 128
git checkout 4445261e2486aeba78303822dbc533a70f82cd5c
fatal: reference is not a tree: 4445261e2486aeba78303822dbc533a70f82cd5c
git_checkout exit 0
git fetch --depth 1 origin 4445261e2486aeba78303822dbc533a70f82cd5c
From https://github.com/promachina/iut-lean * branch 4445261e2486aeba78303822dbc533a70f82cd5c -> FETCH_HEAD
git_checkout exit 0
git checkout 4445261e2486aeba78303822dbc533a70f82cd5c (after fetch)
Note: switching to '4445261e2486aeba78303822dbc533a70f82cd5c'. 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 4445261 Add nonzero scalar multiplication hull source
lean_checker exit 0
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) [0x767a823c6785] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x767a823bdb27] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x767a823bdc0b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x767a822f3c62] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x767a822f4439] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x767a823caf99] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x767a82232923] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x767a82232b2b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x767a82233827] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x767a822341b6] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x767a823c9e8b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x767a82015adb] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x767a823c9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x767a823c9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x767a8239b1f3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x767a82015c92] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x767a7d422638] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x767a7d20cd2e] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x767a7cd69a82] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x767a7cd69f0e] /lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x767a79c4524a] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x767a79c45305] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x6018a32268da] Build completed successfully (3416 jobs).
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
blueprint_build exit 1
lake build :blueprint
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes error: unknown package facet `blueprint`