Verification run
Run 1279
failedcommit
4f5eb57060aatoolchain lean-v4-30-0prover leantook 2h 5m · finished 3w agolake build 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 lake build)
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
Attempting anonymous GitHub clone before installation-auth fallback
$ git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1728-source
exit_code=Some(128) duration_ms=240
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1728-source'...
error: unable to read askpass response from '/usr/bin/false'
fatal: could not read Username for 'https://github.com': terminal prompts disabled
$ git clone (github installation auth fallback)
exit_code=Some(0) duration_ms=3949
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1728-source'...
$ git checkout 4f5eb57060aa8606f34998b5d6fe6dd90ec720a0
exit_code=Some(0) duration_ms=256
stderr:
Note: switching to '4f5eb57060aa8606f34998b5d6fe6dd90ec720a0'.
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 4f5eb57 Merge pull request #967 from promachina/e23-3e-selected-paper-family-hull-procession
Resolved source revision: 4f5eb57060aa8606f34998b5d6fe6dd90ec720a0
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=4f5eb57060aa8606f34998b5d6fe6dd90ec720a0 provenance={"branch":"master","checked_out_revision":"4f5eb57060aa8606f34998b5d6fe6dd90ec720a0","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"github_installation","local_clone":false,"requested_commit_sha":"4f5eb57060aa8606f34998b5d6fe6dd90ec720a0","used_missing_commit_fetch":false}
Resolved toolchain: lean-v4-30-0 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base@sha256:0c31befa50c7261b818ef62dfad7f4ee9a1b0a0cf85cc8da68a532f5930ffe8d)
Skipped Lean workspace build cache for dependency-overlay execution
Lean dependency cache mode=oci_build_overlay source_clones=9 clone_duration_ms=6828 overlay_mounts=0 lower_files=0 lower_directories=0 lower_logical_bytes=0 snapshot_copy_bytes=0
Lean dependency overlay upper files=0 directories=0 logical_bytes=0 whiteouts=0 opaque_directories=0
Lean semantic module cache: pre-semantic phase failed; not running semantic extraction
$ lake exe cache get
exit_code=Some(0) duration_ms=223064
stdout:
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)
stderr:
✔ [8/25] Built Cache.Lean (551ms)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (47s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (388ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (176ms)
✔ [13/25] Built Cache.Lean:c.o (164ms)
✔ [15/25] Built Cache.Init (8.6s)
✔ [16/25] Built Cache.IO (8.6s)
✔ [17/25] Built Cache.Init:c.o (113ms)
✔ [18/25] Built Cache.IO:c.o (1.2s)
✔ [19/25] Built Cache.Hashing (995ms)
✔ [20/25] Built Cache.Hashing:c.o (364ms)
✔ [21/25] Built Cache.Requests (2.1s)
✔ [22/25] Built Cache.Requests:c.o (1.8s)
✔ [23/25] Built Cache.Main (906ms)
✔ [24/25] Built Cache.Main:c.o (549ms)
✔ [25/25] Built cache:exe (5.3s)
Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 12 file(s) [attempted 12/8459 = 0%, 9 KB/s], Decompressed: 9
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 27 KB/s], Decompressed: 19
Downloaded: 64 file(s) [attempted 64/8459 = 0%, 57 KB/s], Decompressed: 44
Downloaded: 96 file(s) [attempted 96/8459 = 1%, 244 KB/s], Decompressed: 64
Downloaded: 127 file(s) [attempted 127/8459 = 1%, 499 KB/s], Decompressed: 64
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 384 KB/s], Decompressed: 96
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 154 KB/s], Decompressed: 138
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 989 KB/s], Decompressed: 182
Downloaded: 275 file(s) [attempted 275/8459 = 3%, 486 KB/s], Decompressed: 182
Downloaded: 313 file(s) [attempted 313/8459 = 3%, 178 KB/s], Decompressed: 230
Downloaded: 354 file(s) [attempted 354/8459 = 4%, 84 KB/s], Decompressed: 278
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 80 KB/s], Decompressed: 337
Downloaded: 436 file(s) [attempted 436/8459 = 5%, 91 KB/s], Decompressed: 337
Downloaded: 477 file(s) [attempted 477/8459 = 5%, 99 KB/s], Decompressed: 391
Downloaded: 515 file(s) [attempted 515/8459 = 6%, 918 KB/s], Decompressed: 439
Downloaded: 559 file(s) [attempted 559/8459 = 6%, 246 KB/s], Decompressed: 439
Downloaded: 597 file(s) [attempted 597/8459 = 7%, 405 KB/s], Decompressed: 501
Downloaded: 638 file(s) [attempted 638/8459 = 7%, 915 KB/s], Decompressed: 563
Downloaded: 683 file(s) [attempted 683/8459 = 8%, 346 KB/s], Decompressed: 563
Downloaded: 727 file(s) [attempted 727/8459 = 8%, 102 KB/s], Decompressed: 635
Downloaded: 772 file(s) [attempted 772/8459 = 9%, 197 KB/s], Decompressed: 635
Downloaded: 813 file(s) [attempted 813/8459 = 9%, 278 KB/s], Decompressed: 711
Downloaded: 854 file(s) [attempted 854/8459 = 10%, 542 KB/s], Decompressed: 711
Downloaded: 895 file(s) [attempted 895/8459 = 10%, 73 KB/s], Decompressed: 782
Downloaded: 940 file(s) [attempted 940/8459 = 11%, 72 KB/s], Decompressed: 782
Downloaded: 978 file(s) [attempted 978/8459 = 11%, 627 KB/s], Decompressed: 782
Downloaded: 1019 file(s) [attempted 1019/8459 = 12%, 853 KB/s], Decompressed: 782
Downloaded: 1063 file(s) [attempted 1063/8459 = 12%, 190 KB/s], Decompressed: 782
Downloaded: 1108 file(s) [attempted 1108/8459 = 13%, 63 KB/s], Decompressed: 875
Downloaded: 1146 file(s) [attempted 1146/8459 = 13%, 1722 KB/s], Decompressed: 875
Downloaded: 1187 file(s) [attempted 1187/8459 = 14%, 192 KB/s], Decompressed: 875
Downloaded: 1224 file(s) [attempted 1224/8459 = 14%, 200 KB/s], Decompressed: 875
Downloaded: 1265 file(s) [attempted 1265/8459 = 14%, 637 KB/s], Decompressed: 875
Downloaded: 1310 file(s) [attempted 1310/8459 = 15%, 851 KB/s], Decompressed: 1094
Downloaded: 1351 file(s) [attempted 1351/8459 = 15%, 53 KB/s], Decompressed: 1094
Downloaded: 1392 file(s) [attempted 1392/8459 = 16%, 394 KB/s], Decompressed: 1094
Downloaded: 1433 file(s) [attempted 1433/8459 = 16%, 62 KB/s], Decompressed: 1094
Downloaded: 1474 file(s) [attempted 1474/8459 = 17%, 252 KB/s], Decompressed: 1283
Downloaded: 1519 file(s) [attempted 1519/8459 = 17%, 77 KB/s], Decompressed: 1283
Downloaded: 1563 file(s) [attempted 1563/8459 = 18%, 319 KB/s], Decompressed: 1283
Downloaded: 1608 file(s) [attempted 1608/8459 = 19%, 200 KB/s], Decompressed: 1283
Downloaded: 1646 file(s) [attempted 1646/8459 = 19%, 348 KB/s], Decompressed: 1471
Downloaded: 1687 file(s) [attempted 1687/8459 = 19%, 137 KB/s], Decompressed: 1471
Downloaded: 1728 file(s) [attempted 1728/8459 = 20%, 118 KB/s], Decompressed: 1471
Downloaded: 1772 file(s) [attempted 1772/8459 = 20%, 179 KB/s], Decompressed: 1471
Downloaded: 1813 file(s) [attempted 1813/8459 = 21%, 94 KB/s], Decompressed: 1642
Downloaded: 1858 file(s) [attempted 1858/8459 = 21%, 393 KB/s], Decompressed: 1642
Downloaded: 1892 file(s) [attempted 1892/8459 = 22%, 589 KB/s], Decompressed: 1642
Downloaded: 1930 file(s) [attempted 1930/8459 = 22%, 80 KB/s], Decompressed: 1642
Downloaded: 1971 file(s) [attempted 1971/8459 = 23%, 119 KB/s], Decompressed: 1803
Downloaded: 2016 file(s) [attempted 2016/8459 = 23%, 126 KB/s], Decompressed: 1803
Downloaded: 2060 file(s) [attempted 2060/8459 = 24%, 355 KB/s], Decompressed: 1803
Downloaded: 2101 file(s) [attempted 2101/8459 = 24%, 1448 KB/s], Decompressed: 1954
Downloaded: 2142 file(s) [attempted 2142/8459 = 25%, 968 KB/s], Decompressed: 1954
Downloaded: 2183 file(s) [attempted 2183/8459 = 25%, 529 KB/s], Decompressed: 1954
Downloaded: 2224 file(s) [attempted 2224/8459 = 26%, 337 KB/s], Decompressed: 1954
Downloaded: 2266 file(s) [attempted 2266/8459 = 26%, 494 KB/s], Decompressed: 2091
Downloaded: 2310 file(s) [attempted 2310/8459 = 27%, 201 KB/s], Decompressed: 2091
Downloaded: 2351 file(s) [attempted 2351/8459 = 27%, 924 KB/s], Decompressed: 2091
Downloaded: 2392 file(s) [attempted 2392/8459 = 28%, 42 KB/s], Decompressed: 2242
Downloaded: 2437 file(s) [attempted 2437/8459 = 28%, 155 KB/s], Decompressed: 2242
Downloaded: 2474 file(s) [attempted 2474/8459 = 29%, 1071 KB/s], Decompressed: 2242
Downloaded: 2519 file(s) [attempted 2519/8459 = 29%, 961 KB/s], Decompressed: 2242
Downloaded: 2560 file(s) [attempted 2560/8459 = 30%, 54 KB/s], Decompressed: 2389
Downloaded: 2601 file(s) [attempted 2601/8459 = 30%, 24 KB/s], Decompressed: 2389
Downloaded: 2646 file(s) [attempted 2646/8459 = 31%, 24 KB/s], Decompressed: 2389
Downloaded: 2690 file(s) [attempted 2690/8459 = 31%, 57 KB/s], Decompressed: 2526
Downloaded: 2731 file(s) [attempted 2731/8459 = 32%, 78 KB/s], Decompressed: 2526
Downloaded: 2774 file(s) [attempted 2774/8459 = 32%, 34 KB/s], Decompressed: 2526
Downloaded: 2817 file(s) [attempted 2817/8459 = 33%, 84 KB/s], Decompressed: 2666
Downloaded: 2858 file(s) [attempted 2858/8459 = 33%, 326 KB/s], Decompressed: 2666
Downloaded: 2896 file(s) [attempted 2896/8459 = 34%, 166 KB/s], Decompressed: 2666
Downloaded: 2935 file(s) [attempted 2935/8459 = 34%, 682 KB/s], Decompressed: 2666
Downloaded: 2978 file(s) [attempted 2978/8459 = 35%, 591 KB/s], Decompressed: 2666
Downloaded: 3023 file(s) [attempted 3023/8459 = 35%, 27 KB/s], Decompressed: 2796
Downloaded: 3064 file(s) [attempted 3064/8459 = 36%, 154 KB/s], Decompressed: 2796
Downloaded: 3105 file(s) [attempted 3105/8459 = 36%, 165 KB/s], Decompressed: 2796
Downloaded: 3139 file(s) [attempted 3139/8459 = 37%, 339 KB/s], Decompressed: 2796
Downloaded: 3181 file(s) [attempted 3181/8459 = 37%, 206 KB/s], Decompressed: 2796
Downloaded: 3225 file(s) [attempted 3225/8459 = 38%, 560 KB/s], Decompressed: 2796
Downloaded: 3266 file(s) [attempted 3266/8459 = 38%, 90 KB/s], Decompressed: 2796
Downloaded: 3310 file(s) [attempted 3310/8459 = 39%, 1232 KB/s], Decompressed: 2796
Downloaded: 3351 file(s) [attempted 3351/8459 = 39%, 54 KB/s], Decompressed: 3005
Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 47 KB/s], Decompressed: 3005
Downloaded: 3430 file(s) [attempted 3430/8459 = 40%, 82 KB/s], Decompressed: 3005
Downloaded: 3471 file(s) [attempted 3471/8459 = 41%, 96 KB/s], Decompressed: 3005
Downloaded: 3516 file(s) [attempted 3516/8459 = 41%, 131 KB/s], Decompressed: 3005
Downloaded: 3560 file(s) [attempted 3560/8459 = 42%, 237 KB/s], Decompressed: 3005
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 38 KB/s], Decompressed: 3314
Downloaded: 3642 file(s) [attempted 3642/8459 = 43%, 518 KB/s], Decompressed: 3314
Downloaded: 3684 file(s) [attempted 3684/8459 = 43%, 749 KB/s], Decompressed: 3314
Downloaded: 3728 file(s) [attempted 3728/8459 = 44%, 140 KB/s], Decompressed: 3314
Downloaded: 3773 file(s) [attempted 3773/8459 = 44%, 509 KB/s], Decompressed: 3314
Downloaded: 3815 file(s) [attempted 3815/8459 = 45%, 104 KB/s], Decompressed: 3314
Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 224 KB/s], Decompressed: 3581
Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 351 KB/s], Decompressed: 3581
Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 41 KB/s], Decompressed: 3581
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 311 KB/s], Decompressed: 3581
Downloaded: 4016 file(s) [attempted 4016/8459 = 47%, 460 KB/s], Decompressed: 3581
Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 958 KB/s], Decompressed: 3581
Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 154 KB/s], Decompressed: 3833
Downloaded: 4143 file(s) [attempted 4143/8459 = 48%, 527 KB/s], Decompressed: 3833
Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 307 KB/s], Decompressed: 3833
Downloaded: 4232 file(s) [attempted 4232/8459 = 50%, 550 KB/s], Decompressed: 3833
Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 76 KB/s], Decompressed: 3833
Downloaded: 4321 file(s) [attempted 4321/8459 = 51%, 188 KB/s], Decompressed: 3833
Downloaded: 4362 file(s) [attempted 4362/8459 = 51%, 228 KB/s], Decompressed: 4081
Downloaded: 4399 file(s) [attempted 4399/8459 = 52%, 208 KB/s], Decompressed: 4081
Downloaded: 4441 file(s) [attempted 4441/8459 = 52%, 277 KB/s], Decompressed: 4081
Downloaded: 4485 file(s) [attempted 4485/8459 = 53%, 432 KB/s], Decompressed: 4081
Downloaded: 4527 file(s) [attempted 4527/8459 = 53%, 242 KB/s], Decompressed: 4081
Downloaded: 4571 file(s) [attempted 4571/8459 = 54%, 253 KB/s], Decompressed: 4081
Downloaded: 4612 file(s) [attempted 4612/8459 = 54%, 317 KB/s], Decompressed: 4328
Downloaded: 4653 file(s) [attempted 4653/8459 = 55%, 216 KB/s], Decompressed: 4328
Downloaded: 4694 file(s) [attempted 4694/8459 = 55%, 75 KB/s], Decompressed: 4328
Downloaded: 4742 file(s) [attempted 4742/8459 = 56%, 287 KB/s], Decompressed: 4328
Downloaded: 4780 file(s) [attempted 4780/8459 = 56%, 545 KB/s], Decompressed: 4328
Downloaded: 4824 file(s) [attempted 4824/8459 = 57%, 42 KB/s], Decompressed: 4574
Downloaded: 4869 file(s) [attempted 4869/8459 = 57%, 193 KB/s], Decompressed: 4574
Downloaded: 4906 file(s) [attempted 4906/8459 = 57%, 69 KB/s], Decompressed: 4574
Downloaded: 4947 file(s) [attempted 4947/8459 = 58%, 54 KB/s], Decompressed: 4574
Downloaded: 4995 file(s) [attempted 4995/8459 = 59%, 495 KB/s], Decompressed: 4574
Downloaded: 5040 file(s) [attempted 5040/8459 = 59%, 99 KB/s], Decompressed: 4574
Downloaded: 5078 file(s) [attempted 5078/8459 = 60%, 156 KB/s], Decompressed: 4574
Downloaded: 5119 file(s) [attempted 5119/8459 = 60%, 339 KB/s], Decompressed: 4574
Downloaded: 5160 file(s) [attempted 5160/8459 = 61%, 62 KB/s], Decompressed: 4574
Downloaded: 5204 file(s) [attempted 5204/8459 = 61%, 122 KB/s], Decompressed: 4574
Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 72 KB/s], Decompressed: 4821
Downloaded: 5290 file(s) [attempted 5290/8459 = 62%, 626 KB/s], Decompressed: 4821
Downloaded: 5331 file(s) [attempted 5331/8459 = 63%, 702 KB/s], Decompressed: 4821
Downloaded: 5372 file(s) [attempted 5372/8459 = 63%, 394 KB/s], Decompressed: 4821
Downloaded: 5413 file(s) [attempted 5413/8459 = 63%, 166 KB/s], Decompressed: 4821
Downloaded: 5454 file(s) [attempted 5454/8459 = 64%, 985 KB/s], Decompressed: 4821
Downloaded: 5496 file(s) [attempted 5496/8459 = 64%, 643 KB/s], Decompressed: 4821
Downloaded: 5540 file(s) [attempted 5540/8459 = 65%, 231 KB/s], Decompressed: 4821
Downloaded: 5581 file(s) [attempted 5581/8459 = 65%, 1150 KB/s], Decompressed: 4821
Downloaded: 5622 file(s) [attempted 5622/8459 = 66%, 124 KB/s], Decompressed: 4821
Downloaded: 5663 file(s) [attempted 5663/8459 = 66%, 1364 KB/s], Decompressed: 5232
Downloaded: 5704 file(s) [attempted 5704/8459 = 67%, 456 KB/s], Decompressed: 5232
Downloaded: 5749 file(s) [attempted 5749/8459 = 67%, 101 KB/s], Decompressed: 5232
Downloaded: 5794 file(s) [attempted 5794/8459 = 68%, 409 KB/s], Decompressed: 5232
Downloaded: 5835 file(s) [attempted 5835/8459 = 68%, 709 KB/s], Decompressed: 5232
Downloaded: 5872 file(s) [attempted 5872/8459 = 69%, 160 KB/s], Decompressed: 5232
Downloaded: 5920 file(s) [attempted 5920/8459 = 69%, 627 KB/s], Decompressed: 5232
Downloaded: 5951 file(s) [attempted 5951/8459 = 70%, 376 KB/s], Decompressed: 5232
Downloaded: 5968 file(s) [attempted 5968/8459 = 70%, 44 KB/s], Decompressed: 5232
Downloaded: 6020 file(s) [attempted 6020/8459 = 71%, 25 KB/s], Decompressed: 5232
Downloaded: 6068 file(s) [attempted 6068/8459 = 71%, 102 KB/s], Decompressed: 5232
Downloaded: 6119 file(s) [attempted 6119/8459 = 72%, 100 KB/s], Decompressed: 5232
Downloaded: 6170 file(s) [attempted 6170/8459 = 72%, 215 KB/s], Decompressed: 5639
Downloaded: 6237 file(s) [attempted 6237/8459 = 73%, 853 KB/s], Decompressed: 5639
Downloaded: 6270 file(s) [attempted 6270/8459 = 74%, 130 KB/s], Decompressed: 5639
Downloaded: 6318 file(s) [attempted 6318/8459 = 74%, 181 KB/s], Decompressed: 5639
Downloaded: 6369 file(s) [attempted 6369/8459 = 75%, 534 KB/s], Decompressed: 5639
Downloaded: 6417 file(s) [attempted 6417/8459 = 75%, 287 KB/s], Decompressed: 5639
Downloaded: 6468 file(s) [attempted 6468/8459 = 76%, 141 KB/s], Decompressed: 5639
Downloaded: 6516 file(s) [attempted 6516/8459 = 77%, 501 KB/s], Decompressed: 5639
Downloaded: 6568 file(s) [attempted 6568/8459 = 77%, 91 KB/s], Decompressed: 5639
Downloaded: 6616 file(s) [attempted 6616/8459 = 78%, 2651 KB/s], Decompressed: 5639
Downloaded: 6664 file(s) [attempted 6664/8459 = 78%, 247 KB/s], Decompressed: 5639
Downloaded: 6712 file(s) [attempted 6712/8459 = 79%, 29 KB/s], Decompressed: 5639
Downloaded: 6756 file(s) [attempted 6756/8459 = 79%, 484 KB/s], Decompressed: 6170
Downloaded: 6797 file(s) [attempted 6797/8459 = 80%, 207 KB/s], Decompressed: 6170
Downloaded: 6835 file(s) [attempted 6835/8459 = 80%, 294 KB/s], Decompressed: 6170
Downloaded: 6873 file(s) [attempted 6873/8459 = 81%, 652 KB/s], Decompressed: 6170
Downloaded: 6917 file(s) [attempted 6917/8459 = 81%, 35 KB/s], Decompressed: 6170
Downloaded: 6958 file(s) [attempted 6958/8459 = 82%, 141 KB/s], Decompressed: 6170
Downloaded: 7006 file(s) [attempted 7006/8459 = 82%, 280 KB/s], Decompressed: 6170
Downloaded: 7054 file(s) [attempted 7054/8459 = 83%, 244 KB/s], Decompressed: 6170
Downloaded: 7102 file(s) [attempted 7102/8459 = 83%, 70 KB/s], Decompressed: 6170
Downloaded: 7140 file(s) [attempted 7140/8459 = 84%, 105 KB/s], Decompressed: 6170
Downloaded: 7179 file(s) [attempted 7179/8459 = 84%, 974 KB/s], Decompressed: 6170
Downloaded: 7219 file(s) [attempted 7219/8459 = 85%, 612 KB/s], Decompressed: 6722
Downloaded: 7258 file(s) [attempted 7258/8459 = 85%, 186 KB/s], Decompressed: 6722
Downloaded: 7304 file(s) [attempted 7304/8459 = 86%, 89 KB/s], Decompressed: 6722
Downloaded: 7352 file(s) [attempted 7352/8459 = 86%, 72 KB/s], Decompressed: 6722
Downloaded: 7403 file(s) [attempted 7403/8459 = 87%, 2482 KB/s], Decompressed: 6722
Downloaded: 7451 file(s) [attempted 7451/8459 = 88%, 109 KB/s], Decompressed: 6722
Downloaded: 7499 file(s) [attempted 7499/8459 = 88%, 168 KB/s], Decompressed: 6722
Downloaded: 7540 file(s) [attempted 7540/8459 = 89%, 170 KB/s], Decompressed: 6722
Downloaded: 7582 file(s) [attempted 7582/8459 = 89%, 30 KB/s], Decompressed: 7201
Downloaded: 7619 file(s) [attempted 7619/8459 = 90%, 518 KB/s], Decompressed: 7201
Downloaded: 7664 file(s) [attempted 7664/8459 = 90%, 208 KB/s], Decompressed: 7201
Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 95 KB/s], Decompressed: 7201
Downloaded: 7746 file(s) [attempted 7746/8459 = 91%, 189 KB/s], Decompressed: 7201
Downloaded: 7790 file(s) [attempted 7790/8459 = 92%, 24 KB/s], Decompressed: 7201
Downloaded: 7835 file(s) [attempted 7835/8459 = 92%, 783 KB/s], Decompressed: 7201
Downloaded: 7876 file(s) [attempted 7876/8459 = 93%, 208 KB/s], Decompressed: 7201
Downloaded: 7914 file(s) [attempted 7914/8459 = 93%, 856 KB/s], Decompressed: 7582
Downloaded: 7955 file(s) [attempted 7955/8459 = 94%, 546 KB/s], Decompressed: 7582
Downloaded: 7999 file(s) [attempted 7999/8459 = 94%, 107 KB/s], Decompressed: 7582
Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 189 KB/s], Decompressed: 7582
Downloaded: 8082 file(s) [attempted 8082/8459 = 95%, 61 KB/s], Decompressed: 7582
Downloaded: 8126 file(s) [attempted 8126/8459 = 96%, 172 KB/s], Decompressed: 7582
Downloaded: 8164 file(s) [attempted 8164/8459 = 96%, 382 KB/s], Decompressed: 7886
Downloaded: 8208 file(s) [attempted 8208/8459 = 97%, 82 KB/s], Decompressed: 7886
Downloaded: 8246 file(s) [attempted 8246/8459 = 97%, 191 KB/s], Decompressed: 7886
Downloaded: 8287 file(s) [attempted 8287/8459 = 97%, 131 KB/s], Decompressed: 7886
Downloaded: 8332 file(s) [attempted 8332/8459 = 98%, 46 KB/s], Decompressed: 7886
Downloaded: 8376 file(s) [attempted 8376/8459 = 99%, 355 KB/s], Decompressed: 7886
Downloaded: 8417 file(s) [attempted 8417/8459 = 99%, 116 KB/s], Decompressed: 8136
Downloaded: 8445 file(s) [attempted 8445/8459 = 99%, 218 KB/s], Decompressed: 8136
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 111 KB/s], Decompressed: 8136
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 111 KB/s], Decompressed: 8136
apx-runtime-resource-v1 apx-verifier-job-1728-runtime-lake_cache-3977608-1787619513269338976-0 3952640 4100096 21474836480 0 0 0 0 0 0 3003162624 3612663808 21474836480 0 0 0 0 0 0
$ lake build
exit_code=None duration_ms=7200862
stdout:
✔ [500/502] Built Iut.Foundations.Species (181s)
✔ [501/506] Built Iut.Foundations.SourceGameplanSpeciesMutation (66s)
✔ [784/791] Built Iut.Foundations.RealLineCopy (74s)
✔ [785/791] Built Iut.Foundations.TransportDiagram (90s)
✔ [786/791] Built Iut.Foundations.IndeterminacyRelation (67s)
✔ [787/791] Built Iut.Foundations.RegionMeasure (66s)
✔ [788/791] Built Iut.Foundations.CommonTargetBound (92s)
✔ [789/791] Built Iut.Foundations.TransportedRegionFamily (108s)
✔ [790/794] Built Iut.Foundations.QualitativeData (97s)
✔ [3508/3513] Built Iut.Foundations.EtaleThetaQuotient (291s)
✔ [3509/3513] Built Iut.Foundations.Orbicurve (1239s)
✔ [3956/3959] Built Iut.Foundations.InitialThetaData (1148s)
✔ [3964/3966] Built Iut.Foundations.OrbicurvePullback (2182s)
✔ [3965/3969] Built Iut.Foundations.EtaleThetaCovers (619s)
✔ [3974/3982] Built Iut.Foundations.SourceTateCurve (408s)
✔ [3981/3984] Built Iut.Foundations.GaloisImage (289s)
stderr:
/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1728-runtime-lean_checker-3977608-1787619736338037565-1 on attempt 2
$ lake build :blueprint
exit_code=Some(1) duration_ms=21564
stderr:
error: unknown package facet `blueprint`
apx-runtime-resource-v1 apx-verifier-job-1728-runtime-blueprint_build-3977608-1787626981219035763-2 1150976 1564672 21474836480 0 0 0 0 0 0 886128640 989937664 21474836480 0 0 0 0 0 0
blueprint_build failed; continuing (non-fatal phase).
Command runs
git_cloneexit 128
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1728-source
Cloning into '/var/lib/apodeixis/repos/job-1728-source'... error: unable to read askpass response from '/usr/bin/false' fatal: could not read Username for 'https://github.com': terminal prompts disabled
git_cloneexit 0
git clone (github installation auth fallback)
Cloning into '/var/lib/apodeixis/repos/job-1728-source'...
git_checkoutexit 0
git checkout 4f5eb57060aa8606f34998b5d6fe6dd90ec720a0
Note: switching to '4f5eb57060aa8606f34998b5d6fe6dd90ec720a0'. 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 4f5eb57 Merge pull request #967 from promachina/e23-3e-selected-paper-family-hull-procession
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)
✔ [8/25] Built Cache.Lean (551ms) ✔ [10/25] Built Batteries.Data.Array.Match:c.o (47s) ✔ [11/25] Built Batteries.Data.String.Basic:c.o (388ms) ✔ [12/25] Built Batteries.Data.String.Matcher:c.o (176ms) ✔ [13/25] Built Cache.Lean:c.o (164ms) ✔ [15/25] Built Cache.Init (8.6s) ✔ [16/25] Built Cache.IO (8.6s) ✔ [17/25] Built Cache.Init:c.o (113ms) ✔ [18/25] Built Cache.IO:c.o (1.2s) ✔ [19/25] Built Cache.Hashing (995ms) ✔ [20/25] Built Cache.Hashing:c.o (364ms) ✔ [21/25] Built Cache.Requests (2.1s) ✔ [22/25] Built Cache.Requests:c.o (1.8s) ✔ [23/25] Built Cache.Main (906ms) ✔ [24/25] Built Cache.Main:c.o (549ms) ✔ [25/25] Built cache:exe (5.3s) Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0 Downloaded: 12 file(s) [attempted 12/8459 = 0%, 9 KB/s], Decompressed: 9 Downloaded: 37 file(s) [attempted 37/8459 = 0%, 27 KB/s], Decompressed: 19 Downloaded: 64 file(s) [attempted 64/8459 = 0%, 57 KB/s], Decompressed: 44 Downloaded: 96 file(s) [attempted 96/8459 = 1%, 244 KB/s], Decompressed: 64 Downloaded: 127 file(s) [attempted 127/8459 = 1%, 499 KB/s], Decompressed: 64 Downloaded: 162 file(s) [attempted 162/8459 = 1%, 384 KB/s], Decompressed: 96 Downloaded: 196 file(s) [attempted 196/8459 = 2%, 154 KB/s], Decompressed: 138 Downloaded: 234 file(s) [attempted 234/8459 = 2%, 989 KB/s], Decompressed: 182 Downloaded: 275 file(s) [attempted 275/8459 = 3%, 486 KB/s], Decompressed: 182 Downloaded: 313 file(s) [attempted 313/8459 = 3%, 178 KB/s], Decompressed: 230 Downloaded: 354 file(s) [attempted 354/8459 = 4%, 84 KB/s], Decompressed: 278 Downloaded: 391 file(s) [attempted 391/8459 = 4%, 80 KB/s], Decompressed: 337 Downloaded: 436 file(s) [attempted 436/8459 = 5%, 91 KB/s], Decompressed: 337 Downloaded: 477 file(s) [attempted 477/8459 = 5%, 99 KB/s], Decompressed: 391 Downloaded: 515 file(s) [attempted 515/8459 = 6%, 918 KB/s], Decompressed: 439 Downloaded: 559 file(s) [attempted 559/8459 = 6%, 246 KB/s], Decompressed: 439 Downloaded: 597 file(s) [attempted 597/8459 = 7%, 405 KB/s], Decompressed: 501 Downloaded: 638 file(s) [attempted 638/8459 = 7%, 915 KB/s], Decompressed: 563 Downloaded: 683 file(s) [attempted 683/8459 = 8%, 346 KB/s], Decompressed: 563 Downloaded: 727 file(s) [attempted 727/8459 = 8%, 102 KB/s], Decompressed: 635 Downloaded: 772 file(s) [attempted 772/8459 = 9%, 197 KB/s], Decompressed: 635 Downloaded: 813 file(s) [attempted 813/8459 = 9%, 278 KB/s], Decompressed: 711 Downloaded: 854 file(s) [attempted 854/8459 = 10%, 542 KB/s], Decompressed: 711 Downloaded: 895 file(s) [attempted 895/8459 = 10%, 73 KB/s], Decompressed: 782 Downloaded: 940 file(s) [attempted 940/8459 = 11%, 72 KB/s], Decompressed: 782 Downloaded: 978 file(s) [attempted 978/8459 = 11%, 627 KB/s], Decompressed: 782 Downloaded: 1019 file(s) [attempted 1019/8459 = 12%, 853 KB/s], Decompressed: 782 Downloaded: 1063 file(s) [attempted 1063/8459 = 12%, 190 KB/s], Decompressed: 782 Downloaded: 1108 file(s) [attempted 1108/8459 = 13%, 63 KB/s], Decompressed: 875 Downloaded: 1146 file(s) [attempted 1146/8459 = 13%, 1722 KB/s], Decompressed: 875 Downloaded: 1187 file(s) [attempted 1187/8459 = 14%, 192 KB/s], Decompressed: 875 Downloaded: 1224 file(s) [attempted 1224/8459 = 14%, 200 KB/s], Decompressed: 875 Downloaded: 1265 file(s) [attempted 1265/8459 = 14%, 637 KB/s], Decompressed: 875 Downloaded: 1310 file(s) [attempted 1310/8459 = 15%, 851 KB/s], Decompressed: 1094 Downloaded: 1351 file(s) [attempted 1351/8459 = 15%, 53 KB/s], Decompressed: 1094 Downloaded: 1392 file(s) [attempted 1392/8459 = 16%, 394 KB/s], Decompressed: 1094 Downloaded: 1433 file(s) [attempted 1433/8459 = 16%, 62 KB/s], Decompressed: 1094 Downloaded: 1474 file(s) [attempted 1474/8459 = 17%, 252 KB/s], Decompressed: 1283 Downloaded: 1519 file(s) [attempted 1519/8459 = 17%, 77 KB/s], Decompressed: 1283 Downloaded: 1563 file(s) [attempted 1563/8459 = 18%, 319 KB/s], Decompressed: 1283 Downloaded: 1608 file(s) [attempted 1608/8459 = 19%, 200 KB/s], Decompressed: 1283 Downloaded: 1646 file(s) [attempted 1646/8459 = 19%, 348 KB/s], Decompressed: 1471 Downloaded: 1687 file(s) [attempted 1687/8459 = 19%, 137 KB/s], Decompressed: 1471 Downloaded: 1728 file(s) [attempted 1728/8459 = 20%, 118 KB/s], Decompressed: 1471 Downloaded: 1772 file(s) [attempted 1772/8459 = 20%, 179 KB/s], Decompressed: 1471 Downloaded: 1813 file(s) [attempted 1813/8459 = 21%, 94 KB/s], Decompressed: 1642 Downloaded: 1858 file(s) [attempted 1858/8459 = 21%, 393 KB/s], Decompressed: 1642 Downloaded: 1892 file(s) [attempted 1892/8459 = 22%, 589 KB/s], Decompressed: 1642 Downloaded: 1930 file(s) [attempted 1930/8459 = 22%, 80 KB/s], Decompressed: 1642 Downloaded: 1971 file(s) [attempted 1971/8459 = 23%, 119 KB/s], Decompressed: 1803 Downloaded: 2016 file(s) [attempted 2016/8459 = 23%, 126 KB/s], Decompressed: 1803 Downloaded: 2060 file(s) [attempted 2060/8459 = 24%, 355 KB/s], Decompressed: 1803 Downloaded: 2101 file(s) [attempted 2101/8459 = 24%, 1448 KB/s], Decompressed: 1954 Downloaded: 2142 file(s) [attempted 2142/8459 = 25%, 968 KB/s], Decompressed: 1954 Downloaded: 2183 file(s) [attempted 2183/8459 = 25%, 529 KB/s], Decompressed: 1954 Downloaded: 2224 file(s) [attempted 2224/8459 = 26%, 337 KB/s], Decompressed: 1954 Downloaded: 2266 file(s) [attempted 2266/8459 = 26%, 494 KB/s], Decompressed: 2091 Downloaded: 2310 file(s) [attempted 2310/8459 = 27%, 201 KB/s], Decompressed: 2091 Downloaded: 2351 file(s) [attempted 2351/8459 = 27%, 924 KB/s], Decompressed: 2091 Downloaded: 2392 file(s) [attempted 2392/8459 = 28%, 42 KB/s], Decompressed: 2242 Downloaded: 2437 file(s) [attempted 2437/8459 = 28%, 155 KB/s], Decompressed: 2242 Downloaded: 2474 file(s) [attempted 2474/8459 = 29%, 1071 KB/s], Decompressed: 2242 Downloaded: 2519 file(s) [attempted 2519/8459 = 29%, 961 KB/s], Decompressed: 2242 Downloaded: 2560 file(s) [attempted 2560/8459 = 30%, 54 KB/s], Decompressed: 2389 Downloaded: 2601 file(s) [attempted 2601/8459 = 30%, 24 KB/s], Decompressed: 2389 Downloaded: 2646 file(s) [attempted 2646/8459 = 31%, 24 KB/s], Decompressed: 2389 Downloaded: 2690 file(s) [attempted 2690/8459 = 31%, 57 KB/s], Decompressed: 2526 Downloaded: 2731 file(s) [attempted 2731/8459 = 32%, 78 KB/s], Decompressed: 2526 Downloaded: 2774 file(s) [attempted 2774/8459 = 32%, 34 KB/s], Decompressed: 2526 Downloaded: 2817 file(s) [attempted 2817/8459 = 33%, 84 KB/s], Decompressed: 2666 Downloaded: 2858 file(s) [attempted 2858/8459 = 33%, 326 KB/s], Decompressed: 2666 Downloaded: 2896 file(s) [attempted 2896/8459 = 34%, 166 KB/s], Decompressed: 2666 Downloaded: 2935 file(s) [attempted 2935/8459 = 34%, 682 KB/s], Decompressed: 2666 Downloaded: 2978 file(s) [attempted 2978/8459 = 35%, 591 KB/s], Decompressed: 2666 Downloaded: 3023 file(s) [attempted 3023/8459 = 35%, 27 KB/s], Decompressed: 2796 Downloaded: 3064 file(s) [attempted 3064/8459 = 36%, 154 KB/s], Decompressed: 2796 Downloaded: 3105 file(s) [attempted 3105/8459 = 36%, 165 KB/s], Decompressed: 2796 Downloaded: 3139 file(s) [attempted 3139/8459 = 37%, 339 KB/s], Decompressed: 2796 Downloaded: 3181 file(s) [attempted 3181/8459 = 37%, 206 KB/s], Decompressed: 2796 Downloaded: 3225 file(s) [attempted 3225/8459 = 38%, 560 KB/s], Decompressed: 2796 Downloaded: 3266 file(s) [attempted 3266/8459 = 38%, 90 KB/s], Decompressed: 2796 Downloaded: 3310 file(s) [attempted 3310/8459 = 39%, 1232 KB/s], Decompressed: 2796 Downloaded: 3351 file(s) [attempted 3351/8459 = 39%, 54 KB/s], Decompressed: 3005 Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 47 KB/s], Decompressed: 3005 Downloaded: 3430 file(s) [attempted 3430/8459 = 40%, 82 KB/s], Decompressed: 3005 Downloaded: 3471 file(s) [attempted 3471/8459 = 41%, 96 KB/s], Decompressed: 3005 Downloaded: 3516 file(s) [attempted 3516/8459 = 41%, 131 KB/s], Decompressed: 3005 Downloaded: 3560 file(s) [attempted 3560/8459 = 42%, 237 KB/s], Decompressed: 3005 Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 38 KB/s], Decompressed: 3314 Downloaded: 3642 file(s) [attempted 3642/8459 = 43%, 518 KB/s], Decompressed: 3314 Downloaded: 3684 file(s) [attempted 3684/8459 = 43%, 749 KB/s], Decompressed: 3314 Downloaded: 3728 file(s) [attempted 3728/8459 = 44%, 140 KB/s], Decompressed: 3314 Downloaded: 3773 file(s) [attempted 3773/8459 = 44%, 509 KB/s], Decompressed: 3314 Downloaded: 3815 file(s) [attempted 3815/8459 = 45%, 104 KB/s], Decompressed: 3314 Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 224 KB/s], Decompressed: 3581 Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 351 KB/s], Decompressed: 3581 Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 41 KB/s], Decompressed: 3581 Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 311 KB/s], Decompressed: 3581 Downloaded: 4016 file(s) [attempted 4016/8459 = 47%, 460 KB/s], Decompressed: 3581 Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 958 KB/s], Decompressed: 3581 Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 154 KB/s], Decompressed: 3833 Downloaded: 4143 file(s) [attempted 4143/8459 = 48%, 527 KB/s], Decompressed: 3833 Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 307 KB/s], Decompressed: 3833 Downloaded: 4232 file(s) [attempted 4232/8459 = 50%, 550 KB/s], Decompressed: 3833 Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 76 KB/s], Decompressed: 3833 Downloaded: 4321 file(s) [attempted 4321/8459 = 51%, 188 KB/s], Decompressed: 3833 Downloaded: 4362 file(s) [attempted 4362/8459 = 51%, 228 KB/s], Decompressed: 4081 Downloaded: 4399 file(s) [attempted 4399/8459 = 52%, 208 KB/s], Decompressed: 4081 Downloaded: 4441 file(s) [attempted 4441/8459 = 52%, 277 KB/s], Decompressed: 4081 Downloaded: 4485 file(s) [attempted 4485/8459 = 53%, 432 KB/s], Decompressed: 4081 Downloaded: 4527 file(s) [attempted 4527/8459 = 53%, 242 KB/s], Decompressed: 4081 Downloaded: 4571 file(s) [attempted 4571/8459 = 54%, 253 KB/s], Decompressed: 4081 Downloaded: 4612 file(s) [attempted 4612/8459 = 54%, 317 KB/s], Decompressed: 4328 Downloaded: 4653 file(s) [attempted 4653/8459 = 55%, 216 KB/s], Decompressed: 4328 Downloaded: 4694 file(s) [attempted 4694/8459 = 55%, 75 KB/s], Decompressed: 4328 Downloaded: 4742 file(s) [attempted 4742/8459 = 56%, 287 KB/s], Decompressed: 4328 Downloaded: 4780 file(s) [attempted 4780/8459 = 56%, 545 KB/s], Decompressed: 4328 Downloaded: 4824 file(s) [attempted 4824/8459 = 57%, 42 KB/s], Decompressed: 4574 Downloaded: 4869 file(s) [attempted 4869/8459 = 57%, 193 KB/s], Decompressed: 4574 Downloaded: 4906 file(s) [attempted 4906/8459 = 57%, 69 KB/s], Decompressed: 4574 Downloaded: 4947 file(s) [attempted 4947/8459 = 58%, 54 KB/s], Decompressed: 4574 Downloaded: 4995 file(s) [attempted 4995/8459 = 59%, 495 KB/s], Decompressed: 4574 Downloaded: 5040 file(s) [attempted 5040/8459 = 59%, 99 KB/s], Decompressed: 4574 Downloaded: 5078 file(s) [attempted 5078/8459 = 60%, 156 KB/s], Decompressed: 4574 Downloaded: 5119 file(s) [attempted 5119/8459 = 60%, 339 KB/s], Decompressed: 4574 Downloaded: 5160 file(s) [attempted 5160/8459 = 61%, 62 KB/s], Decompressed: 4574 Downloaded: 5204 file(s) [attempted 5204/8459 = 61%, 122 KB/s], Decompressed: 4574 Downloaded: 5245 file(s) [attempted 5245/8459 = 62%, 72 KB/s], Decompressed: 4821 Downloaded: 5290 file(s) [attempted 5290/8459 = 62%, 626 KB/s], Decompressed: 4821 Downloaded: 5331 file(s) [attempted 5331/8459 = 63%, 702 KB/s], Decompressed: 4821 Downloaded: 5372 file(s) [attempted 5372/8459 = 63%, 394 KB/s], Decompressed: 4821 Downloaded: 5413 file(s) [attempted 5413/8459 = 63%, 166 KB/s], Decompressed: 4821 Downloaded: 5454 file(s) [attempted 5454/8459 = 64%, 985 KB/s], Decompressed: 4821 Downloaded: 5496 file(s) [attempted 5496/8459 = 64%, 643 KB/s], Decompressed: 4821 Downloaded: 5540 file(s) [attempted 5540/8459 = 65%, 231 KB/s], Decompressed: 4821 Downloaded: 5581 file(s) [attempted 5581/8459 = 65%, 1150 KB/s], Decompressed: 4821 Downloaded: 5622 file(s) [attempted 5622/8459 = 66%, 124 KB/s], Decompressed: 4821 Downloaded: 5663 file(s) [attempted 5663/8459 = 66%, 1364 KB/s], Decompressed: 5232 Downloaded: 5704 file(s) [attempted 5704/8459 = 67%, 456 KB/s], Decompressed: 5232 Downloaded: 5749 file(s) [attempted 5749/8459 = 67%, 101 KB/s], Decompressed: 5232 Downloaded: 5794 file(s) [attempted 5794/8459 = 68%, 409 KB/s], Decompressed: 5232 Downloaded: 5835 file(s) [attempted 5835/8459 = 68%, 709 KB/s], Decompressed: 5232 Downloaded: 5872 file(s) [attempted 5872/8459 = 69%, 160 KB/s], Decompressed: 5232 Downloaded: 5920 file(s) [attempted 5920/8459 = 69%, 627 KB/s], Decompressed: 5232 Downloaded: 5951 file(s) [attempted 5951/8459 = 70%, 376 KB/s], Decompressed: 5232 Downloaded: 5968 file(s) [attempted 5968/8459 = 70%, 44 KB/s], Decompressed: 5232 Downloaded: 6020 file(s) [attempted 6020/8459 = 71%, 25 KB/s], Decompressed: 5232 Downloaded: 6068 file(s) [attempted 6068/8459 = 71%, 102 KB/s], Decompressed: 5232 Downloaded: 6119 file(s) [attempted 6119/8459 = 72%, 100 KB/s], Decompressed: 5232 Downloaded: 6170 file(s) [attempted 6170/8459 = 72%, 215 KB/s], Decompressed: 5639 Downloaded: 6237 file(s) [attempted 6237/8459 = 73%, 853 KB/s], Decompressed: 5639 Downloaded: 6270 file(s) [attempted 6270/8459 = 74%, 130 KB/s], Decompressed: 5639 Downloaded: 6318 file(s) [attempted 6318/8459 = 74%, 181 KB/s], Decompressed: 5639 Downloaded: 6369 file(s) [attempted 6369/8459 = 75%, 534 KB/s], Decompressed: 5639 Downloaded: 6417 file(s) [attempted 6417/8459 = 75%, 287 KB/s], Decompressed: 5639 Downloaded: 6468 file(s) [attempted 6468/8459 = 76%, 141 KB/s], Decompressed: 5639 Downloaded: 6516 file(s) [attempted 6516/8459 = 77%, 501 KB/s], Decompressed: 5639 Downloaded: 6568 file(s) [attempted 6568/8459 = 77%, 91 KB/s], Decompressed: 5639 Downloaded: 6616 file(s) [attempted 6616/8459 = 78%, 2651 KB/s], Decompressed: 5639 Downloaded: 6664 file(s) [attempted 6664/8459 = 78%, 247 KB/s], Decompressed: 5639 Downloaded: 6712 file(s) [attempted 6712/8459 = 79%, 29 KB/s], Decompressed: 5639 Downloaded: 6756 file(s) [attempted 6756/8459 = 79%, 484 KB/s], Decompressed: 6170 Downloaded: 6797 file(s) [attempted 6797/8459 = 80%, 207 KB/s], Decompressed: 6170 Downloaded: 6835 file(s) [attempted 6835/8459 = 80%, 294 KB/s], Decompressed: 6170 Downloaded: 6873 file(s) [attempted 6873/8459 = 81%, 652 KB/s], Decompressed: 6170 Downloaded: 6917 file(s) [attempted 6917/8459 = 81%, 35 KB/s], Decompressed: 6170 Downloaded: 6958 file(s) [attempted 6958/8459 = 82%, 141 KB/s], Decompressed: 6170 Downloaded: 7006 file(s) [attempted 7006/8459 = 82%, 280 KB/s], Decompressed: 6170 Downloaded: 7054 file(s) [attempted 7054/8459 = 83%, 244 KB/s], Decompressed: 6170 Downloaded: 7102 file(s) [attempted 7102/8459 = 83%, 70 KB/s], Decompressed: 6170 Downloaded: 7140 file(s) [attempted 7140/8459 = 84%, 105 KB/s], Decompressed: 6170 Downloaded: 7179 file(s) [attempted 7179/8459 = 84%, 974 KB/s], Decompressed: 6170 Downloaded: 7219 file(s) [attempted 7219/8459 = 85%, 612 KB/s], Decompressed: 6722 Downloaded: 7258 file(s) [attempted 7258/8459 = 85%, 186 KB/s], Decompressed: 6722 Downloaded: 7304 file(s) [attempted 7304/8459 = 86%, 89 KB/s], Decompressed: 6722 Downloaded: 7352 file(s) [attempted 7352/8459 = 86%, 72 KB/s], Decompressed: 6722 Downloaded: 7403 file(s) [attempted 7403/8459 = 87%, 2482 KB/s], Decompressed: 6722 Downloaded: 7451 file(s) [attempted 7451/8459 = 88%, 109 KB/s], Decompressed: 6722 Downloaded: 7499 file(s) [attempted 7499/8459 = 88%, 168 KB/s], Decompressed: 6722 Downloaded: 7540 file(s) [attempted 7540/8459 = 89%, 170 KB/s], Decompressed: 6722 Downloaded: 7582 file(s) [attempted 7582/8459 = 89%, 30 KB/s], Decompressed: 7201 Downloaded: 7619 file(s) [attempted 7619/8459 = 90%, 518 KB/s], Decompressed: 7201 Downloaded: 7664 file(s) [attempted 7664/8459 = 90%, 208 KB/s], Decompressed: 7201 Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 95 KB/s], Decompressed: 7201 Downloaded: 7746 file(s) [attempted 7746/8459 = 91%, 189 KB/s], Decompressed: 7201 Downloaded: 7790 file(s) [attempted 7790/8459 = 92%, 24 KB/s], Decompressed: 7201 Downloaded: 7835 file(s) [attempted 7835/8459 = 92%, 783 KB/s], Decompressed: 7201 Downloaded: 7876 file(s) [attempted 7876/8459 = 93%, 208 KB/s], Decompressed: 7201 Downloaded: 7914 file(s) [attempted 7914/8459 = 93%, 856 KB/s], Decompressed: 7582 Downloaded: 7955 file(s) [attempted 7955/8459 = 94%, 546 KB/s], Decompressed: 7582 Downloaded: 7999 file(s) [attempted 7999/8459 = 94%, 107 KB/s], Decompressed: 7582 Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 189 KB/s], Decompressed: 7582 Downloaded: 8082 file(s) [attempted 8082/8459 = 95%, 61 KB/s], Decompressed: 7582 Downloaded: 8126 file(s) [attempted 8126/8459 = 96%, 172 KB/s], Decompressed: 7582 Downloaded: 8164 file(s) [attempted 8164/8459 = 96%, 382 KB/s], Decompressed: 7886 Downloaded: 8208 file(s) [attempted 8208/8459 = 97%, 82 KB/s], Decompressed: 7886 Downloaded: 8246 file(s) [attempted 8246/8459 = 97%, 191 KB/s], Decompressed: 7886 Downloaded: 8287 file(s) [attempted 8287/8459 = 97%, 131 KB/s], Decompressed: 7886 Downloaded: 8332 file(s) [attempted 8332/8459 = 98%, 46 KB/s], Decompressed: 7886 Downloaded: 8376 file(s) [attempted 8376/8459 = 99%, 355 KB/s], Decompressed: 7886 Downloaded: 8417 file(s) [attempted 8417/8459 = 99%, 116 KB/s], Decompressed: 8136 Downloaded: 8445 file(s) [attempted 8445/8459 = 99%, 218 KB/s], Decompressed: 8136 Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 111 KB/s], Decompressed: 8136 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 111 KB/s], Decompressed: 8136 apx-runtime-resource-v1 apx-verifier-job-1728-runtime-lake_cache-3977608-1787619513269338976-0 3952640 4100096 21474836480 0 0 0 0 0 0 3003162624 3612663808 21474836480 0 0 0 0 0 0
lean_checkerexit -
lake build
✔ [500/502] Built Iut.Foundations.Species (181s) ✔ [501/506] Built Iut.Foundations.SourceGameplanSpeciesMutation (66s) ✔ [784/791] Built Iut.Foundations.RealLineCopy (74s) ✔ [785/791] Built Iut.Foundations.TransportDiagram (90s) ✔ [786/791] Built Iut.Foundations.IndeterminacyRelation (67s) ✔ [787/791] Built Iut.Foundations.RegionMeasure (66s) ✔ [788/791] Built Iut.Foundations.CommonTargetBound (92s) ✔ [789/791] Built Iut.Foundations.TransportedRegionFamily (108s) ✔ [790/794] Built Iut.Foundations.QualitativeData (97s) ✔ [3508/3513] Built Iut.Foundations.EtaleThetaQuotient (291s) ✔ [3509/3513] Built Iut.Foundations.Orbicurve (1239s) ✔ [3956/3959] Built Iut.Foundations.InitialThetaData (1148s) ✔ [3964/3966] Built Iut.Foundations.OrbicurvePullback (2182s) ✔ [3965/3969] Built Iut.Foundations.EtaleThetaCovers (619s) ✔ [3974/3982] Built Iut.Foundations.SourceTateCurve (408s) ✔ [3981/3984] Built Iut.Foundations.GaloisImage (289s)
/usr/bin/podman timed out after 7200s podman cleanup removed verifier container apx-verifier-job-1728-runtime-lean_checker-3977608-1787619736338037565-1 on attempt 2
blueprint_buildexit 1
lake build :blueprint
error: unknown package facet `blueprint` apx-runtime-resource-v1 apx-verifier-job-1728-runtime-blueprint_build-3977608-1787626981219035763-2 1150976 1564672 21474836480 0 0 0 0 0 0 886128640 989937664 21474836480 0 0 0 0 0 0