Verification run

Run 1258

promachina/iut-leanbranch mastertriggered via github_push

failedcommit 0ba19051b071toolchain lean-v4-30-0prover leantook 2h 27m · 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-1698-source
exit_code=Some(128) duration_ms=369
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1698-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=4246
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1698-source'...


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

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 0ba1905 E21.7: construct extended Tate parameter family (#933)

Resolved source revision: 0ba19051b07134332fac96744a4abfe7c46a3059

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=0ba19051b07134332fac96744a4abfe7c46a3059 provenance={"branch":"master","checked_out_revision":"0ba19051b07134332fac96744a4abfe7c46a3059","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"github_installation","local_clone":false,"requested_commit_sha":"0ba19051b07134332fac96744a4abfe7c46a3059","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=5562 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=1602002
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.3s)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (1.3s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (124ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (157ms)
✔ [13/25] Built Cache.Lean:c.o (128ms)
✔ [15/25] Built Cache.Init (324ms)
✔ [16/25] Built Cache.IO (2.5s)
✔ [17/25] Built Cache.Init:c.o (96ms)
✔ [18/25] Built Cache.IO:c.o (1.1s)
✔ [19/25] Built Cache.Hashing (1.1s)
✔ [20/25] Built Cache.Hashing:c.o (504ms)
✔ [21/25] Built Cache.Requests (45s)
✔ [22/25] Built Cache.Requests:c.o (2.8s)
✔ [23/25] Built Cache.Main (1.1s)
✔ [24/25] Built Cache.Main:c.o (525ms)
✔ [25/25] Built cache:exe (5.2s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 13 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 3 KB/s], Decompressed: 7
Downloaded: 34 file(s) [attempted 34/8459 = 0%, 20 KB/s], Decompressed: 23
Downloaded: 59 file(s) [attempted 59/8459 = 0%, 53 KB/s], Decompressed: 32
Downloaded: 83 file(s) [attempted 83/8459 = 0%, 158 KB/s], Decompressed: 49
Downloaded: 117 file(s) [attempted 117/8459 = 1%, 138 KB/s], Decompressed: 68
Downloaded: 148 file(s) [attempted 148/8459 = 1%, 483 KB/s], Decompressed: 93
Downloaded: 182 file(s) [attempted 182/8459 = 2%, 420 KB/s], Decompressed: 127
Downloaded: 213 file(s) [attempted 213/8459 = 2%, 202 KB/s], Decompressed: 169
Downloaded: 244 file(s) [attempted 244/8459 = 2%, 293 KB/s], Decompressed: 169
Downloaded: 282 file(s) [attempted 282/8459 = 3%, 70 KB/s], Decompressed: 213
Downloaded: 323 file(s) [attempted 323/8459 = 3%, 105 KB/s], Decompressed: 254
Downloaded: 361 file(s) [attempted 361/8459 = 4%, 157 KB/s], Decompressed: 302
Downloaded: 398 file(s) [attempted 398/8459 = 4%, 207 KB/s], Decompressed: 302
Downloaded: 433 file(s) [attempted 433/8459 = 5%, 264 KB/s], Decompressed: 357
Downloaded: 474 file(s) [attempted 474/8459 = 5%, 729 KB/s], Decompressed: 412
Downloaded: 515 file(s) [attempted 515/8459 = 6%, 297 KB/s], Decompressed: 412
Downloaded: 556 file(s) [attempted 556/8459 = 6%, 247 KB/s], Decompressed: 470
Downloaded: 594 file(s) [attempted 594/8459 = 7%, 863 KB/s], Decompressed: 525
Downloaded: 631 file(s) [attempted 631/8459 = 7%, 726 KB/s], Decompressed: 525
Downloaded: 673 file(s) [attempted 673/8459 = 7%, 313 KB/s], Decompressed: 590
Downloaded: 710 file(s) [attempted 710/8459 = 8%, 295 KB/s], Decompressed: 590
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 210 KB/s], Decompressed: 652
Downloaded: 793 file(s) [attempted 793/8459 = 9%, 298 KB/s], Decompressed: 652
Downloaded: 830 file(s) [attempted 830/8459 = 9%, 353 KB/s], Decompressed: 717
Downloaded: 871 file(s) [attempted 871/8459 = 10%, 42 KB/s], Decompressed: 717
Downloaded: 916 file(s) [attempted 916/8459 = 10%, 886 KB/s], Decompressed: 717
Downloaded: 950 file(s) [attempted 950/8459 = 11%, 857 KB/s], Decompressed: 810
Downloaded: 988 file(s) [attempted 988/8459 = 11%, 249 KB/s], Decompressed: 810
Downloaded: 1033 file(s) [attempted 1033/8459 = 12%, 1911 KB/s], Decompressed: 919
Downloaded: 1070 file(s) [attempted 1070/8459 = 12%, 216 KB/s], Decompressed: 919
Downloaded: 1111 file(s) [attempted 1111/8459 = 13%, 178 KB/s], Decompressed: 919
Downloaded: 1152 file(s) [attempted 1152/8459 = 13%, 104 KB/s], Decompressed: 1029
Downloaded: 1193 file(s) [attempted 1193/8459 = 14%, 58 KB/s], Decompressed: 1029
Downloaded: 1231 file(s) [attempted 1231/8459 = 14%, 271 KB/s], Decompressed: 1128
Downloaded: 1272 file(s) [attempted 1272/8459 = 15%, 358 KB/s], Decompressed: 1128
Downloaded: 1310 file(s) [attempted 1310/8459 = 15%, 654 KB/s], Decompressed: 1128
Downloaded: 1354 file(s) [attempted 1354/8459 = 16%, 50 KB/s], Decompressed: 1224
Downloaded: 1396 file(s) [attempted 1396/8459 = 16%, 210 KB/s], Decompressed: 1224
Downloaded: 1430 file(s) [attempted 1430/8459 = 16%, 29 KB/s], Decompressed: 1324
Downloaded: 1471 file(s) [attempted 1471/8459 = 17%, 198 KB/s], Decompressed: 1324
Downloaded: 1512 file(s) [attempted 1512/8459 = 17%, 23 KB/s], Decompressed: 1416
Downloaded: 1557 file(s) [attempted 1557/8459 = 18%, 244 KB/s], Decompressed: 1416
Downloaded: 1598 file(s) [attempted 1598/8459 = 18%, 383 KB/s], Decompressed: 1495
Downloaded: 1632 file(s) [attempted 1632/8459 = 19%, 1069 KB/s], Decompressed: 1563
Downloaded: 1676 file(s) [attempted 1676/8459 = 19%, 976 KB/s], Decompressed: 1563
Downloaded: 1714 file(s) [attempted 1714/8459 = 20%, 166 KB/s], Decompressed: 1628
Downloaded: 1752 file(s) [attempted 1752/8459 = 20%, 678 KB/s], Decompressed: 1694
Downloaded: 1796 file(s) [attempted 1796/8459 = 21%, 222 KB/s], Decompressed: 1694
Downloaded: 1831 file(s) [attempted 1831/8459 = 21%, 138 KB/s], Decompressed: 1748
Downloaded: 1868 file(s) [attempted 1868/8459 = 22%, 83 KB/s], Decompressed: 1800
Downloaded: 1903 file(s) [attempted 1903/8459 = 22%, 552 KB/s], Decompressed: 1848
Downloaded: 1947 file(s) [attempted 1947/8459 = 23%, 457 KB/s], Decompressed: 1896
Downloaded: 1995 file(s) [attempted 1995/8459 = 23%, 131 KB/s], Decompressed: 1896
Downloaded: 2036 file(s) [attempted 2036/8459 = 24%, 462 KB/s], Decompressed: 1947
Downloaded: 2077 file(s) [attempted 2077/8459 = 24%, 244 KB/s], Decompressed: 1999
Downloaded: 2112 file(s) [attempted 2112/8459 = 24%, 81 KB/s], Decompressed: 1999
Downloaded: 2156 file(s) [attempted 2156/8459 = 25%, 520 KB/s], Decompressed: 1999
Downloaded: 2197 file(s) [attempted 2197/8459 = 25%, 386 KB/s], Decompressed: 2071
Downloaded: 2238 file(s) [attempted 2238/8459 = 26%, 701 KB/s], Decompressed: 2071
Downloaded: 2279 file(s) [attempted 2279/8459 = 26%, 198 KB/s], Decompressed: 2160
Downloaded: 2317 file(s) [attempted 2317/8459 = 27%, 108 KB/s], Decompressed: 2160
Downloaded: 2358 file(s) [attempted 2358/8459 = 27%, 286 KB/s], Decompressed: 2245
Downloaded: 2396 file(s) [attempted 2396/8459 = 28%, 301 KB/s], Decompressed: 2245
Downloaded: 2437 file(s) [attempted 2437/8459 = 28%, 416 KB/s], Decompressed: 2321
Downloaded: 2471 file(s) [attempted 2471/8459 = 29%, 110 KB/s], Decompressed: 2321
Downloaded: 2512 file(s) [attempted 2512/8459 = 29%, 652 KB/s], Decompressed: 2403
Downloaded: 2554 file(s) [attempted 2554/8459 = 30%, 216 KB/s], Decompressed: 2403
Downloaded: 2581 file(s) [attempted 2581/8459 = 30%, 61 KB/s], Decompressed: 2482
Downloaded: 2625 file(s) [attempted 2625/8459 = 31%, 333 KB/s], Decompressed: 2482
Downloaded: 2670 file(s) [attempted 2670/8459 = 31%, 370 KB/s], Decompressed: 2560
Downloaded: 2715 file(s) [attempted 2715/8459 = 32%, 122 KB/s], Decompressed: 2560
Downloaded: 2756 file(s) [attempted 2756/8459 = 32%, 225 KB/s], Decompressed: 2629
Downloaded: 2790 file(s) [attempted 2790/8459 = 32%, 522 KB/s], Decompressed: 2629
Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 39 KB/s], Decompressed: 2722
Downloaded: 2869 file(s) [attempted 2869/8459 = 33%, 1044 KB/s], Decompressed: 2722
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 691 KB/s], Decompressed: 2722
Downloaded: 2961 file(s) [attempted 2961/8459 = 35%, 303 KB/s], Decompressed: 2821
Downloaded: 2992 file(s) [attempted 2992/8459 = 35%, 194 KB/s], Decompressed: 2821
Downloaded: 3033 file(s) [attempted 3033/8459 = 35%, 159 KB/s], Decompressed: 2927
Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 356 KB/s], Decompressed: 2927
Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 159 KB/s], Decompressed: 3026
Downloaded: 3164 file(s) [attempted 3164/8459 = 37%, 321 KB/s], Decompressed: 3026
Downloaded: 3205 file(s) [attempted 3205/8459 = 37%, 260 KB/s], Decompressed: 3026
Downloaded: 3246 file(s) [attempted 3246/8459 = 38%, 44 KB/s], Decompressed: 3119
Downloaded: 3283 file(s) [attempted 3283/8459 = 38%, 91 KB/s], Decompressed: 3119
Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 313 KB/s], Decompressed: 3218
Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 469 KB/s], Decompressed: 3218
Downloaded: 3403 file(s) [attempted 3403/8459 = 40%, 125 KB/s], Decompressed: 3218
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 302 KB/s], Decompressed: 3311
Downloaded: 3482 file(s) [attempted 3482/8459 = 41%, 166 KB/s], Decompressed: 3311
Downloaded: 3523 file(s) [attempted 3523/8459 = 41%, 183 KB/s], Decompressed: 3407
Downloaded: 3561 file(s) [attempted 3561/8459 = 42%, 425 KB/s], Decompressed: 3407
Downloaded: 3602 file(s) [attempted 3602/8459 = 42%, 103 KB/s], Decompressed: 3407
Downloaded: 3647 file(s) [attempted 3647/8459 = 43%, 316 KB/s], Decompressed: 3513
Downloaded: 3688 file(s) [attempted 3688/8459 = 43%, 555 KB/s], Decompressed: 3513
Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 161 KB/s], Decompressed: 3619
Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 633 KB/s], Decompressed: 3619
Downloaded: 3811 file(s) [attempted 3811/8459 = 45%, 126 KB/s], Decompressed: 3619
Downloaded: 3849 file(s) [attempted 3849/8459 = 45%, 708 KB/s], Decompressed: 3715
Downloaded: 3886 file(s) [attempted 3886/8459 = 45%, 216 KB/s], Decompressed: 3715
Downloaded: 3927 file(s) [attempted 3927/8459 = 46%, 151 KB/s], Decompressed: 3814
Downloaded: 3969 file(s) [attempted 3969/8459 = 46%, 186 KB/s], Decompressed: 3814
Downloaded: 4010 file(s) [attempted 4010/8459 = 47%, 303 KB/s], Decompressed: 3907
Downloaded: 4047 file(s) [attempted 4047/8459 = 47%, 603 KB/s], Decompressed: 3907
Downloaded: 4092 file(s) [attempted 4092/8459 = 48%, 1252 KB/s], Decompressed: 3999
Downloaded: 4136 file(s) [attempted 4136/8459 = 48%, 140 KB/s], Decompressed: 3999
Downloaded: 4177 file(s) [attempted 4177/8459 = 49%, 803 KB/s], Decompressed: 3999
Downloaded: 4219 file(s) [attempted 4219/8459 = 49%, 317 KB/s], Decompressed: 4092
Downloaded: 4253 file(s) [attempted 4253/8459 = 50%, 888 KB/s], Decompressed: 4092
Downloaded: 4294 file(s) [attempted 4294/8459 = 50%, 1021 KB/s], Decompressed: 4188
Downloaded: 4338 file(s) [attempted 4338/8459 = 51%, 70 KB/s], Decompressed: 4188
Downloaded: 4386 file(s) [attempted 4386/8459 = 51%, 1341 KB/s], Decompressed: 4287
Downloaded: 4431 file(s) [attempted 4431/8459 = 52%, 114 KB/s], Decompressed: 4287
Downloaded: 4469 file(s) [attempted 4469/8459 = 52%, 328 KB/s], Decompressed: 4287
Downloaded: 4503 file(s) [attempted 4503/8459 = 53%, 861 KB/s], Decompressed: 4386
Downloaded: 4541 file(s) [attempted 4541/8459 = 53%, 21 KB/s], Decompressed: 4386
Downloaded: 4589 file(s) [attempted 4589/8459 = 54%, 4245 KB/s], Decompressed: 4482
Downloaded: 4636 file(s) [attempted 4636/8459 = 54%, 133 KB/s], Decompressed: 4482
Downloaded: 4681 file(s) [attempted 4681/8459 = 55%, 433 KB/s], Decompressed: 4482
Downloaded: 4712 file(s) [attempted 4712/8459 = 55%, 326 KB/s], Decompressed: 4482
Downloaded: 4753 file(s) [attempted 4753/8459 = 56%, 106 KB/s], Decompressed: 4568
Downloaded: 4787 file(s) [attempted 4787/8459 = 56%, 355 KB/s], Decompressed: 4568
Downloaded: 4828 file(s) [attempted 4828/8459 = 57%, 376 KB/s], Decompressed: 4568
Downloaded: 4869 file(s) [attempted 4869/8459 = 57%, 4 KB/s], Decompressed: 4568
Downloaded: 4910 file(s) [attempted 4910/8459 = 58%, 271 KB/s], Decompressed: 4722
Downloaded: 4948 file(s) [attempted 4948/8459 = 58%, 360 KB/s], Decompressed: 4722
Downloaded: 4989 file(s) [attempted 4989/8459 = 58%, 328 KB/s], Decompressed: 4722
Downloaded: 5030 file(s) [attempted 5030/8459 = 59%, 61 KB/s], Decompressed: 4722
Downloaded: 5071 file(s) [attempted 5071/8459 = 59%, 94 KB/s], Decompressed: 4722
Downloaded: 5109 file(s) [attempted 5109/8459 = 60%, 153 KB/s], Decompressed: 4893
Downloaded: 5150 file(s) [attempted 5150/8459 = 60%, 465 KB/s], Decompressed: 4893
Downloaded: 5195 file(s) [attempted 5195/8459 = 61%, 131 KB/s], Decompressed: 4893
Downloaded: 5236 file(s) [attempted 5236/8459 = 61%, 90 KB/s], Decompressed: 4893
Downloaded: 5274 file(s) [attempted 5274/8459 = 62%, 424 KB/s], Decompressed: 4893
Downloaded: 5315 file(s) [attempted 5315/8459 = 62%, 147 KB/s], Decompressed: 4893
Downloaded: 5352 file(s) [attempted 5352/8459 = 63%, 650 KB/s], Decompressed: 5106
Downloaded: 5397 file(s) [attempted 5397/8459 = 63%, 183 KB/s], Decompressed: 5106
Downloaded: 5432 file(s) [attempted 5432/8459 = 64%, 143 KB/s], Decompressed: 5106
Downloaded: 5472 file(s) [attempted 5472/8459 = 64%, 1033 KB/s], Decompressed: 5106
Downloaded: 5513 file(s) [attempted 5513/8459 = 65%, 114 KB/s], Decompressed: 5106
Downloaded: 5554 file(s) [attempted 5554/8459 = 65%, 1193 KB/s], Decompressed: 5106
Downloaded: 5599 file(s) [attempted 5599/8459 = 66%, 165 KB/s], Decompressed: 5349
Downloaded: 5637 file(s) [attempted 5637/8459 = 66%, 33 KB/s], Decompressed: 5349
Downloaded: 5674 file(s) [attempted 5674/8459 = 67%, 68 KB/s], Decompressed: 5349
Downloaded: 5715 file(s) [attempted 5715/8459 = 67%, 693 KB/s], Decompressed: 5349
Downloaded: 5753 file(s) [attempted 5753/8459 = 68%, 60 KB/s], Decompressed: 5349
Downloaded: 5798 file(s) [attempted 5798/8459 = 68%, 40 KB/s], Decompressed: 5349
Downloaded: 5842 file(s) [attempted 5842/8459 = 69%, 56 KB/s], Decompressed: 5575
Downloaded: 5883 file(s) [attempted 5883/8459 = 69%, 47 KB/s], Decompressed: 5575
Downloaded: 5921 file(s) [attempted 5921/8459 = 69%, 592 KB/s], Decompressed: 5575
Downloaded: 5962 file(s) [attempted 5962/8459 = 70%, 938 KB/s], Decompressed: 5575
Downloaded: 6003 file(s) [attempted 6003/8459 = 70%, 174 KB/s], Decompressed: 5575
Downloaded: 6041 file(s) [attempted 6041/8459 = 71%, 223 KB/s], Decompressed: 5804
Downloaded: 6085 file(s) [attempted 6085/8459 = 71%, 143 KB/s], Decompressed: 5804
Downloaded: 6117 file(s) [attempted 6117/8459 = 72%, 296 KB/s], Decompressed: 5804
Downloaded: 6161 file(s) [attempted 6161/8459 = 72%, 40 KB/s], Decompressed: 5804
Downloaded: 6198 file(s) [attempted 6198/8459 = 73%, 421 KB/s], Decompressed: 5804
Downloaded: 6239 file(s) [attempted 6239/8459 = 73%, 51 KB/s], Decompressed: 5804
Downloaded: 6284 file(s) [attempted 6284/8459 = 74%, 48 KB/s], Decompressed: 6013
Downloaded: 6325 file(s) [attempted 6325/8459 = 74%, 79 KB/s], Decompressed: 6013
Downloaded: 6363 file(s) [attempted 6363/8459 = 75%, 338 KB/s], Decompressed: 6013
Downloaded: 6400 file(s) [attempted 6400/8459 = 75%, 123 KB/s], Decompressed: 6013
Downloaded: 6445 file(s) [attempted 6445/8459 = 76%, 653 KB/s], Decompressed: 6013
Downloaded: 6486 file(s) [attempted 6486/8459 = 76%, 299 KB/s], Decompressed: 6013
Downloaded: 6527 file(s) [attempted 6527/8459 = 77%, 438 KB/s], Decompressed: 6013
Downloaded: 6568 file(s) [attempted 6568/8459 = 77%, 593 KB/s], Decompressed: 6013
Downloaded: 6603 file(s) [attempted 6603/8459 = 78%, 660 KB/s], Decompressed: 6263
Downloaded: 6644 file(s) [attempted 6644/8459 = 78%, 469 KB/s], Decompressed: 6263
Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 78 KB/s], Decompressed: 6263
Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 122 KB/s], Decompressed: 6263
Downloaded: 6764 file(s) [attempted 6764/8459 = 79%, 490 KB/s], Decompressed: 6263
Downloaded: 6805 file(s) [attempted 6805/8459 = 80%, 232 KB/s], Decompressed: 6263
Downloaded: 6845 file(s) [attempted 6845/8459 = 80%, 375 KB/s], Decompressed: 6263
Downloaded: 6881 file(s) [attempted 6881/8459 = 81%, 218 KB/s], Decompressed: 6263
Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 171 KB/s], Decompressed: 6263
Downloaded: 6962 file(s) [attempted 6962/8459 = 82%, 118 KB/s], Decompressed: 6592
Downloaded: 7003 file(s) [attempted 7003/8459 = 82%, 116 KB/s], Decompressed: 6592
Downloaded: 7038 file(s) [attempted 7038/8459 = 83%, 898 KB/s], Decompressed: 6592
Downloaded: 7075 file(s) [attempted 7075/8459 = 83%, 244 KB/s], Decompressed: 6592
Downloaded: 7123 file(s) [attempted 7123/8459 = 84%, 23 KB/s], Decompressed: 6592
Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 37 KB/s], Decompressed: 6592
Downloaded: 7188 file(s) [attempted 7188/8459 = 84%, 136 KB/s], Decompressed: 6592
Downloaded: 7236 file(s) [attempted 7236/8459 = 85%, 41 KB/s], Decompressed: 6592
Downloaded: 7288 file(s) [attempted 7288/8459 = 86%, 38 KB/s], Decompressed: 6592
Downloaded: 7339 file(s) [attempted 7339/8459 = 86%, 83 KB/s], Decompressed: 6592
Downloaded: 7387 file(s) [attempted 7387/8459 = 87%, 65 KB/s], Decompressed: 6592
Downloaded: 7438 file(s) [attempted 7438/8459 = 87%, 7 KB/s], Decompressed: 6592
Downloaded: 7486 file(s) [attempted 7486/8459 = 88%, 31 KB/s], Decompressed: 6592
Downloaded: 7538 file(s) [attempted 7538/8459 = 89%, 115 KB/s], Decompressed: 6952
Downloaded: 7586 file(s) [attempted 7586/8459 = 89%, 151 KB/s], Decompressed: 6952
Downloaded: 7637 file(s) [attempted 7637/8459 = 90%, 73 KB/s], Decompressed: 6952
Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 49 KB/s], Decompressed: 6952
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 25 KB/s], Decompressed: 6952
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 110 KB/s], Decompressed: 6952
Downloaded: 7836 file(s) [attempted 7836/8459 = 92%, 1431 KB/s], Decompressed: 6952
Downloaded: 7884 file(s) [attempted 7884/8459 = 93%, 85 KB/s], Decompressed: 6952
Downloaded: 7932 file(s) [attempted 7932/8459 = 93%, 208 KB/s], Decompressed: 6952
Downloaded: 7973 file(s) [attempted 7973/8459 = 94%, 368 KB/s], Decompressed: 6952
Downloaded: 8010 file(s) [attempted 8010/8459 = 94%, 276 KB/s], Decompressed: 6952
Downloaded: 8052 file(s) [attempted 8052/8459 = 95%, 101 KB/s], Decompressed: 6952
Downloaded: 8089 file(s) [attempted 8089/8459 = 95%, 374 KB/s], Decompressed: 7534
Downloaded: 8134 file(s) [attempted 8134/8459 = 96%, 104 KB/s], Decompressed: 7534
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 1088 KB/s], Decompressed: 7534
Downloaded: 8216 file(s) [attempted 8216/8459 = 97%, 101 KB/s], Decompressed: 7534
Downloaded: 8257 file(s) [attempted 8257/8459 = 97%, 1158 KB/s], Decompressed: 7534
Downloaded: 8298 file(s) [attempted 8298/8459 = 98%, 590 KB/s], Decompressed: 7534
Downloaded: 8336 file(s) [attempted 8336/8459 = 98%, 80 KB/s], Decompressed: 7534
Downloaded: 8374 file(s) [attempted 8374/8459 = 98%, 93 KB/s], Decompressed: 7534
Downloaded: 8418 file(s) [attempted 8418/8459 = 99%, 72 KB/s], Decompressed: 7534
Downloaded: 8456 file(s) [attempted 8456/8459 = 99%, 795 KB/s], Decompressed: 7534
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 95 KB/s], Decompressed: 7534
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 95 KB/s], Decompressed: 7534

apx-runtime-resource-v1	apx-verifier-job-1698-runtime-lake_cache-3367592-1787240071523533169-0	4055040	4308992	21474836480	0	0	0	0	0	0	591589376	4560195584	21474836480	0	0	0	0	0	0


$ lake build
exit_code=None duration_ms=7202830
stdout:
✔ [500/502] Built Iut.Foundations.Species (167s)
✔ [501/506] Built Iut.Foundations.SourceGameplanSpeciesMutation (79s)
✔ [784/791] Built Iut.Foundations.RealLineCopy (226s)
✔ [785/791] Built Iut.Foundations.TransportDiagram (141s)
✔ [786/791] Built Iut.Foundations.IndeterminacyRelation (111s)
✔ [787/791] Built Iut.Foundations.RegionMeasure (172s)
✔ [788/791] Built Iut.Foundations.CommonTargetBound (142s)
✔ [789/791] Built Iut.Foundations.TransportedRegionFamily (105s)
✔ [790/794] Built Iut.Foundations.QualitativeData (82s)
✔ [3508/3513] Built Iut.Foundations.EtaleThetaQuotient (348s)
✔ [3509/3513] Built Iut.Foundations.Orbicurve (1114s)
✔ [3956/3959] Built Iut.Foundations.InitialThetaData (1217s)
✔ [3963/3966] Built Iut.Foundations.OrbicurvePullback (1049s)
✔ [3965/3968] Built Iut.Foundations.EtaleThetaCovers (465s)
✔ [3975/3984] Built Iut.Foundations.SourceTateCurve (391s)
✔ [3981/3986] Built Iut.Foundations.GaloisImage (448s)

stderr:
/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1698-runtime-lean_checker-3367592-1787241673531943491-1 on attempt 1

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

apx-runtime-resource-v1	apx-verifier-job-1698-runtime-blueprint_build-3367592-1787248903209917815-2	847872	1359872	21474836480	0	0	0	0	0	0	881848320	979959808	21474836480	0	0	0	0	0	0


blueprint_build failed; continuing (non-fatal phase).

Command runs

git_cloneexit 128duration 369 ms · created 8/20/2026, 6:02:06 PM

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

Cloning into '/var/lib/apodeixis/repos/job-1698-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/20/2026, 6:02:06 PM

git clone (github installation auth fallback)

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

git_checkoutexit 0duration 275 ms · created 8/20/2026, 6:02:06 PM

git checkout 0ba19051b07134332fac96744a4abfe7c46a3059

Note: switching to '0ba19051b07134332fac96744a4abfe7c46a3059'.

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 0ba1905 E21.7: construct extended Tate parameter family (#933)

lake_cacheexit 0duration 26m 42s · created 8/20/2026, 6:02:06 PM

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.3s)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (1.3s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (124ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (157ms)
✔ [13/25] Built Cache.Lean:c.o (128ms)
✔ [15/25] Built Cache.Init (324ms)
✔ [16/25] Built Cache.IO (2.5s)
✔ [17/25] Built Cache.Init:c.o (96ms)
✔ [18/25] Built Cache.IO:c.o (1.1s)
✔ [19/25] Built Cache.Hashing (1.1s)
✔ [20/25] Built Cache.Hashing:c.o (504ms)
✔ [21/25] Built Cache.Requests (45s)
✔ [22/25] Built Cache.Requests:c.o (2.8s)
✔ [23/25] Built Cache.Main (1.1s)
✔ [24/25] Built Cache.Main:c.o (525ms)
✔ [25/25] Built cache:exe (5.2s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 13 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 3 KB/s], Decompressed: 7
Downloaded: 34 file(s) [attempted 34/8459 = 0%, 20 KB/s], Decompressed: 23
Downloaded: 59 file(s) [attempted 59/8459 = 0%, 53 KB/s], Decompressed: 32
Downloaded: 83 file(s) [attempted 83/8459 = 0%, 158 KB/s], Decompressed: 49
Downloaded: 117 file(s) [attempted 117/8459 = 1%, 138 KB/s], Decompressed: 68
Downloaded: 148 file(s) [attempted 148/8459 = 1%, 483 KB/s], Decompressed: 93
Downloaded: 182 file(s) [attempted 182/8459 = 2%, 420 KB/s], Decompressed: 127
Downloaded: 213 file(s) [attempted 213/8459 = 2%, 202 KB/s], Decompressed: 169
Downloaded: 244 file(s) [attempted 244/8459 = 2%, 293 KB/s], Decompressed: 169
Downloaded: 282 file(s) [attempted 282/8459 = 3%, 70 KB/s], Decompressed: 213
Downloaded: 323 file(s) [attempted 323/8459 = 3%, 105 KB/s], Decompressed: 254
Downloaded: 361 file(s) [attempted 361/8459 = 4%, 157 KB/s], Decompressed: 302
Downloaded: 398 file(s) [attempted 398/8459 = 4%, 207 KB/s], Decompressed: 302
Downloaded: 433 file(s) [attempted 433/8459 = 5%, 264 KB/s], Decompressed: 357
Downloaded: 474 file(s) [attempted 474/8459 = 5%, 729 KB/s], Decompressed: 412
Downloaded: 515 file(s) [attempted 515/8459 = 6%, 297 KB/s], Decompressed: 412
Downloaded: 556 file(s) [attempted 556/8459 = 6%, 247 KB/s], Decompressed: 470
Downloaded: 594 file(s) [attempted 594/8459 = 7%, 863 KB/s], Decompressed: 525
Downloaded: 631 file(s) [attempted 631/8459 = 7%, 726 KB/s], Decompressed: 525
Downloaded: 673 file(s) [attempted 673/8459 = 7%, 313 KB/s], Decompressed: 590
Downloaded: 710 file(s) [attempted 710/8459 = 8%, 295 KB/s], Decompressed: 590
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 210 KB/s], Decompressed: 652
Downloaded: 793 file(s) [attempted 793/8459 = 9%, 298 KB/s], Decompressed: 652
Downloaded: 830 file(s) [attempted 830/8459 = 9%, 353 KB/s], Decompressed: 717
Downloaded: 871 file(s) [attempted 871/8459 = 10%, 42 KB/s], Decompressed: 717
Downloaded: 916 file(s) [attempted 916/8459 = 10%, 886 KB/s], Decompressed: 717
Downloaded: 950 file(s) [attempted 950/8459 = 11%, 857 KB/s], Decompressed: 810
Downloaded: 988 file(s) [attempted 988/8459 = 11%, 249 KB/s], Decompressed: 810
Downloaded: 1033 file(s) [attempted 1033/8459 = 12%, 1911 KB/s], Decompressed: 919
Downloaded: 1070 file(s) [attempted 1070/8459 = 12%, 216 KB/s], Decompressed: 919
Downloaded: 1111 file(s) [attempted 1111/8459 = 13%, 178 KB/s], Decompressed: 919
Downloaded: 1152 file(s) [attempted 1152/8459 = 13%, 104 KB/s], Decompressed: 1029
Downloaded: 1193 file(s) [attempted 1193/8459 = 14%, 58 KB/s], Decompressed: 1029
Downloaded: 1231 file(s) [attempted 1231/8459 = 14%, 271 KB/s], Decompressed: 1128
Downloaded: 1272 file(s) [attempted 1272/8459 = 15%, 358 KB/s], Decompressed: 1128
Downloaded: 1310 file(s) [attempted 1310/8459 = 15%, 654 KB/s], Decompressed: 1128
Downloaded: 1354 file(s) [attempted 1354/8459 = 16%, 50 KB/s], Decompressed: 1224
Downloaded: 1396 file(s) [attempted 1396/8459 = 16%, 210 KB/s], Decompressed: 1224
Downloaded: 1430 file(s) [attempted 1430/8459 = 16%, 29 KB/s], Decompressed: 1324
Downloaded: 1471 file(s) [attempted 1471/8459 = 17%, 198 KB/s], Decompressed: 1324
Downloaded: 1512 file(s) [attempted 1512/8459 = 17%, 23 KB/s], Decompressed: 1416
Downloaded: 1557 file(s) [attempted 1557/8459 = 18%, 244 KB/s], Decompressed: 1416
Downloaded: 1598 file(s) [attempted 1598/8459 = 18%, 383 KB/s], Decompressed: 1495
Downloaded: 1632 file(s) [attempted 1632/8459 = 19%, 1069 KB/s], Decompressed: 1563
Downloaded: 1676 file(s) [attempted 1676/8459 = 19%, 976 KB/s], Decompressed: 1563
Downloaded: 1714 file(s) [attempted 1714/8459 = 20%, 166 KB/s], Decompressed: 1628
Downloaded: 1752 file(s) [attempted 1752/8459 = 20%, 678 KB/s], Decompressed: 1694
Downloaded: 1796 file(s) [attempted 1796/8459 = 21%, 222 KB/s], Decompressed: 1694
Downloaded: 1831 file(s) [attempted 1831/8459 = 21%, 138 KB/s], Decompressed: 1748
Downloaded: 1868 file(s) [attempted 1868/8459 = 22%, 83 KB/s], Decompressed: 1800
Downloaded: 1903 file(s) [attempted 1903/8459 = 22%, 552 KB/s], Decompressed: 1848
Downloaded: 1947 file(s) [attempted 1947/8459 = 23%, 457 KB/s], Decompressed: 1896
Downloaded: 1995 file(s) [attempted 1995/8459 = 23%, 131 KB/s], Decompressed: 1896
Downloaded: 2036 file(s) [attempted 2036/8459 = 24%, 462 KB/s], Decompressed: 1947
Downloaded: 2077 file(s) [attempted 2077/8459 = 24%, 244 KB/s], Decompressed: 1999
Downloaded: 2112 file(s) [attempted 2112/8459 = 24%, 81 KB/s], Decompressed: 1999
Downloaded: 2156 file(s) [attempted 2156/8459 = 25%, 520 KB/s], Decompressed: 1999
Downloaded: 2197 file(s) [attempted 2197/8459 = 25%, 386 KB/s], Decompressed: 2071
Downloaded: 2238 file(s) [attempted 2238/8459 = 26%, 701 KB/s], Decompressed: 2071
Downloaded: 2279 file(s) [attempted 2279/8459 = 26%, 198 KB/s], Decompressed: 2160
Downloaded: 2317 file(s) [attempted 2317/8459 = 27%, 108 KB/s], Decompressed: 2160
Downloaded: 2358 file(s) [attempted 2358/8459 = 27%, 286 KB/s], Decompressed: 2245
Downloaded: 2396 file(s) [attempted 2396/8459 = 28%, 301 KB/s], Decompressed: 2245
Downloaded: 2437 file(s) [attempted 2437/8459 = 28%, 416 KB/s], Decompressed: 2321
Downloaded: 2471 file(s) [attempted 2471/8459 = 29%, 110 KB/s], Decompressed: 2321
Downloaded: 2512 file(s) [attempted 2512/8459 = 29%, 652 KB/s], Decompressed: 2403
Downloaded: 2554 file(s) [attempted 2554/8459 = 30%, 216 KB/s], Decompressed: 2403
Downloaded: 2581 file(s) [attempted 2581/8459 = 30%, 61 KB/s], Decompressed: 2482
Downloaded: 2625 file(s) [attempted 2625/8459 = 31%, 333 KB/s], Decompressed: 2482
Downloaded: 2670 file(s) [attempted 2670/8459 = 31%, 370 KB/s], Decompressed: 2560
Downloaded: 2715 file(s) [attempted 2715/8459 = 32%, 122 KB/s], Decompressed: 2560
Downloaded: 2756 file(s) [attempted 2756/8459 = 32%, 225 KB/s], Decompressed: 2629
Downloaded: 2790 file(s) [attempted 2790/8459 = 32%, 522 KB/s], Decompressed: 2629
Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 39 KB/s], Decompressed: 2722
Downloaded: 2869 file(s) [attempted 2869/8459 = 33%, 1044 KB/s], Decompressed: 2722
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 691 KB/s], Decompressed: 2722
Downloaded: 2961 file(s) [attempted 2961/8459 = 35%, 303 KB/s], Decompressed: 2821
Downloaded: 2992 file(s) [attempted 2992/8459 = 35%, 194 KB/s], Decompressed: 2821
Downloaded: 3033 file(s) [attempted 3033/8459 = 35%, 159 KB/s], Decompressed: 2927
Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 356 KB/s], Decompressed: 2927
Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 159 KB/s], Decompressed: 3026
Downloaded: 3164 file(s) [attempted 3164/8459 = 37%, 321 KB/s], Decompressed: 3026
Downloaded: 3205 file(s) [attempted 3205/8459 = 37%, 260 KB/s], Decompressed: 3026
Downloaded: 3246 file(s) [attempted 3246/8459 = 38%, 44 KB/s], Decompressed: 3119
Downloaded: 3283 file(s) [attempted 3283/8459 = 38%, 91 KB/s], Decompressed: 3119
Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 313 KB/s], Decompressed: 3218
Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 469 KB/s], Decompressed: 3218
Downloaded: 3403 file(s) [attempted 3403/8459 = 40%, 125 KB/s], Decompressed: 3218
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 302 KB/s], Decompressed: 3311
Downloaded: 3482 file(s) [attempted 3482/8459 = 41%, 166 KB/s], Decompressed: 3311
Downloaded: 3523 file(s) [attempted 3523/8459 = 41%, 183 KB/s], Decompressed: 3407
Downloaded: 3561 file(s) [attempted 3561/8459 = 42%, 425 KB/s], Decompressed: 3407
Downloaded: 3602 file(s) [attempted 3602/8459 = 42%, 103 KB/s], Decompressed: 3407
Downloaded: 3647 file(s) [attempted 3647/8459 = 43%, 316 KB/s], Decompressed: 3513
Downloaded: 3688 file(s) [attempted 3688/8459 = 43%, 555 KB/s], Decompressed: 3513
Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 161 KB/s], Decompressed: 3619
Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 633 KB/s], Decompressed: 3619
Downloaded: 3811 file(s) [attempted 3811/8459 = 45%, 126 KB/s], Decompressed: 3619
Downloaded: 3849 file(s) [attempted 3849/8459 = 45%, 708 KB/s], Decompressed: 3715
Downloaded: 3886 file(s) [attempted 3886/8459 = 45%, 216 KB/s], Decompressed: 3715
Downloaded: 3927 file(s) [attempted 3927/8459 = 46%, 151 KB/s], Decompressed: 3814
Downloaded: 3969 file(s) [attempted 3969/8459 = 46%, 186 KB/s], Decompressed: 3814
Downloaded: 4010 file(s) [attempted 4010/8459 = 47%, 303 KB/s], Decompressed: 3907
Downloaded: 4047 file(s) [attempted 4047/8459 = 47%, 603 KB/s], Decompressed: 3907
Downloaded: 4092 file(s) [attempted 4092/8459 = 48%, 1252 KB/s], Decompressed: 3999
Downloaded: 4136 file(s) [attempted 4136/8459 = 48%, 140 KB/s], Decompressed: 3999
Downloaded: 4177 file(s) [attempted 4177/8459 = 49%, 803 KB/s], Decompressed: 3999
Downloaded: 4219 file(s) [attempted 4219/8459 = 49%, 317 KB/s], Decompressed: 4092
Downloaded: 4253 file(s) [attempted 4253/8459 = 50%, 888 KB/s], Decompressed: 4092
Downloaded: 4294 file(s) [attempted 4294/8459 = 50%, 1021 KB/s], Decompressed: 4188
Downloaded: 4338 file(s) [attempted 4338/8459 = 51%, 70 KB/s], Decompressed: 4188
Downloaded: 4386 file(s) [attempted 4386/8459 = 51%, 1341 KB/s], Decompressed: 4287
Downloaded: 4431 file(s) [attempted 4431/8459 = 52%, 114 KB/s], Decompressed: 4287
Downloaded: 4469 file(s) [attempted 4469/8459 = 52%, 328 KB/s], Decompressed: 4287
Downloaded: 4503 file(s) [attempted 4503/8459 = 53%, 861 KB/s], Decompressed: 4386
Downloaded: 4541 file(s) [attempted 4541/8459 = 53%, 21 KB/s], Decompressed: 4386
Downloaded: 4589 file(s) [attempted 4589/8459 = 54%, 4245 KB/s], Decompressed: 4482
Downloaded: 4636 file(s) [attempted 4636/8459 = 54%, 133 KB/s], Decompressed: 4482
Downloaded: 4681 file(s) [attempted 4681/8459 = 55%, 433 KB/s], Decompressed: 4482
Downloaded: 4712 file(s) [attempted 4712/8459 = 55%, 326 KB/s], Decompressed: 4482
Downloaded: 4753 file(s) [attempted 4753/8459 = 56%, 106 KB/s], Decompressed: 4568
Downloaded: 4787 file(s) [attempted 4787/8459 = 56%, 355 KB/s], Decompressed: 4568
Downloaded: 4828 file(s) [attempted 4828/8459 = 57%, 376 KB/s], Decompressed: 4568
Downloaded: 4869 file(s) [attempted 4869/8459 = 57%, 4 KB/s], Decompressed: 4568
Downloaded: 4910 file(s) [attempted 4910/8459 = 58%, 271 KB/s], Decompressed: 4722
Downloaded: 4948 file(s) [attempted 4948/8459 = 58%, 360 KB/s], Decompressed: 4722
Downloaded: 4989 file(s) [attempted 4989/8459 = 58%, 328 KB/s], Decompressed: 4722
Downloaded: 5030 file(s) [attempted 5030/8459 = 59%, 61 KB/s], Decompressed: 4722
Downloaded: 5071 file(s) [attempted 5071/8459 = 59%, 94 KB/s], Decompressed: 4722
Downloaded: 5109 file(s) [attempted 5109/8459 = 60%, 153 KB/s], Decompressed: 4893
Downloaded: 5150 file(s) [attempted 5150/8459 = 60%, 465 KB/s], Decompressed: 4893
Downloaded: 5195 file(s) [attempted 5195/8459 = 61%, 131 KB/s], Decompressed: 4893
Downloaded: 5236 file(s) [attempted 5236/8459 = 61%, 90 KB/s], Decompressed: 4893
Downloaded: 5274 file(s) [attempted 5274/8459 = 62%, 424 KB/s], Decompressed: 4893
Downloaded: 5315 file(s) [attempted 5315/8459 = 62%, 147 KB/s], Decompressed: 4893
Downloaded: 5352 file(s) [attempted 5352/8459 = 63%, 650 KB/s], Decompressed: 5106
Downloaded: 5397 file(s) [attempted 5397/8459 = 63%, 183 KB/s], Decompressed: 5106
Downloaded: 5432 file(s) [attempted 5432/8459 = 64%, 143 KB/s], Decompressed: 5106
Downloaded: 5472 file(s) [attempted 5472/8459 = 64%, 1033 KB/s], Decompressed: 5106
Downloaded: 5513 file(s) [attempted 5513/8459 = 65%, 114 KB/s], Decompressed: 5106
Downloaded: 5554 file(s) [attempted 5554/8459 = 65%, 1193 KB/s], Decompressed: 5106
Downloaded: 5599 file(s) [attempted 5599/8459 = 66%, 165 KB/s], Decompressed: 5349
Downloaded: 5637 file(s) [attempted 5637/8459 = 66%, 33 KB/s], Decompressed: 5349
Downloaded: 5674 file(s) [attempted 5674/8459 = 67%, 68 KB/s], Decompressed: 5349
Downloaded: 5715 file(s) [attempted 5715/8459 = 67%, 693 KB/s], Decompressed: 5349
Downloaded: 5753 file(s) [attempted 5753/8459 = 68%, 60 KB/s], Decompressed: 5349
Downloaded: 5798 file(s) [attempted 5798/8459 = 68%, 40 KB/s], Decompressed: 5349
Downloaded: 5842 file(s) [attempted 5842/8459 = 69%, 56 KB/s], Decompressed: 5575
Downloaded: 5883 file(s) [attempted 5883/8459 = 69%, 47 KB/s], Decompressed: 5575
Downloaded: 5921 file(s) [attempted 5921/8459 = 69%, 592 KB/s], Decompressed: 5575
Downloaded: 5962 file(s) [attempted 5962/8459 = 70%, 938 KB/s], Decompressed: 5575
Downloaded: 6003 file(s) [attempted 6003/8459 = 70%, 174 KB/s], Decompressed: 5575
Downloaded: 6041 file(s) [attempted 6041/8459 = 71%, 223 KB/s], Decompressed: 5804
Downloaded: 6085 file(s) [attempted 6085/8459 = 71%, 143 KB/s], Decompressed: 5804
Downloaded: 6117 file(s) [attempted 6117/8459 = 72%, 296 KB/s], Decompressed: 5804
Downloaded: 6161 file(s) [attempted 6161/8459 = 72%, 40 KB/s], Decompressed: 5804
Downloaded: 6198 file(s) [attempted 6198/8459 = 73%, 421 KB/s], Decompressed: 5804
Downloaded: 6239 file(s) [attempted 6239/8459 = 73%, 51 KB/s], Decompressed: 5804
Downloaded: 6284 file(s) [attempted 6284/8459 = 74%, 48 KB/s], Decompressed: 6013
Downloaded: 6325 file(s) [attempted 6325/8459 = 74%, 79 KB/s], Decompressed: 6013
Downloaded: 6363 file(s) [attempted 6363/8459 = 75%, 338 KB/s], Decompressed: 6013
Downloaded: 6400 file(s) [attempted 6400/8459 = 75%, 123 KB/s], Decompressed: 6013
Downloaded: 6445 file(s) [attempted 6445/8459 = 76%, 653 KB/s], Decompressed: 6013
Downloaded: 6486 file(s) [attempted 6486/8459 = 76%, 299 KB/s], Decompressed: 6013
Downloaded: 6527 file(s) [attempted 6527/8459 = 77%, 438 KB/s], Decompressed: 6013
Downloaded: 6568 file(s) [attempted 6568/8459 = 77%, 593 KB/s], Decompressed: 6013
Downloaded: 6603 file(s) [attempted 6603/8459 = 78%, 660 KB/s], Decompressed: 6263
Downloaded: 6644 file(s) [attempted 6644/8459 = 78%, 469 KB/s], Decompressed: 6263
Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 78 KB/s], Decompressed: 6263
Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 122 KB/s], Decompressed: 6263
Downloaded: 6764 file(s) [attempted 6764/8459 = 79%, 490 KB/s], Decompressed: 6263
Downloaded: 6805 file(s) [attempted 6805/8459 = 80%, 232 KB/s], Decompressed: 6263
Downloaded: 6845 file(s) [attempted 6845/8459 = 80%, 375 KB/s], Decompressed: 6263
Downloaded: 6881 file(s) [attempted 6881/8459 = 81%, 218 KB/s], Decompressed: 6263
Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 171 KB/s], Decompressed: 6263
Downloaded: 6962 file(s) [attempted 6962/8459 = 82%, 118 KB/s], Decompressed: 6592
Downloaded: 7003 file(s) [attempted 7003/8459 = 82%, 116 KB/s], Decompressed: 6592
Downloaded: 7038 file(s) [attempted 7038/8459 = 83%, 898 KB/s], Decompressed: 6592
Downloaded: 7075 file(s) [attempted 7075/8459 = 83%, 244 KB/s], Decompressed: 6592
Downloaded: 7123 file(s) [attempted 7123/8459 = 84%, 23 KB/s], Decompressed: 6592
Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 37 KB/s], Decompressed: 6592
Downloaded: 7188 file(s) [attempted 7188/8459 = 84%, 136 KB/s], Decompressed: 6592
Downloaded: 7236 file(s) [attempted 7236/8459 = 85%, 41 KB/s], Decompressed: 6592
Downloaded: 7288 file(s) [attempted 7288/8459 = 86%, 38 KB/s], Decompressed: 6592
Downloaded: 7339 file(s) [attempted 7339/8459 = 86%, 83 KB/s], Decompressed: 6592
Downloaded: 7387 file(s) [attempted 7387/8459 = 87%, 65 KB/s], Decompressed: 6592
Downloaded: 7438 file(s) [attempted 7438/8459 = 87%, 7 KB/s], Decompressed: 6592
Downloaded: 7486 file(s) [attempted 7486/8459 = 88%, 31 KB/s], Decompressed: 6592
Downloaded: 7538 file(s) [attempted 7538/8459 = 89%, 115 KB/s], Decompressed: 6952
Downloaded: 7586 file(s) [attempted 7586/8459 = 89%, 151 KB/s], Decompressed: 6952
Downloaded: 7637 file(s) [attempted 7637/8459 = 90%, 73 KB/s], Decompressed: 6952
Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 49 KB/s], Decompressed: 6952
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 25 KB/s], Decompressed: 6952
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 110 KB/s], Decompressed: 6952
Downloaded: 7836 file(s) [attempted 7836/8459 = 92%, 1431 KB/s], Decompressed: 6952
Downloaded: 7884 file(s) [attempted 7884/8459 = 93%, 85 KB/s], Decompressed: 6952
Downloaded: 7932 file(s) [attempted 7932/8459 = 93%, 208 KB/s], Decompressed: 6952
Downloaded: 7973 file(s) [attempted 7973/8459 = 94%, 368 KB/s], Decompressed: 6952
Downloaded: 8010 file(s) [attempted 8010/8459 = 94%, 276 KB/s], Decompressed: 6952
Downloaded: 8052 file(s) [attempted 8052/8459 = 95%, 101 KB/s], Decompressed: 6952
Downloaded: 8089 file(s) [attempted 8089/8459 = 95%, 374 KB/s], Decompressed: 7534
Downloaded: 8134 file(s) [attempted 8134/8459 = 96%, 104 KB/s], Decompressed: 7534
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 1088 KB/s], Decompressed: 7534
Downloaded: 8216 file(s) [attempted 8216/8459 = 97%, 101 KB/s], Decompressed: 7534
Downloaded: 8257 file(s) [attempted 8257/8459 = 97%, 1158 KB/s], Decompressed: 7534
Downloaded: 8298 file(s) [attempted 8298/8459 = 98%, 590 KB/s], Decompressed: 7534
Downloaded: 8336 file(s) [attempted 8336/8459 = 98%, 80 KB/s], Decompressed: 7534
Downloaded: 8374 file(s) [attempted 8374/8459 = 98%, 93 KB/s], Decompressed: 7534
Downloaded: 8418 file(s) [attempted 8418/8459 = 99%, 72 KB/s], Decompressed: 7534
Downloaded: 8456 file(s) [attempted 8456/8459 = 99%, 795 KB/s], Decompressed: 7534
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 95 KB/s], Decompressed: 7534
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 95 KB/s], Decompressed: 7534

apx-runtime-resource-v1	apx-verifier-job-1698-runtime-lake_cache-3367592-1787240071523533169-0	4055040	4308992	21474836480	0	0	0	0	0	0	591589376	4560195584	21474836480	0	0	0	0	0	0

lean_checkerexit -duration 2h 0m · created 8/20/2026, 6:02:06 PM

lake build

✔ [500/502] Built Iut.Foundations.Species (167s)
✔ [501/506] Built Iut.Foundations.SourceGameplanSpeciesMutation (79s)
✔ [784/791] Built Iut.Foundations.RealLineCopy (226s)
✔ [785/791] Built Iut.Foundations.TransportDiagram (141s)
✔ [786/791] Built Iut.Foundations.IndeterminacyRelation (111s)
✔ [787/791] Built Iut.Foundations.RegionMeasure (172s)
✔ [788/791] Built Iut.Foundations.CommonTargetBound (142s)
✔ [789/791] Built Iut.Foundations.TransportedRegionFamily (105s)
✔ [790/794] Built Iut.Foundations.QualitativeData (82s)
✔ [3508/3513] Built Iut.Foundations.EtaleThetaQuotient (348s)
✔ [3509/3513] Built Iut.Foundations.Orbicurve (1114s)
✔ [3956/3959] Built Iut.Foundations.InitialThetaData (1217s)
✔ [3963/3966] Built Iut.Foundations.OrbicurvePullback (1049s)
✔ [3965/3968] Built Iut.Foundations.EtaleThetaCovers (465s)
✔ [3975/3984] Built Iut.Foundations.SourceTateCurve (391s)
✔ [3981/3986] Built Iut.Foundations.GaloisImage (448s)

/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1698-runtime-lean_checker-3367592-1787241673531943491-1 on attempt 1

blueprint_buildexit 1duration 22s · created 8/20/2026, 6:02:06 PM

lake build :blueprint

error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1698-runtime-blueprint_build-3367592-1787248903209917815-2	847872	1359872	21474836480	0	0	0	0	0	0	881848320	979959808	21474836480	0	0	0	0	0	0