Verification run
Run 362
succeededcommit
c7cfbdfd1126toolchain lean-v4-30-0prover leantook 3h 31m · 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-554-source
Cloning into '/var/lib/apodeixis/repos/job-554-source'...
git_checkoutexit 128
git checkout c7cfbdfd1126573d6257b09294829e409f3a8107
fatal: reference is not a tree: c7cfbdfd1126573d6257b09294829e409f3a8107
git_checkoutexit 0
git fetch --depth 1 origin c7cfbdfd1126573d6257b09294829e409f3a8107
From https://github.com/promachina/iut-lean * branch c7cfbdfd1126573d6257b09294829e409f3a8107 -> FETCH_HEAD
git_checkoutexit 0
git checkout c7cfbdfd1126573d6257b09294829e409f3a8107 (after fetch)
Note: switching to 'c7cfbdfd1126573d6257b09294829e409f3a8107'. 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 c7cfbdf Back arbitrary q exact theta by hull obligations
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%, 10 KB/s], Decompressed: 0 Downloaded: 16 file(s) [attempted 16/8459 = 0%, 2 KB/s], Decompressed: 14 Downloaded: 41 file(s) [attempted 41/8459 = 0%, 13 KB/s], Decompressed: 37 Downloaded: 68 file(s) [attempted 68/8459 = 0%, 447 KB/s], Decompressed: 62 Downloaded: 93 file(s) [attempted 93/8459 = 1%, 493 KB/s], Decompressed: 92 Downloaded: 124 file(s) [attempted 124/8459 = 1%, 245 KB/s], Decompressed: 121 Downloaded: 158 file(s) [attempted 158/8459 = 1%, 73 KB/s], Decompressed: 155 Downloaded: 196 file(s) [attempted 196/8459 = 2%, 40 KB/s], Decompressed: 192 Downloaded: 234 file(s) [attempted 234/8459 = 2%, 576 KB/s], Decompressed: 227 Downloaded: 264 file(s) [attempted 264/8459 = 3%, 754 KB/s], Decompressed: 261 Downloaded: 306 file(s) [attempted 306/8459 = 3%, 432 KB/s], Decompressed: 302 Downloaded: 350 file(s) [attempted 350/8459 = 4%, 281 KB/s], Decompressed: 347 Downloaded: 388 file(s) [attempted 388/8459 = 4%, 77 KB/s], Decompressed: 384 Downloaded: 425 file(s) [attempted 425/8459 = 5%, 116 KB/s], Decompressed: 412 Downloaded: 460 file(s) [attempted 460/8459 = 5%, 76 KB/s], Decompressed: 453 Downloaded: 498 file(s) [attempted 498/8459 = 5%, 183 KB/s], Decompressed: 494 Downloaded: 536 file(s) [attempted 536/8459 = 6%, 280 KB/s], Decompressed: 532 Downloaded: 571 file(s) [attempted 571/8459 = 6%, 96 KB/s], Decompressed: 566 Downloaded: 610 file(s) [attempted 610/8459 = 7%, 143 KB/s], Decompressed: 604 Downloaded: 651 file(s) [attempted 651/8459 = 7%, 123 KB/s], Decompressed: 648 Downloaded: 693 file(s) [attempted 693/8459 = 8%, 102 KB/s], Decompressed: 689 Downloaded: 730 file(s) [attempted 730/8459 = 8%, 115 KB/s], Decompressed: 727 Downloaded: 765 file(s) [attempted 765/8459 = 9%, 204 KB/s], Decompressed: 754 Downloaded: 806 file(s) [attempted 806/8459 = 9%, 175 KB/s], Decompressed: 802 Downloaded: 847 file(s) [attempted 847/8459 = 10%, 57 KB/s], Decompressed: 843 Downloaded: 884 file(s) [attempted 884/8459 = 10%, 41 KB/s], Decompressed: 881 Downloaded: 916 file(s) [attempted 916/8459 = 10%, 388 KB/s], Decompressed: 912 Downloaded: 960 file(s) [attempted 960/8459 = 11%, 216 KB/s], Decompressed: 956 Downloaded: 1004 file(s) [attempted 1004/8459 = 11%, 493 KB/s], Decompressed: 1001 Downloaded: 1047 file(s) [attempted 1047/8459 = 12%, 572 KB/s], Decompressed: 1035 Downloaded: 1083 file(s) [attempted 1083/8459 = 12%, 74 KB/s], Decompressed: 1076 Downloaded: 1117 file(s) [attempted 1117/8459 = 13%, 238 KB/s], Decompressed: 1114 Downloaded: 1159 file(s) [attempted 1159/8459 = 13%, 254 KB/s], Decompressed: 1155 Downloaded: 1203 file(s) [attempted 1203/8459 = 14%, 2312 KB/s], Decompressed: 1199 Downloaded: 1237 file(s) [attempted 1237/8459 = 14%, 91 KB/s], Decompressed: 1230 Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 261 KB/s], Decompressed: 1268 Downloaded: 1314 file(s) [attempted 1314/8459 = 15%, 44 KB/s], Decompressed: 1309 Downloaded: 1353 file(s) [attempted 1353/8459 = 15%, 339 KB/s], Decompressed: 1350 Downloaded: 1398 file(s) [attempted 1398/8459 = 16%, 204 KB/s], Decompressed: 1384 Downloaded: 1425 file(s) [attempted 1425/8459 = 16%, 617 KB/s], Decompressed: 1415 Downloaded: 1464 file(s) [attempted 1464/8459 = 17%, 474 KB/s], Decompressed: 1459 Downloaded: 1507 file(s) [attempted 1507/8459 = 17%, 24 KB/s], Decompressed: 1504 Downloaded: 1548 file(s) [attempted 1548/8459 = 18%, 165 KB/s], Decompressed: 1542 Downloaded: 1583 file(s) [attempted 1583/8459 = 18%, 948 KB/s], Decompressed: 1572 Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 328 KB/s], Decompressed: 1613 Downloaded: 1665 file(s) [attempted 1665/8459 = 19%, 303 KB/s], Decompressed: 1661 Downloaded: 1704 file(s) [attempted 1704/8459 = 20%, 145 KB/s], Decompressed: 1696 Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 955 KB/s], Decompressed: 1733 Downloaded: 1781 file(s) [attempted 1781/8459 = 21%, 25 KB/s], Decompressed: 1771 Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 207 KB/s], Decompressed: 1812 Downloaded: 1861 file(s) [attempted 1861/8459 = 22%, 115 KB/s], Decompressed: 1856 Downloaded: 1897 file(s) [attempted 1897/8459 = 22%, 444 KB/s], Decompressed: 1894 Downloaded: 1939 file(s) [attempted 1939/8459 = 22%, 1325 KB/s], Decompressed: 1928 Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 836 KB/s], Decompressed: 1963 Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 126 KB/s], Decompressed: 2007 Downloaded: 2052 file(s) [attempted 2052/8459 = 24%, 88 KB/s], Decompressed: 2045 Downloaded: 2089 file(s) [attempted 2089/8459 = 24%, 94 KB/s], Decompressed: 2082 Downloaded: 2130 file(s) [attempted 2130/8459 = 25%, 103 KB/s], Decompressed: 2123 Downloaded: 2158 file(s) [attempted 2158/8459 = 25%, 406 KB/s], Decompressed: 2154 Downloaded: 2203 file(s) [attempted 2203/8459 = 26%, 491 KB/s], Decompressed: 2199 Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 191 KB/s], Decompressed: 2240 Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 292 KB/s], Decompressed: 2271 Downloaded: 2308 file(s) [attempted 2308/8459 = 27%, 133 KB/s], Decompressed: 2301 Downloaded: 2353 file(s) [attempted 2353/8459 = 27%, 844 KB/s], Decompressed: 2349 Downloaded: 2390 file(s) [attempted 2390/8459 = 28%, 457 KB/s], Decompressed: 2387 Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 220 KB/s], Decompressed: 2425 Downloaded: 2466 file(s) [attempted 2466/8459 = 29%, 231 KB/s], Decompressed: 2455 Downloaded: 2503 file(s) [attempted 2503/8459 = 29%, 346 KB/s], Decompressed: 2500 Downloaded: 2548 file(s) [attempted 2548/8459 = 30%, 166 KB/s], Decompressed: 2544 Downloaded: 2585 file(s) [attempted 2585/8459 = 30%, 60 KB/s], Decompressed: 2576 Downloaded: 2623 file(s) [attempted 2623/8459 = 31%, 238 KB/s], Decompressed: 2616 Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 192 KB/s], Decompressed: 2654 Downloaded: 2702 file(s) [attempted 2702/8459 = 31%, 230 KB/s], Decompressed: 2698 Downloaded: 2746 file(s) [attempted 2746/8459 = 32%, 43 KB/s], Decompressed: 2743 Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 460 KB/s], Decompressed: 2780 Downloaded: 2822 file(s) [attempted 2822/8459 = 33%, 80 KB/s], Decompressed: 2815 Downloaded: 2859 file(s) [attempted 2859/8459 = 33%, 496 KB/s], Decompressed: 2856 Downloaded: 2904 file(s) [attempted 2904/8459 = 34%, 119 KB/s], Decompressed: 2900 Downloaded: 2941 file(s) [attempted 2941/8459 = 34%, 779 KB/s], Decompressed: 2935 Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 540 KB/s], Decompressed: 2972 Downloaded: 3020 file(s) [attempted 3020/8459 = 35%, 27 KB/s], Decompressed: 3017 Downloaded: 3054 file(s) [attempted 3054/8459 = 36%, 29 KB/s], Decompressed: 3051 Downloaded: 3099 file(s) [attempted 3099/8459 = 36%, 174 KB/s], Decompressed: 3092 Downloaded: 3140 file(s) [attempted 3140/8459 = 37%, 49 KB/s], Decompressed: 3136 Downloaded: 3177 file(s) [attempted 3177/8459 = 37%, 165 KB/s], Decompressed: 3174 Downloaded: 3213 file(s) [attempted 3213/8459 = 37%, 116 KB/s], Decompressed: 3208 Downloaded: 3254 file(s) [attempted 3254/8459 = 38%, 1351 KB/s], Decompressed: 3249 Downloaded: 3292 file(s) [attempted 3292/8459 = 38%, 169 KB/s], Decompressed: 3284 Downloaded: 3328 file(s) [attempted 3328/8459 = 39%, 163 KB/s], Decompressed: 3325 Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 450 KB/s], Decompressed: 3359 Downloaded: 3403 file(s) [attempted 3403/8459 = 40%, 411 KB/s], Decompressed: 3393 Downloaded: 3444 file(s) [attempted 3444/8459 = 40%, 252 KB/s], Decompressed: 3441 Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 234 KB/s], Decompressed: 3475 Downloaded: 3521 file(s) [attempted 3521/8459 = 41%, 230 KB/s], Decompressed: 3513 Downloaded: 3557 file(s) [attempted 3557/8459 = 42%, 186 KB/s], Decompressed: 3554 Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 71 KB/s], Decompressed: 3592 Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 189 KB/s], Decompressed: 3636 Downloaded: 3678 file(s) [attempted 3678/8459 = 43%, 71 KB/s], Decompressed: 3670 Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 245 KB/s], Decompressed: 3708 Downloaded: 3756 file(s) [attempted 3756/8459 = 44%, 861 KB/s], Decompressed: 3749 Downloaded: 3794 file(s) [attempted 3794/8459 = 44%, 601 KB/s], Decompressed: 3790 Downloaded: 3835 file(s) [attempted 3835/8459 = 45%, 118 KB/s], Decompressed: 3831 Downloaded: 3872 file(s) [attempted 3872/8459 = 45%, 246 KB/s], Decompressed: 3869 Downloaded: 3907 file(s) [attempted 3907/8459 = 46%, 80 KB/s], Decompressed: 3905 Downloaded: 3948 file(s) [attempted 3948/8459 = 46%, 210 KB/s], Decompressed: 3941 Downloaded: 3985 file(s) [attempted 3985/8459 = 47%, 47 KB/s], Decompressed: 3978 Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 1329 KB/s], Decompressed: 4013 Downloaded: 4054 file(s) [attempted 4054/8459 = 47%, 1425 KB/s], Decompressed: 4050 Downloaded: 4093 file(s) [attempted 4093/8459 = 48%, 1375 KB/s], Decompressed: 4088 Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 583 KB/s], Decompressed: 4129 Downloaded: 4173 file(s) [attempted 4173/8459 = 49%, 276 KB/s], Decompressed: 4160 Downloaded: 4210 file(s) [attempted 4210/8459 = 49%, 54 KB/s], Decompressed: 4204 Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 143 KB/s], Decompressed: 4249 Downloaded: 4291 file(s) [attempted 4291/8459 = 50%, 104 KB/s], Decompressed: 4286 Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 50 KB/s], Decompressed: 4321 Downloaded: 4368 file(s) [attempted 4368/8459 = 51%, 412 KB/s], Decompressed: 4365 Downloaded: 4403 file(s) [attempted 4403/8459 = 52%, 197 KB/s], Decompressed: 4399 Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 528 KB/s], Decompressed: 4437 Downloaded: 4481 file(s) [attempted 4481/8459 = 52%, 378 KB/s], Decompressed: 4478 Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 448 KB/s], Decompressed: 4516 Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 459 KB/s], Decompressed: 4550 Downloaded: 4594 file(s) [attempted 4594/8459 = 54%, 38 KB/s], Decompressed: 4591 Downloaded: 4635 file(s) [attempted 4635/8459 = 54%, 1059 KB/s], Decompressed: 4629 Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 140 KB/s], Decompressed: 4673 Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 196 KB/s], Decompressed: 4700 Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 262 KB/s], Decompressed: 4742 Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 339 KB/s], Decompressed: 4786 Downloaded: 4827 file(s) [attempted 4827/8459 = 57%, 72 KB/s], Decompressed: 4820 Downloaded: 4865 file(s) [attempted 4865/8459 = 57%, 343 KB/s], Decompressed: 4861 Downloaded: 4902 file(s) [attempted 4902/8459 = 57%, 566 KB/s], Decompressed: 4896 Downloaded: 4943 file(s) [attempted 4943/8459 = 58%, 486 KB/s], Decompressed: 4940 Downloaded: 4988 file(s) [attempted 4988/8459 = 58%, 105 KB/s], Decompressed: 4981 Downloaded: 5028 file(s) [attempted 5028/8459 = 59%, 220 KB/s], Decompressed: 5015 Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 52 KB/s], Decompressed: 5053 Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 136 KB/s], Decompressed: 5094 Downloaded: 5143 file(s) [attempted 5143/8459 = 60%, 161 KB/s], Decompressed: 5135 Downloaded: 5183 file(s) [attempted 5183/8459 = 61%, 68 KB/s], Decompressed: 5180 Downloaded: 5221 file(s) [attempted 5221/8459 = 61%, 119 KB/s], Decompressed: 5210 Downloaded: 5249 file(s) [attempted 5249/8459 = 62%, 510 KB/s], Decompressed: 5245 Downloaded: 5293 file(s) [attempted 5293/8459 = 62%, 69 KB/s], Decompressed: 5289 Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 187 KB/s], Decompressed: 5330 Downloaded: 5375 file(s) [attempted 5375/8459 = 63%, 320 KB/s], Decompressed: 5364 Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 301 KB/s], Decompressed: 5399 Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 961 KB/s], Decompressed: 5440 Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 266 KB/s], Decompressed: 5481 Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 922 KB/s], Decompressed: 5525 Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 298 KB/s], Decompressed: 5549 Downloaded: 5597 file(s) [attempted 5597/8459 = 66%, 82 KB/s], Decompressed: 5594 Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 28 KB/s], Decompressed: 5638 Downloaded: 5686 file(s) [attempted 5686/8459 = 67%, 246 KB/s], Decompressed: 5683 Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 287 KB/s], Decompressed: 5724 Downloaded: 5758 file(s) [attempted 5758/8459 = 68%, 359 KB/s], Decompressed: 5751 Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 405 KB/s], Decompressed: 5789 Downloaded: 5840 file(s) [attempted 5840/8459 = 69%, 220 KB/s], Decompressed: 5837 Downloaded: 5885 file(s) [attempted 5885/8459 = 69%, 90 KB/s], Decompressed: 5881 Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 697 KB/s], Decompressed: 5921 Downloaded: 5953 file(s) [attempted 5953/8459 = 70%, 84 KB/s], Decompressed: 5946 Downloaded: 5994 file(s) [attempted 5994/8459 = 70%, 52 KB/s], Decompressed: 5991 Downloaded: 6039 file(s) [attempted 6039/8459 = 71%, 129 KB/s], Decompressed: 6035 Downloaded: 6080 file(s) [attempted 6080/8459 = 71%, 152 KB/s], Decompressed: 6069 Downloaded: 6109 file(s) [attempted 6109/8459 = 72%, 119 KB/s], Decompressed: 6097 Downloaded: 6147 file(s) [attempted 6147/8459 = 72%, 355 KB/s], Decompressed: 6141 Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 200 KB/s], Decompressed: 6186 Downloaded: 6234 file(s) [attempted 6234/8459 = 73%, 641 KB/s], Decompressed: 6220 Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 91 KB/s], Decompressed: 6254 Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 693 KB/s], Decompressed: 6288 Downloaded: 6340 file(s) [attempted 6340/8459 = 74%, 54 KB/s], Decompressed: 6336 Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 28 KB/s], Decompressed: 6374 Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 276 KB/s], Decompressed: 6408 Downloaded: 6450 file(s) [attempted 6450/8459 = 76%, 227 KB/s], Decompressed: 6446 Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 1236 KB/s], Decompressed: 6490 Downloaded: 6537 file(s) [attempted 6537/8459 = 77%, 593 KB/s], Decompressed: 6525 Downloaded: 6566 file(s) [attempted 6566/8459 = 77%, 100 KB/s], Decompressed: 6555 Downloaded: 6603 file(s) [attempted 6603/8459 = 78%, 204 KB/s], Decompressed: 6596 Downloaded: 6645 file(s) [attempted 6645/8459 = 78%, 124 KB/s], Decompressed: 6641 Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 233 KB/s], Decompressed: 6682 Downloaded: 6723 file(s) [attempted 6723/8459 = 79%, 165 KB/s], Decompressed: 6716 Downloaded: 6761 file(s) [attempted 6761/8459 = 79%, 338 KB/s], Decompressed: 6757 Downloaded: 6802 file(s) [attempted 6802/8459 = 80%, 23 KB/s], Decompressed: 6795 Downloaded: 6843 file(s) [attempted 6843/8459 = 80%, 55 KB/s], Decompressed: 6833 Downloaded: 6877 file(s) [attempted 6877/8459 = 81%, 355 KB/s], Decompressed: 6874 Downloaded: 6915 file(s) [attempted 6915/8459 = 81%, 410 KB/s], Decompressed: 6908 Downloaded: 6952 file(s) [attempted 6952/8459 = 82%, 378 KB/s], Decompressed: 6949 Downloaded: 6993 file(s) [attempted 6993/8459 = 82%, 235 KB/s], Decompressed: 6987 Downloaded: 7031 file(s) [attempted 7031/8459 = 83%, 1741 KB/s], Decompressed: 7024 Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 748 KB/s], Decompressed: 7065 Downloaded: 7110 file(s) [attempted 7110/8459 = 84%, 697 KB/s], Decompressed: 7103 Downloaded: 7149 file(s) [attempted 7149/8459 = 84%, 454 KB/s], Decompressed: 7144 Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 1227 KB/s], Decompressed: 7182 Downloaded: 7226 file(s) [attempted 7226/8459 = 85%, 150 KB/s], Decompressed: 7223 Downloaded: 7264 file(s) [attempted 7264/8459 = 85%, 116 KB/s], Decompressed: 7260 Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 82 KB/s], Decompressed: 7301 Downloaded: 7343 file(s) [attempted 7343/8459 = 86%, 553 KB/s], Decompressed: 7336 Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 182 KB/s], Decompressed: 7377 Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 962 KB/s], Decompressed: 7414 Downloaded: 7459 file(s) [attempted 7459/8459 = 88%, 85 KB/s], Decompressed: 7452 Downloaded: 7503 file(s) [attempted 7503/8459 = 88%, 461 KB/s], Decompressed: 7497 Downloaded: 7544 file(s) [attempted 7544/8459 = 89%, 190 KB/s], Decompressed: 7541 Downloaded: 7580 file(s) [attempted 7580/8459 = 89%, 218 KB/s], Decompressed: 7575 Downloaded: 7620 file(s) [attempted 7620/8459 = 90%, 153 KB/s], Decompressed: 7616 Downloaded: 7658 file(s) [attempted 7658/8459 = 90%, 453 KB/s], Decompressed: 7654 Downloaded: 7696 file(s) [attempted 7696/8459 = 90%, 108 KB/s], Decompressed: 7692 Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 99 KB/s], Decompressed: 7726 Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 310 KB/s], Decompressed: 7763 Downloaded: 7810 file(s) [attempted 7810/8459 = 92%, 171 KB/s], Decompressed: 7801 Downloaded: 7850 file(s) [attempted 7850/8459 = 92%, 306 KB/s], Decompressed: 7842 Downloaded: 7884 file(s) [attempted 7884/8459 = 93%, 86 KB/s], Decompressed: 7876 Downloaded: 7921 file(s) [attempted 7921/8459 = 93%, 31 KB/s], Decompressed: 7917 Downloaded: 7962 file(s) [attempted 7962/8459 = 94%, 179 KB/s], Decompressed: 7948 Downloaded: 8000 file(s) [attempted 8000/8459 = 94%, 304 KB/s], Decompressed: 7996 Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 424 KB/s], Decompressed: 8041 Downloaded: 8083 file(s) [attempted 8083/8459 = 95%, 110 KB/s], Decompressed: 8075 Downloaded: 8123 file(s) [attempted 8123/8459 = 96%, 472 KB/s], Decompressed: 8119 Downloaded: 8164 file(s) [attempted 8164/8459 = 96%, 23 KB/s], Decompressed: 8157 Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 121 KB/s], Decompressed: 8195 Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 102 KB/s], Decompressed: 8239 Downloaded: 8284 file(s) [attempted 8284/8459 = 97%, 527 KB/s], Decompressed: 8278 Downloaded: 8321 file(s) [attempted 8321/8459 = 98%, 374 KB/s], Decompressed: 8311 Downloaded: 8359 file(s) [attempted 8359/8459 = 98%, 131 KB/s], Decompressed: 8352 Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 317 KB/s], Decompressed: 8390 Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 105 KB/s], Decompressed: 8434 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 105 KB/s], Decompressed: 8448
lean_checkerexit 0
lake build
✔ [3409/3416] Built Iut.Stage1.IUTStage1StepXI (73s) ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (154s) 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) [0x7cd9b47c6785] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7cd9b47bdb27] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7cd9b47bdc0b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7cd9b46f3c62] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7cd9b46f4439] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7cd9b47caf99] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7cd9b4632923] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7cd9b4632b2b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7cd9b4633827] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7cd9b46341b6] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7cd9b47c9e8b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7cd9b4415adb] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7cd9b47c9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7cd9b47c9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7cd9b479b1f3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7cd9b4415c92] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7cd9af822638] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7cd9af60cd2e] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7cd9af169a82] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7cd9af169f0e] /lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7cd9ac04524a] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7cd9ac045305] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x57897b4128da] ✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (20s) ✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.3s) ✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (36s) ✔ [3414/3416] Built Iut.Basic (2.5s) ✔ [3415/3416] Built Iut (2.5s) 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":4,"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":331759,"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":49,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":337087,"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":1,"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":7591,"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":334546,"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":7,"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":1892,"diagnostic_count":116,"duration_ms":1560631,"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":341132,"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":1892,"diagnostic_count":116,"duration_ms":89,"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":43332215,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":29,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":43332215,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":7804,"diagnostic_count":3119,"duration_ms":6189646,"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":428138,"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":547,"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":175,"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":19977,"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":734437,"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":111,"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":6,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1647482,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":2726,"diagnostic_count":896,"duration_ms":949627,"module_name":"Iut.Stage1.IUTStage1StepXI","module_path":"Iut/Stage1/IUTStage1StepXI.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":778271,"module_count":1,"module_name":"Iut.Stage1.IUTStage1StepXI","module_path":"Iut/Stage1/IUTStage1StepXI.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":2726,"diagnostic_count":896,"duration_ms":133,"module_count":1,"module_name":"Iut.Stage1.IUTStage1StepXI","module_path":"Iut/Stage1/IUTStage1StepXI.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase {"duration_ms":0,"module_index":6,"module_payload_kind":"fragment","ok":true,"payload_bytes":33395505,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":23,"module_index":6,"module_payload_kind":"fragment","ok":true,"payload_bytes":33395505,"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":3338}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":877,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"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":3536,"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 e5c6a7f9c7c521013353176634e2468fe4ab1dee3cb3be167d353e08621c37b7
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":12023838,"ok":true}