Verification run
Run 338
failed commit
f203c05a9f98 toolchain lean-v4-30-0 prover lean took 55m 19s · finished 5w ago ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007) failed with exit code 1 (toolchain lean-v4-30-0, command: <command argv unavailable>)
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_clone exit 0
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-414-source
Cloning into '/var/lib/apodeixis/repos/job-414-source'...
git_checkout exit 128
git checkout f203c05a9f9834367260c6a301b89e5c65fa3fd1
fatal: reference is not a tree: f203c05a9f9834367260c6a301b89e5c65fa3fd1
git_checkout exit 0
git fetch --depth 1 origin f203c05a9f9834367260c6a301b89e5c65fa3fd1
From https://github.com/promachina/iut-lean * branch f203c05a9f9834367260c6a301b89e5c65fa3fd1 -> FETCH_HEAD
git_checkout exit 0
git checkout f203c05a9f9834367260c6a301b89e5c65fa3fd1 (after fetch)
Note: switching to 'f203c05a9f9834367260c6a301b89e5c65fa3fd1'. 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 f203c05 Add coordinate scalar image hull source
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: 14 file(s) [attempted 14/8459 = 0%, 9 KB/s], Decompressed: 13 Downloaded: 42 file(s) [attempted 42/8459 = 0%, 15 KB/s], Decompressed: 39 Downloaded: 68 file(s) [attempted 68/8459 = 0%, 339 KB/s], Decompressed: 65 Downloaded: 94 file(s) [attempted 94/8459 = 1%, 59 KB/s], Decompressed: 89 Downloaded: 131 file(s) [attempted 131/8459 = 1%, 540 KB/s], Decompressed: 127 Downloaded: 165 file(s) [attempted 165/8459 = 1%, 115 KB/s], Decompressed: 162 Downloaded: 206 file(s) [attempted 206/8459 = 2%, 415 KB/s], Decompressed: 203 Downloaded: 242 file(s) [attempted 242/8459 = 2%, 136 KB/s], Decompressed: 237 Downloaded: 278 file(s) [attempted 278/8459 = 3%, 961 KB/s], Decompressed: 275 Downloaded: 323 file(s) [attempted 323/8459 = 3%, 317 KB/s], Decompressed: 319 Downloaded: 364 file(s) [attempted 364/8459 = 4%, 632 KB/s], Decompressed: 357 Downloaded: 401 file(s) [attempted 401/8459 = 4%, 109 KB/s], Decompressed: 398 Downloaded: 443 file(s) [attempted 443/8459 = 5%, 568 KB/s], Decompressed: 439 Downloaded: 487 file(s) [attempted 487/8459 = 5%, 79 KB/s], Decompressed: 480 Downloaded: 521 file(s) [attempted 521/8459 = 6%, 1530 KB/s], Decompressed: 518 Downloaded: 562 file(s) [attempted 562/8459 = 6%, 562 KB/s], Decompressed: 556 Downloaded: 603 file(s) [attempted 603/8459 = 7%, 161 KB/s], Decompressed: 600 Downloaded: 645 file(s) [attempted 645/8459 = 7%, 190 KB/s], Decompressed: 641 Downloaded: 683 file(s) [attempted 683/8459 = 8%, 338 KB/s], Decompressed: 679 Downloaded: 727 file(s) [attempted 727/8459 = 8%, 92 KB/s], Decompressed: 723 Downloaded: 771 file(s) [attempted 771/8459 = 9%, 319 KB/s], Decompressed: 761 Downloaded: 809 file(s) [attempted 809/8459 = 9%, 310 KB/s], Decompressed: 806 Downloaded: 847 file(s) [attempted 847/8459 = 10%, 57 KB/s], Decompressed: 840 Downloaded: 885 file(s) [attempted 885/8459 = 10%, 412 KB/s], Decompressed: 878 Downloaded: 927 file(s) [attempted 927/8459 = 10%, 176 KB/s], Decompressed: 919 Downloaded: 973 file(s) [attempted 973/8459 = 11%, 1533 KB/s], Decompressed: 967 Downloaded: 1015 file(s) [attempted 1015/8459 = 11%, 174 KB/s], Decompressed: 1011 Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 679 KB/s], Decompressed: 1042 Downloaded: 1086 file(s) [attempted 1086/8459 = 12%, 202 KB/s], Decompressed: 1083 Downloaded: 1131 file(s) [attempted 1131/8459 = 13%, 100 KB/s], Decompressed: 1127 Downloaded: 1179 file(s) [attempted 1179/8459 = 13%, 132 KB/s], Decompressed: 1175 Downloaded: 1220 file(s) [attempted 1220/8459 = 14%, 372 KB/s], Decompressed: 1213 Downloaded: 1256 file(s) [attempted 1256/8459 = 14%, 41 KB/s], Decompressed: 1247 Downloaded: 1295 file(s) [attempted 1295/8459 = 15%, 250 KB/s], Decompressed: 1288 Downloaded: 1333 file(s) [attempted 1333/8459 = 15%, 52 KB/s], Decompressed: 1329 Downloaded: 1378 file(s) [attempted 1378/8459 = 16%, 28 KB/s], Decompressed: 1374 Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 910 KB/s], Decompressed: 1413 Downloaded: 1457 file(s) [attempted 1457/8459 = 17%, 351 KB/s], Decompressed: 1453 Downloaded: 1494 file(s) [attempted 1494/8459 = 17%, 189 KB/s], Decompressed: 1490 Downloaded: 1538 file(s) [attempted 1538/8459 = 18%, 98 KB/s], Decompressed: 1535 Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 144 KB/s], Decompressed: 1579 Downloaded: 1624 file(s) [attempted 1624/8459 = 19%, 45 KB/s], Decompressed: 1620 Downloaded: 1665 file(s) [attempted 1665/8459 = 19%, 249 KB/s], Decompressed: 1661 Downloaded: 1707 file(s) [attempted 1707/8459 = 20%, 696 KB/s], Decompressed: 1702 Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 51 KB/s], Decompressed: 1737 Downloaded: 1788 file(s) [attempted 1788/8459 = 21%, 66 KB/s], Decompressed: 1785 Downloaded: 1827 file(s) [attempted 1827/8459 = 21%, 299 KB/s], Decompressed: 1822 Downloaded: 1863 file(s) [attempted 1863/8459 = 22%, 1724 KB/s], Decompressed: 1860 Downloaded: 1908 file(s) [attempted 1908/8459 = 22%, 228 KB/s], Decompressed: 1904 Downloaded: 1952 file(s) [attempted 1952/8459 = 23%, 694 KB/s], Decompressed: 1945 Downloaded: 1993 file(s) [attempted 1993/8459 = 23%, 515 KB/s], Decompressed: 1990 Downloaded: 2034 file(s) [attempted 2034/8459 = 24%, 658 KB/s], Decompressed: 2028 Downloaded: 2072 file(s) [attempted 2072/8459 = 24%, 37 KB/s], Decompressed: 2065 Downloaded: 2113 file(s) [attempted 2113/8459 = 24%, 378 KB/s], Decompressed: 2110 Downloaded: 2158 file(s) [attempted 2158/8459 = 25%, 122 KB/s], Decompressed: 2154 Downloaded: 2195 file(s) [attempted 2195/8459 = 25%, 406 KB/s], Decompressed: 2192 Downloaded: 2240 file(s) [attempted 2240/8459 = 26%, 1296 KB/s], Decompressed: 2236 Downloaded: 2284 file(s) [attempted 2284/8459 = 27%, 583 KB/s], Decompressed: 2281 Downloaded: 2325 file(s) [attempted 2325/8459 = 27%, 238 KB/s], Decompressed: 2318 Downloaded: 2359 file(s) [attempted 2359/8459 = 27%, 194 KB/s], Decompressed: 2356 Downloaded: 2398 file(s) [attempted 2398/8459 = 28%, 524 KB/s], Decompressed: 2394 Downloaded: 2439 file(s) [attempted 2439/8459 = 28%, 402 KB/s], Decompressed: 2435 Downloaded: 2483 file(s) [attempted 2483/8459 = 29%, 148 KB/s], Decompressed: 2479 Downloaded: 2524 file(s) [attempted 2524/8459 = 29%, 583 KB/s], Decompressed: 2520 Downloaded: 2558 file(s) [attempted 2558/8459 = 30%, 414 KB/s], Decompressed: 2555 Downloaded: 2599 file(s) [attempted 2599/8459 = 30%, 120 KB/s], Decompressed: 2596 Downloaded: 2640 file(s) [attempted 2640/8459 = 31%, 26 KB/s], Decompressed: 2637 Downloaded: 2683 file(s) [attempted 2683/8459 = 31%, 582 KB/s], Decompressed: 2678 Downloaded: 2722 file(s) [attempted 2722/8459 = 32%, 169 KB/s], Decompressed: 2715 Downloaded: 2757 file(s) [attempted 2757/8459 = 32%, 228 KB/s], Decompressed: 2753 Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 1202 KB/s], Decompressed: 2794 Downloaded: 2841 file(s) [attempted 2841/8459 = 33%, 81 KB/s], Decompressed: 2835 Downloaded: 2880 file(s) [attempted 2880/8459 = 34%, 38 KB/s], Decompressed: 2873 Downloaded: 2918 file(s) [attempted 2918/8459 = 34%, 677 KB/s], Decompressed: 2914 Downloaded: 2962 file(s) [attempted 2962/8459 = 35%, 1218 KB/s], Decompressed: 2958 Downloaded: 3004 file(s) [attempted 3004/8459 = 35%, 96 KB/s], Decompressed: 2999 Downloaded: 3044 file(s) [attempted 3044/8459 = 35%, 283 KB/s], Decompressed: 3041 Downloaded: 3082 file(s) [attempted 3082/8459 = 36%, 249 KB/s], Decompressed: 3078 Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 139 KB/s], Decompressed: 3112 Downloaded: 3159 file(s) [attempted 3159/8459 = 37%, 1631 KB/s], Decompressed: 3153 Downloaded: 3201 file(s) [attempted 3201/8459 = 37%, 187 KB/s], Decompressed: 3198 Downloaded: 3246 file(s) [attempted 3246/8459 = 38%, 259 KB/s], Decompressed: 3242 Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 88 KB/s], Decompressed: 3280 Downloaded: 3325 file(s) [attempted 3325/8459 = 39%, 352 KB/s], Decompressed: 3321 Downloaded: 3361 file(s) [attempted 3361/8459 = 39%, 62 KB/s], Decompressed: 3355 Downloaded: 3405 file(s) [attempted 3405/8459 = 40%, 123 KB/s], Decompressed: 3396 Downloaded: 3450 file(s) [attempted 3450/8459 = 40%, 321 KB/s], Decompressed: 3438 Downloaded: 3483 file(s) [attempted 3483/8459 = 41%, 161 KB/s], Decompressed: 3479 Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 413 KB/s], Decompressed: 3516 Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 731 KB/s], Decompressed: 3561 Downloaded: 3609 file(s) [attempted 3609/8459 = 42%, 421 KB/s], Decompressed: 3602 Downloaded: 3651 file(s) [attempted 3651/8459 = 43%, 732 KB/s], Decompressed: 3646 Downloaded: 3691 file(s) [attempted 3691/8459 = 43%, 193 KB/s], Decompressed: 3680 Downloaded: 3728 file(s) [attempted 3728/8459 = 44%, 135 KB/s], Decompressed: 3722 Downloaded: 3769 file(s) [attempted 3769/8459 = 44%, 36 KB/s], Decompressed: 3763 Downloaded: 3811 file(s) [attempted 3811/8459 = 45%, 234 KB/s], Decompressed: 3807 Downloaded: 3852 file(s) [attempted 3852/8459 = 45%, 118 KB/s], Decompressed: 3848 Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 151 KB/s], Decompressed: 3889 Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 306 KB/s], Decompressed: 3934 Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 171 KB/s], Decompressed: 3975 Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 1493 KB/s], Decompressed: 4016 Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 1991 KB/s], Decompressed: 4057 Downloaded: 4099 file(s) [attempted 4099/8459 = 48%, 652 KB/s], Decompressed: 4091 Downloaded: 4143 file(s) [attempted 4143/8459 = 48%, 98 KB/s], Decompressed: 4139 Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 195 KB/s], Decompressed: 4177 Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 311 KB/s], Decompressed: 4214 Downloaded: 4262 file(s) [attempted 4262/8459 = 50%, 1686 KB/s], Decompressed: 4259 Downloaded: 4303 file(s) [attempted 4303/8459 = 50%, 170 KB/s], Decompressed: 4300 Downloaded: 4344 file(s) [attempted 4344/8459 = 51%, 184 KB/s], Decompressed: 4341 Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 1252 KB/s], Decompressed: 4379 Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 1043 KB/s], Decompressed: 4416 Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 238 KB/s], Decompressed: 4461 Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 187 KB/s], Decompressed: 4505 Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 117 KB/s], Decompressed: 4543 Downloaded: 4587 file(s) [attempted 4587/8459 = 54%, 302 KB/s], Decompressed: 4584 Downloaded: 4632 file(s) [attempted 4632/8459 = 54%, 95 KB/s], Decompressed: 4628 Downloaded: 4673 file(s) [attempted 4673/8459 = 55%, 665 KB/s], Decompressed: 4670 Downloaded: 4714 file(s) [attempted 4714/8459 = 55%, 1349 KB/s], Decompressed: 4711 Downloaded: 4754 file(s) [attempted 4754/8459 = 56%, 890 KB/s], Decompressed: 4741 Downloaded: 4796 file(s) [attempted 4796/8459 = 56%, 747 KB/s], Decompressed: 4789 Downloaded: 4834 file(s) [attempted 4834/8459 = 57%, 107 KB/s], Decompressed: 4830 Downloaded: 4882 file(s) [attempted 4882/8459 = 57%, 122 KB/s], Decompressed: 4878 Downloaded: 4927 file(s) [attempted 4927/8459 = 58%, 152 KB/s], Decompressed: 4919 Downloaded: 4965 file(s) [attempted 4965/8459 = 58%, 109 KB/s], Decompressed: 4960 Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 82 KB/s], Decompressed: 5002 Downloaded: 5046 file(s) [attempted 5046/8459 = 59%, 159 KB/s], Decompressed: 5043 Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 140 KB/s], Decompressed: 5080 Downloaded: 5125 file(s) [attempted 5125/8459 = 60%, 648 KB/s], Decompressed: 5121 Downloaded: 5166 file(s) [attempted 5166/8459 = 61%, 92 KB/s], Decompressed: 5162 Downloaded: 5209 file(s) [attempted 5209/8459 = 61%, 570 KB/s], Decompressed: 5203 Downloaded: 5243 file(s) [attempted 5243/8459 = 61%, 80 KB/s], Decompressed: 5234 Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 1256 KB/s], Decompressed: 5279 Downloaded: 5327 file(s) [attempted 5327/8459 = 62%, 241 KB/s], Decompressed: 5323 Downloaded: 5366 file(s) [attempted 5366/8459 = 63%, 93 KB/s], Decompressed: 5363 Downloaded: 5411 file(s) [attempted 5411/8459 = 63%, 165 KB/s], Decompressed: 5402 Downloaded: 5445 file(s) [attempted 5445/8459 = 64%, 494 KB/s], Decompressed: 5440 Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 166 KB/s], Decompressed: 5481 Downloaded: 5525 file(s) [attempted 5525/8459 = 65%, 635 KB/s], Decompressed: 5522 Downloaded: 5570 file(s) [attempted 5570/8459 = 65%, 76 KB/s], Decompressed: 5566 Downloaded: 5611 file(s) [attempted 5611/8459 = 66%, 94 KB/s], Decompressed: 5607 Downloaded: 5648 file(s) [attempted 5648/8459 = 66%, 548 KB/s], Decompressed: 5645 Downloaded: 5693 file(s) [attempted 5693/8459 = 67%, 113 KB/s], Decompressed: 5689 Downloaded: 5737 file(s) [attempted 5737/8459 = 67%, 281 KB/s], Decompressed: 5736 Downloaded: 5778 file(s) [attempted 5778/8459 = 68%, 65 KB/s], Decompressed: 5772 Downloaded: 5819 file(s) [attempted 5819/8459 = 68%, 61 KB/s], Decompressed: 5809 Downloaded: 5854 file(s) [attempted 5854/8459 = 69%, 111 KB/s], Decompressed: 5850 Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 103 KB/s], Decompressed: 5891 Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 850 KB/s], Decompressed: 5936 Downloaded: 5986 file(s) [attempted 5986/8459 = 70%, 1678 KB/s], Decompressed: 5980 Downloaded: 6021 file(s) [attempted 6021/8459 = 71%, 65 KB/s], Decompressed: 6018 Downloaded: 6062 file(s) [attempted 6062/8459 = 71%, 573 KB/s], Decompressed: 6056 Downloaded: 6100 file(s) [attempted 6100/8459 = 72%, 72 KB/s], Decompressed: 6097 Downloaded: 6145 file(s) [attempted 6145/8459 = 72%, 1140 KB/s], Decompressed: 6141 Downloaded: 6186 file(s) [attempted 6186/8459 = 73%, 738 KB/s], Decompressed: 6182 Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 269 KB/s], Decompressed: 6223 Downloaded: 6268 file(s) [attempted 6268/8459 = 74%, 109 KB/s], Decompressed: 6264 Downloaded: 6302 file(s) [attempted 6302/8459 = 74%, 377 KB/s], Decompressed: 6299 Downloaded: 6343 file(s) [attempted 6343/8459 = 74%, 1080 KB/s], Decompressed: 6340 Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 30 KB/s], Decompressed: 6381 Downloaded: 6425 file(s) [attempted 6425/8459 = 75%, 146 KB/s], Decompressed: 6418 Downloaded: 6463 file(s) [attempted 6463/8459 = 76%, 108 KB/s], Decompressed: 6462 Downloaded: 6502 file(s) [attempted 6502/8459 = 76%, 32 KB/s], Decompressed: 6497 Downloaded: 6542 file(s) [attempted 6542/8459 = 77%, 349 KB/s], Decompressed: 6538 Downloaded: 6579 file(s) [attempted 6579/8459 = 77%, 412 KB/s], Decompressed: 6569 Downloaded: 6624 file(s) [attempted 6624/8459 = 78%, 287 KB/s], Decompressed: 6620 Downloaded: 6661 file(s) [attempted 6661/8459 = 78%, 337 KB/s], Decompressed: 6655 Downloaded: 6702 file(s) [attempted 6702/8459 = 79%, 113 KB/s], Decompressed: 6699 Downloaded: 6743 file(s) [attempted 6743/8459 = 79%, 278 KB/s], Decompressed: 6740 Downloaded: 6785 file(s) [attempted 6785/8459 = 80%, 489 KB/s], Decompressed: 6781 Downloaded: 6829 file(s) [attempted 6829/8459 = 80%, 43 KB/s], Decompressed: 6822 Downloaded: 6867 file(s) [attempted 6867/8459 = 81%, 818 KB/s], Decompressed: 6863 Downloaded: 6908 file(s) [attempted 6908/8459 = 81%, 936 KB/s], Decompressed: 6897 Downloaded: 6945 file(s) [attempted 6945/8459 = 82%, 198 KB/s], Decompressed: 6942 Downloaded: 6993 file(s) [attempted 6993/8459 = 82%, 27 KB/s], Decompressed: 6990 Downloaded: 7038 file(s) [attempted 7038/8459 = 83%, 159 KB/s], Decompressed: 7031 Downloaded: 7075 file(s) [attempted 7075/8459 = 83%, 63 KB/s], Decompressed: 7070 Downloaded: 7114 file(s) [attempted 7114/8459 = 84%, 355 KB/s], Decompressed: 7110 Downloaded: 7158 file(s) [attempted 7158/8459 = 84%, 100 KB/s], Decompressed: 7154 Downloaded: 7197 file(s) [attempted 7197/8459 = 85%, 99 KB/s], Decompressed: 7194 Downloaded: 7236 file(s) [attempted 7236/8459 = 85%, 97 KB/s], Decompressed: 7233 Downloaded: 7277 file(s) [attempted 7277/8459 = 86%, 225 KB/s], Decompressed: 7271 Downloaded: 7318 file(s) [attempted 7318/8459 = 86%, 1116 KB/s], Decompressed: 7315 Downloaded: 7360 file(s) [attempted 7360/8459 = 87%, 47 KB/s], Decompressed: 7356 Downloaded: 7402 file(s) [attempted 7402/8459 = 87%, 452 KB/s], Decompressed: 7397 Downloaded: 7442 file(s) [attempted 7442/8459 = 87%, 69 KB/s], Decompressed: 7438 Downloaded: 7483 file(s) [attempted 7483/8459 = 88%, 181 KB/s], Decompressed: 7479 Downloaded: 7524 file(s) [attempted 7524/8459 = 88%, 553 KB/s], Decompressed: 7520 Downloaded: 7561 file(s) [attempted 7561/8459 = 89%, 223 KB/s], Decompressed: 7555 Downloaded: 7604 file(s) [attempted 7604/8459 = 89%, 348 KB/s], Decompressed: 7596 Downloaded: 7644 file(s) [attempted 7644/8459 = 90%, 193 KB/s], Decompressed: 7640 Downloaded: 7688 file(s) [attempted 7688/8459 = 90%, 453 KB/s], Decompressed: 7685 Downloaded: 7729 file(s) [attempted 7729/8459 = 91%, 78 KB/s], Decompressed: 7724 Downloaded: 7770 file(s) [attempted 7770/8459 = 91%, 172 KB/s], Decompressed: 7763 Downloaded: 7806 file(s) [attempted 7806/8459 = 92%, 173 KB/s], Decompressed: 7801 Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 84 KB/s], Decompressed: 7845 Downloaded: 7897 file(s) [attempted 7897/8459 = 93%, 65 KB/s], Decompressed: 7893 Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 1740 KB/s], Decompressed: 7945 Downloaded: 7996 file(s) [attempted 7996/8459 = 94%, 120 KB/s], Decompressed: 7993 Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 540 KB/s], Decompressed: 8041 Downloaded: 8088 file(s) [attempted 8088/8459 = 95%, 353 KB/s], Decompressed: 8085 Downloaded: 8120 file(s) [attempted 8120/8459 = 95%, 387 KB/s], Decompressed: 8116 Downloaded: 8164 file(s) [attempted 8164/8459 = 96%, 1423 KB/s], Decompressed: 8160 Downloaded: 8208 file(s) [attempted 8208/8459 = 97%, 133 KB/s], Decompressed: 8201 Downloaded: 8249 file(s) [attempted 8249/8459 = 97%, 1748 KB/s], Decompressed: 8246 Downloaded: 8291 file(s) [attempted 8291/8459 = 98%, 447 KB/s], Decompressed: 8284 Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 185 KB/s], Decompressed: 8325 Downloaded: 8368 file(s) [attempted 8368/8459 = 98%, 473 KB/s], Decompressed: 8362 Downloaded: 8407 file(s) [attempted 8407/8459 = 99%, 226 KB/s], Decompressed: 8403 Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 197 KB/s], Decompressed: 8448 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 279 KB/s], Decompressed: 8455 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 279 KB/s], Decompressed: 8455
lean_checker exit 0
lake build
✔ [3401/3416] Built Iut.Stage1.IUTStage1SourceCore (47s) ✔ [3402/3416] Built Iut.Stage1.IUTStage1Remark312Absorption (2.8s) ✔ [3403/3416] Built Iut.Stage1.IUTStage1IUTIVAlgebra (9.7s) ✔ [3404/3416] Built Iut.Stage1.IUTStage1FiniteLabels (4.3s) ✔ [3405/3416] Built Iut.Stage1.IUTStage1StepX (4.7s) ✔ [3406/3416] Built Iut.Stage1.IUTStage1Gaussian (9.0s) ✔ [3407/3416] Built Iut.Stage1.IUTStage1HodgeSHE (5.4s) ✔ [3408/3416] Built Iut.Stage1.IUTStage1Theorem311 (4.4s) ✔ [3409/3416] Built Iut.Stage1.IUTStage1StepXI (17s) ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (133s) 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) [0x70076adc6785] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x70076adbdb27] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x70076adbdc0b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x70076acf3c62] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x70076acf4439] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x70076adcaf99] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x70076ac32923] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x70076ac32b2b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x70076ac33827] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x70076ac341b6] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x70076adc9e8b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x70076aa15adb] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x70076adc9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x70076adc9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x70076ad9b1f3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x70076aa15c92] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x700765e22638] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x700765c0cd2e] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x700765769a82] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x700765769f0e] /lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x70076264524a] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x700762645305] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x64137386c8da] ✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (7.8s) ✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.1s) ✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (35s) ✔ [3414/3416] Built Iut.Basic (2.6s) ✔ [3415/3416] Built Iut (2.4s) 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`
semantic_module_facts exit 0
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00000)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes lean semantic helper: restored compiled static runner cache e103fd3939aed645f6a64b867308ee472e79eb2af9586b744c189d70ac5f91ea warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00001)
lean semantic helper: restored compiled static runner cache 60b5e07f9f538c271c74b7f6a814efcb4304463fa74b69c58466604298c0acfe warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00002)
lean semantic helper: restored compiled static runner cache 91173b292067b1a93ea64425cc888039ebce7a3e364765ecea90e7a5cbd3d047 warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00003)
lean semantic helper: restored compiled static runner cache f04752e91581a87c3d8d8a87c9c62d574535d7f0c9532c8f513c6579555ccc6c warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00004)
lean semantic helper: restored compiled static runner cache e6ad3fd83caa15e625545b87ad41df67e06b9649767ec9f22a1000a9a1e49c7e warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00005)
lean semantic helper: restored compiled static runner cache 5e719f139e700d3ec36d870eb0df93c69e39d1b25bc64de0e83c7820c297cc88 warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 0
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00006)
lean semantic helper: restored compiled static runner cache e925bad531c9c8172209069553d6ef13f8bc4d43ffee8f9f45ce1b2a571648d9 warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_module_facts exit 1
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00007)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/build/lib/lean/Iut/Foundations/InitialThetaDataExample.olean' of module Iut.Foundations.InitialThetaDataExample does not exist
lean semantic helper: removing stale runner cache lock /apx/lean-semantic-runner-cache/1125d59a0075ac1f5960dfbae4661de52526e3214afe7845431275e329c6952e.lock after 3672s warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
lean semantic helper: restored compiled static runner cache e103fd3939aed645f6a64b867308ee472e79eb2af9586b744c189d70ac5f91ea warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
lean semantic helper: restored compiled static runner cache 60b5e07f9f538c271c74b7f6a814efcb4304463fa74b69c58466604298c0acfe warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
lean semantic helper: restored compiled static runner cache 91173b292067b1a93ea64425cc888039ebce7a3e364765ecea90e7a5cbd3d047 warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)
lean semantic helper: restored compiled static runner cache f04752e91581a87c3d8d8a87c9c62d574535d7f0c9532c8f513c6579555ccc6c warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)
lean semantic helper: restored compiled static runner cache e6ad3fd83caa15e625545b87ad41df67e06b9649767ec9f22a1000a9a1e49c7e warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)
lean semantic helper: restored compiled static runner cache 5e719f139e700d3ec36d870eb0df93c69e39d1b25bc64de0e83c7820c297cc88 warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006)
lean semantic helper: restored compiled static runner cache e925bad531c9c8172209069553d6ef13f8bc4d43ffee8f9f45ce1b2a571648d9 warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/build/lib/lean/Iut/Foundations/InitialThetaDataExample.olean' of module Iut.Foundations.InitialThetaDataExample does not exist
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile remediation: inspect the generated helper support sources under .apodeixis/lean-runner