Verification run
Run 275
failed commit
cf0aacf6ca72 toolchain lean-v4-30-0 prover lean took 6h 30m · finished 5w ago ./.apodeixis/tools/lean-semantic-extract.sh failed with exit code none (process did not exit cleanly) (toolchain lean-v4-30-0, command: elan run leanprover/lean4:v4.30.0 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase ./.apodeixis/tools/lean-semantic-extract.sh)
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-336-source
Cloning into '/var/lib/apodeixis/repos/job-336-source'...
git_checkout exit 0
git checkout cf0aacf6ca72699e0ab723a7a42657f2f8e62f5c
Note: switching to 'cf0aacf6ca72699e0ab723a7a42657f2f8e62f5c'. 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 cf0aacf Bundle principal constructed coric Ob7
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%, 10 KB/s], Decompressed: 0 Downloaded: 14 file(s) [attempted 14/8459 = 0%, 11 KB/s], Decompressed: 13 Downloaded: 42 file(s) [attempted 42/8459 = 0%, 15 KB/s], Decompressed: 41 Downloaded: 69 file(s) [attempted 69/8459 = 0%, 217 KB/s], Decompressed: 65 Downloaded: 100 file(s) [attempted 100/8459 = 1%, 245 KB/s], Decompressed: 96 Downloaded: 134 file(s) [attempted 134/8459 = 1%, 62 KB/s], Decompressed: 131 Downloaded: 168 file(s) [attempted 168/8459 = 1%, 512 KB/s], Decompressed: 165 Downloaded: 206 file(s) [attempted 206/8459 = 2%, 316 KB/s], Decompressed: 203 Downloaded: 247 file(s) [attempted 247/8459 = 2%, 25 KB/s], Decompressed: 240 Downloaded: 288 file(s) [attempted 288/8459 = 3%, 102 KB/s], Decompressed: 285 Downloaded: 333 file(s) [attempted 333/8459 = 3%, 199 KB/s], Decompressed: 330 Downloaded: 374 file(s) [attempted 374/8459 = 4%, 123 KB/s], Decompressed: 371 Downloaded: 415 file(s) [attempted 415/8459 = 4%, 27 KB/s], Decompressed: 408 Downloaded: 453 file(s) [attempted 453/8459 = 5%, 189 KB/s], Decompressed: 449 Downloaded: 497 file(s) [attempted 497/8459 = 5%, 952 KB/s], Decompressed: 492 Downloaded: 534 file(s) [attempted 534/8459 = 6%, 327 KB/s], Decompressed: 528 Downloaded: 574 file(s) [attempted 574/8459 = 6%, 583 KB/s], Decompressed: 569 Downloaded: 617 file(s) [attempted 617/8459 = 7%, 86 KB/s], Decompressed: 614 Downloaded: 655 file(s) [attempted 655/8459 = 7%, 181 KB/s], Decompressed: 651 Downloaded: 699 file(s) [attempted 699/8459 = 8%, 358 KB/s], Decompressed: 696 Downloaded: 741 file(s) [attempted 741/8459 = 8%, 437 KB/s], Decompressed: 734 Downloaded: 780 file(s) [attempted 780/8459 = 9%, 184 KB/s], Decompressed: 775 Downloaded: 819 file(s) [attempted 819/8459 = 9%, 599 KB/s], Decompressed: 818 Downloaded: 860 file(s) [attempted 860/8459 = 10%, 123 KB/s], Decompressed: 857 Downloaded: 908 file(s) [attempted 908/8459 = 10%, 56 KB/s], Decompressed: 905 Downloaded: 956 file(s) [attempted 956/8459 = 11%, 31 KB/s], Decompressed: 953 Downloaded: 1004 file(s) [attempted 1004/8459 = 11%, 539 KB/s], Decompressed: 997 Downloaded: 1045 file(s) [attempted 1045/8459 = 12%, 641 KB/s], Decompressed: 1042 Downloaded: 1086 file(s) [attempted 1086/8459 = 12%, 446 KB/s], Decompressed: 1082 Downloaded: 1123 file(s) [attempted 1123/8459 = 13%, 396 KB/s], Decompressed: 1117 Downloaded: 1169 file(s) [attempted 1169/8459 = 13%, 318 KB/s], Decompressed: 1162 Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 115 KB/s], Decompressed: 1203 Downloaded: 1251 file(s) [attempted 1251/8459 = 14%, 115 KB/s], Decompressed: 1244 Downloaded: 1292 file(s) [attempted 1292/8459 = 15%, 841 KB/s], Decompressed: 1288 Downloaded: 1333 file(s) [attempted 1333/8459 = 15%, 53 KB/s], Decompressed: 1329 Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 29 KB/s], Decompressed: 1374 Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 906 KB/s], Decompressed: 1415 Downloaded: 1463 file(s) [attempted 1463/8459 = 17%, 115 KB/s], Decompressed: 1459 Downloaded: 1505 file(s) [attempted 1505/8459 = 17%, 74 KB/s], Decompressed: 1500 Downloaded: 1542 file(s) [attempted 1542/8459 = 18%, 333 KB/s], Decompressed: 1538 Downloaded: 1589 file(s) [attempted 1589/8459 = 18%, 179 KB/s], Decompressed: 1586 Downloaded: 1634 file(s) [attempted 1634/8459 = 19%, 1090 KB/s], Decompressed: 1624 Downloaded: 1668 file(s) [attempted 1668/8459 = 19%, 319 KB/s], Decompressed: 1665 Downloaded: 1715 file(s) [attempted 1715/8459 = 20%, 219 KB/s], Decompressed: 1709 Downloaded: 1757 file(s) [attempted 1757/8459 = 20%, 985 KB/s], Decompressed: 1750 Downloaded: 1795 file(s) [attempted 1795/8459 = 21%, 241 KB/s], Decompressed: 1791 Downloaded: 1839 file(s) [attempted 1839/8459 = 21%, 494 KB/s], Decompressed: 1832 Downloaded: 1878 file(s) [attempted 1878/8459 = 22%, 142 KB/s], Decompressed: 1867 Downloaded: 1915 file(s) [attempted 1915/8459 = 22%, 488 KB/s], Decompressed: 1911 Downloaded: 1956 file(s) [attempted 1956/8459 = 23%, 209 KB/s], Decompressed: 1952 Downloaded: 2000 file(s) [attempted 2000/8459 = 23%, 143 KB/s], Decompressed: 1993 Downloaded: 2047 file(s) [attempted 2047/8459 = 24%, 443 KB/s], Decompressed: 2034 Downloaded: 2082 file(s) [attempted 2082/8459 = 24%, 96 KB/s], Decompressed: 2075 Downloaded: 2123 file(s) [attempted 2123/8459 = 25%, 24 KB/s], Decompressed: 2113 Downloaded: 2166 file(s) [attempted 2166/8459 = 25%, 285 KB/s], Decompressed: 2158 Downloaded: 2207 file(s) [attempted 2207/8459 = 26%, 789 KB/s], Decompressed: 2202 Downloaded: 2252 file(s) [attempted 2252/8459 = 26%, 52 KB/s], Decompressed: 2244 Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 1173 KB/s], Decompressed: 2288 Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 557 KB/s], Decompressed: 2325 Downloaded: 2374 file(s) [attempted 2374/8459 = 28%, 998 KB/s], Decompressed: 2370 Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 180 KB/s], Decompressed: 2407 Downloaded: 2460 file(s) [attempted 2460/8459 = 29%, 383 KB/s], Decompressed: 2455 Downloaded: 2497 file(s) [attempted 2497/8459 = 29%, 367 KB/s], Decompressed: 2493 Downloaded: 2541 file(s) [attempted 2541/8459 = 30%, 338 KB/s], Decompressed: 2537 Downloaded: 2585 file(s) [attempted 2585/8459 = 30%, 249 KB/s], Decompressed: 2578 Downloaded: 2621 file(s) [attempted 2621/8459 = 30%, 81 KB/s], Decompressed: 2613 Downloaded: 2661 file(s) [attempted 2661/8459 = 31%, 1757 KB/s], Decompressed: 2657 Downloaded: 2709 file(s) [attempted 2709/8459 = 32%, 355 KB/s], Decompressed: 2705 Downloaded: 2755 file(s) [attempted 2755/8459 = 32%, 49 KB/s], Decompressed: 2746 Downloaded: 2794 file(s) [attempted 2794/8459 = 33%, 167 KB/s], Decompressed: 2787 Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 52 KB/s], Decompressed: 2832 Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 62 KB/s], Decompressed: 2869 Downloaded: 2921 file(s) [attempted 2921/8459 = 34%, 50 KB/s], Decompressed: 2914 Downloaded: 2962 file(s) [attempted 2962/8459 = 35%, 458 KB/s], Decompressed: 2958 Downloaded: 3006 file(s) [attempted 3006/8459 = 35%, 43 KB/s], Decompressed: 3003 Downloaded: 3051 file(s) [attempted 3051/8459 = 36%, 1229 KB/s], Decompressed: 3047 Downloaded: 3095 file(s) [attempted 3095/8459 = 36%, 122 KB/s], Decompressed: 3088 Downloaded: 3134 file(s) [attempted 3134/8459 = 37%, 1090 KB/s], Decompressed: 3129 Downloaded: 3177 file(s) [attempted 3177/8459 = 37%, 24 KB/s], Decompressed: 3167 Downloaded: 3217 file(s) [attempted 3217/8459 = 38%, 1598 KB/s], Decompressed: 3208 Downloaded: 3256 file(s) [attempted 3256/8459 = 38%, 1367 KB/s], Decompressed: 3253 Downloaded: 3304 file(s) [attempted 3304/8459 = 39%, 336 KB/s], Decompressed: 3297 Downloaded: 3345 file(s) [attempted 3345/8459 = 39%, 58 KB/s], Decompressed: 3338 Downloaded: 3390 file(s) [attempted 3390/8459 = 40%, 272 KB/s], Decompressed: 3386 Downloaded: 3437 file(s) [attempted 3437/8459 = 40%, 269 KB/s], Decompressed: 3434 Downloaded: 3483 file(s) [attempted 3483/8459 = 41%, 250 KB/s], Decompressed: 3479 Downloaded: 3523 file(s) [attempted 3523/8459 = 41%, 138 KB/s], Decompressed: 3513 Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 731 KB/s], Decompressed: 3557 Downloaded: 3609 file(s) [attempted 3609/8459 = 42%, 423 KB/s], Decompressed: 3605 Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 403 KB/s], Decompressed: 3646 Downloaded: 3689 file(s) [attempted 3689/8459 = 43%, 212 KB/s], Decompressed: 3684 Downloaded: 3735 file(s) [attempted 3735/8459 = 44%, 97 KB/s], Decompressed: 3732 Downloaded: 3783 file(s) [attempted 3783/8459 = 44%, 375 KB/s], Decompressed: 3781 Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 113 KB/s], Decompressed: 3824 Downloaded: 3869 file(s) [attempted 3869/8459 = 45%, 64 KB/s], Decompressed: 3865 Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 89 KB/s], Decompressed: 3903 Downloaded: 3951 file(s) [attempted 3951/8459 = 46%, 350 KB/s], Decompressed: 3947 Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 207 KB/s], Decompressed: 3988 Downloaded: 4036 file(s) [attempted 4036/8459 = 47%, 75 KB/s], Decompressed: 4030 Downloaded: 4077 file(s) [attempted 4077/8459 = 48%, 798 KB/s], Decompressed: 4074 Downloaded: 4120 file(s) [attempted 4120/8459 = 48%, 330 KB/s], Decompressed: 4112 Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 255 KB/s], Decompressed: 4153 Downloaded: 4197 file(s) [attempted 4197/8459 = 49%, 218 KB/s], Decompressed: 4194 Downloaded: 4242 file(s) [attempted 4242/8459 = 50%, 537 KB/s], Decompressed: 4238 Downloaded: 4283 file(s) [attempted 4283/8459 = 50%, 59 KB/s], Decompressed: 4279 Downloaded: 4326 file(s) [attempted 4326/8459 = 51%, 485 KB/s], Decompressed: 4320 Downloaded: 4365 file(s) [attempted 4365/8459 = 51%, 123 KB/s], Decompressed: 4358 Downloaded: 4403 file(s) [attempted 4403/8459 = 52%, 691 KB/s], Decompressed: 4396 Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 177 KB/s], Decompressed: 4440 Downloaded: 4488 file(s) [attempted 4488/8459 = 53%, 93 KB/s], Decompressed: 4486 Downloaded: 4529 file(s) [attempted 4529/8459 = 53%, 455 KB/s], Decompressed: 4526 Downloaded: 4576 file(s) [attempted 4576/8459 = 54%, 461 KB/s], Decompressed: 4570 Downloaded: 4614 file(s) [attempted 4614/8459 = 54%, 46 KB/s], Decompressed: 4608 Downloaded: 4656 file(s) [attempted 4656/8459 = 55%, 257 KB/s], Decompressed: 4649 Downloaded: 4697 file(s) [attempted 4697/8459 = 55%, 162 KB/s], Decompressed: 4693 Downloaded: 4741 file(s) [attempted 4741/8459 = 56%, 287 KB/s], Decompressed: 4738 Downloaded: 4782 file(s) [attempted 4782/8459 = 56%, 656 KB/s], Decompressed: 4779 Downloaded: 4827 file(s) [attempted 4827/8459 = 57%, 43 KB/s], Decompressed: 4820 Downloaded: 4868 file(s) [attempted 4868/8459 = 57%, 203 KB/s], Decompressed: 4865 Downloaded: 4913 file(s) [attempted 4913/8459 = 58%, 277 KB/s], Decompressed: 4909 Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 472 KB/s], Decompressed: 4947 Downloaded: 4988 file(s) [attempted 4988/8459 = 58%, 317 KB/s], Decompressed: 4984 Downloaded: 5032 file(s) [attempted 5032/8459 = 59%, 255 KB/s], Decompressed: 5029 Downloaded: 5077 file(s) [attempted 5077/8459 = 60%, 158 KB/s], Decompressed: 5073 Downloaded: 5115 file(s) [attempted 5115/8459 = 60%, 539 KB/s], Decompressed: 5111 Downloaded: 5159 file(s) [attempted 5159/8459 = 60%, 1304 KB/s], Decompressed: 5156 Downloaded: 5203 file(s) [attempted 5203/8459 = 61%, 27 KB/s], Decompressed: 5197 Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 99 KB/s], Decompressed: 5238 Downloaded: 5286 file(s) [attempted 5286/8459 = 62%, 287 KB/s], Decompressed: 5282 Downloaded: 5327 file(s) [attempted 5327/8459 = 62%, 51 KB/s], Decompressed: 5323 Downloaded: 5371 file(s) [attempted 5371/8459 = 63%, 415 KB/s], Decompressed: 5364 Downloaded: 5416 file(s) [attempted 5416/8459 = 64%, 331 KB/s], Decompressed: 5412 Downloaded: 5459 file(s) [attempted 5459/8459 = 64%, 275 KB/s], Decompressed: 5453 Downloaded: 5498 file(s) [attempted 5498/8459 = 64%, 246 KB/s], Decompressed: 5494 Downloaded: 5539 file(s) [attempted 5539/8459 = 65%, 173 KB/s], Decompressed: 5536 Downloaded: 5580 file(s) [attempted 5580/8459 = 65%, 521 KB/s], Decompressed: 5576 Downloaded: 5621 file(s) [attempted 5621/8459 = 66%, 100 KB/s], Decompressed: 5618 Downloaded: 5662 file(s) [attempted 5662/8459 = 66%, 156 KB/s], Decompressed: 5655 Downloaded: 5700 file(s) [attempted 5700/8459 = 67%, 808 KB/s], Decompressed: 5696 Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 75 KB/s], Decompressed: 5741 Downloaded: 5785 file(s) [attempted 5785/8459 = 68%, 106 KB/s], Decompressed: 5784 Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 381 KB/s], Decompressed: 5823 Downloaded: 5868 file(s) [attempted 5868/8459 = 69%, 176 KB/s], Decompressed: 5864 Downloaded: 5912 file(s) [attempted 5912/8459 = 69%, 289 KB/s], Decompressed: 5909 Downloaded: 5953 file(s) [attempted 5953/8459 = 70%, 291 KB/s], Decompressed: 5949 Downloaded: 5996 file(s) [attempted 5996/8459 = 70%, 325 KB/s], Decompressed: 5991 Downloaded: 6038 file(s) [attempted 6038/8459 = 71%, 62 KB/s], Decompressed: 6028 Downloaded: 6083 file(s) [attempted 6083/8459 = 71%, 259 KB/s], Decompressed: 6076 Downloaded: 6117 file(s) [attempted 6117/8459 = 72%, 140 KB/s], Decompressed: 6114 Downloaded: 6165 file(s) [attempted 6165/8459 = 72%, 157 KB/s], Decompressed: 6162 Downloaded: 6213 file(s) [attempted 6213/8459 = 73%, 532 KB/s], Decompressed: 6206 Downloaded: 6251 file(s) [attempted 6251/8459 = 73%, 92 KB/s], Decompressed: 6247 Downloaded: 6291 file(s) [attempted 6291/8459 = 74%, 256 KB/s], Decompressed: 6285 Downloaded: 6331 file(s) [attempted 6331/8459 = 74%, 40 KB/s], Decompressed: 6326 Downloaded: 6374 file(s) [attempted 6374/8459 = 75%, 1362 KB/s], Decompressed: 6370 Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 45 KB/s], Decompressed: 6411 Downloaded: 6459 file(s) [attempted 6459/8459 = 76%, 185 KB/s], Decompressed: 6453 Downloaded: 6500 file(s) [attempted 6500/8459 = 76%, 465 KB/s], Decompressed: 6497 Downloaded: 6547 file(s) [attempted 6547/8459 = 77%, 1455 KB/s], Decompressed: 6542 Downloaded: 6586 file(s) [attempted 6586/8459 = 77%, 1826 KB/s], Decompressed: 6576 Downloaded: 6627 file(s) [attempted 6627/8459 = 78%, 114 KB/s], Decompressed: 6624 Downloaded: 6669 file(s) [attempted 6669/8459 = 78%, 185 KB/s], Decompressed: 6665 Downloaded: 6711 file(s) [attempted 6711/8459 = 79%, 54 KB/s], Decompressed: 6702 Downloaded: 6754 file(s) [attempted 6754/8459 = 79%, 308 KB/s], Decompressed: 6750 Downloaded: 6798 file(s) [attempted 6798/8459 = 80%, 265 KB/s], Decompressed: 6795 Downloaded: 6839 file(s) [attempted 6839/8459 = 80%, 46 KB/s], Decompressed: 6836 Downloaded: 6880 file(s) [attempted 6880/8459 = 81%, 71 KB/s], Decompressed: 6873 Downloaded: 6920 file(s) [attempted 6920/8459 = 81%, 207 KB/s], Decompressed: 6915 Downloaded: 6962 file(s) [attempted 6962/8459 = 82%, 126 KB/s], Decompressed: 6956 Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 166 KB/s], Decompressed: 7000 Downloaded: 7046 file(s) [attempted 7046/8459 = 83%, 1952 KB/s], Decompressed: 7041 Downloaded: 7089 file(s) [attempted 7089/8459 = 83%, 1235 KB/s], Decompressed: 7082 Downloaded: 7130 file(s) [attempted 7130/8459 = 84%, 1310 KB/s], Decompressed: 7127 Downloaded: 7170 file(s) [attempted 7170/8459 = 84%, 152 KB/s], Decompressed: 7164 Downloaded: 7212 file(s) [attempted 7212/8459 = 85%, 169 KB/s], Decompressed: 7205 Downloaded: 7257 file(s) [attempted 7257/8459 = 85%, 384 KB/s], Decompressed: 7253 Downloaded: 7298 file(s) [attempted 7298/8459 = 86%, 2108 KB/s], Decompressed: 7294 Downloaded: 7342 file(s) [attempted 7342/8459 = 86%, 614 KB/s], Decompressed: 7339 Downloaded: 7383 file(s) [attempted 7383/8459 = 87%, 63 KB/s], Decompressed: 7380 Downloaded: 7424 file(s) [attempted 7424/8459 = 87%, 235 KB/s], Decompressed: 7421 Downloaded: 7468 file(s) [attempted 7468/8459 = 88%, 284 KB/s], Decompressed: 7464 Downloaded: 7507 file(s) [attempted 7507/8459 = 88%, 252 KB/s], Decompressed: 7496 Downloaded: 7546 file(s) [attempted 7546/8459 = 89%, 127 KB/s], Decompressed: 7541 Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 157 KB/s], Decompressed: 7585 Downloaded: 7631 file(s) [attempted 7631/8459 = 90%, 170 KB/s], Decompressed: 7626 Downloaded: 7671 file(s) [attempted 7671/8459 = 90%, 85 KB/s], Decompressed: 7664 Downloaded: 7712 file(s) [attempted 7712/8459 = 91%, 165 KB/s], Decompressed: 7709 Downloaded: 7753 file(s) [attempted 7753/8459 = 91%, 144 KB/s], Decompressed: 7750 Downloaded: 7797 file(s) [attempted 7797/8459 = 92%, 50 KB/s], Decompressed: 7794 Downloaded: 7839 file(s) [attempted 7839/8459 = 92%, 298 KB/s], Decompressed: 7828 Downloaded: 7880 file(s) [attempted 7880/8459 = 93%, 200 KB/s], Decompressed: 7876 Downloaded: 7921 file(s) [attempted 7921/8459 = 93%, 174 KB/s], Decompressed: 7917 Downloaded: 7965 file(s) [attempted 7965/8459 = 94%, 1257 KB/s], Decompressed: 7958 Downloaded: 8008 file(s) [attempted 8008/8459 = 94%, 299 KB/s], Decompressed: 8003 Downloaded: 8054 file(s) [attempted 8054/8459 = 95%, 102 KB/s], Decompressed: 8051 Downloaded: 8096 file(s) [attempted 8096/8459 = 95%, 48 KB/s], Decompressed: 8092 Downloaded: 8136 file(s) [attempted 8136/8459 = 96%, 68 KB/s], Decompressed: 8133 Downloaded: 8177 file(s) [attempted 8177/8459 = 96%, 55 KB/s], Decompressed: 8174 Downloaded: 8218 file(s) [attempted 8218/8459 = 97%, 104 KB/s], Decompressed: 8215 Downloaded: 8263 file(s) [attempted 8263/8459 = 97%, 955 KB/s], Decompressed: 8259 Downloaded: 8307 file(s) [attempted 8307/8459 = 98%, 63 KB/s], Decompressed: 8304 Downloaded: 8348 file(s) [attempted 8348/8459 = 98%, 1249 KB/s], Decompressed: 8345 Downloaded: 8396 file(s) [attempted 8396/8459 = 99%, 216 KB/s], Decompressed: 8390 Downloaded: 8440 file(s) [attempted 8440/8459 = 99%, 358 KB/s], Decompressed: 8431 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 358 KB/s], Decompressed: 8457
lean_checker exit 0
lake build
✔ [3395/3416] Built Iut.Foundations.QualitativeData (9.6s) ✔ [3396/3416] Built Iut.Foundations.AlgorithmicBridge (2.7s) ✔ [3397/3416] Built Iut.Stage1.CorollarySchema (13s) ✔ [3398/3416] Built Iut.Stage1.SourceObligations (4.5s) ✔ [3399/3416] Built Iut.Stage1.IUTSourceScaffold (2.8s) ✔ [3400/3416] Built Iut.Stage1.IUTStage1Data (3.2s) ✔ [3401/3416] Built Iut.Stage1.IUTStage1SourceCore (34s) ✔ [3402/3416] Built Iut.Stage1.IUTStage1Remark312Absorption (2.8s) ✔ [3403/3416] Built Iut.Stage1.IUTStage1IUTIVAlgebra (9.8s) ✔ [3404/3416] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s) ✔ [3405/3416] Built Iut.Stage1.IUTStage1StepX (5.1s) ✔ [3406/3416] Built Iut.Stage1.IUTStage1Gaussian (9.1s) ✔ [3407/3416] Built Iut.Stage1.IUTStage1HodgeSHE (5.7s) ✔ [3408/3416] Built Iut.Stage1.IUTStage1Theorem311 (4.7s) ✔ [3409/3416] Built Iut.Stage1.IUTStage1StepXI (18s) ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (169s) 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) [0x79529e5c6785] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x79529e5bdb27] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x79529e5bdc0b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x79529e4f3c62] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x79529e4f4439] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x79529e5caf99] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x79529e432923] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x79529e432b2b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x79529e433827] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x79529e4341b6] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x79529e5c9e8b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x79529e215adb] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x79529e5c9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x79529e5c9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x79529e59b1f3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x79529e215c92] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x795299622638] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x79529940cd2e] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x795298f69a82] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x795298f69f0e] /lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x795295e4524a] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x795295e45305] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x59cdec0bf8da] ✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (20s) ✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.9s) ✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (46s) ✔ [3414/3416] Built Iut.Basic (9.9s) ✔ [3415/3416] Built Iut (2.8s) 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
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 b8ade8a5a75badb2412ef674e9cf813e5e33dd881f43d8103f9aabc58695563a 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 -
./.apodeixis/tools/lean-semantic-extract.sh
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: stored compiled static runner cache cce27869c0d4aaab5a9a11452cfb29f4952473614ca88d877d92ab8b59b7ba1f warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes /usr/bin/podman timed out after 14400s podman cleanup removed verifier container apx-verifier-job-336-runtime-semantic_extract-188301-1780865141135474040-9