Verification run
Run 341
succeeded commit
71ef5dc5e76d toolchain lean-v4-30-0 prover lean took 2h 46m · finished 5w ago
Package inputs
This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.
Trust verification
Recomputes trust checks from the recorded attestations, manifest, and command history.
(verification not run)
Manifest
Loads the published files manifest and location metadata for this job.
(manifest not loaded)
Verifier log excerpt
(no log excerpt)
Command runs
git_checkout exit 0
git fetch --depth 1 origin 71ef5dc5e76d60469a81a05df5dd9473c8c42975
From https://github.com/promachina/iut-lean * branch 71ef5dc5e76d60469a81a05df5dd9473c8c42975 -> FETCH_HEAD
semantic_module_facts exit 0
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00010)
lean semantic helper: restored compiled static runner cache a9a06e968839d8b8f7e22b6bb42203d7559473912527ed06adfeb9a10487c71a warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
git_clone exit 0
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-421-source
Cloning into '/var/lib/apodeixis/repos/job-421-source'...
git_checkout exit 128
git checkout 71ef5dc5e76d60469a81a05df5dd9473c8c42975
fatal: reference is not a tree: 71ef5dc5e76d60469a81a05df5dd9473c8c42975
git_checkout exit 0
git checkout 71ef5dc5e76d60469a81a05df5dd9473c8c42975 (after fetch)
Note: switching to '71ef5dc5e76d60469a81a05df5dd9473c8c42975'. 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 71ef5dc Add coordinate scalar valuation hull cover
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: 13 file(s) [attempted 13/8459 = 0%, 9 KB/s], Decompressed: 10 Downloaded: 37 file(s) [attempted 37/8459 = 0%, 15 KB/s], Decompressed: 36 Downloaded: 62 file(s) [attempted 62/8459 = 0%, 352 KB/s], Decompressed: 58 Downloaded: 89 file(s) [attempted 89/8459 = 1%, 186 KB/s], Decompressed: 82 Downloaded: 124 file(s) [attempted 124/8459 = 1%, 255 KB/s], Decompressed: 121 Downloaded: 151 file(s) [attempted 151/8459 = 1%, 87 KB/s], Decompressed: 148 Downloaded: 189 file(s) [attempted 189/8459 = 2%, 566 KB/s], Decompressed: 186 Downloaded: 225 file(s) [attempted 225/8459 = 2%, 779 KB/s], Decompressed: 220 Downloaded: 264 file(s) [attempted 264/8459 = 3%, 144 KB/s], Decompressed: 261 Downloaded: 302 file(s) [attempted 302/8459 = 3%, 670 KB/s], Decompressed: 295 Downloaded: 336 file(s) [attempted 336/8459 = 3%, 131 KB/s], Decompressed: 333 Downloaded: 374 file(s) [attempted 374/8459 = 4%, 101 KB/s], Decompressed: 371 Downloaded: 416 file(s) [attempted 416/8459 = 4%, 227 KB/s], Decompressed: 412 Downloaded: 449 file(s) [attempted 449/8459 = 5%, 75 KB/s], Decompressed: 446 Downloaded: 485 file(s) [attempted 485/8459 = 5%, 78 KB/s], Decompressed: 480 Downloaded: 525 file(s) [attempted 525/8459 = 6%, 607 KB/s], Decompressed: 521 Downloaded: 566 file(s) [attempted 566/8459 = 6%, 164 KB/s], Decompressed: 562 Downloaded: 602 file(s) [attempted 602/8459 = 7%, 241 KB/s], Decompressed: 597 Downloaded: 641 file(s) [attempted 641/8459 = 7%, 86 KB/s], Decompressed: 634 Downloaded: 682 file(s) [attempted 682/8459 = 8%, 87 KB/s], Decompressed: 679 Downloaded: 727 file(s) [attempted 727/8459 = 8%, 75 KB/s], Decompressed: 723 Downloaded: 771 file(s) [attempted 771/8459 = 9%, 836 KB/s], Decompressed: 765 Downloaded: 804 file(s) [attempted 804/8459 = 9%, 117 KB/s], Decompressed: 799 Downloaded: 840 file(s) [attempted 840/8459 = 9%, 493 KB/s], Decompressed: 836 Downloaded: 884 file(s) [attempted 884/8459 = 10%, 37 KB/s], Decompressed: 881 Downloaded: 929 file(s) [attempted 929/8459 = 10%, 131 KB/s], Decompressed: 925 Downloaded: 970 file(s) [attempted 970/8459 = 11%, 284 KB/s], Decompressed: 967 Downloaded: 1004 file(s) [attempted 1004/8459 = 11%, 113 KB/s], Decompressed: 997 Downloaded: 1041 file(s) [attempted 1041/8459 = 12%, 873 KB/s], Decompressed: 1035 Downloaded: 1083 file(s) [attempted 1083/8459 = 12%, 217 KB/s], Decompressed: 1080 Downloaded: 1127 file(s) [attempted 1127/8459 = 13%, 145 KB/s], Decompressed: 1124 Downloaded: 1164 file(s) [attempted 1164/8459 = 13%, 322 KB/s], Decompressed: 1158 Downloaded: 1196 file(s) [attempted 1196/8459 = 14%, 508 KB/s], Decompressed: 1192 Downloaded: 1240 file(s) [attempted 1240/8459 = 14%, 34 KB/s], Decompressed: 1237 Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 522 KB/s], Decompressed: 1278 Downloaded: 1324 file(s) [attempted 1324/8459 = 15%, 358 KB/s], Decompressed: 1319 Downloaded: 1354 file(s) [attempted 1354/8459 = 16%, 148 KB/s], Decompressed: 1350 Downloaded: 1395 file(s) [attempted 1395/8459 = 16%, 44 KB/s], Decompressed: 1391 Downloaded: 1435 file(s) [attempted 1435/8459 = 16%, 480 KB/s], Decompressed: 1432 Downloaded: 1474 file(s) [attempted 1474/8459 = 17%, 581 KB/s], Decompressed: 1470 Downloaded: 1511 file(s) [attempted 1511/8459 = 17%, 133 KB/s], Decompressed: 1505 Downloaded: 1548 file(s) [attempted 1548/8459 = 18%, 168 KB/s], Decompressed: 1542 Downloaded: 1589 file(s) [attempted 1589/8459 = 18%, 401 KB/s], Decompressed: 1586 Downloaded: 1634 file(s) [attempted 1634/8459 = 19%, 244 KB/s], Decompressed: 1631 Downloaded: 1675 file(s) [attempted 1675/8459 = 19%, 110 KB/s], Decompressed: 1668 Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 418 KB/s], Decompressed: 1709 Downloaded: 1754 file(s) [attempted 1754/8459 = 20%, 360 KB/s], Decompressed: 1750 Downloaded: 1795 file(s) [attempted 1795/8459 = 21%, 25 KB/s], Decompressed: 1791 Downloaded: 1834 file(s) [attempted 1834/8459 = 21%, 67 KB/s], Decompressed: 1829 Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 270 KB/s], Decompressed: 1863 Downloaded: 1909 file(s) [attempted 1909/8459 = 22%, 514 KB/s], Decompressed: 1904 Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 723 KB/s], Decompressed: 1945 Downloaded: 1990 file(s) [attempted 1990/8459 = 23%, 990 KB/s], Decompressed: 1988 Downloaded: 2021 file(s) [attempted 2021/8459 = 23%, 316 KB/s], Decompressed: 2014 Downloaded: 2062 file(s) [attempted 2062/8459 = 24%, 57 KB/s], Decompressed: 2058 Downloaded: 2103 file(s) [attempted 2103/8459 = 24%, 456 KB/s], Decompressed: 2099 Downloaded: 2147 file(s) [attempted 2147/8459 = 25%, 79 KB/s], Decompressed: 2144 Downloaded: 2192 file(s) [attempted 2192/8459 = 25%, 440 KB/s], Decompressed: 2188 Downloaded: 2224 file(s) [attempted 2224/8459 = 26%, 168 KB/s], Decompressed: 2216 Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 25 KB/s], Decompressed: 2253 Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 910 KB/s], Decompressed: 2291 Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 123 KB/s], Decompressed: 2329 Downloaded: 2371 file(s) [attempted 2371/8459 = 28%, 223 KB/s], Decompressed: 2366 Downloaded: 2407 file(s) [attempted 2407/8459 = 28%, 289 KB/s], Decompressed: 2404 Downloaded: 2445 file(s) [attempted 2445/8459 = 28%, 262 KB/s], Decompressed: 2442 Downloaded: 2486 file(s) [attempted 2486/8459 = 29%, 131 KB/s], Decompressed: 2479 Downloaded: 2520 file(s) [attempted 2520/8459 = 29%, 48 KB/s], Decompressed: 2517 Downloaded: 2561 file(s) [attempted 2561/8459 = 30%, 674 KB/s], Decompressed: 2558 Downloaded: 2603 file(s) [attempted 2603/8459 = 30%, 571 KB/s], Decompressed: 2599 Downloaded: 2646 file(s) [attempted 2646/8459 = 31%, 195 KB/s], Decompressed: 2640 Downloaded: 2685 file(s) [attempted 2685/8459 = 31%, 350 KB/s], Decompressed: 2678 Downloaded: 2717 file(s) [attempted 2717/8459 = 32%, 474 KB/s], Decompressed: 2712 Downloaded: 2753 file(s) [attempted 2753/8459 = 32%, 198 KB/s], Decompressed: 2750 Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 156 KB/s], Decompressed: 2794 Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 248 KB/s], Decompressed: 2832 Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 84 KB/s], Decompressed: 2873 Downloaded: 2915 file(s) [attempted 2915/8459 = 34%, 224 KB/s], Decompressed: 2911 Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 917 KB/s], Decompressed: 2948 Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 971 KB/s], Decompressed: 2993 Downloaded: 3034 file(s) [attempted 3034/8459 = 35%, 145 KB/s], Decompressed: 3030 Downloaded: 3075 file(s) [attempted 3075/8459 = 36%, 211 KB/s], Decompressed: 3071 Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 74 KB/s], Decompressed: 3112 Downloaded: 3154 file(s) [attempted 3154/8459 = 37%, 211 KB/s], Decompressed: 3150 Downloaded: 3188 file(s) [attempted 3188/8459 = 37%, 233 KB/s], Decompressed: 3184 Downloaded: 3225 file(s) [attempted 3225/8459 = 38%, 159 KB/s], Decompressed: 3222 Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 211 KB/s], Decompressed: 3266 Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 116 KB/s], Decompressed: 3314 Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 40 KB/s], Decompressed: 3359 Downloaded: 3403 file(s) [attempted 3403/8459 = 40%, 403 KB/s], Decompressed: 3400 Downloaded: 3439 file(s) [attempted 3439/8459 = 40%, 254 KB/s], Decompressed: 3434 Downloaded: 3479 file(s) [attempted 3479/8459 = 41%, 163 KB/s], Decompressed: 3472 Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 226 KB/s], Decompressed: 3516 Downloaded: 3561 file(s) [attempted 3561/8459 = 42%, 417 KB/s], Decompressed: 3557 Downloaded: 3600 file(s) [attempted 3600/8459 = 42%, 108 KB/s], Decompressed: 3595 Downloaded: 3638 file(s) [attempted 3638/8459 = 43%, 108 KB/s], Decompressed: 3629 Downloaded: 3676 file(s) [attempted 3676/8459 = 43%, 370 KB/s], Decompressed: 3667 Downloaded: 3715 file(s) [attempted 3715/8459 = 43%, 363 KB/s], Decompressed: 3711 Downloaded: 3751 file(s) [attempted 3751/8459 = 44%, 78 KB/s], Decompressed: 3746 Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 170 KB/s], Decompressed: 3787 Downloaded: 3835 file(s) [attempted 3835/8459 = 45%, 201 KB/s], Decompressed: 3831 Downloaded: 3879 file(s) [attempted 3879/8459 = 45%, 117 KB/s], Decompressed: 3876 Downloaded: 3915 file(s) [attempted 3915/8459 = 46%, 2519 KB/s], Decompressed: 3906 Downloaded: 3949 file(s) [attempted 3949/8459 = 46%, 345 KB/s], Decompressed: 3944 Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 574 KB/s], Decompressed: 3989 Downloaded: 4033 file(s) [attempted 4033/8459 = 47%, 951 KB/s], Decompressed: 4026 Downloaded: 4068 file(s) [attempted 4068/8459 = 48%, 271 KB/s], Decompressed: 4060 Downloaded: 4102 file(s) [attempted 4102/8459 = 48%, 458 KB/s], Decompressed: 4098 Downloaded: 4146 file(s) [attempted 4146/8459 = 49%, 807 KB/s], Decompressed: 4143 Downloaded: 4187 file(s) [attempted 4187/8459 = 49%, 337 KB/s], Decompressed: 4180 Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 43 KB/s], Decompressed: 4221 Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 219 KB/s], Decompressed: 4266 Downloaded: 4308 file(s) [attempted 4308/8459 = 50%, 231 KB/s], Decompressed: 4303 Downloaded: 4347 file(s) [attempted 4347/8459 = 51%, 172 KB/s], Decompressed: 4341 Downloaded: 4386 file(s) [attempted 4386/8459 = 51%, 453 KB/s], Decompressed: 4382 Downloaded: 4420 file(s) [attempted 4420/8459 = 52%, 140 KB/s], Decompressed: 4416 Downloaded: 4461 file(s) [attempted 4461/8459 = 52%, 93 KB/s], Decompressed: 4457 Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 304 KB/s], Decompressed: 4499 Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 458 KB/s], Decompressed: 4540 Downloaded: 4585 file(s) [attempted 4585/8459 = 54%, 599 KB/s], Decompressed: 4577 Downloaded: 4618 file(s) [attempted 4618/8459 = 54%, 928 KB/s], Decompressed: 4615 Downloaded: 4656 file(s) [attempted 4656/8459 = 55%, 56 KB/s], Decompressed: 4649 Downloaded: 4697 file(s) [attempted 4697/8459 = 55%, 35 KB/s], Decompressed: 4694 Downloaded: 4742 file(s) [attempted 4742/8459 = 56%, 421 KB/s], Decompressed: 4735 Downloaded: 4779 file(s) [attempted 4779/8459 = 56%, 138 KB/s], Decompressed: 4776 Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 402 KB/s], Decompressed: 4810 Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 62 KB/s], Decompressed: 4851 Downloaded: 4896 file(s) [attempted 4896/8459 = 57%, 838 KB/s], Decompressed: 4892 Downloaded: 4937 file(s) [attempted 4937/8459 = 58%, 23 KB/s], Decompressed: 4933 Downloaded: 4974 file(s) [attempted 4974/8459 = 58%, 499 KB/s], Decompressed: 4971 Downloaded: 5008 file(s) [attempted 5008/8459 = 59%, 60 KB/s], Decompressed: 5005 Downloaded: 5050 file(s) [attempted 5050/8459 = 59%, 464 KB/s], Decompressed: 5046 Downloaded: 5094 file(s) [attempted 5094/8459 = 60%, 928 KB/s], Decompressed: 5091 Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 598 KB/s], Decompressed: 5125 Downloaded: 5169 file(s) [attempted 5169/8459 = 61%, 111 KB/s], Decompressed: 5162 Downloaded: 5204 file(s) [attempted 5204/8459 = 61%, 119 KB/s], Decompressed: 5200 Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 230 KB/s], Decompressed: 5241 Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 273 KB/s], Decompressed: 5279 Downloaded: 5323 file(s) [attempted 5323/8459 = 62%, 63 KB/s], Decompressed: 5320 Downloaded: 5362 file(s) [attempted 5362/8459 = 63%, 444 KB/s], Decompressed: 5359 Downloaded: 5402 file(s) [attempted 5402/8459 = 63%, 281 KB/s], Decompressed: 5399 Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 466 KB/s], Decompressed: 5436 Downloaded: 5483 file(s) [attempted 5483/8459 = 64%, 299 KB/s], Decompressed: 5477 Downloaded: 5522 file(s) [attempted 5522/8459 = 65%, 161 KB/s], Decompressed: 5518 Downloaded: 5563 file(s) [attempted 5563/8459 = 65%, 80 KB/s], Decompressed: 5559 Downloaded: 5597 file(s) [attempted 5597/8459 = 66%, 646 KB/s], Decompressed: 5594 Downloaded: 5638 file(s) [attempted 5638/8459 = 66%, 141 KB/s], Decompressed: 5635 Downloaded: 5676 file(s) [attempted 5676/8459 = 67%, 58 KB/s], Decompressed: 5669 Downloaded: 5718 file(s) [attempted 5718/8459 = 67%, 169 KB/s], Decompressed: 5713 Downloaded: 5751 file(s) [attempted 5751/8459 = 67%, 306 KB/s], Decompressed: 5750 Downloaded: 5789 file(s) [attempted 5789/8459 = 68%, 235 KB/s], Decompressed: 5785 Downloaded: 5829 file(s) [attempted 5829/8459 = 68%, 1149 KB/s], Decompressed: 5823 Downloaded: 5871 file(s) [attempted 5871/8459 = 69%, 175 KB/s], Decompressed: 5857 Downloaded: 5903 file(s) [attempted 5903/8459 = 69%, 339 KB/s], Decompressed: 5898 Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 822 KB/s], Decompressed: 5936 Downloaded: 5980 file(s) [attempted 5980/8459 = 70%, 1520 KB/s], Decompressed: 5977 Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 76 KB/s], Decompressed: 6021 Downloaded: 6063 file(s) [attempted 6063/8459 = 71%, 1048 KB/s], Decompressed: 6059 Downloaded: 6104 file(s) [attempted 6104/8459 = 72%, 192 KB/s], Decompressed: 6098 Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 68 KB/s], Decompressed: 6138 Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 55 KB/s], Decompressed: 6179 Downloaded: 6221 file(s) [attempted 6221/8459 = 73%, 135 KB/s], Decompressed: 6217 Downloaded: 6262 file(s) [attempted 6262/8459 = 74%, 125 KB/s], Decompressed: 6258 Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 2696 KB/s], Decompressed: 6288 Downloaded: 6334 file(s) [attempted 6334/8459 = 74%, 35 KB/s], Decompressed: 6329 Downloaded: 6371 file(s) [attempted 6371/8459 = 75%, 352 KB/s], Decompressed: 6367 Downloaded: 6414 file(s) [attempted 6414/8459 = 75%, 82 KB/s], Decompressed: 6408 Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 751 KB/s], Decompressed: 6446 Downloaded: 6490 file(s) [attempted 6490/8459 = 76%, 161 KB/s], Decompressed: 6487 Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 488 KB/s], Decompressed: 6525 Downloaded: 6569 file(s) [attempted 6569/8459 = 77%, 141 KB/s], Decompressed: 6566 Downloaded: 6611 file(s) [attempted 6611/8459 = 78%, 575 KB/s], Decompressed: 6607 Downloaded: 6651 file(s) [attempted 6651/8459 = 78%, 460 KB/s], Decompressed: 6648 Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 151 KB/s], Decompressed: 6679 Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 163 KB/s], Decompressed: 6723 Downloaded: 6770 file(s) [attempted 6770/8459 = 80%, 1304 KB/s], Decompressed: 6764 Downloaded: 6805 file(s) [attempted 6805/8459 = 80%, 220 KB/s], Decompressed: 6802 Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 54 KB/s], Decompressed: 6839 Downloaded: 6881 file(s) [attempted 6881/8459 = 81%, 225 KB/s], Decompressed: 6877 Downloaded: 6922 file(s) [attempted 6922/8459 = 81%, 359 KB/s], Decompressed: 6918 Downloaded: 6963 file(s) [attempted 6963/8459 = 82%, 168 KB/s], Decompressed: 6959 Downloaded: 6993 file(s) [attempted 6993/8459 = 82%, 232 KB/s], Decompressed: 6990 Downloaded: 7038 file(s) [attempted 7038/8459 = 83%, 152 KB/s], Decompressed: 7035 Downloaded: 7078 file(s) [attempted 7078/8459 = 83%, 480 KB/s], Decompressed: 7072 Downloaded: 7114 file(s) [attempted 7114/8459 = 84%, 285 KB/s], Decompressed: 7110 Downloaded: 7152 file(s) [attempted 7152/8459 = 84%, 441 KB/s], Decompressed: 7147 Downloaded: 7192 file(s) [attempted 7192/8459 = 85%, 55 KB/s], Decompressed: 7189 Downloaded: 7233 file(s) [attempted 7233/8459 = 85%, 879 KB/s], Decompressed: 7230 Downloaded: 7267 file(s) [attempted 7267/8459 = 85%, 112 KB/s], Decompressed: 7260 Downloaded: 7308 file(s) [attempted 7308/8459 = 86%, 36 KB/s], Decompressed: 7301 Downloaded: 7353 file(s) [attempted 7353/8459 = 86%, 69 KB/s], Decompressed: 7349 Downloaded: 7394 file(s) [attempted 7394/8459 = 87%, 267 KB/s], Decompressed: 7390 Downloaded: 7438 file(s) [attempted 7438/8459 = 87%, 98 KB/s], Decompressed: 7435 Downloaded: 7470 file(s) [attempted 7470/8459 = 88%, 179 KB/s], Decompressed: 7466 Downloaded: 7505 file(s) [attempted 7505/8459 = 88%, 429 KB/s], Decompressed: 7500 Downloaded: 7551 file(s) [attempted 7551/8459 = 89%, 92 KB/s], Decompressed: 7548 Downloaded: 7599 file(s) [attempted 7599/8459 = 89%, 1044 KB/s], Decompressed: 7596 Downloaded: 7644 file(s) [attempted 7644/8459 = 90%, 855 KB/s], Decompressed: 7640 Downloaded: 7674 file(s) [attempted 7674/8459 = 90%, 348 KB/s], Decompressed: 7671 Downloaded: 7712 file(s) [attempted 7712/8459 = 91%, 453 KB/s], Decompressed: 7709 Downloaded: 7757 file(s) [attempted 7757/8459 = 91%, 114 KB/s], Decompressed: 7753 Downloaded: 7799 file(s) [attempted 7799/8459 = 92%, 159 KB/s], Decompressed: 7794 Downloaded: 7833 file(s) [attempted 7833/8459 = 92%, 703 KB/s], Decompressed: 7825 Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 49 KB/s], Decompressed: 7863 Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 817 KB/s], Decompressed: 7904 Downloaded: 7952 file(s) [attempted 7952/8459 = 94%, 119 KB/s], Decompressed: 7948 Downloaded: 7993 file(s) [attempted 7993/8459 = 94%, 184 KB/s], Decompressed: 7982 Downloaded: 8027 file(s) [attempted 8027/8459 = 94%, 558 KB/s], Decompressed: 8024 Downloaded: 8070 file(s) [attempted 8070/8459 = 95%, 248 KB/s], Decompressed: 8061 Downloaded: 8108 file(s) [attempted 8108/8459 = 95%, 95 KB/s], Decompressed: 8102 Downloaded: 8147 file(s) [attempted 8147/8459 = 96%, 589 KB/s], Decompressed: 8140 Downloaded: 8184 file(s) [attempted 8184/8459 = 96%, 1293 KB/s], Decompressed: 8178 Downloaded: 8222 file(s) [attempted 8222/8459 = 97%, 415 KB/s], Decompressed: 8219 Downloaded: 8261 file(s) [attempted 8261/8459 = 97%, 223 KB/s], Decompressed: 8256 Downloaded: 8301 file(s) [attempted 8301/8459 = 98%, 447 KB/s], Decompressed: 8297 Downloaded: 8338 file(s) [attempted 8338/8459 = 98%, 94 KB/s], Decompressed: 8335 Downloaded: 8374 file(s) [attempted 8374/8459 = 98%, 102 KB/s], Decompressed: 8369 Downloaded: 8417 file(s) [attempted 8417/8459 = 99%, 434 KB/s], Decompressed: 8414 Downloaded: 8450 file(s) [attempted 8450/8459 = 99%, 167 KB/s], Decompressed: 8441 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 249 KB/s], Decompressed: 8448 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 249 KB/s], Decompressed: 8448
lean_checker exit 0
lake build
ℹ [3410/3416] Replayed Iut.Stage1.IUTStage1FrobenioidShift info: stderr: PANIC at _private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.Environment.unsafeRunMetaM Lean.LibrarySuggestions.SymbolFrequency:71:24: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context) backtrace: /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85c6785) [0x7792f29c6785] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x7792f29bdb27] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x7792f29bdc0b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x7792f28f3c62] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x7792f28f4439] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x7792f29caf99] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x7792f2832923] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x7792f2832b2b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x7792f2833827] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x7792f28341b6] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x7792f29c9e8b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x7792f2615adb] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7792f29c9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x7792f29c9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x7792f299b1f3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x7792f2615c92] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x7792eda22638] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x7792ed80cd2e] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x7792ed369a82] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x7792ed369f0e] /lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x7792ea24524a] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x7792ea245305] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5e715c4c08da] 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 0
./.apodeixis/tools/lean-semantic-extract.sh --module-facts (module-facts-batch-00007)
lean semantic helper: restored compiled static runner cache b8207442bfba00511b560efc544d5ce67b0aa813df3d432a1aba6b1f99808bdf 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-00008)
lean semantic helper: restored compiled static runner cache 56cf09ccb3908696b8e5e7742ce037825c061cf4f72cf51826c370ecdd278b63 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-00009)
lean semantic helper: restored compiled static runner cache 82cff17b2a0859360c864be978661e734ea49f8bd78dbf096db8866b58caf113 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-00011)
lean semantic helper: restored compiled static runner cache 6b68dbdfef85a7b6943bcf3aed743bff07bc5a8789269f4969952ccbec066986 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-00012)
lean semantic helper: restored compiled static runner cache 5a5015d089cfb0ec2d9e00c036585dab768f83e5b768c8aa0991818ae117b9aa 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-00013)
lean semantic helper: restored compiled static runner cache 916ea7b0333772c3e6f8e394e031f32699844624a1add271ecbcb781a9f49e93 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-00014)
lean semantic helper: restored compiled static runner cache 2bfcdcefc85e86330c36ad81e41c2ddb7c7e852d7b70484d888f87d3783eb3ee 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-00015)
lean semantic helper: restored compiled static runner cache ac720950978d81db58a9b7127c0c29b52147e5d60a6dd5804497dee52cf190ea 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-00016)
lean semantic helper: restored compiled static runner cache 8ce5ff6c967baef3842b8fb460ab7dc29b28a04bbb424be955c4371e23608184 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-00017)
lean semantic helper: restored compiled static runner cache f4d9c003c7452016e42c7fead986b54b7a3d6e7471516ee89e90353366820d66 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-00018)
lean semantic helper: restored compiled static runner cache 75b5977bf3c3f7790c74f7fcdf61319b52a6563d7e4b9f6920235cee9e6766b3 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-00019)
lean semantic helper: restored compiled static runner cache 0efd485e0463b19f5c2e2a591158e669acbf0d05b6feb20ce1b85cba88b2befe 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-00020)
lean semantic helper: restored compiled static runner cache 03585dcb70610534a4ce74449195125e05e01fddbca11f3263fb9006bd27c14e 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-00021)
lean semantic helper: restored compiled static runner cache 08877232589cf9db425b8187c7f232d1869e5ec11e14304e9a4a61a9b73231aa 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-00022)
lean semantic helper: restored compiled static runner cache e538f0251f041ef0b337d3bd2b02e2800bdae1a864fbf6b2380b52ffeb000535 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-00023)
lean semantic helper: restored compiled static runner cache b0ddeaaa2553229aaff1dc72c131add56ca5eaf65331b57c95c4ac371fadb91f 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-00024)
lean semantic helper: restored compiled static runner cache 6247def1945279a6946b34517b575ac426a9bd22cc4c3ceb7a79dc06ef4083db 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-00025)
lean semantic helper: restored compiled static runner cache 361c3a3115683a95ae5a195d9d3288c0f30083b629ae0efa02efc9266225a437 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-00026)
lean semantic helper: restored compiled static runner cache b1361ddd4d800407fee97079d7c69334e9fa98f8d8138ea91735fd01a42f86a2 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-00027)
lean semantic helper: restored compiled static runner cache 9c9cf2b3451621905e924ca74e022d2283294e8f723d50f83339e66904461aaf 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-00028)
lean semantic helper: restored compiled static runner cache e73538885b586c3d3ade36b614bd08578304e5f0d861b518f22c5a691c41fbd9 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-00029)
lean semantic helper: restored compiled static runner cache b278679b96703b88f46c5058abea7a921c64bde7c3009a5f675db878cd3eba6c 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-00030)
lean semantic helper: restored compiled static runner cache 789c65a0d29891fa409358efae098c665e03a540d880d2a888005d1f8a1e3e15 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-00000)
lean semantic helper: restored compiled static runner cache 361c3a3115683a95ae5a195d9d3288c0f30083b629ae0efa02efc9266225a437 warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes