Verification run
Run 357
succeededcommit
274e6323302atoolchain lean-v4-30-0prover leantook 3h 8m · finished 12w agoPackage inputs
This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.
Trust verification
Recomputes trust checks from the recorded attestations, manifest, and command history.
(verification not run)
Manifest
Loads the published files manifest and location metadata for this job.
(manifest not loaded)
Verifier log excerpt
(no log excerpt)
Command runs
git_cloneexit 0
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-525-source
Cloning into '/var/lib/apodeixis/repos/job-525-source'...
git_checkoutexit 128
git checkout 274e6323302a5b771a90562d496de45e98c98199
fatal: reference is not a tree: 274e6323302a5b771a90562d496de45e98c98199
git_checkoutexit 0
git fetch --depth 1 origin 274e6323302a5b771a90562d496de45e98c98199
From https://github.com/promachina/iut-lean * branch 274e6323302a5b771a90562d496de45e98c98199 -> FETCH_HEAD
git_checkoutexit 0
git checkout 274e6323302a5b771a90562d496de45e98c98199 (after fetch)
Note: switching to '274e6323302a5b771a90562d496de45e98c98199'. 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 274e632 Derive local log preimages placewise
lake_cacheexit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache Decompressed 8459 file(s) Already decompressed 8459 file(s)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes Downloaded: 1 file(s) [attempted 1/8459 = 0%, 9 KB/s], Decompressed: 0 Downloaded: 15 file(s) [attempted 15/8459 = 0%, 9 KB/s], Decompressed: 13 Downloaded: 38 file(s) [attempted 38/8459 = 0%, 18 KB/s], Decompressed: 32 Downloaded: 66 file(s) [attempted 66/8459 = 0%, 52 KB/s], Decompressed: 64 Downloaded: 91 file(s) [attempted 91/8459 = 1%, 186 KB/s], Decompressed: 82 Downloaded: 124 file(s) [attempted 124/8459 = 1%, 135 KB/s], Decompressed: 117 Downloaded: 158 file(s) [attempted 158/8459 = 1%, 97 KB/s], Decompressed: 155 Downloaded: 199 file(s) [attempted 199/8459 = 2%, 377 KB/s], Decompressed: 196 Downloaded: 240 file(s) [attempted 240/8459 = 2%, 127 KB/s], Decompressed: 237 Downloaded: 282 file(s) [attempted 282/8459 = 3%, 622 KB/s], Decompressed: 276 Downloaded: 313 file(s) [attempted 313/8459 = 3%, 493 KB/s], Decompressed: 309 Downloaded: 357 file(s) [attempted 357/8459 = 4%, 207 KB/s], Decompressed: 353 Downloaded: 395 file(s) [attempted 395/8459 = 4%, 182 KB/s], Decompressed: 391 Downloaded: 439 file(s) [attempted 439/8459 = 5%, 83 KB/s], Decompressed: 432 Downloaded: 481 file(s) [attempted 481/8459 = 5%, 410 KB/s], Decompressed: 470 Downloaded: 518 file(s) [attempted 518/8459 = 6%, 145 KB/s], Decompressed: 504 Downloaded: 552 file(s) [attempted 552/8459 = 6%, 1454 KB/s], Decompressed: 545 Downloaded: 593 file(s) [attempted 593/8459 = 7%, 270 KB/s], Decompressed: 590 Downloaded: 634 file(s) [attempted 634/8459 = 7%, 806 KB/s], Decompressed: 631 Downloaded: 679 file(s) [attempted 679/8459 = 8%, 151 KB/s], Decompressed: 675 Downloaded: 717 file(s) [attempted 717/8459 = 8%, 496 KB/s], Decompressed: 710 Downloaded: 751 file(s) [attempted 751/8459 = 8%, 62 KB/s], Decompressed: 747 Downloaded: 795 file(s) [attempted 795/8459 = 9%, 111 KB/s], Decompressed: 788 Downloaded: 836 file(s) [attempted 836/8459 = 9%, 712 KB/s], Decompressed: 833 Downloaded: 881 file(s) [attempted 881/8459 = 10%, 285 KB/s], Decompressed: 874 Downloaded: 919 file(s) [attempted 919/8459 = 10%, 149 KB/s], Decompressed: 915 Downloaded: 960 file(s) [attempted 960/8459 = 11%, 232 KB/s], Decompressed: 953 Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 558 KB/s], Decompressed: 997 Downloaded: 1042 file(s) [attempted 1042/8459 = 12%, 884 KB/s], Decompressed: 1038 Downloaded: 1083 file(s) [attempted 1083/8459 = 12%, 267 KB/s], Decompressed: 1076 Downloaded: 1124 file(s) [attempted 1124/8459 = 13%, 143 KB/s], Decompressed: 1121 Downloaded: 1169 file(s) [attempted 1169/8459 = 13%, 222 KB/s], Decompressed: 1158 Downloaded: 1203 file(s) [attempted 1203/8459 = 14%, 181 KB/s], Decompressed: 1192 Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 74 KB/s], Decompressed: 1237 Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 544 KB/s], Decompressed: 1278 Downloaded: 1326 file(s) [attempted 1326/8459 = 15%, 1058 KB/s], Decompressed: 1323 Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 136 KB/s], Decompressed: 1360 Downloaded: 1405 file(s) [attempted 1405/8459 = 16%, 428 KB/s], Decompressed: 1398 Downloaded: 1446 file(s) [attempted 1446/8459 = 17%, 152 KB/s], Decompressed: 1439 Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 51 KB/s], Decompressed: 1439 Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 25 KB/s], Decompressed: 1446 Downloaded: 1572 file(s) [attempted 1572/8459 = 18%, 86 KB/s], Decompressed: 1446 Downloaded: 1613 file(s) [attempted 1613/8459 = 19%, 192 KB/s], Decompressed: 1446 Downloaded: 1648 file(s) [attempted 1648/8459 = 19%, 336 KB/s], Decompressed: 1637 Downloaded: 1692 file(s) [attempted 1692/8459 = 20%, 156 KB/s], Decompressed: 1685 Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 239 KB/s], Decompressed: 1729 Downloaded: 1774 file(s) [attempted 1774/8459 = 20%, 28 KB/s], Decompressed: 1771 Downloaded: 1816 file(s) [attempted 1816/8459 = 21%, 161 KB/s], Decompressed: 1809 Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 128 KB/s], Decompressed: 1853 Downloaded: 1896 file(s) [attempted 1896/8459 = 22%, 43 KB/s], Decompressed: 1891 Downloaded: 1931 file(s) [attempted 1931/8459 = 22%, 292 KB/s], Decompressed: 1925 Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 44 KB/s], Decompressed: 1969 Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 308 KB/s], Decompressed: 2021 Downloaded: 2069 file(s) [attempted 2069/8459 = 24%, 912 KB/s], Decompressed: 2065 Downloaded: 2106 file(s) [attempted 2106/8459 = 24%, 132 KB/s], Decompressed: 2103 Downloaded: 2148 file(s) [attempted 2148/8459 = 25%, 1669 KB/s], Decompressed: 2140 Downloaded: 2185 file(s) [attempted 2185/8459 = 25%, 486 KB/s], Decompressed: 2182 Downloaded: 2225 file(s) [attempted 2225/8459 = 26%, 301 KB/s], Decompressed: 2219 Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 205 KB/s], Decompressed: 2257 Downloaded: 2305 file(s) [attempted 2305/8459 = 27%, 123 KB/s], Decompressed: 2298 Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 168 KB/s], Decompressed: 2339 Downloaded: 2380 file(s) [attempted 2380/8459 = 28%, 108 KB/s], Decompressed: 2373 Downloaded: 2421 file(s) [attempted 2421/8459 = 28%, 35 KB/s], Decompressed: 2414 Downloaded: 2466 file(s) [attempted 2466/8459 = 29%, 242 KB/s], Decompressed: 2462 Downloaded: 2504 file(s) [attempted 2504/8459 = 29%, 89 KB/s], Decompressed: 2496 Downloaded: 2541 file(s) [attempted 2541/8459 = 30%, 331 KB/s], Decompressed: 2534 Downloaded: 2579 file(s) [attempted 2579/8459 = 30%, 109 KB/s], Decompressed: 2572 Downloaded: 2620 file(s) [attempted 2620/8459 = 30%, 260 KB/s], Decompressed: 2616 Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 589 KB/s], Decompressed: 2654 Downloaded: 2693 file(s) [attempted 2693/8459 = 31%, 334 KB/s], Decompressed: 2688 Downloaded: 2736 file(s) [attempted 2736/8459 = 32%, 123 KB/s], Decompressed: 2729 Downloaded: 2774 file(s) [attempted 2774/8459 = 32%, 243 KB/s], Decompressed: 2763 Downloaded: 2815 file(s) [attempted 2815/8459 = 33%, 776 KB/s], Decompressed: 2811 Downloaded: 2856 file(s) [attempted 2856/8459 = 33%, 324 KB/s], Decompressed: 2849 Downloaded: 2891 file(s) [attempted 2891/8459 = 34%, 28 KB/s], Decompressed: 2887 Downloaded: 2934 file(s) [attempted 2934/8459 = 34%, 110 KB/s], Decompressed: 2924 Downloaded: 2979 file(s) [attempted 2979/8459 = 35%, 594 KB/s], Decompressed: 2924 Downloaded: 3020 file(s) [attempted 3020/8459 = 35%, 200 KB/s], Decompressed: 2928 Downloaded: 3058 file(s) [attempted 3058/8459 = 36%, 312 KB/s], Decompressed: 3051 Downloaded: 3094 file(s) [attempted 3094/8459 = 36%, 300 KB/s], Decompressed: 3088 Downloaded: 3133 file(s) [attempted 3133/8459 = 37%, 1023 KB/s], Decompressed: 3130 Downloaded: 3177 file(s) [attempted 3177/8459 = 37%, 82 KB/s], Decompressed: 3174 Downloaded: 3221 file(s) [attempted 3221/8459 = 38%, 1465 KB/s], Decompressed: 3215 Downloaded: 3253 file(s) [attempted 3253/8459 = 38%, 1418 KB/s], Decompressed: 3242 Downloaded: 3290 file(s) [attempted 3290/8459 = 38%, 314 KB/s], Decompressed: 3287 Downloaded: 3335 file(s) [attempted 3335/8459 = 39%, 146 KB/s], Decompressed: 3331 Downloaded: 3376 file(s) [attempted 3376/8459 = 39%, 483 KB/s], Decompressed: 3373 Downloaded: 3420 file(s) [attempted 3420/8459 = 40%, 353 KB/s], Decompressed: 3414 Downloaded: 3455 file(s) [attempted 3455/8459 = 40%, 471 KB/s], Decompressed: 3451 Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 192 KB/s], Decompressed: 3489 Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 165 KB/s], Decompressed: 3531 Downloaded: 3575 file(s) [attempted 3575/8459 = 42%, 186 KB/s], Decompressed: 3571 Downloaded: 3617 file(s) [attempted 3617/8459 = 42%, 566 KB/s], Decompressed: 3609 Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 692 KB/s], Decompressed: 3646 Downloaded: 3693 file(s) [attempted 3693/8459 = 43%, 53 KB/s], Decompressed: 3687 Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 288 KB/s], Decompressed: 3725 Downloaded: 3770 file(s) [attempted 3770/8459 = 44%, 300 KB/s], Decompressed: 3766 Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 101 KB/s], Decompressed: 3807 Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 430 KB/s], Decompressed: 3845 Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 407 KB/s], Decompressed: 3886 Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 69 KB/s], Decompressed: 3927 Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 176 KB/s], Decompressed: 3961 Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 1864 KB/s], Decompressed: 3961 Downloaded: 4059 file(s) [attempted 4059/8459 = 47%, 384 KB/s], Decompressed: 3961 Downloaded: 4094 file(s) [attempted 4094/8459 = 48%, 182 KB/s], Decompressed: 3968 Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 631 KB/s], Decompressed: 4125 Downloaded: 4177 file(s) [attempted 4177/8459 = 49%, 48 KB/s], Decompressed: 4173 Downloaded: 4214 file(s) [attempted 4214/8459 = 49%, 70 KB/s], Decompressed: 4208 Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 53 KB/s], Decompressed: 4242 Downloaded: 4286 file(s) [attempted 4286/8459 = 50%, 320 KB/s], Decompressed: 4283 Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 187 KB/s], Decompressed: 4324 Downloaded: 4375 file(s) [attempted 4375/8459 = 51%, 166 KB/s], Decompressed: 4368 Downloaded: 4412 file(s) [attempted 4412/8459 = 52%, 1146 KB/s], Decompressed: 4403 Downloaded: 4449 file(s) [attempted 4449/8459 = 52%, 371 KB/s], Decompressed: 4440 Downloaded: 4485 file(s) [attempted 4485/8459 = 53%, 364 KB/s], Decompressed: 4475 Downloaded: 4529 file(s) [attempted 4529/8459 = 53%, 60 KB/s], Decompressed: 4522 Downloaded: 4570 file(s) [attempted 4570/8459 = 54%, 67 KB/s], Decompressed: 4560 Downloaded: 4610 file(s) [attempted 4610/8459 = 54%, 349 KB/s], Decompressed: 4601 Downloaded: 4644 file(s) [attempted 4644/8459 = 54%, 112 KB/s], Decompressed: 4635 Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 360 KB/s], Decompressed: 4666 Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 100 KB/s], Decompressed: 4666 Downloaded: 4769 file(s) [attempted 4769/8459 = 56%, 329 KB/s], Decompressed: 4666 Downloaded: 4808 file(s) [attempted 4808/8459 = 56%, 93 KB/s], Decompressed: 4670 Downloaded: 4848 file(s) [attempted 4848/8459 = 57%, 280 KB/s], Decompressed: 4670 Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 212 KB/s], Decompressed: 4670 Downloaded: 4930 file(s) [attempted 4930/8459 = 58%, 132 KB/s], Decompressed: 4670 Downloaded: 4974 file(s) [attempted 4974/8459 = 58%, 179 KB/s], Decompressed: 4789 Downloaded: 5015 file(s) [attempted 5015/8459 = 59%, 792 KB/s], Decompressed: 4789 Downloaded: 5050 file(s) [attempted 5050/8459 = 59%, 139 KB/s], Decompressed: 4789 Downloaded: 5091 file(s) [attempted 5091/8459 = 60%, 197 KB/s], Decompressed: 4789 Downloaded: 5132 file(s) [attempted 5132/8459 = 60%, 489 KB/s], Decompressed: 4789 Downloaded: 5169 file(s) [attempted 5169/8459 = 61%, 74 KB/s], Decompressed: 4789 Downloaded: 5214 file(s) [attempted 5214/8459 = 61%, 46 KB/s], Decompressed: 4954 Downloaded: 5251 file(s) [attempted 5251/8459 = 62%, 267 KB/s], Decompressed: 4954 Downloaded: 5293 file(s) [attempted 5293/8459 = 62%, 1464 KB/s], Decompressed: 4954 Downloaded: 5332 file(s) [attempted 5332/8459 = 63%, 1021 KB/s], Decompressed: 5323 Downloaded: 5368 file(s) [attempted 5368/8459 = 63%, 1130 KB/s], Decompressed: 5364 Downloaded: 5412 file(s) [attempted 5412/8459 = 63%, 164 KB/s], Decompressed: 5409 Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 351 KB/s], Decompressed: 5450 Downloaded: 5498 file(s) [attempted 5498/8459 = 64%, 301 KB/s], Decompressed: 5481 Downloaded: 5539 file(s) [attempted 5539/8459 = 65%, 301 KB/s], Decompressed: 5481 Downloaded: 5573 file(s) [attempted 5573/8459 = 65%, 830 KB/s], Decompressed: 5481 Downloaded: 5618 file(s) [attempted 5618/8459 = 66%, 1117 KB/s], Decompressed: 5481 Downloaded: 5666 file(s) [attempted 5666/8459 = 66%, 229 KB/s], Decompressed: 5490 Downloaded: 5710 file(s) [attempted 5710/8459 = 67%, 565 KB/s], Decompressed: 5700 Downloaded: 5748 file(s) [attempted 5748/8459 = 67%, 30 KB/s], Decompressed: 5744 Downloaded: 5789 file(s) [attempted 5789/8459 = 68%, 63 KB/s], Decompressed: 5785 Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 102 KB/s], Decompressed: 5789 Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 206 KB/s], Decompressed: 5789 Downloaded: 5905 file(s) [attempted 5905/8459 = 69%, 71 KB/s], Decompressed: 5792 Downloaded: 5939 file(s) [attempted 5939/8459 = 70%, 352 KB/s], Decompressed: 5891 Downloaded: 5980 file(s) [attempted 5980/8459 = 70%, 1497 KB/s], Decompressed: 5912 Downloaded: 6018 file(s) [attempted 6018/8459 = 71%, 291 KB/s], Decompressed: 5912 Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 167 KB/s], Decompressed: 5970 Downloaded: 6100 file(s) [attempted 6100/8459 = 72%, 57 KB/s], Decompressed: 6035 Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 126 KB/s], Decompressed: 6035 Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 548 KB/s], Decompressed: 6035 Downloaded: 6217 file(s) [attempted 6217/8459 = 73%, 309 KB/s], Decompressed: 6035 Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 69 KB/s], Decompressed: 6035 Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 240 KB/s], Decompressed: 6086 Downloaded: 6336 file(s) [attempted 6336/8459 = 74%, 777 KB/s], Decompressed: 6086 Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 491 KB/s], Decompressed: 6295 Downloaded: 6418 file(s) [attempted 6418/8459 = 75%, 1595 KB/s], Decompressed: 6295 Downloaded: 6460 file(s) [attempted 6460/8459 = 76%, 620 KB/s], Decompressed: 6343 Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 77 KB/s], Decompressed: 6343 Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 47 KB/s], Decompressed: 6343 Downloaded: 6576 file(s) [attempted 6576/8459 = 77%, 496 KB/s], Decompressed: 6425 Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 93 KB/s], Decompressed: 6425 Downloaded: 6661 file(s) [attempted 6661/8459 = 78%, 336 KB/s], Decompressed: 6562 Downloaded: 6696 file(s) [attempted 6696/8459 = 79%, 47 KB/s], Decompressed: 6562 Downloaded: 6733 file(s) [attempted 6733/8459 = 79%, 397 KB/s], Decompressed: 6562 Downloaded: 6778 file(s) [attempted 6778/8459 = 80%, 977 KB/s], Decompressed: 6641 Downloaded: 6819 file(s) [attempted 6819/8459 = 80%, 127 KB/s], Decompressed: 6641 Downloaded: 6863 file(s) [attempted 6863/8459 = 81%, 109 KB/s], Decompressed: 6641 Downloaded: 6908 file(s) [attempted 6908/8459 = 81%, 223 KB/s], Decompressed: 6641 Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 449 KB/s], Decompressed: 6641 Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 110 KB/s], Decompressed: 6747 Downloaded: 7021 file(s) [attempted 7021/8459 = 83%, 451 KB/s], Decompressed: 6747 Downloaded: 7062 file(s) [attempted 7062/8459 = 83%, 87 KB/s], Decompressed: 6747 Downloaded: 7103 file(s) [attempted 7103/8459 = 83%, 180 KB/s], Decompressed: 6963 Downloaded: 7139 file(s) [attempted 7139/8459 = 84%, 114 KB/s], Decompressed: 7134 Downloaded: 7182 file(s) [attempted 7182/8459 = 84%, 287 KB/s], Decompressed: 7171 Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 281 KB/s], Decompressed: 7171 Downloaded: 7264 file(s) [attempted 7264/8459 = 85%, 121 KB/s], Decompressed: 7171 Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 146 KB/s], Decompressed: 7178 Downloaded: 7342 file(s) [attempted 7342/8459 = 86%, 526 KB/s], Decompressed: 7178 Downloaded: 7387 file(s) [attempted 7387/8459 = 87%, 243 KB/s], Decompressed: 7178 Downloaded: 7428 file(s) [attempted 7428/8459 = 87%, 101 KB/s], Decompressed: 7271 Downloaded: 7473 file(s) [attempted 7473/8459 = 88%, 180 KB/s], Decompressed: 7271 Downloaded: 7517 file(s) [attempted 7517/8459 = 88%, 195 KB/s], Decompressed: 7271 Downloaded: 7552 file(s) [attempted 7552/8459 = 89%, 948 KB/s], Decompressed: 7271 Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 142 KB/s], Decompressed: 7572 Downloaded: 7630 file(s) [attempted 7630/8459 = 90%, 129 KB/s], Decompressed: 7623 Downloaded: 7671 file(s) [attempted 7671/8459 = 90%, 38 KB/s], Decompressed: 7637 Downloaded: 7712 file(s) [attempted 7712/8459 = 91%, 126 KB/s], Decompressed: 7637 Downloaded: 7750 file(s) [attempted 7750/8459 = 91%, 219 KB/s], Decompressed: 7637 Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 112 KB/s], Decompressed: 7640 Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 487 KB/s], Decompressed: 7640 Downloaded: 7869 file(s) [attempted 7869/8459 = 93%, 487 KB/s], Decompressed: 7640 Downloaded: 7909 file(s) [attempted 7909/8459 = 93%, 1540 KB/s], Decompressed: 7897 Downloaded: 7943 file(s) [attempted 7943/8459 = 93%, 38 KB/s], Decompressed: 7931 Downloaded: 7981 file(s) [attempted 7981/8459 = 94%, 211 KB/s], Decompressed: 7972 Downloaded: 8023 file(s) [attempted 8023/8459 = 94%, 244 KB/s], Decompressed: 8020 Downloaded: 8068 file(s) [attempted 8068/8459 = 95%, 77 KB/s], Decompressed: 8054 Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 150 KB/s], Decompressed: 8099 Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 78 KB/s], Decompressed: 8133 Downloaded: 8177 file(s) [attempted 8177/8459 = 96%, 51 KB/s], Decompressed: 8174 Downloaded: 8220 file(s) [attempted 8220/8459 = 97%, 99 KB/s], Decompressed: 8215 Downloaded: 8256 file(s) [attempted 8256/8459 = 97%, 137 KB/s], Decompressed: 8253 Downloaded: 8296 file(s) [attempted 8296/8459 = 98%, 93 KB/s], Decompressed: 8290 Downloaded: 8335 file(s) [attempted 8335/8459 = 98%, 82 KB/s], Decompressed: 8328 Downloaded: 8373 file(s) [attempted 8373/8459 = 98%, 771 KB/s], Decompressed: 8369 Downloaded: 8412 file(s) [attempted 8412/8459 = 99%, 974 KB/s], Decompressed: 8407 Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 87 KB/s], Decompressed: 8444 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 87 KB/s], Decompressed: 8455
lean_checkerexit 0
lake build
ℹ [3410/3416] Built Iut.Stage1.IUTStage1FrobenioidShift (240s) 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) [0x71dad6dc6785] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x85bdb27) [0x71dad6dbdb27] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_panic_fn_borrowed+0x2b) [0x71dad6dbdc0b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 [private]+0xe2) [0x71dad6cf3c62] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.LibrarySuggestions.SineQuaNon.initFn._lam_2 [boxed]+0x9) [0x71dad6cf4439] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/2>+0x119) [0x71dad6dcaf99] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Array.mapMUnsafe.map [private] spec at Lean.computeExtEntries+0x193) [0x71dad6c32923] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.computeExtEntries [private]+0x2b) [0x71dad6c32b2b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.mkModuleData+0x87) [0x71dad6c33827] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.writeModule+0xf6) [0x71dad6c341b6] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xa1b) [0x71dad6dc9e8b] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [λ, arity↓]+0xb) [0x71dad6a15adb] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x71dad6dc9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(<apply/1>+0xb53) [0x71dad6dc9fc3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_profileit+0x83) [0x71dad6d9b1f3] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.profileitIOUnsafe [arity↓]+0x82) [0x71dad6a15c92] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(Lean.Elab.runFrontend+0xaa8) [0x71dad1e22638] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_shell_main+0x3a2e) [0x71dad1c0cd2e] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(+0x2f69a82) [0x71dad1769a82] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/../lib/lean/libleanshared.so(lean_main+0x21e) [0x71dad1769f0e] /lib/x86_64-linux-gnu/libc.so.6(+0x2724a) [0x71dace64524a] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x85) [0x71dace645305] /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean(_start+0x2a) [0x5de27bfb08da] ✔ [3411/3416] Built Iut.Stage1.IUTStage1EndpointAudit (7.9s) ✔ [3412/3416] Built Iut.Stage1.IUTStage1Source (3.3s) ✔ [3413/3416] Built Iut.Stage1.IUTStage1Experiments (35s) ✔ [3414/3416] Built Iut.Basic (2.5s) ✔ [3415/3416] Built Iut (2.5s) Build completed successfully (3416 jobs).
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
blueprint_buildexit 1
lake build :blueprint
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes error: unknown package facet `blueprint`
semantic_extractexit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)
apx-semantic-phase {"duration_ms":5,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":9,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":328368,"module_count":1,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":56,"module_count":1,"module_name":"Iut","module_path":"Iut.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"ok":true,"payload_bytes":738,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"ok":true,"payload_bytes":738,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":1,"diagnostic_count":0,"duration_ms":81,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":332937,"module_count":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":1,"diagnostic_count":0,"duration_ms":56,"module_count":1,"module_name":"Iut.Basic","module_path":"Iut/Basic.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"ok":true,"payload_bytes":1330,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"ok":true,"payload_bytes":1330,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":97,"diagnostic_count":15,"duration_ms":7530,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":330199,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":97,"diagnostic_count":15,"duration_ms":393,"module_count":1,"module_name":"Iut.Stage1.IUTStage1EndpointAudit","module_path":"Iut/Stage1/IUTStage1EndpointAudit.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"ok":true,"payload_bytes":3002937,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":2,"module_index":2,"ok":true,"payload_bytes":3002937,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":1888,"diagnostic_count":116,"duration_ms":1534050,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":346976,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":1888,"diagnostic_count":116,"duration_ms":7425,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Experiments","module_path":"Iut/Stage1/IUTStage1Experiments.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"ok":true,"payload_bytes":66851125,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":48,"module_index":3,"ok":true,"payload_bytes":66851125,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":7706,"diagnostic_count":3080,"duration_ms":6091253,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":502588,"module_count":1,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":7706,"diagnostic_count":3080,"duration_ms":39094,"module_count":1,"module_name":"Iut.Stage1.IUTStage1FrobenioidShift","module_path":"Iut/Stage1/IUTStage1FrobenioidShift.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":4,"ok":true,"payload_bytes":460841742,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":495,"module_index":4,"ok":true,"payload_bytes":460841742,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":152,"diagnostic_count":23,"duration_ms":25038,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":916383,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":152,"diagnostic_count":23,"duration_ms":1094,"module_count":1,"module_name":"Iut.Stage1.IUTStage1Source","module_path":"Iut/Stage1/IUTStage1Source.lean","ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"module_index":5,"ok":true,"payload_bytes":2722873,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":4,"module_index":5,"ok":true,"payload_bytes":2722873,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":9844,"diagnostic_count":3234,"duration_ms":57650,"module_count":6,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":534535836,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1283,"ok":true,"payload_bytes":534535836,"phase":"lean_json_write"}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"core_compile","duration_ms":3386}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":353,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3448,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 5e463795818150aa4211cd980cc51c16a0f42edef395609205431c2db2b498db
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":10546498,"ok":true}