Verification run

Run 1279

promachina/iut-leanbranch mastertriggered via github_push
failedcommit 4f5eb57060aatoolchain lean-v4-30-0prover leantook 2h 5m · finished 3w ago

lake 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)

Open project

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 128duration 240 ms · created
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 0duration 4s · created
git clone (github installation auth fallback)
Cloning into '/var/lib/apodeixis/repos/job-1728-source'...
git_checkoutexit 0duration 256 ms · created
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 0duration 3m 43s · created
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 -duration 2h 0m · created
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 1duration 22s · created
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

Keyboard shortcuts