Verification run

Run 1281

promachina/iut-leanbranch mastertriggered via poller

failedcommit cc2a2720d812toolchain lean-v4-30-0prover leantook 2h 29m · 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-1731-source
exit_code=Some(128) duration_ms=215
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1731-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=3794
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1731-source'...


$ git checkout cc2a2720d812d21060341d59487502453d8e23cd
exit_code=Some(0) duration_ms=290
stderr:
Note: switching to 'cc2a2720d812d21060341d59487502453d8e23cd'.

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 cc2a272 Merge pull request #969 from promachina/e23-3g-selected-family-exceptional-profile

Resolved source revision: cc2a2720d812d21060341d59487502453d8e23cd

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=cc2a2720d812d21060341d59487502453d8e23cd provenance={"branch":"master","checked_out_revision":"cc2a2720d812d21060341d59487502453d8e23cd","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"github_installation","local_clone":false,"requested_commit_sha":"cc2a2720d812d21060341d59487502453d8e23cd","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=58970 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=1694291
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 (1.1s)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (2.3s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (1.0s)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (239ms)
✔ [13/25] Built Cache.Lean:c.o (134ms)
✔ [15/25] Built Cache.Init (11s)
✔ [16/25] Built Cache.IO (13s)
✔ [17/25] Built Cache.Init:c.o (77ms)
✔ [18/25] Built Cache.IO:c.o (1.2s)
✔ [19/25] Built Cache.Hashing (908ms)
✔ [20/25] Built Cache.Hashing:c.o (397ms)
✔ [21/25] Built Cache.Requests (2.4s)
✔ [22/25] Built Cache.Requests:c.o (23s)
✔ [23/25] Built Cache.Main (19s)
✔ [24/25] Built Cache.Main:c.o (1.1s)
✔ [25/25] Built cache:exe (6.1s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 6 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 6 KB/s], Decompressed: 6
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 11 KB/s], Decompressed: 25
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 21 KB/s], Decompressed: 25
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 255 KB/s], Decompressed: 30
Downloaded: 128 file(s) [attempted 128/8459 = 1%, 98 KB/s], Decompressed: 30
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 71 KB/s], Decompressed: 89
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 386 KB/s], Decompressed: 89
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 236 KB/s], Decompressed: 152
Downloaded: 268 file(s) [attempted 268/8459 = 3%, 265 KB/s], Decompressed: 152
Downloaded: 302 file(s) [attempted 302/8459 = 3%, 453 KB/s], Decompressed: 213
Downloaded: 343 file(s) [attempted 343/8459 = 4%, 86 KB/s], Decompressed: 278
Downloaded: 385 file(s) [attempted 385/8459 = 4%, 138 KB/s], Decompressed: 278
Downloaded: 426 file(s) [attempted 426/8459 = 5%, 126 KB/s], Decompressed: 343
Downloaded: 463 file(s) [attempted 463/8459 = 5%, 483 KB/s], Decompressed: 398
Downloaded: 498 file(s) [attempted 498/8459 = 5%, 879 KB/s], Decompressed: 398
Downloaded: 535 file(s) [attempted 535/8459 = 6%, 35 KB/s], Decompressed: 453
Downloaded: 580 file(s) [attempted 580/8459 = 6%, 284 KB/s], Decompressed: 453
Downloaded: 625 file(s) [attempted 625/8459 = 7%, 362 KB/s], Decompressed: 515
Downloaded: 669 file(s) [attempted 669/8459 = 7%, 468 KB/s], Decompressed: 583
Downloaded: 714 file(s) [attempted 714/8459 = 8%, 387 KB/s], Decompressed: 583
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 366 KB/s], Decompressed: 659
Downloaded: 789 file(s) [attempted 789/8459 = 9%, 337 KB/s], Decompressed: 659
Downloaded: 834 file(s) [attempted 834/8459 = 9%, 401 KB/s], Decompressed: 738
Downloaded: 875 file(s) [attempted 875/8459 = 10%, 324 KB/s], Decompressed: 738
Downloaded: 916 file(s) [attempted 916/8459 = 10%, 405 KB/s], Decompressed: 813
Downloaded: 957 file(s) [attempted 957/8459 = 11%, 827 KB/s], Decompressed: 813
Downloaded: 998 file(s) [attempted 998/8459 = 11%, 103 KB/s], Decompressed: 889
Downloaded: 1033 file(s) [attempted 1033/8459 = 12%, 953 KB/s], Decompressed: 889
Downloaded: 1077 file(s) [attempted 1077/8459 = 12%, 121 KB/s], Decompressed: 967
Downloaded: 1122 file(s) [attempted 1122/8459 = 13%, 250 KB/s], Decompressed: 1043
Downloaded: 1159 file(s) [attempted 1159/8459 = 13%, 1681 KB/s], Decompressed: 1043
Downloaded: 1200 file(s) [attempted 1200/8459 = 14%, 185 KB/s], Decompressed: 1122
Downloaded: 1241 file(s) [attempted 1241/8459 = 14%, 155 KB/s], Decompressed: 1122
Downloaded: 1286 file(s) [attempted 1286/8459 = 15%, 1137 KB/s], Decompressed: 1200
Downloaded: 1330 file(s) [attempted 1330/8459 = 15%, 297 KB/s], Decompressed: 1200
Downloaded: 1372 file(s) [attempted 1372/8459 = 16%, 221 KB/s], Decompressed: 1279
Downloaded: 1409 file(s) [attempted 1409/8459 = 16%, 723 KB/s], Decompressed: 1279
Downloaded: 1450 file(s) [attempted 1450/8459 = 17%, 152 KB/s], Decompressed: 1279
Downloaded: 1488 file(s) [attempted 1488/8459 = 17%, 63 KB/s], Decompressed: 1372
Downloaded: 1529 file(s) [attempted 1529/8459 = 18%, 119 KB/s], Decompressed: 1372
Downloaded: 1577 file(s) [attempted 1577/8459 = 18%, 429 KB/s], Decompressed: 1468
Downloaded: 1622 file(s) [attempted 1622/8459 = 19%, 204 KB/s], Decompressed: 1468
Downloaded: 1666 file(s) [attempted 1666/8459 = 19%, 597 KB/s], Decompressed: 1468
Downloaded: 1707 file(s) [attempted 1707/8459 = 20%, 57 KB/s], Decompressed: 1570
Downloaded: 1745 file(s) [attempted 1745/8459 = 20%, 232 KB/s], Decompressed: 1570
Downloaded: 1783 file(s) [attempted 1783/8459 = 21%, 300 KB/s], Decompressed: 1680
Downloaded: 1824 file(s) [attempted 1824/8459 = 21%, 456 KB/s], Decompressed: 1680
Downloaded: 1865 file(s) [attempted 1865/8459 = 22%, 1478 KB/s], Decompressed: 1680
Downloaded: 1906 file(s) [attempted 1906/8459 = 22%, 237 KB/s], Decompressed: 1772
Downloaded: 1944 file(s) [attempted 1944/8459 = 22%, 114 KB/s], Decompressed: 1772
Downloaded: 1985 file(s) [attempted 1985/8459 = 23%, 74 KB/s], Decompressed: 1868
Downloaded: 2026 file(s) [attempted 2026/8459 = 23%, 279 KB/s], Decompressed: 1868
Downloaded: 2064 file(s) [attempted 2064/8459 = 24%, 132 KB/s], Decompressed: 1957
Downloaded: 2105 file(s) [attempted 2105/8459 = 24%, 53 KB/s], Decompressed: 1957
Downloaded: 2146 file(s) [attempted 2146/8459 = 25%, 330 KB/s], Decompressed: 1957
Downloaded: 2187 file(s) [attempted 2187/8459 = 25%, 950 KB/s], Decompressed: 2064
Downloaded: 2231 file(s) [attempted 2231/8459 = 26%, 296 KB/s], Decompressed: 2064
Downloaded: 2269 file(s) [attempted 2269/8459 = 26%, 76 KB/s], Decompressed: 2064
Downloaded: 2307 file(s) [attempted 2307/8459 = 27%, 135 KB/s], Decompressed: 2166
Downloaded: 2344 file(s) [attempted 2344/8459 = 27%, 38 KB/s], Decompressed: 2166
Downloaded: 2385 file(s) [attempted 2385/8459 = 28%, 1204 KB/s], Decompressed: 2166
Downloaded: 2427 file(s) [attempted 2427/8459 = 28%, 811 KB/s], Decompressed: 2283
Downloaded: 2468 file(s) [attempted 2468/8459 = 29%, 465 KB/s], Decompressed: 2283
Downloaded: 2512 file(s) [attempted 2512/8459 = 29%, 282 KB/s], Decompressed: 2283
Downloaded: 2560 file(s) [attempted 2560/8459 = 30%, 157 KB/s], Decompressed: 2409
Downloaded: 2598 file(s) [attempted 2598/8459 = 30%, 41 KB/s], Decompressed: 2409
Downloaded: 2635 file(s) [attempted 2635/8459 = 31%, 129 KB/s], Decompressed: 2409
Downloaded: 2676 file(s) [attempted 2676/8459 = 31%, 240 KB/s], Decompressed: 2529
Downloaded: 2714 file(s) [attempted 2714/8459 = 32%, 76 KB/s], Decompressed: 2529
Downloaded: 2755 file(s) [attempted 2755/8459 = 32%, 237 KB/s], Decompressed: 2529
Downloaded: 2800 file(s) [attempted 2800/8459 = 33%, 463 KB/s], Decompressed: 2529
Downloaded: 2838 file(s) [attempted 2838/8459 = 33%, 211 KB/s], Decompressed: 2529
Downloaded: 2875 file(s) [attempted 2875/8459 = 33%, 527 KB/s], Decompressed: 2673
Downloaded: 2920 file(s) [attempted 2920/8459 = 34%, 122 KB/s], Decompressed: 2673
Downloaded: 2961 file(s) [attempted 2961/8459 = 35%, 341 KB/s], Decompressed: 2673
Downloaded: 3002 file(s) [attempted 3002/8459 = 35%, 607 KB/s], Decompressed: 2673
Downloaded: 3040 file(s) [attempted 3040/8459 = 35%, 233 KB/s], Decompressed: 2673
Downloaded: 3081 file(s) [attempted 3081/8459 = 36%, 544 KB/s], Decompressed: 2848
Downloaded: 3122 file(s) [attempted 3122/8459 = 36%, 657 KB/s], Decompressed: 2848
Downloaded: 3166 file(s) [attempted 3166/8459 = 37%, 68 KB/s], Decompressed: 2848
Downloaded: 3204 file(s) [attempted 3204/8459 = 37%, 234 KB/s], Decompressed: 2848
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 254 KB/s], Decompressed: 2848
Downloaded: 3286 file(s) [attempted 3286/8459 = 38%, 435 KB/s], Decompressed: 2848
Downloaded: 3327 file(s) [attempted 3327/8459 = 39%, 172 KB/s], Decompressed: 2848
Downloaded: 3368 file(s) [attempted 3368/8459 = 39%, 316 KB/s], Decompressed: 3070
Downloaded: 3411 file(s) [attempted 3411/8459 = 40%, 171 KB/s], Decompressed: 3070
Downloaded: 3454 file(s) [attempted 3454/8459 = 40%, 236 KB/s], Decompressed: 3070
Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 1913 KB/s], Decompressed: 3070
Downloaded: 3526 file(s) [attempted 3526/8459 = 41%, 159 KB/s], Decompressed: 3070
Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 126 KB/s], Decompressed: 3070
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 40 KB/s], Decompressed: 3070
Downloaded: 3646 file(s) [attempted 3646/8459 = 43%, 248 KB/s], Decompressed: 3070
Downloaded: 3690 file(s) [attempted 3690/8459 = 43%, 57 KB/s], Decompressed: 3070
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 100 KB/s], Decompressed: 3365
Downloaded: 3762 file(s) [attempted 3762/8459 = 44%, 1133 KB/s], Decompressed: 3365
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 70 KB/s], Decompressed: 3365
Downloaded: 3845 file(s) [attempted 3845/8459 = 45%, 739 KB/s], Decompressed: 3365
Downloaded: 3879 file(s) [attempted 3879/8459 = 45%, 569 KB/s], Decompressed: 3365
Downloaded: 3920 file(s) [attempted 3920/8459 = 46%, 80 KB/s], Decompressed: 3365
Downloaded: 3961 file(s) [attempted 3961/8459 = 46%, 123 KB/s], Decompressed: 3365
Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 291 KB/s], Decompressed: 3365
Downloaded: 4006 file(s) [attempted 4006/8459 = 47%, 1038 KB/s], Decompressed: 3365
Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 215 KB/s], Decompressed: 3365
Downloaded: 4088 file(s) [attempted 4088/8459 = 48%, 178 KB/s], Decompressed: 3365
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 116 KB/s], Decompressed: 3365
Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 2017 KB/s], Decompressed: 3365
Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 705 KB/s], Decompressed: 3721
Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 75 KB/s], Decompressed: 3721
Downloaded: 4324 file(s) [attempted 4324/8459 = 51%, 106 KB/s], Decompressed: 3721
Downloaded: 4369 file(s) [attempted 4369/8459 = 51%, 268 KB/s], Decompressed: 3721
Downloaded: 4413 file(s) [attempted 4413/8459 = 52%, 69 KB/s], Decompressed: 3721
Downloaded: 4461 file(s) [attempted 4461/8459 = 52%, 442 KB/s], Decompressed: 3721
Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 80 KB/s], Decompressed: 3721
Downloaded: 4554 file(s) [attempted 4554/8459 = 53%, 463 KB/s], Decompressed: 3721
Downloaded: 4588 file(s) [attempted 4588/8459 = 54%, 610 KB/s], Decompressed: 3721
Downloaded: 4629 file(s) [attempted 4629/8459 = 54%, 100 KB/s], Decompressed: 3721
Downloaded: 4670 file(s) [attempted 4670/8459 = 55%, 686 KB/s], Decompressed: 3721
Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 248 KB/s], Decompressed: 3721
Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 85 KB/s], Decompressed: 3721
Downloaded: 4787 file(s) [attempted 4787/8459 = 56%, 104 KB/s], Decompressed: 3721
Downloaded: 4824 file(s) [attempted 4824/8459 = 57%, 390 KB/s], Decompressed: 3721
Downloaded: 4865 file(s) [attempted 4865/8459 = 57%, 202 KB/s], Decompressed: 4228
Downloaded: 4903 file(s) [attempted 4903/8459 = 57%, 162 KB/s], Decompressed: 4228
Downloaded: 4930 file(s) [attempted 4930/8459 = 58%, 213 KB/s], Decompressed: 4228
Downloaded: 4972 file(s) [attempted 4972/8459 = 58%, 78 KB/s], Decompressed: 4228
Downloaded: 5013 file(s) [attempted 5013/8459 = 59%, 1456 KB/s], Decompressed: 4228
Downloaded: 5050 file(s) [attempted 5050/8459 = 59%, 5010 KB/s], Decompressed: 4228
Downloaded: 5088 file(s) [attempted 5088/8459 = 60%, 1883 KB/s], Decompressed: 4228
Downloaded: 5122 file(s) [attempted 5122/8459 = 60%, 533 KB/s], Decompressed: 4228
Downloaded: 5160 file(s) [attempted 5160/8459 = 61%, 53 KB/s], Decompressed: 4228
Downloaded: 5198 file(s) [attempted 5198/8459 = 61%, 122 KB/s], Decompressed: 4228
Downloaded: 5239 file(s) [attempted 5239/8459 = 61%, 100 KB/s], Decompressed: 4228
Downloaded: 5276 file(s) [attempted 5276/8459 = 62%, 631 KB/s], Decompressed: 4228
Downloaded: 5314 file(s) [attempted 5314/8459 = 62%, 1223 KB/s], Decompressed: 4228
Downloaded: 5355 file(s) [attempted 5355/8459 = 63%, 175 KB/s], Decompressed: 4228
Downloaded: 5400 file(s) [attempted 5400/8459 = 63%, 85 KB/s], Decompressed: 4228
Downloaded: 5437 file(s) [attempted 5437/8459 = 64%, 136 KB/s], Decompressed: 4228
Downloaded: 5475 file(s) [attempted 5475/8459 = 64%, 149 KB/s], Decompressed: 4228
Downloaded: 5516 file(s) [attempted 5516/8459 = 65%, 1360 KB/s], Decompressed: 4835
Downloaded: 5557 file(s) [attempted 5557/8459 = 65%, 301 KB/s], Decompressed: 4835
Downloaded: 5602 file(s) [attempted 5602/8459 = 66%, 727 KB/s], Decompressed: 4835
Downloaded: 5643 file(s) [attempted 5643/8459 = 66%, 575 KB/s], Decompressed: 4835
Downloaded: 5681 file(s) [attempted 5681/8459 = 67%, 1525 KB/s], Decompressed: 4835
Downloaded: 5722 file(s) [attempted 5722/8459 = 67%, 56 KB/s], Decompressed: 4835
Downloaded: 5759 file(s) [attempted 5759/8459 = 68%, 213 KB/s], Decompressed: 4835
Downloaded: 5807 file(s) [attempted 5807/8459 = 68%, 121 KB/s], Decompressed: 4835
Downloaded: 5852 file(s) [attempted 5852/8459 = 69%, 594 KB/s], Decompressed: 4835
Downloaded: 5893 file(s) [attempted 5893/8459 = 69%, 166 KB/s], Decompressed: 4835
Downloaded: 5927 file(s) [attempted 5927/8459 = 70%, 128 KB/s], Decompressed: 4835
Downloaded: 5965 file(s) [attempted 5965/8459 = 70%, 390 KB/s], Decompressed: 4835
Downloaded: 5999 file(s) [attempted 5999/8459 = 70%, 530 KB/s], Decompressed: 5499
Downloaded: 6047 file(s) [attempted 6047/8459 = 71%, 3 KB/s], Decompressed: 5499
Downloaded: 6049 file(s) [attempted 6049/8459 = 71%, 0 KB/s], Decompressed: 5499
Downloaded: 6051 file(s) [attempted 6051/8459 = 71%, 83 KB/s], Decompressed: 5499
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 7 KB/s], Decompressed: 5499
Downloaded: 6053 file(s) [attempted 6053/8459 = 71%, 60 KB/s], Decompressed: 5499
Downloaded: 6054 file(s) [attempted 6054/8459 = 71%, 320 KB/s], Decompressed: 5499
Downloaded: 6055 file(s) [attempted 6055/8459 = 71%, 56 KB/s], Decompressed: 5499
Downloaded: 6056 file(s) [attempted 6056/8459 = 71%, 17 KB/s], Decompressed: 5499
Downloaded: 6057 file(s) [attempted 6057/8459 = 71%, 62 KB/s], Decompressed: 5499
Downloaded: 6058 file(s) [attempted 6058/8459 = 71%, 98 KB/s], Decompressed: 5999
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 38 KB/s], Decompressed: 5999
Downloaded: 6060 file(s) [attempted 6060/8459 = 71%, 26 KB/s], Decompressed: 5999
Downloaded: 6061 file(s) [attempted 6061/8459 = 71%, 24 KB/s], Decompressed: 5999
Downloaded: 6062 file(s) [attempted 6062/8459 = 71%, 28 KB/s], Decompressed: 5999
Downloaded: 6081 file(s) [attempted 6081/8459 = 71%, 27 KB/s], Decompressed: 6058
Downloaded: 6085 file(s) [attempted 6085/8459 = 71%, 54 KB/s], Decompressed: 6064
Downloaded: 6099 file(s) [attempted 6099/8459 = 72%, 29 KB/s], Decompressed: 6082
Downloaded: 6102 file(s) [attempted 6102/8459 = 72%, 41 KB/s], Decompressed: 6099
Downloaded: 6104 file(s) [attempted 6104/8459 = 72%, 6 KB/s], Decompressed: 6099
Downloaded: 6105 file(s) [attempted 6105/8459 = 72%, 0 KB/s], Decompressed: 6099
Downloaded: 6106 file(s) [attempted 6106/8459 = 72%, 1 KB/s], Decompressed: 6102
Downloaded: 6108 file(s) [attempted 6108/8459 = 72%, 19 KB/s], Decompressed: 6102
Downloaded: 6110 file(s) [attempted 6110/8459 = 72%, 6 KB/s], Decompressed: 6102
Downloaded: 6111 file(s) [attempted 6111/8459 = 72%, 1 KB/s], Decompressed: 6102
Downloaded: 6112 file(s) [attempted 6112/8459 = 72%, 3 KB/s], Decompressed: 6106
Downloaded: 6113 file(s) [attempted 6113/8459 = 72%, 4 KB/s], Decompressed: 6106
Downloaded: 6114 file(s) [attempted 6114/8459 = 72%, 11 KB/s], Decompressed: 6112
Downloaded: 6115 file(s) [attempted 6115/8459 = 72%, 2 KB/s], Decompressed: 6112
Downloaded: 6116 file(s) [attempted 6116/8459 = 72%, 14 KB/s], Decompressed: 6112
Downloaded: 6118 file(s) [attempted 6118/8459 = 72%, 3 KB/s], Decompressed: 6114
Downloaded: 6119 file(s) [attempted 6119/8459 = 72%, 1 KB/s], Decompressed: 6114
Downloaded: 6120 file(s) [attempted 6120/8459 = 72%, 5 KB/s], Decompressed: 6118
Downloaded: 6121 file(s) [attempted 6121/8459 = 72%, 6 KB/s], Decompressed: 6118
Downloaded: 6122 file(s) [attempted 6122/8459 = 72%, 2 KB/s], Decompressed: 6118
Downloaded: 6123 file(s) [attempted 6123/8459 = 72%, 12 KB/s], Decompressed: 6120
Downloaded: 6150 file(s) [attempted 6150/8459 = 72%, 41 KB/s], Decompressed: 6123
Downloaded: 6153 file(s) [attempted 6153/8459 = 72%, 20 KB/s], Decompressed: 6150
Downloaded: 6168 file(s) [attempted 6168/8459 = 72%, 5 KB/s], Decompressed: 6165
Downloaded: 6169 file(s) [attempted 6169/8459 = 72%, 1 KB/s], Decompressed: 6165
Downloaded: 6170 file(s) [attempted 6170/8459 = 72%, 0 KB/s], Decompressed: 6168
Downloaded: 6171 file(s) [attempted 6171/8459 = 72%, 3 KB/s], Decompressed: 6168
Downloaded: 6172 file(s) [attempted 6172/8459 = 72%, 1 KB/s], Decompressed: 6168
Downloaded: 6173 file(s) [attempted 6173/8459 = 72%, 3 KB/s], Decompressed: 6170
Downloaded: 6174 file(s) [attempted 6174/8459 = 72%, 2 KB/s], Decompressed: 6170
Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 3 KB/s], Decompressed: 6170
Downloaded: 6176 file(s) [attempted 6176/8459 = 73%, 1 KB/s], Decompressed: 6173
Downloaded: 6177 file(s) [attempted 6177/8459 = 73%, 2 KB/s], Decompressed: 6173
Downloaded: 6178 file(s) [attempted 6178/8459 = 73%, 0 KB/s], Decompressed: 6176
Downloaded: 6179 file(s) [attempted 6179/8459 = 73%, 2 KB/s], Decompressed: 6178
Downloaded: 6180 file(s) [attempted 6180/8459 = 73%, 0 KB/s], Decompressed: 6178
Downloaded: 6181 file(s) [attempted 6181/8459 = 73%, 2 KB/s], Decompressed: 6178
Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 3 KB/s], Decompressed: 6179
Downloaded: 6183 file(s) [attempted 6183/8459 = 73%, 13 KB/s], Decompressed: 6179
Downloaded: 6184 file(s) [attempted 6184/8459 = 73%, 7 KB/s], Decompressed: 6182
Downloaded: 6211 file(s) [attempted 6211/8459 = 73%, 1 KB/s], Decompressed: 6184
Downloaded: 6228 file(s) [attempted 6228/8459 = 73%, 21 KB/s], Decompressed: 6211
Downloaded: 6229 file(s) [attempted 6229/8459 = 73%, 17 KB/s], Decompressed: 6211
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 24 KB/s], Decompressed: 6228
Downloaded: 6231 file(s) [attempted 6231/8459 = 73%, 18 KB/s], Decompressed: 6228
Downloaded: 6232 file(s) [attempted 6232/8459 = 73%, 4 KB/s], Decompressed: 6228
Downloaded: 6233 file(s) [attempted 6233/8459 = 73%, 40 KB/s], Decompressed: 6230
Downloaded: 6234 file(s) [attempted 6234/8459 = 73%, 33 KB/s], Decompressed: 6230
Downloaded: 6236 file(s) [attempted 6236/8459 = 73%, 17 KB/s], Decompressed: 6233
Downloaded: 6237 file(s) [attempted 6237/8459 = 73%, 11 KB/s], Decompressed: 6233
Downloaded: 6238 file(s) [attempted 6238/8459 = 73%, 6 KB/s], Decompressed: 6233
Downloaded: 6239 file(s) [attempted 6239/8459 = 73%, 25 KB/s], Decompressed: 6236
Downloaded: 6240 file(s) [attempted 6240/8459 = 73%, 31 KB/s], Decompressed: 6236
Downloaded: 6241 file(s) [attempted 6241/8459 = 73%, 2 KB/s], Decompressed: 6239
Downloaded: 6242 file(s) [attempted 6242/8459 = 73%, 9 KB/s], Decompressed: 6239
Downloaded: 6243 file(s) [attempted 6243/8459 = 73%, 3 KB/s], Decompressed: 6241
Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 4 KB/s], Decompressed: 6241
Downloaded: 6245 file(s) [attempted 6245/8459 = 73%, 1 KB/s], Decompressed: 6241
Downloaded: 6246 file(s) [attempted 6246/8459 = 73%, 3 KB/s], Decompressed: 6241
Downloaded: 6247 file(s) [attempted 6247/8459 = 73%, 15 KB/s], Decompressed: 6243
Downloaded: 6248 file(s) [attempted 6248/8459 = 73%, 31 KB/s], Decompressed: 6243
Downloaded: 6249 file(s) [attempted 6249/8459 = 73%, 24 KB/s], Decompressed: 6243
Downloaded: 6250 file(s) [attempted 6250/8459 = 73%, 9 KB/s], Decompressed: 6243
Downloaded: 6251 file(s) [attempted 6251/8459 = 73%, 7 KB/s], Decompressed: 6247
Downloaded: 6252 file(s) [attempted 6252/8459 = 73%, 4 KB/s], Decompressed: 6247
Downloaded: 6253 file(s) [attempted 6253/8459 = 73%, 1 KB/s], Decompressed: 6251
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 1 KB/s], Decompressed: 6251
Downloaded: 6255 file(s) [attempted 6255/8459 = 73%, 4 KB/s], Decompressed: 6251
Downloaded: 6257 file(s) [attempted 6257/8459 = 73%, 4 KB/s], Decompressed: 6253
Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 16 KB/s], Decompressed: 6253
Downloaded: 6259 file(s) [attempted 6259/8459 = 73%, 3 KB/s], Decompressed: 6256
Downloaded: 6280 file(s) [attempted 6280/8459 = 74%, 3 KB/s], Decompressed: 6259
Downloaded: 6281 file(s) [attempted 6281/8459 = 74%, 221 KB/s], Decompressed: 6259
Downloaded: 6283 file(s) [attempted 6283/8459 = 74%, 30 KB/s], Decompressed: 6280
Downloaded: 6286 file(s) [attempted 6286/8459 = 74%, 116 KB/s], Decompressed: 6283
Downloaded: 6287 file(s) [attempted 6287/8459 = 74%, 42 KB/s], Decompressed: 6286
Downloaded: 6288 file(s) [attempted 6288/8459 = 74%, 254 KB/s], Decompressed: 6287
Downloaded: 6328 file(s) [attempted 6328/8459 = 74%, 33 KB/s], Decompressed: 6301
Downloaded: 6366 file(s) [attempted 6366/8459 = 75%, 421 KB/s], Decompressed: 6328
Downloaded: 6393 file(s) [attempted 6393/8459 = 75%, 61 KB/s], Decompressed: 6328
Downloaded: 6417 file(s) [attempted 6417/8459 = 75%, 739 KB/s], Decompressed: 6366
Downloaded: 6434 file(s) [attempted 6434/8459 = 76%, 144 KB/s], Decompressed: 6366
Downloaded: 6448 file(s) [attempted 6448/8459 = 76%, 539 KB/s], Decompressed: 6417
Downloaded: 6462 file(s) [attempted 6462/8459 = 76%, 669 KB/s], Decompressed: 6448
Downloaded: 6465 file(s) [attempted 6465/8459 = 76%, 93 KB/s], Decompressed: 6462
Downloaded: 6472 file(s) [attempted 6472/8459 = 76%, 32 KB/s], Decompressed: 6462
Downloaded: 6489 file(s) [attempted 6489/8459 = 76%, 19 KB/s], Decompressed: 6465
Downloaded: 6506 file(s) [attempted 6506/8459 = 76%, 35 KB/s], Decompressed: 6465
Downloaded: 6510 file(s) [attempted 6510/8459 = 76%, 86 KB/s], Decompressed: 6489
Downloaded: 6527 file(s) [attempted 6527/8459 = 77%, 83 KB/s], Decompressed: 6489
Downloaded: 6530 file(s) [attempted 6530/8459 = 77%, 24 KB/s], Decompressed: 6510
Downloaded: 6537 file(s) [attempted 6537/8459 = 77%, 46 KB/s], Decompressed: 6510
Downloaded: 6544 file(s) [attempted 6544/8459 = 77%, 40 KB/s], Decompressed: 6541
Downloaded: 6554 file(s) [attempted 6554/8459 = 77%, 41 KB/s], Decompressed: 6551
Downloaded: 6561 file(s) [attempted 6561/8459 = 77%, 57 KB/s], Decompressed: 6554
Downloaded: 6568 file(s) [attempted 6568/8459 = 77%, 38 KB/s], Decompressed: 6558
Downloaded: 6575 file(s) [attempted 6575/8459 = 77%, 45 KB/s], Decompressed: 6571
Downloaded: 6585 file(s) [attempted 6585/8459 = 77%, 44 KB/s], Decompressed: 6575
Downloaded: 6599 file(s) [attempted 6599/8459 = 78%, 47 KB/s], Decompressed: 6585
Downloaded: 6606 file(s) [attempted 6606/8459 = 78%, 30 KB/s], Decompressed: 6595
Downloaded: 6616 file(s) [attempted 6616/8459 = 78%, 27 KB/s], Decompressed: 6613
Downloaded: 6620 file(s) [attempted 6620/8459 = 78%, 240 KB/s], Decompressed: 6616
Downloaded: 6630 file(s) [attempted 6630/8459 = 78%, 41 KB/s], Decompressed: 6619
Downloaded: 6637 file(s) [attempted 6637/8459 = 78%, 44 KB/s], Decompressed: 6630
Downloaded: 6643 file(s) [attempted 6643/8459 = 78%, 74 KB/s], Decompressed: 6637
Downloaded: 6650 file(s) [attempted 6650/8459 = 78%, 47 KB/s], Decompressed: 6643
Downloaded: 6654 file(s) [attempted 6654/8459 = 78%, 29 KB/s], Decompressed: 6650
Downloaded: 6655 file(s) [attempted 6655/8459 = 78%, 46 KB/s], Decompressed: 6650
Downloaded: 6656 file(s) [attempted 6656/8459 = 78%, 40 KB/s], Decompressed: 6654
Downloaded: 6657 file(s) [attempted 6657/8459 = 78%, 89 KB/s], Decompressed: 6656
Downloaded: 6705 file(s) [attempted 6705/8459 = 79%, 0 KB/s], Decompressed: 6657
Downloaded: 6709 file(s) [attempted 6709/8459 = 79%, 27 KB/s], Decompressed: 6657
Downloaded: 6729 file(s) [attempted 6729/8459 = 79%, 31 KB/s], Decompressed: 6705
Downloaded: 6757 file(s) [attempted 6757/8459 = 79%, 169 KB/s], Decompressed: 6705
Downloaded: 6801 file(s) [attempted 6801/8459 = 80%, 291 KB/s], Decompressed: 6705
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 30 KB/s], Decompressed: 6729
Downloaded: 6894 file(s) [attempted 6894/8459 = 81%, 100 KB/s], Decompressed: 6729
Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 949 KB/s], Decompressed: 6729
Downloaded: 6989 file(s) [attempted 6989/8459 = 82%, 37 KB/s], Decompressed: 6835
Downloaded: 7031 file(s) [attempted 7031/8459 = 83%, 1879 KB/s], Decompressed: 6835
Downloaded: 7075 file(s) [attempted 7075/8459 = 83%, 67 KB/s], Decompressed: 6835
Downloaded: 7116 file(s) [attempted 7116/8459 = 84%, 363 KB/s], Decompressed: 6952
Downloaded: 7150 file(s) [attempted 7150/8459 = 84%, 82 KB/s], Decompressed: 6952
Downloaded: 7192 file(s) [attempted 7192/8459 = 85%, 1181 KB/s], Decompressed: 6952
Downloaded: 7233 file(s) [attempted 7233/8459 = 85%, 1251 KB/s], Decompressed: 7079
Downloaded: 7274 file(s) [attempted 7274/8459 = 85%, 185 KB/s], Decompressed: 7079
Downloaded: 7318 file(s) [attempted 7318/8459 = 86%, 339 KB/s], Decompressed: 7079
Downloaded: 7363 file(s) [attempted 7363/8459 = 87%, 47 KB/s], Decompressed: 7212
Downloaded: 7400 file(s) [attempted 7400/8459 = 87%, 1406 KB/s], Decompressed: 7212
Downloaded: 7442 file(s) [attempted 7442/8459 = 87%, 88 KB/s], Decompressed: 7212
Downloaded: 7476 file(s) [attempted 7476/8459 = 88%, 192 KB/s], Decompressed: 7212
Downloaded: 7520 file(s) [attempted 7520/8459 = 88%, 25 KB/s], Decompressed: 7346
Downloaded: 7565 file(s) [attempted 7565/8459 = 89%, 283 KB/s], Decompressed: 7346
Downloaded: 7606 file(s) [attempted 7606/8459 = 89%, 229 KB/s], Decompressed: 7346
Downloaded: 7640 file(s) [attempted 7640/8459 = 90%, 274 KB/s], Decompressed: 7346
Downloaded: 7678 file(s) [attempted 7678/8459 = 90%, 54 KB/s], Decompressed: 7496
Downloaded: 7722 file(s) [attempted 7722/8459 = 91%, 644 KB/s], Decompressed: 7496
Downloaded: 7764 file(s) [attempted 7764/8459 = 91%, 541 KB/s], Decompressed: 7496
Downloaded: 7802 file(s) [attempted 7802/8459 = 92%, 99 KB/s], Decompressed: 7496
Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 285 KB/s], Decompressed: 7657
Downloaded: 7880 file(s) [attempted 7880/8459 = 93%, 890 KB/s], Decompressed: 7657
Downloaded: 7921 file(s) [attempted 7921/8459 = 93%, 37 KB/s], Decompressed: 7657
Downloaded: 7966 file(s) [attempted 7966/8459 = 94%, 78 KB/s], Decompressed: 7657
Downloaded: 8014 file(s) [attempted 8014/8459 = 94%, 469 KB/s], Decompressed: 7657
Downloaded: 8051 file(s) [attempted 8051/8459 = 95%, 414 KB/s], Decompressed: 7829
Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 376 KB/s], Decompressed: 7829
Downloaded: 8137 file(s) [attempted 8137/8459 = 96%, 316 KB/s], Decompressed: 7829
Downloaded: 8175 file(s) [attempted 8175/8459 = 96%, 56 KB/s], Decompressed: 7829
Downloaded: 8219 file(s) [attempted 8219/8459 = 97%, 83 KB/s], Decompressed: 7829
Downloaded: 8266 file(s) [attempted 8266/8459 = 97%, 47 KB/s], Decompressed: 7829
Downloaded: 8301 file(s) [attempted 8301/8459 = 98%, 66 KB/s], Decompressed: 7829
Downloaded: 8342 file(s) [attempted 8342/8459 = 98%, 829 KB/s], Decompressed: 8048
Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 56 KB/s], Decompressed: 8048
Downloaded: 8425 file(s) [attempted 8425/8459 = 99%, 653 KB/s], Decompressed: 8048
Downloaded: 8455 file(s) [attempted 8455/8459 = 99%, 107 KB/s], Decompressed: 8325
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 13 KB/s], Decompressed: 8325
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 13 KB/s], Decompressed: 8325

apx-runtime-resource-v1	apx-verifier-job-1731-runtime-lake_cache-4011476-1787639010726920297-0	4018176	4018176	21474836480	0	0	0	0	0	0	574349312	2476326912	21474836480	0	0	0	0	0	0


$ lake build
exit_code=None duration_ms=7200009
stdout:
✔ [500/502] Built Iut.Foundations.Species (380s)
✔ [501/502] Built Iut.Foundations.SourceGameplanSpeciesMutation (172s)
✔ [784/791] Built Iut.Foundations.RealLineCopy (425s)
✔ [785/791] Built Iut.Foundations.TransportDiagram (154s)
✔ [786/791] Built Iut.Foundations.IndeterminacyRelation (79s)
✔ [787/791] Built Iut.Foundations.RegionMeasure (198s)
✔ [788/791] Built Iut.Foundations.CommonTargetBound (236s)
✔ [789/791] Built Iut.Foundations.TransportedRegionFamily (65s)
✔ [790/791] Built Iut.Foundations.QualitativeData (68s)
✔ [3508/3513] Built Iut.Foundations.EtaleThetaQuotient (538s)
✔ [3509/3513] Built Iut.Foundations.Orbicurve (936s)
✔ [3956/3959] Built Iut.Foundations.InitialThetaData (1170s)
✔ [3962/3966] Built Iut.Foundations.OrbicurvePullback (817s)
✔ [3965/3968] Built Iut.Foundations.EtaleThetaCovers (286s)
✔ [3974/3982] Built Iut.Foundations.SourceTateCurve (438s)
✔ [3981/3986] Built Iut.Foundations.GaloisImage (171s)
✔ [3983/3989] Built Iut.Foundations.SourceAnabelioid (813s)

stderr:
/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1731-runtime-lean_checker-4011476-1787640705021891485-1 on attempt 1

$ lake build :blueprint
exit_code=Some(1) duration_ms=14789
stderr:
error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1731-runtime-blueprint_build-4011476-1787647905719450612-2	970752	1486848	21474836480	0	0	0	0	0	0	817074176	920621056	21474836480	0	0	0	0	0	0


blueprint_build failed; continuing (non-fatal phase).

Command runs

git_cloneexit 128duration 215 ms · created 8/25/2026, 8:52:02 AM

git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1731-source

Cloning into '/var/lib/apodeixis/repos/job-1731-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 8/25/2026, 8:52:02 AM

git clone (github installation auth fallback)

Cloning into '/var/lib/apodeixis/repos/job-1731-source'...

git_checkoutexit 0duration 290 ms · created 8/25/2026, 8:52:02 AM

git checkout cc2a2720d812d21060341d59487502453d8e23cd

Note: switching to 'cc2a2720d812d21060341d59487502453d8e23cd'.

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 cc2a272 Merge pull request #969 from promachina/e23-3g-selected-family-exceptional-profile

lake_cacheexit 0duration 28m 14s · created 8/25/2026, 8:52:02 AM

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 (1.1s)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (2.3s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (1.0s)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (239ms)
✔ [13/25] Built Cache.Lean:c.o (134ms)
✔ [15/25] Built Cache.Init (11s)
✔ [16/25] Built Cache.IO (13s)
✔ [17/25] Built Cache.Init:c.o (77ms)
✔ [18/25] Built Cache.IO:c.o (1.2s)
✔ [19/25] Built Cache.Hashing (908ms)
✔ [20/25] Built Cache.Hashing:c.o (397ms)
✔ [21/25] Built Cache.Requests (2.4s)
✔ [22/25] Built Cache.Requests:c.o (23s)
✔ [23/25] Built Cache.Main (19s)
✔ [24/25] Built Cache.Main:c.o (1.1s)
✔ [25/25] Built cache:exe (6.1s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 6 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 6 KB/s], Decompressed: 6
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 11 KB/s], Decompressed: 25
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 21 KB/s], Decompressed: 25
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 255 KB/s], Decompressed: 30
Downloaded: 128 file(s) [attempted 128/8459 = 1%, 98 KB/s], Decompressed: 30
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 71 KB/s], Decompressed: 89
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 386 KB/s], Decompressed: 89
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 236 KB/s], Decompressed: 152
Downloaded: 268 file(s) [attempted 268/8459 = 3%, 265 KB/s], Decompressed: 152
Downloaded: 302 file(s) [attempted 302/8459 = 3%, 453 KB/s], Decompressed: 213
Downloaded: 343 file(s) [attempted 343/8459 = 4%, 86 KB/s], Decompressed: 278
Downloaded: 385 file(s) [attempted 385/8459 = 4%, 138 KB/s], Decompressed: 278
Downloaded: 426 file(s) [attempted 426/8459 = 5%, 126 KB/s], Decompressed: 343
Downloaded: 463 file(s) [attempted 463/8459 = 5%, 483 KB/s], Decompressed: 398
Downloaded: 498 file(s) [attempted 498/8459 = 5%, 879 KB/s], Decompressed: 398
Downloaded: 535 file(s) [attempted 535/8459 = 6%, 35 KB/s], Decompressed: 453
Downloaded: 580 file(s) [attempted 580/8459 = 6%, 284 KB/s], Decompressed: 453
Downloaded: 625 file(s) [attempted 625/8459 = 7%, 362 KB/s], Decompressed: 515
Downloaded: 669 file(s) [attempted 669/8459 = 7%, 468 KB/s], Decompressed: 583
Downloaded: 714 file(s) [attempted 714/8459 = 8%, 387 KB/s], Decompressed: 583
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 366 KB/s], Decompressed: 659
Downloaded: 789 file(s) [attempted 789/8459 = 9%, 337 KB/s], Decompressed: 659
Downloaded: 834 file(s) [attempted 834/8459 = 9%, 401 KB/s], Decompressed: 738
Downloaded: 875 file(s) [attempted 875/8459 = 10%, 324 KB/s], Decompressed: 738
Downloaded: 916 file(s) [attempted 916/8459 = 10%, 405 KB/s], Decompressed: 813
Downloaded: 957 file(s) [attempted 957/8459 = 11%, 827 KB/s], Decompressed: 813
Downloaded: 998 file(s) [attempted 998/8459 = 11%, 103 KB/s], Decompressed: 889
Downloaded: 1033 file(s) [attempted 1033/8459 = 12%, 953 KB/s], Decompressed: 889
Downloaded: 1077 file(s) [attempted 1077/8459 = 12%, 121 KB/s], Decompressed: 967
Downloaded: 1122 file(s) [attempted 1122/8459 = 13%, 250 KB/s], Decompressed: 1043
Downloaded: 1159 file(s) [attempted 1159/8459 = 13%, 1681 KB/s], Decompressed: 1043
Downloaded: 1200 file(s) [attempted 1200/8459 = 14%, 185 KB/s], Decompressed: 1122
Downloaded: 1241 file(s) [attempted 1241/8459 = 14%, 155 KB/s], Decompressed: 1122
Downloaded: 1286 file(s) [attempted 1286/8459 = 15%, 1137 KB/s], Decompressed: 1200
Downloaded: 1330 file(s) [attempted 1330/8459 = 15%, 297 KB/s], Decompressed: 1200
Downloaded: 1372 file(s) [attempted 1372/8459 = 16%, 221 KB/s], Decompressed: 1279
Downloaded: 1409 file(s) [attempted 1409/8459 = 16%, 723 KB/s], Decompressed: 1279
Downloaded: 1450 file(s) [attempted 1450/8459 = 17%, 152 KB/s], Decompressed: 1279
Downloaded: 1488 file(s) [attempted 1488/8459 = 17%, 63 KB/s], Decompressed: 1372
Downloaded: 1529 file(s) [attempted 1529/8459 = 18%, 119 KB/s], Decompressed: 1372
Downloaded: 1577 file(s) [attempted 1577/8459 = 18%, 429 KB/s], Decompressed: 1468
Downloaded: 1622 file(s) [attempted 1622/8459 = 19%, 204 KB/s], Decompressed: 1468
Downloaded: 1666 file(s) [attempted 1666/8459 = 19%, 597 KB/s], Decompressed: 1468
Downloaded: 1707 file(s) [attempted 1707/8459 = 20%, 57 KB/s], Decompressed: 1570
Downloaded: 1745 file(s) [attempted 1745/8459 = 20%, 232 KB/s], Decompressed: 1570
Downloaded: 1783 file(s) [attempted 1783/8459 = 21%, 300 KB/s], Decompressed: 1680
Downloaded: 1824 file(s) [attempted 1824/8459 = 21%, 456 KB/s], Decompressed: 1680
Downloaded: 1865 file(s) [attempted 1865/8459 = 22%, 1478 KB/s], Decompressed: 1680
Downloaded: 1906 file(s) [attempted 1906/8459 = 22%, 237 KB/s], Decompressed: 1772
Downloaded: 1944 file(s) [attempted 1944/8459 = 22%, 114 KB/s], Decompressed: 1772
Downloaded: 1985 file(s) [attempted 1985/8459 = 23%, 74 KB/s], Decompressed: 1868
Downloaded: 2026 file(s) [attempted 2026/8459 = 23%, 279 KB/s], Decompressed: 1868
Downloaded: 2064 file(s) [attempted 2064/8459 = 24%, 132 KB/s], Decompressed: 1957
Downloaded: 2105 file(s) [attempted 2105/8459 = 24%, 53 KB/s], Decompressed: 1957
Downloaded: 2146 file(s) [attempted 2146/8459 = 25%, 330 KB/s], Decompressed: 1957
Downloaded: 2187 file(s) [attempted 2187/8459 = 25%, 950 KB/s], Decompressed: 2064
Downloaded: 2231 file(s) [attempted 2231/8459 = 26%, 296 KB/s], Decompressed: 2064
Downloaded: 2269 file(s) [attempted 2269/8459 = 26%, 76 KB/s], Decompressed: 2064
Downloaded: 2307 file(s) [attempted 2307/8459 = 27%, 135 KB/s], Decompressed: 2166
Downloaded: 2344 file(s) [attempted 2344/8459 = 27%, 38 KB/s], Decompressed: 2166
Downloaded: 2385 file(s) [attempted 2385/8459 = 28%, 1204 KB/s], Decompressed: 2166
Downloaded: 2427 file(s) [attempted 2427/8459 = 28%, 811 KB/s], Decompressed: 2283
Downloaded: 2468 file(s) [attempted 2468/8459 = 29%, 465 KB/s], Decompressed: 2283
Downloaded: 2512 file(s) [attempted 2512/8459 = 29%, 282 KB/s], Decompressed: 2283
Downloaded: 2560 file(s) [attempted 2560/8459 = 30%, 157 KB/s], Decompressed: 2409
Downloaded: 2598 file(s) [attempted 2598/8459 = 30%, 41 KB/s], Decompressed: 2409
Downloaded: 2635 file(s) [attempted 2635/8459 = 31%, 129 KB/s], Decompressed: 2409
Downloaded: 2676 file(s) [attempted 2676/8459 = 31%, 240 KB/s], Decompressed: 2529
Downloaded: 2714 file(s) [attempted 2714/8459 = 32%, 76 KB/s], Decompressed: 2529
Downloaded: 2755 file(s) [attempted 2755/8459 = 32%, 237 KB/s], Decompressed: 2529
Downloaded: 2800 file(s) [attempted 2800/8459 = 33%, 463 KB/s], Decompressed: 2529
Downloaded: 2838 file(s) [attempted 2838/8459 = 33%, 211 KB/s], Decompressed: 2529
Downloaded: 2875 file(s) [attempted 2875/8459 = 33%, 527 KB/s], Decompressed: 2673
Downloaded: 2920 file(s) [attempted 2920/8459 = 34%, 122 KB/s], Decompressed: 2673
Downloaded: 2961 file(s) [attempted 2961/8459 = 35%, 341 KB/s], Decompressed: 2673
Downloaded: 3002 file(s) [attempted 3002/8459 = 35%, 607 KB/s], Decompressed: 2673
Downloaded: 3040 file(s) [attempted 3040/8459 = 35%, 233 KB/s], Decompressed: 2673
Downloaded: 3081 file(s) [attempted 3081/8459 = 36%, 544 KB/s], Decompressed: 2848
Downloaded: 3122 file(s) [attempted 3122/8459 = 36%, 657 KB/s], Decompressed: 2848
Downloaded: 3166 file(s) [attempted 3166/8459 = 37%, 68 KB/s], Decompressed: 2848
Downloaded: 3204 file(s) [attempted 3204/8459 = 37%, 234 KB/s], Decompressed: 2848
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 254 KB/s], Decompressed: 2848
Downloaded: 3286 file(s) [attempted 3286/8459 = 38%, 435 KB/s], Decompressed: 2848
Downloaded: 3327 file(s) [attempted 3327/8459 = 39%, 172 KB/s], Decompressed: 2848
Downloaded: 3368 file(s) [attempted 3368/8459 = 39%, 316 KB/s], Decompressed: 3070
Downloaded: 3411 file(s) [attempted 3411/8459 = 40%, 171 KB/s], Decompressed: 3070
Downloaded: 3454 file(s) [attempted 3454/8459 = 40%, 236 KB/s], Decompressed: 3070
Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 1913 KB/s], Decompressed: 3070
Downloaded: 3526 file(s) [attempted 3526/8459 = 41%, 159 KB/s], Decompressed: 3070
Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 126 KB/s], Decompressed: 3070
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 40 KB/s], Decompressed: 3070
Downloaded: 3646 file(s) [attempted 3646/8459 = 43%, 248 KB/s], Decompressed: 3070
Downloaded: 3690 file(s) [attempted 3690/8459 = 43%, 57 KB/s], Decompressed: 3070
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 100 KB/s], Decompressed: 3365
Downloaded: 3762 file(s) [attempted 3762/8459 = 44%, 1133 KB/s], Decompressed: 3365
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 70 KB/s], Decompressed: 3365
Downloaded: 3845 file(s) [attempted 3845/8459 = 45%, 739 KB/s], Decompressed: 3365
Downloaded: 3879 file(s) [attempted 3879/8459 = 45%, 569 KB/s], Decompressed: 3365
Downloaded: 3920 file(s) [attempted 3920/8459 = 46%, 80 KB/s], Decompressed: 3365
Downloaded: 3961 file(s) [attempted 3961/8459 = 46%, 123 KB/s], Decompressed: 3365
Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 291 KB/s], Decompressed: 3365
Downloaded: 4006 file(s) [attempted 4006/8459 = 47%, 1038 KB/s], Decompressed: 3365
Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 215 KB/s], Decompressed: 3365
Downloaded: 4088 file(s) [attempted 4088/8459 = 48%, 178 KB/s], Decompressed: 3365
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 116 KB/s], Decompressed: 3365
Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 2017 KB/s], Decompressed: 3365
Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 705 KB/s], Decompressed: 3721
Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 75 KB/s], Decompressed: 3721
Downloaded: 4324 file(s) [attempted 4324/8459 = 51%, 106 KB/s], Decompressed: 3721
Downloaded: 4369 file(s) [attempted 4369/8459 = 51%, 268 KB/s], Decompressed: 3721
Downloaded: 4413 file(s) [attempted 4413/8459 = 52%, 69 KB/s], Decompressed: 3721
Downloaded: 4461 file(s) [attempted 4461/8459 = 52%, 442 KB/s], Decompressed: 3721
Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 80 KB/s], Decompressed: 3721
Downloaded: 4554 file(s) [attempted 4554/8459 = 53%, 463 KB/s], Decompressed: 3721
Downloaded: 4588 file(s) [attempted 4588/8459 = 54%, 610 KB/s], Decompressed: 3721
Downloaded: 4629 file(s) [attempted 4629/8459 = 54%, 100 KB/s], Decompressed: 3721
Downloaded: 4670 file(s) [attempted 4670/8459 = 55%, 686 KB/s], Decompressed: 3721
Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 248 KB/s], Decompressed: 3721
Downloaded: 4745 file(s) [attempted 4745/8459 = 56%, 85 KB/s], Decompressed: 3721
Downloaded: 4787 file(s) [attempted 4787/8459 = 56%, 104 KB/s], Decompressed: 3721
Downloaded: 4824 file(s) [attempted 4824/8459 = 57%, 390 KB/s], Decompressed: 3721
Downloaded: 4865 file(s) [attempted 4865/8459 = 57%, 202 KB/s], Decompressed: 4228
Downloaded: 4903 file(s) [attempted 4903/8459 = 57%, 162 KB/s], Decompressed: 4228
Downloaded: 4930 file(s) [attempted 4930/8459 = 58%, 213 KB/s], Decompressed: 4228
Downloaded: 4972 file(s) [attempted 4972/8459 = 58%, 78 KB/s], Decompressed: 4228
Downloaded: 5013 file(s) [attempted 5013/8459 = 59%, 1456 KB/s], Decompressed: 4228
Downloaded: 5050 file(s) [attempted 5050/8459 = 59%, 5010 KB/s], Decompressed: 4228
Downloaded: 5088 file(s) [attempted 5088/8459 = 60%, 1883 KB/s], Decompressed: 4228
Downloaded: 5122 file(s) [attempted 5122/8459 = 60%, 533 KB/s], Decompressed: 4228
Downloaded: 5160 file(s) [attempted 5160/8459 = 61%, 53 KB/s], Decompressed: 4228
Downloaded: 5198 file(s) [attempted 5198/8459 = 61%, 122 KB/s], Decompressed: 4228
Downloaded: 5239 file(s) [attempted 5239/8459 = 61%, 100 KB/s], Decompressed: 4228
Downloaded: 5276 file(s) [attempted 5276/8459 = 62%, 631 KB/s], Decompressed: 4228
Downloaded: 5314 file(s) [attempted 5314/8459 = 62%, 1223 KB/s], Decompressed: 4228
Downloaded: 5355 file(s) [attempted 5355/8459 = 63%, 175 KB/s], Decompressed: 4228
Downloaded: 5400 file(s) [attempted 5400/8459 = 63%, 85 KB/s], Decompressed: 4228
Downloaded: 5437 file(s) [attempted 5437/8459 = 64%, 136 KB/s], Decompressed: 4228
Downloaded: 5475 file(s) [attempted 5475/8459 = 64%, 149 KB/s], Decompressed: 4228
Downloaded: 5516 file(s) [attempted 5516/8459 = 65%, 1360 KB/s], Decompressed: 4835
Downloaded: 5557 file(s) [attempted 5557/8459 = 65%, 301 KB/s], Decompressed: 4835
Downloaded: 5602 file(s) [attempted 5602/8459 = 66%, 727 KB/s], Decompressed: 4835
Downloaded: 5643 file(s) [attempted 5643/8459 = 66%, 575 KB/s], Decompressed: 4835
Downloaded: 5681 file(s) [attempted 5681/8459 = 67%, 1525 KB/s], Decompressed: 4835
Downloaded: 5722 file(s) [attempted 5722/8459 = 67%, 56 KB/s], Decompressed: 4835
Downloaded: 5759 file(s) [attempted 5759/8459 = 68%, 213 KB/s], Decompressed: 4835
Downloaded: 5807 file(s) [attempted 5807/8459 = 68%, 121 KB/s], Decompressed: 4835
Downloaded: 5852 file(s) [attempted 5852/8459 = 69%, 594 KB/s], Decompressed: 4835
Downloaded: 5893 file(s) [attempted 5893/8459 = 69%, 166 KB/s], Decompressed: 4835
Downloaded: 5927 file(s) [attempted 5927/8459 = 70%, 128 KB/s], Decompressed: 4835
Downloaded: 5965 file(s) [attempted 5965/8459 = 70%, 390 KB/s], Decompressed: 4835
Downloaded: 5999 file(s) [attempted 5999/8459 = 70%, 530 KB/s], Decompressed: 5499
Downloaded: 6047 file(s) [attempted 6047/8459 = 71%, 3 KB/s], Decompressed: 5499
Downloaded: 6049 file(s) [attempted 6049/8459 = 71%, 0 KB/s], Decompressed: 5499
Downloaded: 6051 file(s) [attempted 6051/8459 = 71%, 83 KB/s], Decompressed: 5499
Downloaded: 6052 file(s) [attempted 6052/8459 = 71%, 7 KB/s], Decompressed: 5499
Downloaded: 6053 file(s) [attempted 6053/8459 = 71%, 60 KB/s], Decompressed: 5499
Downloaded: 6054 file(s) [attempted 6054/8459 = 71%, 320 KB/s], Decompressed: 5499
Downloaded: 6055 file(s) [attempted 6055/8459 = 71%, 56 KB/s], Decompressed: 5499
Downloaded: 6056 file(s) [attempted 6056/8459 = 71%, 17 KB/s], Decompressed: 5499
Downloaded: 6057 file(s) [attempted 6057/8459 = 71%, 62 KB/s], Decompressed: 5499
Downloaded: 6058 file(s) [attempted 6058/8459 = 71%, 98 KB/s], Decompressed: 5999
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 38 KB/s], Decompressed: 5999
Downloaded: 6060 file(s) [attempted 6060/8459 = 71%, 26 KB/s], Decompressed: 5999
Downloaded: 6061 file(s) [attempted 6061/8459 = 71%, 24 KB/s], Decompressed: 5999
Downloaded: 6062 file(s) [attempted 6062/8459 = 71%, 28 KB/s], Decompressed: 5999
Downloaded: 6081 file(s) [attempted 6081/8459 = 71%, 27 KB/s], Decompressed: 6058
Downloaded: 6085 file(s) [attempted 6085/8459 = 71%, 54 KB/s], Decompressed: 6064
Downloaded: 6099 file(s) [attempted 6099/8459 = 72%, 29 KB/s], Decompressed: 6082
Downloaded: 6102 file(s) [attempted 6102/8459 = 72%, 41 KB/s], Decompressed: 6099
Downloaded: 6104 file(s) [attempted 6104/8459 = 72%, 6 KB/s], Decompressed: 6099
Downloaded: 6105 file(s) [attempted 6105/8459 = 72%, 0 KB/s], Decompressed: 6099
Downloaded: 6106 file(s) [attempted 6106/8459 = 72%, 1 KB/s], Decompressed: 6102
Downloaded: 6108 file(s) [attempted 6108/8459 = 72%, 19 KB/s], Decompressed: 6102
Downloaded: 6110 file(s) [attempted 6110/8459 = 72%, 6 KB/s], Decompressed: 6102
Downloaded: 6111 file(s) [attempted 6111/8459 = 72%, 1 KB/s], Decompressed: 6102
Downloaded: 6112 file(s) [attempted 6112/8459 = 72%, 3 KB/s], Decompressed: 6106
Downloaded: 6113 file(s) [attempted 6113/8459 = 72%, 4 KB/s], Decompressed: 6106
Downloaded: 6114 file(s) [attempted 6114/8459 = 72%, 11 KB/s], Decompressed: 6112
Downloaded: 6115 file(s) [attempted 6115/8459 = 72%, 2 KB/s], Decompressed: 6112
Downloaded: 6116 file(s) [attempted 6116/8459 = 72%, 14 KB/s], Decompressed: 6112
Downloaded: 6118 file(s) [attempted 6118/8459 = 72%, 3 KB/s], Decompressed: 6114
Downloaded: 6119 file(s) [attempted 6119/8459 = 72%, 1 KB/s], Decompressed: 6114
Downloaded: 6120 file(s) [attempted 6120/8459 = 72%, 5 KB/s], Decompressed: 6118
Downloaded: 6121 file(s) [attempted 6121/8459 = 72%, 6 KB/s], Decompressed: 6118
Downloaded: 6122 file(s) [attempted 6122/8459 = 72%, 2 KB/s], Decompressed: 6118
Downloaded: 6123 file(s) [attempted 6123/8459 = 72%, 12 KB/s], Decompressed: 6120
Downloaded: 6150 file(s) [attempted 6150/8459 = 72%, 41 KB/s], Decompressed: 6123
Downloaded: 6153 file(s) [attempted 6153/8459 = 72%, 20 KB/s], Decompressed: 6150
Downloaded: 6168 file(s) [attempted 6168/8459 = 72%, 5 KB/s], Decompressed: 6165
Downloaded: 6169 file(s) [attempted 6169/8459 = 72%, 1 KB/s], Decompressed: 6165
Downloaded: 6170 file(s) [attempted 6170/8459 = 72%, 0 KB/s], Decompressed: 6168
Downloaded: 6171 file(s) [attempted 6171/8459 = 72%, 3 KB/s], Decompressed: 6168
Downloaded: 6172 file(s) [attempted 6172/8459 = 72%, 1 KB/s], Decompressed: 6168
Downloaded: 6173 file(s) [attempted 6173/8459 = 72%, 3 KB/s], Decompressed: 6170
Downloaded: 6174 file(s) [attempted 6174/8459 = 72%, 2 KB/s], Decompressed: 6170
Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 3 KB/s], Decompressed: 6170
Downloaded: 6176 file(s) [attempted 6176/8459 = 73%, 1 KB/s], Decompressed: 6173
Downloaded: 6177 file(s) [attempted 6177/8459 = 73%, 2 KB/s], Decompressed: 6173
Downloaded: 6178 file(s) [attempted 6178/8459 = 73%, 0 KB/s], Decompressed: 6176
Downloaded: 6179 file(s) [attempted 6179/8459 = 73%, 2 KB/s], Decompressed: 6178
Downloaded: 6180 file(s) [attempted 6180/8459 = 73%, 0 KB/s], Decompressed: 6178
Downloaded: 6181 file(s) [attempted 6181/8459 = 73%, 2 KB/s], Decompressed: 6178
Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 3 KB/s], Decompressed: 6179
Downloaded: 6183 file(s) [attempted 6183/8459 = 73%, 13 KB/s], Decompressed: 6179
Downloaded: 6184 file(s) [attempted 6184/8459 = 73%, 7 KB/s], Decompressed: 6182
Downloaded: 6211 file(s) [attempted 6211/8459 = 73%, 1 KB/s], Decompressed: 6184
Downloaded: 6228 file(s) [attempted 6228/8459 = 73%, 21 KB/s], Decompressed: 6211
Downloaded: 6229 file(s) [attempted 6229/8459 = 73%, 17 KB/s], Decompressed: 6211
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 24 KB/s], Decompressed: 6228
Downloaded: 6231 file(s) [attempted 6231/8459 = 73%, 18 KB/s], Decompressed: 6228
Downloaded: 6232 file(s) [attempted 6232/8459 = 73%, 4 KB/s], Decompressed: 6228
Downloaded: 6233 file(s) [attempted 6233/8459 = 73%, 40 KB/s], Decompressed: 6230
Downloaded: 6234 file(s) [attempted 6234/8459 = 73%, 33 KB/s], Decompressed: 6230
Downloaded: 6236 file(s) [attempted 6236/8459 = 73%, 17 KB/s], Decompressed: 6233
Downloaded: 6237 file(s) [attempted 6237/8459 = 73%, 11 KB/s], Decompressed: 6233
Downloaded: 6238 file(s) [attempted 6238/8459 = 73%, 6 KB/s], Decompressed: 6233
Downloaded: 6239 file(s) [attempted 6239/8459 = 73%, 25 KB/s], Decompressed: 6236
Downloaded: 6240 file(s) [attempted 6240/8459 = 73%, 31 KB/s], Decompressed: 6236
Downloaded: 6241 file(s) [attempted 6241/8459 = 73%, 2 KB/s], Decompressed: 6239
Downloaded: 6242 file(s) [attempted 6242/8459 = 73%, 9 KB/s], Decompressed: 6239
Downloaded: 6243 file(s) [attempted 6243/8459 = 73%, 3 KB/s], Decompressed: 6241
Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 4 KB/s], Decompressed: 6241
Downloaded: 6245 file(s) [attempted 6245/8459 = 73%, 1 KB/s], Decompressed: 6241
Downloaded: 6246 file(s) [attempted 6246/8459 = 73%, 3 KB/s], Decompressed: 6241
Downloaded: 6247 file(s) [attempted 6247/8459 = 73%, 15 KB/s], Decompressed: 6243
Downloaded: 6248 file(s) [attempted 6248/8459 = 73%, 31 KB/s], Decompressed: 6243
Downloaded: 6249 file(s) [attempted 6249/8459 = 73%, 24 KB/s], Decompressed: 6243
Downloaded: 6250 file(s) [attempted 6250/8459 = 73%, 9 KB/s], Decompressed: 6243
Downloaded: 6251 file(s) [attempted 6251/8459 = 73%, 7 KB/s], Decompressed: 6247
Downloaded: 6252 file(s) [attempted 6252/8459 = 73%, 4 KB/s], Decompressed: 6247
Downloaded: 6253 file(s) [attempted 6253/8459 = 73%, 1 KB/s], Decompressed: 6251
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 1 KB/s], Decompressed: 6251
Downloaded: 6255 file(s) [attempted 6255/8459 = 73%, 4 KB/s], Decompressed: 6251
Downloaded: 6257 file(s) [attempted 6257/8459 = 73%, 4 KB/s], Decompressed: 6253
Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 16 KB/s], Decompressed: 6253
Downloaded: 6259 file(s) [attempted 6259/8459 = 73%, 3 KB/s], Decompressed: 6256
Downloaded: 6280 file(s) [attempted 6280/8459 = 74%, 3 KB/s], Decompressed: 6259
Downloaded: 6281 file(s) [attempted 6281/8459 = 74%, 221 KB/s], Decompressed: 6259
Downloaded: 6283 file(s) [attempted 6283/8459 = 74%, 30 KB/s], Decompressed: 6280
Downloaded: 6286 file(s) [attempted 6286/8459 = 74%, 116 KB/s], Decompressed: 6283
Downloaded: 6287 file(s) [attempted 6287/8459 = 74%, 42 KB/s], Decompressed: 6286
Downloaded: 6288 file(s) [attempted 6288/8459 = 74%, 254 KB/s], Decompressed: 6287
Downloaded: 6328 file(s) [attempted 6328/8459 = 74%, 33 KB/s], Decompressed: 6301
Downloaded: 6366 file(s) [attempted 6366/8459 = 75%, 421 KB/s], Decompressed: 6328
Downloaded: 6393 file(s) [attempted 6393/8459 = 75%, 61 KB/s], Decompressed: 6328
Downloaded: 6417 file(s) [attempted 6417/8459 = 75%, 739 KB/s], Decompressed: 6366
Downloaded: 6434 file(s) [attempted 6434/8459 = 76%, 144 KB/s], Decompressed: 6366
Downloaded: 6448 file(s) [attempted 6448/8459 = 76%, 539 KB/s], Decompressed: 6417
Downloaded: 6462 file(s) [attempted 6462/8459 = 76%, 669 KB/s], Decompressed: 6448
Downloaded: 6465 file(s) [attempted 6465/8459 = 76%, 93 KB/s], Decompressed: 6462
Downloaded: 6472 file(s) [attempted 6472/8459 = 76%, 32 KB/s], Decompressed: 6462
Downloaded: 6489 file(s) [attempted 6489/8459 = 76%, 19 KB/s], Decompressed: 6465
Downloaded: 6506 file(s) [attempted 6506/8459 = 76%, 35 KB/s], Decompressed: 6465
Downloaded: 6510 file(s) [attempted 6510/8459 = 76%, 86 KB/s], Decompressed: 6489
Downloaded: 6527 file(s) [attempted 6527/8459 = 77%, 83 KB/s], Decompressed: 6489
Downloaded: 6530 file(s) [attempted 6530/8459 = 77%, 24 KB/s], Decompressed: 6510
Downloaded: 6537 file(s) [attempted 6537/8459 = 77%, 46 KB/s], Decompressed: 6510
Downloaded: 6544 file(s) [attempted 6544/8459 = 77%, 40 KB/s], Decompressed: 6541
Downloaded: 6554 file(s) [attempted 6554/8459 = 77%, 41 KB/s], Decompressed: 6551
Downloaded: 6561 file(s) [attempted 6561/8459 = 77%, 57 KB/s], Decompressed: 6554
Downloaded: 6568 file(s) [attempted 6568/8459 = 77%, 38 KB/s], Decompressed: 6558
Downloaded: 6575 file(s) [attempted 6575/8459 = 77%, 45 KB/s], Decompressed: 6571
Downloaded: 6585 file(s) [attempted 6585/8459 = 77%, 44 KB/s], Decompressed: 6575
Downloaded: 6599 file(s) [attempted 6599/8459 = 78%, 47 KB/s], Decompressed: 6585
Downloaded: 6606 file(s) [attempted 6606/8459 = 78%, 30 KB/s], Decompressed: 6595
Downloaded: 6616 file(s) [attempted 6616/8459 = 78%, 27 KB/s], Decompressed: 6613
Downloaded: 6620 file(s) [attempted 6620/8459 = 78%, 240 KB/s], Decompressed: 6616
Downloaded: 6630 file(s) [attempted 6630/8459 = 78%, 41 KB/s], Decompressed: 6619
Downloaded: 6637 file(s) [attempted 6637/8459 = 78%, 44 KB/s], Decompressed: 6630
Downloaded: 6643 file(s) [attempted 6643/8459 = 78%, 74 KB/s], Decompressed: 6637
Downloaded: 6650 file(s) [attempted 6650/8459 = 78%, 47 KB/s], Decompressed: 6643
Downloaded: 6654 file(s) [attempted 6654/8459 = 78%, 29 KB/s], Decompressed: 6650
Downloaded: 6655 file(s) [attempted 6655/8459 = 78%, 46 KB/s], Decompressed: 6650
Downloaded: 6656 file(s) [attempted 6656/8459 = 78%, 40 KB/s], Decompressed: 6654
Downloaded: 6657 file(s) [attempted 6657/8459 = 78%, 89 KB/s], Decompressed: 6656
Downloaded: 6705 file(s) [attempted 6705/8459 = 79%, 0 KB/s], Decompressed: 6657
Downloaded: 6709 file(s) [attempted 6709/8459 = 79%, 27 KB/s], Decompressed: 6657
Downloaded: 6729 file(s) [attempted 6729/8459 = 79%, 31 KB/s], Decompressed: 6705
Downloaded: 6757 file(s) [attempted 6757/8459 = 79%, 169 KB/s], Decompressed: 6705
Downloaded: 6801 file(s) [attempted 6801/8459 = 80%, 291 KB/s], Decompressed: 6705
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 30 KB/s], Decompressed: 6729
Downloaded: 6894 file(s) [attempted 6894/8459 = 81%, 100 KB/s], Decompressed: 6729
Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 949 KB/s], Decompressed: 6729
Downloaded: 6989 file(s) [attempted 6989/8459 = 82%, 37 KB/s], Decompressed: 6835
Downloaded: 7031 file(s) [attempted 7031/8459 = 83%, 1879 KB/s], Decompressed: 6835
Downloaded: 7075 file(s) [attempted 7075/8459 = 83%, 67 KB/s], Decompressed: 6835
Downloaded: 7116 file(s) [attempted 7116/8459 = 84%, 363 KB/s], Decompressed: 6952
Downloaded: 7150 file(s) [attempted 7150/8459 = 84%, 82 KB/s], Decompressed: 6952
Downloaded: 7192 file(s) [attempted 7192/8459 = 85%, 1181 KB/s], Decompressed: 6952
Downloaded: 7233 file(s) [attempted 7233/8459 = 85%, 1251 KB/s], Decompressed: 7079
Downloaded: 7274 file(s) [attempted 7274/8459 = 85%, 185 KB/s], Decompressed: 7079
Downloaded: 7318 file(s) [attempted 7318/8459 = 86%, 339 KB/s], Decompressed: 7079
Downloaded: 7363 file(s) [attempted 7363/8459 = 87%, 47 KB/s], Decompressed: 7212
Downloaded: 7400 file(s) [attempted 7400/8459 = 87%, 1406 KB/s], Decompressed: 7212
Downloaded: 7442 file(s) [attempted 7442/8459 = 87%, 88 KB/s], Decompressed: 7212
Downloaded: 7476 file(s) [attempted 7476/8459 = 88%, 192 KB/s], Decompressed: 7212
Downloaded: 7520 file(s) [attempted 7520/8459 = 88%, 25 KB/s], Decompressed: 7346
Downloaded: 7565 file(s) [attempted 7565/8459 = 89%, 283 KB/s], Decompressed: 7346
Downloaded: 7606 file(s) [attempted 7606/8459 = 89%, 229 KB/s], Decompressed: 7346
Downloaded: 7640 file(s) [attempted 7640/8459 = 90%, 274 KB/s], Decompressed: 7346
Downloaded: 7678 file(s) [attempted 7678/8459 = 90%, 54 KB/s], Decompressed: 7496
Downloaded: 7722 file(s) [attempted 7722/8459 = 91%, 644 KB/s], Decompressed: 7496
Downloaded: 7764 file(s) [attempted 7764/8459 = 91%, 541 KB/s], Decompressed: 7496
Downloaded: 7802 file(s) [attempted 7802/8459 = 92%, 99 KB/s], Decompressed: 7496
Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 285 KB/s], Decompressed: 7657
Downloaded: 7880 file(s) [attempted 7880/8459 = 93%, 890 KB/s], Decompressed: 7657
Downloaded: 7921 file(s) [attempted 7921/8459 = 93%, 37 KB/s], Decompressed: 7657
Downloaded: 7966 file(s) [attempted 7966/8459 = 94%, 78 KB/s], Decompressed: 7657
Downloaded: 8014 file(s) [attempted 8014/8459 = 94%, 469 KB/s], Decompressed: 7657
Downloaded: 8051 file(s) [attempted 8051/8459 = 95%, 414 KB/s], Decompressed: 7829
Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 376 KB/s], Decompressed: 7829
Downloaded: 8137 file(s) [attempted 8137/8459 = 96%, 316 KB/s], Decompressed: 7829
Downloaded: 8175 file(s) [attempted 8175/8459 = 96%, 56 KB/s], Decompressed: 7829
Downloaded: 8219 file(s) [attempted 8219/8459 = 97%, 83 KB/s], Decompressed: 7829
Downloaded: 8266 file(s) [attempted 8266/8459 = 97%, 47 KB/s], Decompressed: 7829
Downloaded: 8301 file(s) [attempted 8301/8459 = 98%, 66 KB/s], Decompressed: 7829
Downloaded: 8342 file(s) [attempted 8342/8459 = 98%, 829 KB/s], Decompressed: 8048
Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 56 KB/s], Decompressed: 8048
Downloaded: 8425 file(s) [attempted 8425/8459 = 99%, 653 KB/s], Decompressed: 8048
Downloaded: 8455 file(s) [attempted 8455/8459 = 99%, 107 KB/s], Decompressed: 8325
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 13 KB/s], Decompressed: 8325
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 13 KB/s], Decompressed: 8325

apx-runtime-resource-v1	apx-verifier-job-1731-runtime-lake_cache-4011476-1787639010726920297-0	4018176	4018176	21474836480	0	0	0	0	0	0	574349312	2476326912	21474836480	0	0	0	0	0	0

lean_checkerexit -duration 2h 0m · created 8/25/2026, 8:52:02 AM

lake build

✔ [500/502] Built Iut.Foundations.Species (380s)
✔ [501/502] Built Iut.Foundations.SourceGameplanSpeciesMutation (172s)
✔ [784/791] Built Iut.Foundations.RealLineCopy (425s)
✔ [785/791] Built Iut.Foundations.TransportDiagram (154s)
✔ [786/791] Built Iut.Foundations.IndeterminacyRelation (79s)
✔ [787/791] Built Iut.Foundations.RegionMeasure (198s)
✔ [788/791] Built Iut.Foundations.CommonTargetBound (236s)
✔ [789/791] Built Iut.Foundations.TransportedRegionFamily (65s)
✔ [790/791] Built Iut.Foundations.QualitativeData (68s)
✔ [3508/3513] Built Iut.Foundations.EtaleThetaQuotient (538s)
✔ [3509/3513] Built Iut.Foundations.Orbicurve (936s)
✔ [3956/3959] Built Iut.Foundations.InitialThetaData (1170s)
✔ [3962/3966] Built Iut.Foundations.OrbicurvePullback (817s)
✔ [3965/3968] Built Iut.Foundations.EtaleThetaCovers (286s)
✔ [3974/3982] Built Iut.Foundations.SourceTateCurve (438s)
✔ [3981/3986] Built Iut.Foundations.GaloisImage (171s)
✔ [3983/3989] Built Iut.Foundations.SourceAnabelioid (813s)

/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1731-runtime-lean_checker-4011476-1787640705021891485-1 on attempt 1

blueprint_buildexit 1duration 15s · created 8/25/2026, 8:52:02 AM

lake build :blueprint

error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1731-runtime-blueprint_build-4011476-1787647905719450612-2	970752	1486848	21474836480	0	0	0	0	0	0	817074176	920621056	21474836480	0	0	0	0	0	0