Verification run
Run 359
succeededcommit
4dbaeefd0b23toolchain lean-v4-30-0prover leantook 3h 10m · finished 12w agoPackage 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_cloneexit 0
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-537-source
Cloning into '/var/lib/apodeixis/repos/job-537-source'...
git_checkoutexit 128
git checkout 4dbaeefd0b2318363be5f0e8efd077d6497c387d
fatal: reference is not a tree: 4dbaeefd0b2318363be5f0e8efd077d6497c387d
git_checkoutexit 0
git fetch --depth 1 origin 4dbaeefd0b2318363be5f0e8efd077d6497c387d
From https://github.com/promachina/iut-lean * branch 4dbaeefd0b2318363be5f0e8efd077d6497c387d -> FETCH_HEAD
git_checkoutexit 0
git checkout 4dbaeefd0b2318363be5f0e8efd077d6497c387d (after fetch)
Note: switching to '4dbaeefd0b2318363be5f0e8efd077d6497c387d'. 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 4dbaeef Project local log factors through product coordinates
lake_cacheexit 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%, 14 KB/s], Decompressed: 0 Downloaded: 16 file(s) [attempted 16/8459 = 0%, 23 KB/s], Decompressed: 13 Downloaded: 42 file(s) [attempted 42/8459 = 0%, 86 KB/s], Decompressed: 41 Downloaded: 65 file(s) [attempted 65/8459 = 0%, 44 KB/s], Decompressed: 61 Downloaded: 100 file(s) [attempted 100/8459 = 1%, 321 KB/s], Decompressed: 75 Downloaded: 134 file(s) [attempted 134/8459 = 1%, 260 KB/s], Decompressed: 75 Downloaded: 169 file(s) [attempted 169/8459 = 1%, 678 KB/s], Decompressed: 162 Downloaded: 206 file(s) [attempted 206/8459 = 2%, 31 KB/s], Decompressed: 186 Downloaded: 247 file(s) [attempted 247/8459 = 2%, 24 KB/s], Decompressed: 186 Downloaded: 292 file(s) [attempted 292/8459 = 3%, 96 KB/s], Decompressed: 288 Downloaded: 329 file(s) [attempted 329/8459 = 3%, 301 KB/s], Decompressed: 326 Downloaded: 371 file(s) [attempted 371/8459 = 4%, 277 KB/s], Decompressed: 367 Downloaded: 408 file(s) [attempted 408/8459 = 4%, 60 KB/s], Decompressed: 405 Downloaded: 443 file(s) [attempted 443/8459 = 5%, 1724 KB/s], Decompressed: 439 Downloaded: 487 file(s) [attempted 487/8459 = 5%, 281 KB/s], Decompressed: 480 Downloaded: 529 file(s) [attempted 529/8459 = 6%, 269 KB/s], Decompressed: 525 Downloaded: 570 file(s) [attempted 570/8459 = 6%, 23 KB/s], Decompressed: 566 Downloaded: 610 file(s) [attempted 610/8459 = 7%, 135 KB/s], Decompressed: 603 Downloaded: 648 file(s) [attempted 648/8459 = 7%, 133 KB/s], Decompressed: 614 Downloaded: 682 file(s) [attempted 682/8459 = 8%, 569 KB/s], Decompressed: 614 Downloaded: 730 file(s) [attempted 730/8459 = 8%, 71 KB/s], Decompressed: 727 Downloaded: 775 file(s) [attempted 775/8459 = 9%, 195 KB/s], Decompressed: 768 Downloaded: 816 file(s) [attempted 816/8459 = 9%, 107 KB/s], Decompressed: 812 Downloaded: 857 file(s) [attempted 857/8459 = 10%, 122 KB/s], Decompressed: 854 Downloaded: 898 file(s) [attempted 898/8459 = 10%, 184 KB/s], Decompressed: 891 Downloaded: 932 file(s) [attempted 932/8459 = 11%, 1001 KB/s], Decompressed: 929 Downloaded: 977 file(s) [attempted 977/8459 = 11%, 753 KB/s], Decompressed: 973 Downloaded: 1018 file(s) [attempted 1018/8459 = 12%, 238 KB/s], Decompressed: 1015 Downloaded: 1059 file(s) [attempted 1059/8459 = 12%, 141 KB/s], Decompressed: 1052 Downloaded: 1097 file(s) [attempted 1097/8459 = 12%, 694 KB/s], Decompressed: 1090 Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 70 KB/s], Decompressed: 1127 Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 770 KB/s], Decompressed: 1127 Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 380 KB/s], Decompressed: 1131 Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 204 KB/s], Decompressed: 1240 Downloaded: 1299 file(s) [attempted 1299/8459 = 15%, 214 KB/s], Decompressed: 1295 Downloaded: 1340 file(s) [attempted 1340/8459 = 15%, 1157 KB/s], Decompressed: 1336 Downloaded: 1379 file(s) [attempted 1379/8459 = 16%, 198 KB/s], Decompressed: 1374 Downloaded: 1422 file(s) [attempted 1422/8459 = 16%, 81 KB/s], Decompressed: 1415 Downloaded: 1456 file(s) [attempted 1456/8459 = 17%, 226 KB/s], Decompressed: 1449 Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 246 KB/s], Decompressed: 1494 Downloaded: 1542 file(s) [attempted 1542/8459 = 18%, 330 KB/s], Decompressed: 1538 Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 141 KB/s], Decompressed: 1579 Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 1701 KB/s], Decompressed: 1613 Downloaded: 1666 file(s) [attempted 1666/8459 = 19%, 451 KB/s], Decompressed: 1651 Downloaded: 1699 file(s) [attempted 1699/8459 = 20%, 468 KB/s], Decompressed: 1696 Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 89 KB/s], Decompressed: 1740 Downloaded: 1788 file(s) [attempted 1788/8459 = 21%, 262 KB/s], Decompressed: 1785 Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 689 KB/s], Decompressed: 1788 Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 283 KB/s], Decompressed: 1788 Downloaded: 1901 file(s) [attempted 1901/8459 = 22%, 539 KB/s], Decompressed: 1897 Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 425 KB/s], Decompressed: 1939 Downloaded: 1986 file(s) [attempted 1986/8459 = 23%, 122 KB/s], Decompressed: 1976 Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 51 KB/s], Decompressed: 2021 Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 127 KB/s], Decompressed: 2058 Downloaded: 2106 file(s) [attempted 2106/8459 = 24%, 457 KB/s], Decompressed: 2103 Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 172 KB/s], Decompressed: 2147 Downloaded: 2196 file(s) [attempted 2196/8459 = 25%, 328 KB/s], Decompressed: 2192 Downloaded: 2239 file(s) [attempted 2239/8459 = 26%, 119 KB/s], Decompressed: 2229 Downloaded: 2274 file(s) [attempted 2274/8459 = 26%, 889 KB/s], Decompressed: 2271 Downloaded: 2315 file(s) [attempted 2315/8459 = 27%, 35 KB/s], Decompressed: 2305 Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 334 KB/s], Decompressed: 2349 Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 318 KB/s], Decompressed: 2390 Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 470 KB/s], Decompressed: 2425 Downloaded: 2469 file(s) [attempted 2469/8459 = 29%, 470 KB/s], Decompressed: 2462 Downloaded: 2507 file(s) [attempted 2507/8459 = 29%, 151 KB/s], Decompressed: 2503 Downloaded: 2551 file(s) [attempted 2551/8459 = 30%, 101 KB/s], Decompressed: 2548 Downloaded: 2592 file(s) [attempted 2592/8459 = 30%, 365 KB/s], Decompressed: 2585 Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 23 KB/s], Decompressed: 2623 Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 169 KB/s], Decompressed: 2657 Downloaded: 2705 file(s) [attempted 2705/8459 = 31%, 478 KB/s], Decompressed: 2678 Downloaded: 2750 file(s) [attempted 2750/8459 = 32%, 126 KB/s], Decompressed: 2678 Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 767 KB/s], Decompressed: 2685 Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 560 KB/s], Decompressed: 2685 Downloaded: 2863 file(s) [attempted 2863/8459 = 33%, 243 KB/s], Decompressed: 2685 Downloaded: 2904 file(s) [attempted 2904/8459 = 34%, 929 KB/s], Decompressed: 2685 Downloaded: 2948 file(s) [attempted 2948/8459 = 34%, 2450 KB/s], Decompressed: 2685 Downloaded: 2993 file(s) [attempted 2993/8459 = 35%, 198 KB/s], Decompressed: 2685 Downloaded: 3038 file(s) [attempted 3038/8459 = 35%, 297 KB/s], Decompressed: 2760 Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 229 KB/s], Decompressed: 2760 Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 691 KB/s], Decompressed: 3109 Downloaded: 3153 file(s) [attempted 3153/8459 = 37%, 535 KB/s], Decompressed: 3150 Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 86 KB/s], Decompressed: 3191 Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 194 KB/s], Decompressed: 3229 Downloaded: 3284 file(s) [attempted 3284/8459 = 38%, 222 KB/s], Decompressed: 3273 Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 86 KB/s], Decompressed: 3304 Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 274 KB/s], Decompressed: 3349 Downloaded: 3398 file(s) [attempted 3398/8459 = 40%, 827 KB/s], Decompressed: 3390 Downloaded: 3441 file(s) [attempted 3441/8459 = 40%, 67 KB/s], Decompressed: 3438 Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 194 KB/s], Decompressed: 3472 Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 70 KB/s], Decompressed: 3472 Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 706 KB/s], Decompressed: 3482 Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 120 KB/s], Decompressed: 3595 Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 205 KB/s], Decompressed: 3595 Downloaded: 3691 file(s) [attempted 3691/8459 = 43%, 196 KB/s], Decompressed: 3598 Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 402 KB/s], Decompressed: 3715 Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 636 KB/s], Decompressed: 3756 Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 49 KB/s], Decompressed: 3804 Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 419 KB/s], Decompressed: 3841 Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 332 KB/s], Decompressed: 3886 Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 230 KB/s], Decompressed: 3896 Downloaded: 3971 file(s) [attempted 3971/8459 = 46%, 447 KB/s], Decompressed: 3896 Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 47 KB/s], Decompressed: 3989 Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 137 KB/s], Decompressed: 4043 Downloaded: 4091 file(s) [attempted 4091/8459 = 48%, 1340 KB/s], Decompressed: 4084 Downloaded: 4136 file(s) [attempted 4136/8459 = 48%, 195 KB/s], Decompressed: 4084 Downloaded: 4173 file(s) [attempted 4173/8459 = 49%, 1131 KB/s], Decompressed: 4084 Downloaded: 4214 file(s) [attempted 4214/8459 = 49%, 925 KB/s], Decompressed: 4091 Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 883 KB/s], Decompressed: 4091 Downloaded: 4293 file(s) [attempted 4293/8459 = 50%, 592 KB/s], Decompressed: 4180 Downloaded: 4338 file(s) [attempted 4338/8459 = 51%, 219 KB/s], Decompressed: 4334 Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 845 KB/s], Decompressed: 4379 Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 136 KB/s], Decompressed: 4416 Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 112 KB/s], Decompressed: 4461 Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 195 KB/s], Decompressed: 4502 Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 437 KB/s], Decompressed: 4540 Downloaded: 4584 file(s) [attempted 4584/8459 = 54%, 163 KB/s], Decompressed: 4581 Downloaded: 4626 file(s) [attempted 4626/8459 = 54%, 155 KB/s], Decompressed: 4618 Downloaded: 4663 file(s) [attempted 4663/8459 = 55%, 1210 KB/s], Decompressed: 4652 Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 25 KB/s], Decompressed: 4697 Downloaded: 4748 file(s) [attempted 4748/8459 = 56%, 149 KB/s], Decompressed: 4736 Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 360 KB/s], Decompressed: 4786 Downloaded: 4834 file(s) [attempted 4834/8459 = 57%, 273 KB/s], Decompressed: 4827 Downloaded: 4868 file(s) [attempted 4868/8459 = 57%, 164 KB/s], Decompressed: 4861 Downloaded: 4909 file(s) [attempted 4909/8459 = 58%, 61 KB/s], Decompressed: 4882 Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 456 KB/s], Decompressed: 4947 Downloaded: 4991 file(s) [attempted 4991/8459 = 59%, 1094 KB/s], Decompressed: 4984 Downloaded: 5036 file(s) [attempted 5036/8459 = 59%, 209 KB/s], Decompressed: 5026 Downloaded: 5067 file(s) [attempted 5067/8459 = 59%, 284 KB/s], Decompressed: 5060 Downloaded: 5111 file(s) [attempted 5111/8459 = 60%, 152 KB/s], Decompressed: 5108 Downloaded: 5156 file(s) [attempted 5156/8459 = 60%, 1281 KB/s], Decompressed: 5145 Downloaded: 5193 file(s) [attempted 5193/8459 = 61%, 137 KB/s], Decompressed: 5190 Downloaded: 5238 file(s) [attempted 5238/8459 = 61%, 1642 KB/s], Decompressed: 5231 Downloaded: 5279 file(s) [attempted 5279/8459 = 62%, 304 KB/s], Decompressed: 5272 Downloaded: 5317 file(s) [attempted 5317/8459 = 62%, 1274 KB/s], Decompressed: 5310 Downloaded: 5357 file(s) [attempted 5357/8459 = 63%, 1074 KB/s], Decompressed: 5354 Downloaded: 5396 file(s) [attempted 5396/8459 = 63%, 493 KB/s], Decompressed: 5388 Downloaded: 5436 file(s) [attempted 5436/8459 = 64%, 274 KB/s], Decompressed: 5419 Downloaded: 5477 file(s) [attempted 5477/8459 = 64%, 68 KB/s], Decompressed: 5470 Downloaded: 5518 file(s) [attempted 5518/8459 = 65%, 448 KB/s], Decompressed: 5515 Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 132 KB/s], Decompressed: 5559 Downloaded: 5604 file(s) [attempted 5604/8459 = 66%, 289 KB/s], Decompressed: 5590 Downloaded: 5645 file(s) [attempted 5645/8459 = 66%, 548 KB/s], Decompressed: 5638 Downloaded: 5683 file(s) [attempted 5683/8459 = 67%, 133 KB/s], Decompressed: 5672 Downloaded: 5726 file(s) [attempted 5726/8459 = 67%, 485 KB/s], Decompressed: 5717 Downloaded: 5765 file(s) [attempted 5765/8459 = 68%, 762 KB/s], Decompressed: 5754 Downloaded: 5806 file(s) [attempted 5806/8459 = 68%, 119 KB/s], Decompressed: 5802 Downloaded: 5847 file(s) [attempted 5847/8459 = 69%, 133 KB/s], Decompressed: 5833 Downloaded: 5882 file(s) [attempted 5882/8459 = 69%, 51 KB/s], Decompressed: 5878 Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 732 KB/s], Decompressed: 5915 Downloaded: 5967 file(s) [attempted 5967/8459 = 70%, 96 KB/s], Decompressed: 5915 Downloaded: 6005 file(s) [attempted 6005/8459 = 70%, 1126 KB/s], Decompressed: 5915 Downloaded: 6045 file(s) [attempted 6045/8459 = 71%, 106 KB/s], Decompressed: 6035 Downloaded: 6086 file(s) [attempted 6086/8459 = 71%, 317 KB/s], Decompressed: 6076 Downloaded: 6127 file(s) [attempted 6127/8459 = 72%, 159 KB/s], Decompressed: 6121 Downloaded: 6172 file(s) [attempted 6172/8459 = 72%, 121 KB/s], Decompressed: 6162 Downloaded: 6210 file(s) [attempted 6210/8459 = 73%, 723 KB/s], Decompressed: 6206 Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 38 KB/s], Decompressed: 6220 Downloaded: 6299 file(s) [attempted 6299/8459 = 74%, 243 KB/s], Decompressed: 6220 Downloaded: 6340 file(s) [attempted 6340/8459 = 74%, 690 KB/s], Decompressed: 6336 Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 125 KB/s], Decompressed: 6379 Downloaded: 6422 file(s) [attempted 6422/8459 = 75%, 280 KB/s], Decompressed: 6408 Downloaded: 6459 file(s) [attempted 6459/8459 = 76%, 1493 KB/s], Decompressed: 6446 Downloaded: 6504 file(s) [attempted 6504/8459 = 76%, 101 KB/s], Decompressed: 6446 Downloaded: 6548 file(s) [attempted 6548/8459 = 77%, 109 KB/s], Decompressed: 6449 Downloaded: 6593 file(s) [attempted 6593/8459 = 77%, 469 KB/s], Decompressed: 6590 Downloaded: 6634 file(s) [attempted 6634/8459 = 78%, 374 KB/s], Decompressed: 6631 Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 80 KB/s], Decompressed: 6655 Downloaded: 6706 file(s) [attempted 6706/8459 = 79%, 476 KB/s], Decompressed: 6702 Downloaded: 6750 file(s) [attempted 6750/8459 = 79%, 48 KB/s], Decompressed: 6747 Downloaded: 6798 file(s) [attempted 6798/8459 = 80%, 205 KB/s], Decompressed: 6791 Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 545 KB/s], Decompressed: 6815 Downloaded: 6884 file(s) [attempted 6884/8459 = 81%, 2098 KB/s], Decompressed: 6860 Downloaded: 6917 file(s) [attempted 6917/8459 = 81%, 420 KB/s], Decompressed: 6901 Downloaded: 6956 file(s) [attempted 6956/8459 = 82%, 174 KB/s], Decompressed: 6952 Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 1929 KB/s], Decompressed: 6973 Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 1919 KB/s], Decompressed: 6973 Downloaded: 7075 file(s) [attempted 7075/8459 = 83%, 195 KB/s], Decompressed: 6987 Downloaded: 7120 file(s) [attempted 7120/8459 = 84%, 177 KB/s], Decompressed: 7113 Downloaded: 7164 file(s) [attempted 7164/8459 = 84%, 482 KB/s], Decompressed: 7158 Downloaded: 7206 file(s) [attempted 7206/8459 = 85%, 875 KB/s], Decompressed: 7202 Downloaded: 7247 file(s) [attempted 7247/8459 = 85%, 119 KB/s], Decompressed: 7243 Downloaded: 7284 file(s) [attempted 7284/8459 = 86%, 170 KB/s], Decompressed: 7277 Downloaded: 7325 file(s) [attempted 7325/8459 = 86%, 319 KB/s], Decompressed: 7318 Downloaded: 7370 file(s) [attempted 7370/8459 = 87%, 78 KB/s], Decompressed: 7366 Downloaded: 7411 file(s) [attempted 7411/8459 = 87%, 128 KB/s], Decompressed: 7404 Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 111 KB/s], Decompressed: 7442 Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 284 KB/s], Decompressed: 7486 Downloaded: 7527 file(s) [attempted 7527/8459 = 88%, 180 KB/s], Decompressed: 7514 Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 462 KB/s], Decompressed: 7514 Downloaded: 7616 file(s) [attempted 7616/8459 = 90%, 33 KB/s], Decompressed: 7609 Downloaded: 7655 file(s) [attempted 7655/8459 = 90%, 431 KB/s], Decompressed: 7650 Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 874 KB/s], Decompressed: 7692 Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 135 KB/s], Decompressed: 7726 Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 88 KB/s], Decompressed: 7767 Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 231 KB/s], Decompressed: 7811 Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 161 KB/s], Decompressed: 7863 Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 224 KB/s], Decompressed: 7900 Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 132 KB/s], Decompressed: 7945 Downloaded: 7993 file(s) [attempted 7993/8459 = 94%, 127 KB/s], Decompressed: 7986 Downloaded: 8024 file(s) [attempted 8024/8459 = 94%, 170 KB/s], Decompressed: 8020 Downloaded: 8071 file(s) [attempted 8071/8459 = 95%, 812 KB/s], Decompressed: 8068 Downloaded: 8116 file(s) [attempted 8116/8459 = 95%, 658 KB/s], Decompressed: 8109 Downloaded: 8153 file(s) [attempted 8153/8459 = 96%, 75 KB/s], Decompressed: 8150 Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 154 KB/s], Decompressed: 8195 Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 239 KB/s], Decompressed: 8215 Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 723 KB/s], Decompressed: 8215 Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 684 KB/s], Decompressed: 8321 Downloaded: 8369 file(s) [attempted 8369/8459 = 98%, 468 KB/s], Decompressed: 8362 Downloaded: 8405 file(s) [attempted 8405/8459 = 99%, 596 KB/s], Decompressed: 8396 Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 110 KB/s], Decompressed: 8438 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 110 KB/s], Decompressed: 8451
lean_checkerexit 0
lake build
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (433s) 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) [0x74ee3bbc6785] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x74ee3bbbdb27] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x74ee3bbbdc0b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x74ee3baf3c62] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x74ee3baf4439] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x74ee3bbcaf99] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x74ee3ba32923] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x74ee3ba32b2b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x74ee3ba33827] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x74ee3ba341b6] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x74ee3bbc9e8b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x74ee3b815adb] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x74ee3bbc9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x74ee3bbc9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x74ee3bb9b1f3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x74ee3b815c92] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x74ee36c22638] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x74ee36a0cd2e] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x74ee36569a82] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x74ee36569f0e] /lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x74ee3344524a] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x74ee33445305] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x62f14a8168da] ✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (28s) ✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.7s) ✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (37s) ✔ [3414/3416] Built Iut.Basic (2.9s) ✔ [3415/3416] Built Iut (2.7s) 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_buildexit 1
lake build :blueprint
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes error: unknown package facet `blueprint`
semantic_extractexit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)
apx-semantic-phase {"duration_ms":3,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":6,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":359673,"module_count":1,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":422,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":422,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":1,"diagnostic_count":0,"duration_ms":94,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":357494,"module_count":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":1,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1014,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1014,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":97,"diagnostic_count":15,"duration_ms":7638,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":358652,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":97,"diagnostic_count":15,"duration_ms":3,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1216278,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1216278,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":1890,"diagnostic_count":116,"duration_ms":1556132,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":369399,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":1890,"diagnostic_count":116,"duration_ms":111,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":43182777,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":27,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":43182777,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":7804,"diagnostic_count":3119,"duration_ms":6201167,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":432359,"module_count":1,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":7804,"diagnostic_count":3119,"duration_ms":568,"module_count":1,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase {"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":266651932,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":187,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":266651932,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":152,"diagnostic_count":23,"duration_ms":19930,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":687062,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":152,"diagnostic_count":23,"duration_ms":28,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase {"duration_ms":0,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1647482,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":7,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1647482,"phase":"lean_module_json_write"}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"core_compile","duration_ms":3493}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":997,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":21,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":4303,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache eb4ab944cd7296b3dd740e7a5c23f2d20af8c66ab56098012314a22d01cf18c9
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":10359244,"ok":true}