Verification run

Run 1283

promachina/iut-leanbranch e23-3i-selected-k-root-cyclic-normalizationtriggered via github_push

failedcommit 907f18405b19toolchain lean-v4-30-0prover leantook 2h 3m · 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 e23-3i-selected-k-root-cyclic-normalization --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1733-source
exit_code=Some(128) duration_ms=358
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1733-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=3899
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1733-source'...


$ git checkout 907f18405b19a3e00562fb8c643cd9409a54c681
exit_code=Some(0) duration_ms=288
stderr:
Note: switching to '907f18405b19a3e00562fb8c643cd9409a54c681'.

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 907f184 E23.3I: audit selected K-root cyclic normalization

Resolved source revision: 907f18405b19a3e00562fb8c643cd9409a54c681

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=907f18405b19a3e00562fb8c643cd9409a54c681 provenance={"branch":"e23-3i-selected-k-root-cyclic-normalization","checked_out_revision":"907f18405b19a3e00562fb8c643cd9409a54c681","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"github_installation","local_clone":false,"requested_commit_sha":"907f18405b19a3e00562fb8c643cd9409a54c681","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=5269 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=186344
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.8s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (166ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (198ms)
✔ [13/25] Built Cache.Lean:c.o (183ms)
✔ [15/25] Built Cache.Init (37s)
✔ [16/25] Built Cache.IO (10s)
✔ [17/25] Built Cache.Init:c.o (1.2s)
✔ [18/25] Built Cache.IO:c.o (1.2s)
✔ [19/25] Built Cache.Hashing (965ms)
✔ [20/25] Built Cache.Hashing:c.o (368ms)
✔ [21/25] Built Cache.Requests (2.3s)
✔ [22/25] Built Cache.Requests:c.o (1.8s)
✔ [23/25] Built Cache.Main (993ms)
✔ [24/25] Built Cache.Main:c.o (522ms)
✔ [25/25] Built cache:exe (8.3s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 6 KB/s], Decompressed: 9
Downloaded: 35 file(s) [attempted 35/8459 = 0%, 27 KB/s], Decompressed: 22
Downloaded: 59 file(s) [attempted 59/8459 = 0%, 27 KB/s], Decompressed: 42
Downloaded: 82 file(s) [attempted 82/8459 = 0%, 183 KB/s], Decompressed: 59
Downloaded: 107 file(s) [attempted 107/8459 = 1%, 202 KB/s], Decompressed: 72
Downloaded: 141 file(s) [attempted 141/8459 = 1%, 55 KB/s], Decompressed: 93
Downloaded: 175 file(s) [attempted 175/8459 = 2%, 143 KB/s], Decompressed: 144
Downloaded: 213 file(s) [attempted 213/8459 = 2%, 336 KB/s], Decompressed: 175
Downloaded: 240 file(s) [attempted 240/8459 = 2%, 581 KB/s], Decompressed: 175
Downloaded: 271 file(s) [attempted 271/8459 = 3%, 47 KB/s], Decompressed: 213
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 159 KB/s], Decompressed: 254
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 24 KB/s], Decompressed: 292
Downloaded: 394 file(s) [attempted 394/8459 = 4%, 116 KB/s], Decompressed: 336
Downloaded: 435 file(s) [attempted 435/8459 = 5%, 423 KB/s], Decompressed: 370
Downloaded: 463 file(s) [attempted 463/8459 = 5%, 813 KB/s], Decompressed: 411
Downloaded: 502 file(s) [attempted 502/8459 = 5%, 150 KB/s], Decompressed: 456
Downloaded: 541 file(s) [attempted 541/8459 = 6%, 389 KB/s], Decompressed: 456
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 814 KB/s], Decompressed: 500
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 346 KB/s], Decompressed: 545
Downloaded: 661 file(s) [attempted 661/8459 = 7%, 145 KB/s], Decompressed: 589
Downloaded: 695 file(s) [attempted 695/8459 = 8%, 100 KB/s], Decompressed: 589
Downloaded: 740 file(s) [attempted 740/8459 = 8%, 796 KB/s], Decompressed: 641
Downloaded: 784 file(s) [attempted 784/8459 = 9%, 113 KB/s], Decompressed: 699
Downloaded: 825 file(s) [attempted 825/8459 = 9%, 190 KB/s], Decompressed: 699
Downloaded: 864 file(s) [attempted 864/8459 = 10%, 279 KB/s], Decompressed: 774
Downloaded: 904 file(s) [attempted 904/8459 = 10%, 46 KB/s], Decompressed: 774
Downloaded: 938 file(s) [attempted 938/8459 = 11%, 26 KB/s], Decompressed: 843
Downloaded: 979 file(s) [attempted 979/8459 = 11%, 487 KB/s], Decompressed: 843
Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 178 KB/s], Decompressed: 925
Downloaded: 1065 file(s) [attempted 1065/8459 = 12%, 394 KB/s], Decompressed: 925
Downloaded: 1113 file(s) [attempted 1113/8459 = 13%, 347 KB/s], Decompressed: 1010
Downloaded: 1157 file(s) [attempted 1157/8459 = 13%, 1942 KB/s], Decompressed: 1010
Downloaded: 1192 file(s) [attempted 1192/8459 = 14%, 175 KB/s], Decompressed: 1010
Downloaded: 1229 file(s) [attempted 1229/8459 = 14%, 299 KB/s], Decompressed: 1010
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 46 KB/s], Decompressed: 1113
Downloaded: 1311 file(s) [attempted 1311/8459 = 15%, 266 KB/s], Decompressed: 1113
Downloaded: 1352 file(s) [attempted 1352/8459 = 15%, 347 KB/s], Decompressed: 1113
Downloaded: 1397 file(s) [attempted 1397/8459 = 16%, 41 KB/s], Decompressed: 1113
Downloaded: 1434 file(s) [attempted 1434/8459 = 16%, 672 KB/s], Decompressed: 1113
Downloaded: 1479 file(s) [attempted 1479/8459 = 17%, 1486 KB/s], Decompressed: 1256
Downloaded: 1523 file(s) [attempted 1523/8459 = 18%, 70 KB/s], Decompressed: 1256
Downloaded: 1564 file(s) [attempted 1564/8459 = 18%, 57 KB/s], Decompressed: 1256
Downloaded: 1602 file(s) [attempted 1602/8459 = 18%, 462 KB/s], Decompressed: 1256
Downloaded: 1639 file(s) [attempted 1639/8459 = 19%, 411 KB/s], Decompressed: 1256
Downloaded: 1684 file(s) [attempted 1684/8459 = 19%, 142 KB/s], Decompressed: 1479
Downloaded: 1728 file(s) [attempted 1728/8459 = 20%, 293 KB/s], Decompressed: 1479
Downloaded: 1769 file(s) [attempted 1769/8459 = 20%, 1062 KB/s], Decompressed: 1479
Downloaded: 1810 file(s) [attempted 1810/8459 = 21%, 45 KB/s], Decompressed: 1479
Downloaded: 1851 file(s) [attempted 1851/8459 = 21%, 647 KB/s], Decompressed: 1479
Downloaded: 1889 file(s) [attempted 1889/8459 = 22%, 736 KB/s], Decompressed: 1684
Downloaded: 1940 file(s) [attempted 1940/8459 = 22%, 42 KB/s], Decompressed: 1684
Downloaded: 1985 file(s) [attempted 1985/8459 = 23%, 992 KB/s], Decompressed: 1684
Downloaded: 2033 file(s) [attempted 2033/8459 = 24%, 626 KB/s], Decompressed: 1886
Downloaded: 2081 file(s) [attempted 2081/8459 = 24%, 30 KB/s], Decompressed: 1886
Downloaded: 2125 file(s) [attempted 2125/8459 = 25%, 1322 KB/s], Decompressed: 1886
Downloaded: 2173 file(s) [attempted 2173/8459 = 25%, 1150 KB/s], Decompressed: 1886
Downloaded: 2221 file(s) [attempted 2221/8459 = 26%, 302 KB/s], Decompressed: 2033
Downloaded: 2265 file(s) [attempted 2265/8459 = 26%, 538 KB/s], Decompressed: 2033
Downloaded: 2310 file(s) [attempted 2310/8459 = 27%, 197 KB/s], Decompressed: 2033
Downloaded: 2351 file(s) [attempted 2351/8459 = 27%, 633 KB/s], Decompressed: 2033
Downloaded: 2388 file(s) [attempted 2388/8459 = 28%, 88 KB/s], Decompressed: 2033
Downloaded: 2429 file(s) [attempted 2429/8459 = 28%, 609 KB/s], Decompressed: 2221
Downloaded: 2470 file(s) [attempted 2470/8459 = 29%, 425 KB/s], Decompressed: 2221
Downloaded: 2511 file(s) [attempted 2511/8459 = 29%, 274 KB/s], Decompressed: 2221
Downloaded: 2552 file(s) [attempted 2552/8459 = 30%, 106 KB/s], Decompressed: 2221
Downloaded: 2597 file(s) [attempted 2597/8459 = 30%, 123 KB/s], Decompressed: 2402
Downloaded: 2638 file(s) [attempted 2638/8459 = 31%, 35 KB/s], Decompressed: 2402
Downloaded: 2682 file(s) [attempted 2682/8459 = 31%, 189 KB/s], Decompressed: 2402
Downloaded: 2723 file(s) [attempted 2723/8459 = 32%, 254 KB/s], Decompressed: 2402
Downloaded: 2761 file(s) [attempted 2761/8459 = 32%, 169 KB/s], Decompressed: 2580
Downloaded: 2806 file(s) [attempted 2806/8459 = 33%, 473 KB/s], Decompressed: 2580
Downloaded: 2847 file(s) [attempted 2847/8459 = 33%, 489 KB/s], Decompressed: 2580
Downloaded: 2881 file(s) [attempted 2881/8459 = 34%, 627 KB/s], Decompressed: 2580
Downloaded: 2922 file(s) [attempted 2922/8459 = 34%, 651 KB/s], Decompressed: 2754
Downloaded: 2959 file(s) [attempted 2959/8459 = 34%, 229 KB/s], Decompressed: 2754
Downloaded: 2997 file(s) [attempted 2997/8459 = 35%, 99 KB/s], Decompressed: 2754
Downloaded: 3035 file(s) [attempted 3035/8459 = 35%, 148 KB/s], Decompressed: 2754
Downloaded: 3072 file(s) [attempted 3072/8459 = 36%, 131 KB/s], Decompressed: 2754
Downloaded: 3117 file(s) [attempted 3117/8459 = 36%, 78 KB/s], Decompressed: 2919
Downloaded: 3161 file(s) [attempted 3161/8459 = 37%, 1591 KB/s], Decompressed: 2919
Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 422 KB/s], Decompressed: 2919
Downloaded: 3233 file(s) [attempted 3233/8459 = 38%, 113 KB/s], Decompressed: 2919
Downloaded: 3274 file(s) [attempted 3274/8459 = 38%, 65 KB/s], Decompressed: 3082
Downloaded: 3322 file(s) [attempted 3322/8459 = 39%, 87 KB/s], Decompressed: 3082
Downloaded: 3366 file(s) [attempted 3366/8459 = 39%, 888 KB/s], Decompressed: 3082
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 56 KB/s], Decompressed: 3243
Downloaded: 3442 file(s) [attempted 3442/8459 = 40%, 70 KB/s], Decompressed: 3243
Downloaded: 3483 file(s) [attempted 3483/8459 = 41%, 585 KB/s], Decompressed: 3243
Downloaded: 3527 file(s) [attempted 3527/8459 = 41%, 132 KB/s], Decompressed: 3243
Downloaded: 3570 file(s) [attempted 3570/8459 = 42%, 508 KB/s], Decompressed: 3390
Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 177 KB/s], Decompressed: 3390
Downloaded: 3654 file(s) [attempted 3654/8459 = 43%, 1406 KB/s], Decompressed: 3390
Downloaded: 3695 file(s) [attempted 3695/8459 = 43%, 294 KB/s], Decompressed: 3390
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 340 KB/s], Decompressed: 3541
Downloaded: 3773 file(s) [attempted 3773/8459 = 44%, 182 KB/s], Decompressed: 3541
Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 528 KB/s], Decompressed: 3541
Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 85 KB/s], Decompressed: 3541
Downloaded: 3900 file(s) [attempted 3900/8459 = 46%, 243 KB/s], Decompressed: 3719
Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 306 KB/s], Decompressed: 3719
Downloaded: 3975 file(s) [attempted 3975/8459 = 46%, 404 KB/s], Decompressed: 3719
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 49 KB/s], Decompressed: 3719
Downloaded: 4054 file(s) [attempted 4054/8459 = 47%, 655 KB/s], Decompressed: 3889
Downloaded: 4095 file(s) [attempted 4095/8459 = 48%, 191 KB/s], Decompressed: 3889
Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 79 KB/s], Decompressed: 3889
Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 192 KB/s], Decompressed: 3889
Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 408 KB/s], Decompressed: 4050
Downloaded: 4259 file(s) [attempted 4259/8459 = 50%, 48 KB/s], Decompressed: 4050
Downloaded: 4296 file(s) [attempted 4296/8459 = 50%, 272 KB/s], Decompressed: 4050
Downloaded: 4339 file(s) [attempted 4339/8459 = 51%, 66 KB/s], Decompressed: 4050
Downloaded: 4378 file(s) [attempted 4378/8459 = 51%, 174 KB/s], Decompressed: 4218
Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 271 KB/s], Decompressed: 4218
Downloaded: 4461 file(s) [attempted 4461/8459 = 52%, 35 KB/s], Decompressed: 4218
Downloaded: 4498 file(s) [attempted 4498/8459 = 53%, 135 KB/s], Decompressed: 4218
Downloaded: 4539 file(s) [attempted 4539/8459 = 53%, 549 KB/s], Decompressed: 4378
Downloaded: 4580 file(s) [attempted 4580/8459 = 54%, 426 KB/s], Decompressed: 4378
Downloaded: 4628 file(s) [attempted 4628/8459 = 54%, 256 KB/s], Decompressed: 4378
Downloaded: 4673 file(s) [attempted 4673/8459 = 55%, 664 KB/s], Decompressed: 4378
Downloaded: 4710 file(s) [attempted 4710/8459 = 55%, 177 KB/s], Decompressed: 4529
Downloaded: 4751 file(s) [attempted 4751/8459 = 56%, 109 KB/s], Decompressed: 4529
Downloaded: 4792 file(s) [attempted 4792/8459 = 56%, 379 KB/s], Decompressed: 4529
Downloaded: 4833 file(s) [attempted 4833/8459 = 57%, 49 KB/s], Decompressed: 4683
Downloaded: 4874 file(s) [attempted 4874/8459 = 57%, 109 KB/s], Decompressed: 4683
Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 711 KB/s], Decompressed: 4683
Downloaded: 4956 file(s) [attempted 4956/8459 = 58%, 1351 KB/s], Decompressed: 4826
Downloaded: 4997 file(s) [attempted 4997/8459 = 59%, 1122 KB/s], Decompressed: 4826
Downloaded: 5042 file(s) [attempted 5042/8459 = 59%, 255 KB/s], Decompressed: 4826
Downloaded: 5079 file(s) [attempted 5079/8459 = 60%, 143 KB/s], Decompressed: 4950
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 1944 KB/s], Decompressed: 4950
Downloaded: 5158 file(s) [attempted 5158/8459 = 60%, 632 KB/s], Decompressed: 4950
Downloaded: 5203 file(s) [attempted 5203/8459 = 61%, 119 KB/s], Decompressed: 5076
Downloaded: 5244 file(s) [attempted 5244/8459 = 61%, 75 KB/s], Decompressed: 5076
Downloaded: 5285 file(s) [attempted 5285/8459 = 62%, 283 KB/s], Decompressed: 5076
Downloaded: 5322 file(s) [attempted 5322/8459 = 62%, 219 KB/s], Decompressed: 5196
Downloaded: 5360 file(s) [attempted 5360/8459 = 63%, 221 KB/s], Decompressed: 5196
Downloaded: 5404 file(s) [attempted 5404/8459 = 63%, 62 KB/s], Decompressed: 5302
Downloaded: 5452 file(s) [attempted 5452/8459 = 64%, 319 KB/s], Decompressed: 5302
Downloaded: 5500 file(s) [attempted 5500/8459 = 65%, 63 KB/s], Decompressed: 5398
Downloaded: 5541 file(s) [attempted 5541/8459 = 65%, 296 KB/s], Decompressed: 5398
Downloaded: 5582 file(s) [attempted 5582/8459 = 65%, 1111 KB/s], Decompressed: 5480
Downloaded: 5623 file(s) [attempted 5623/8459 = 66%, 122 KB/s], Decompressed: 5480
Downloaded: 5664 file(s) [attempted 5664/8459 = 66%, 235 KB/s], Decompressed: 5568
Downloaded: 5705 file(s) [attempted 5705/8459 = 67%, 466 KB/s], Decompressed: 5568
Downloaded: 5746 file(s) [attempted 5746/8459 = 67%, 368 KB/s], Decompressed: 5654
Downloaded: 5791 file(s) [attempted 5791/8459 = 68%, 136 KB/s], Decompressed: 5654
Downloaded: 5832 file(s) [attempted 5832/8459 = 68%, 1499 KB/s], Decompressed: 5739
Downloaded: 5873 file(s) [attempted 5873/8459 = 69%, 220 KB/s], Decompressed: 5739
Downloaded: 5907 file(s) [attempted 5907/8459 = 69%, 352 KB/s], Decompressed: 5739
Downloaded: 5948 file(s) [attempted 5948/8459 = 70%, 299 KB/s], Decompressed: 5832
Downloaded: 5992 file(s) [attempted 5992/8459 = 70%, 142 KB/s], Decompressed: 5832
Downloaded: 6034 file(s) [attempted 6034/8459 = 71%, 378 KB/s], Decompressed: 5924
Downloaded: 6081 file(s) [attempted 6081/8459 = 71%, 105 KB/s], Decompressed: 5924
Downloaded: 6119 file(s) [attempted 6119/8459 = 72%, 2219 KB/s], Decompressed: 5924
Downloaded: 6153 file(s) [attempted 6153/8459 = 72%, 1199 KB/s], Decompressed: 6030
Downloaded: 6194 file(s) [attempted 6194/8459 = 73%, 329 KB/s], Decompressed: 6030
Downloaded: 6235 file(s) [attempted 6235/8459 = 73%, 241 KB/s], Decompressed: 6030
Downloaded: 6280 file(s) [attempted 6280/8459 = 74%, 58 KB/s], Decompressed: 6133
Downloaded: 6317 file(s) [attempted 6317/8459 = 74%, 475 KB/s], Decompressed: 6133
Downloaded: 6355 file(s) [attempted 6355/8459 = 75%, 1028 KB/s], Decompressed: 6239
Downloaded: 6399 file(s) [attempted 6399/8459 = 75%, 36 KB/s], Decompressed: 6239
Downloaded: 6437 file(s) [attempted 6437/8459 = 76%, 632 KB/s], Decompressed: 6239
Downloaded: 6478 file(s) [attempted 6478/8459 = 76%, 319 KB/s], Decompressed: 6341
Downloaded: 6522 file(s) [attempted 6522/8459 = 77%, 113 KB/s], Decompressed: 6341
Downloaded: 6560 file(s) [attempted 6560/8459 = 77%, 785 KB/s], Decompressed: 6341
Downloaded: 6601 file(s) [attempted 6601/8459 = 78%, 72 KB/s], Decompressed: 6471
Downloaded: 6642 file(s) [attempted 6642/8459 = 78%, 223 KB/s], Decompressed: 6471
Downloaded: 6676 file(s) [attempted 6676/8459 = 78%, 57 KB/s], Decompressed: 6471
Downloaded: 6721 file(s) [attempted 6721/8459 = 79%, 171 KB/s], Decompressed: 6471
Downloaded: 6765 file(s) [attempted 6765/8459 = 79%, 433 KB/s], Decompressed: 6601
Downloaded: 6810 file(s) [attempted 6810/8459 = 80%, 873 KB/s], Decompressed: 6601
Downloaded: 6850 file(s) [attempted 6850/8459 = 80%, 217 KB/s], Decompressed: 6724
Downloaded: 6885 file(s) [attempted 6885/8459 = 81%, 411 KB/s], Decompressed: 6724
Downloaded: 6926 file(s) [attempted 6926/8459 = 81%, 307 KB/s], Decompressed: 6724
Downloaded: 6970 file(s) [attempted 6970/8459 = 82%, 29 KB/s], Decompressed: 6844
Downloaded: 7018 file(s) [attempted 7018/8459 = 82%, 211 KB/s], Decompressed: 6844
Downloaded: 7063 file(s) [attempted 7063/8459 = 83%, 89 KB/s], Decompressed: 6953
Downloaded: 7100 file(s) [attempted 7100/8459 = 83%, 531 KB/s], Decompressed: 6953
Downloaded: 7135 file(s) [attempted 7135/8459 = 84%, 267 KB/s], Decompressed: 7037
Downloaded: 7179 file(s) [attempted 7179/8459 = 84%, 1673 KB/s], Decompressed: 7037
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 1860 KB/s], Decompressed: 7117
Downloaded: 7268 file(s) [attempted 7268/8459 = 85%, 695 KB/s], Decompressed: 7193
Downloaded: 7306 file(s) [attempted 7306/8459 = 86%, 137 KB/s], Decompressed: 7193
Downloaded: 7347 file(s) [attempted 7347/8459 = 86%, 109 KB/s], Decompressed: 7268
Downloaded: 7384 file(s) [attempted 7384/8459 = 87%, 380 KB/s], Decompressed: 7268
Downloaded: 7425 file(s) [attempted 7425/8459 = 87%, 499 KB/s], Decompressed: 7333
Downloaded: 7470 file(s) [attempted 7470/8459 = 88%, 157 KB/s], Decompressed: 7401
Downloaded: 7511 file(s) [attempted 7511/8459 = 88%, 236 KB/s], Decompressed: 7401
Downloaded: 7548 file(s) [attempted 7548/8459 = 89%, 655 KB/s], Decompressed: 7463
Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 143 KB/s], Decompressed: 7521
Downloaded: 7630 file(s) [attempted 7630/8459 = 90%, 1269 KB/s], Decompressed: 7521
Downloaded: 7668 file(s) [attempted 7668/8459 = 90%, 40 KB/s], Decompressed: 7579
Downloaded: 7702 file(s) [attempted 7702/8459 = 91%, 426 KB/s], Decompressed: 7634
Downloaded: 7747 file(s) [attempted 7747/8459 = 91%, 479 KB/s], Decompressed: 7682
Downloaded: 7791 file(s) [attempted 7791/8459 = 92%, 297 KB/s], Decompressed: 7682
Downloaded: 7829 file(s) [attempted 7829/8459 = 92%, 1855 KB/s], Decompressed: 7733
Downloaded: 7870 file(s) [attempted 7870/8459 = 93%, 647 KB/s], Decompressed: 7733
Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 232 KB/s], Decompressed: 7733
Downloaded: 7945 file(s) [attempted 7945/8459 = 93%, 36 KB/s], Decompressed: 7805
Downloaded: 7989 file(s) [attempted 7989/8459 = 94%, 619 KB/s], Decompressed: 7805
Downloaded: 8030 file(s) [attempted 8030/8459 = 94%, 428 KB/s], Decompressed: 7805
Downloaded: 8071 file(s) [attempted 8071/8459 = 95%, 103 KB/s], Decompressed: 7805
Downloaded: 8109 file(s) [attempted 8109/8459 = 95%, 128 KB/s], Decompressed: 7918
Downloaded: 8147 file(s) [attempted 8147/8459 = 96%, 345 KB/s], Decompressed: 7918
Downloaded: 8188 file(s) [attempted 8188/8459 = 96%, 269 KB/s], Decompressed: 7918
Downloaded: 8232 file(s) [attempted 8232/8459 = 97%, 484 KB/s], Decompressed: 7918
Downloaded: 8273 file(s) [attempted 8273/8459 = 97%, 526 KB/s], Decompressed: 7918
Downloaded: 8314 file(s) [attempted 8314/8459 = 98%, 541 KB/s], Decompressed: 7918
Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 541 KB/s], Decompressed: 8102
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 90 KB/s], Decompressed: 8102
Downloaded: 8437 file(s) [attempted 8437/8459 = 99%, 322 KB/s], Decompressed: 8102
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 279 KB/s], Decompressed: 8102
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 279 KB/s], Decompressed: 8102

apx-runtime-resource-v1	apx-verifier-job-1733-runtime-lake_cache-4060749-1787670439593654145-0	3960832	4100096	21474836480	0	0	0	0	0	0	6075846656	6480429056	21474836480	0	0	0	0	0	0


$ lake build
exit_code=None duration_ms=7200220
stdout:
✔ [500/502] Built Iut.Foundations.Species (78s)
✔ [501/506] Built Iut.Foundations.SourceGameplanSpeciesMutation (83s)
✔ [784/791] Built Iut.Foundations.RealLineCopy (103s)
✔ [785/791] Built Iut.Foundations.TransportDiagram (86s)
✔ [786/791] Built Iut.Foundations.IndeterminacyRelation (97s)
✔ [787/791] Built Iut.Foundations.RegionMeasure (194s)
✔ [788/791] Built Iut.Foundations.CommonTargetBound (302s)
✔ [789/791] Built Iut.Foundations.TransportedRegionFamily (238s)
✔ [790/794] Built Iut.Foundations.QualitativeData (236s)
✔ [3508/3513] Built Iut.Foundations.EtaleThetaQuotient (441s)
✔ [3509/3513] Built Iut.Foundations.Orbicurve (1346s)
✔ [3956/3959] Built Iut.Foundations.InitialThetaData (1185s)
✔ [3962/3966] Built Iut.Foundations.OrbicurvePullback (1182s)
✔ [3965/3968] Built Iut.Foundations.EtaleThetaCovers (360s)
✔ [3974/3982] Built Iut.Foundations.SourceTateCurve (319s)
✔ [3981/3986] Built Iut.Foundations.GaloisImage (230s)

stderr:
/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1733-runtime-lean_checker-4060749-1787670625944459414-1 on attempt 1

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

apx-runtime-resource-v1	apx-verifier-job-1733-runtime-blueprint_build-4060749-1787677833037015955-2	950272	1462272	21474836480	0	0	0	0	0	0	880103424	983916544	21474836480	0	0	0	0	0	0


blueprint_build failed; continuing (non-fatal phase).

Command runs

git_cloneexit 128duration 358 ms · created 8/25/2026, 5:10:50 PM

git clone --depth 1 --branch e23-3i-selected-k-root-cyclic-normalization --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1733-source

Cloning into '/var/lib/apodeixis/repos/job-1733-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, 5:10:50 PM

git clone (github installation auth fallback)

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

git_checkoutexit 0duration 288 ms · created 8/25/2026, 5:10:50 PM

git checkout 907f18405b19a3e00562fb8c643cd9409a54c681

Note: switching to '907f18405b19a3e00562fb8c643cd9409a54c681'.

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 907f184 E23.3I: audit selected K-root cyclic normalization

lake_cacheexit 0duration 3m 6s · created 8/25/2026, 5:10:50 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.8s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (166ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (198ms)
✔ [13/25] Built Cache.Lean:c.o (183ms)
✔ [15/25] Built Cache.Init (37s)
✔ [16/25] Built Cache.IO (10s)
✔ [17/25] Built Cache.Init:c.o (1.2s)
✔ [18/25] Built Cache.IO:c.o (1.2s)
✔ [19/25] Built Cache.Hashing (965ms)
✔ [20/25] Built Cache.Hashing:c.o (368ms)
✔ [21/25] Built Cache.Requests (2.3s)
✔ [22/25] Built Cache.Requests:c.o (1.8s)
✔ [23/25] Built Cache.Main (993ms)
✔ [24/25] Built Cache.Main:c.o (522ms)
✔ [25/25] Built cache:exe (8.3s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 6 KB/s], Decompressed: 9
Downloaded: 35 file(s) [attempted 35/8459 = 0%, 27 KB/s], Decompressed: 22
Downloaded: 59 file(s) [attempted 59/8459 = 0%, 27 KB/s], Decompressed: 42
Downloaded: 82 file(s) [attempted 82/8459 = 0%, 183 KB/s], Decompressed: 59
Downloaded: 107 file(s) [attempted 107/8459 = 1%, 202 KB/s], Decompressed: 72
Downloaded: 141 file(s) [attempted 141/8459 = 1%, 55 KB/s], Decompressed: 93
Downloaded: 175 file(s) [attempted 175/8459 = 2%, 143 KB/s], Decompressed: 144
Downloaded: 213 file(s) [attempted 213/8459 = 2%, 336 KB/s], Decompressed: 175
Downloaded: 240 file(s) [attempted 240/8459 = 2%, 581 KB/s], Decompressed: 175
Downloaded: 271 file(s) [attempted 271/8459 = 3%, 47 KB/s], Decompressed: 213
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 159 KB/s], Decompressed: 254
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 24 KB/s], Decompressed: 292
Downloaded: 394 file(s) [attempted 394/8459 = 4%, 116 KB/s], Decompressed: 336
Downloaded: 435 file(s) [attempted 435/8459 = 5%, 423 KB/s], Decompressed: 370
Downloaded: 463 file(s) [attempted 463/8459 = 5%, 813 KB/s], Decompressed: 411
Downloaded: 502 file(s) [attempted 502/8459 = 5%, 150 KB/s], Decompressed: 456
Downloaded: 541 file(s) [attempted 541/8459 = 6%, 389 KB/s], Decompressed: 456
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 814 KB/s], Decompressed: 500
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 346 KB/s], Decompressed: 545
Downloaded: 661 file(s) [attempted 661/8459 = 7%, 145 KB/s], Decompressed: 589
Downloaded: 695 file(s) [attempted 695/8459 = 8%, 100 KB/s], Decompressed: 589
Downloaded: 740 file(s) [attempted 740/8459 = 8%, 796 KB/s], Decompressed: 641
Downloaded: 784 file(s) [attempted 784/8459 = 9%, 113 KB/s], Decompressed: 699
Downloaded: 825 file(s) [attempted 825/8459 = 9%, 190 KB/s], Decompressed: 699
Downloaded: 864 file(s) [attempted 864/8459 = 10%, 279 KB/s], Decompressed: 774
Downloaded: 904 file(s) [attempted 904/8459 = 10%, 46 KB/s], Decompressed: 774
Downloaded: 938 file(s) [attempted 938/8459 = 11%, 26 KB/s], Decompressed: 843
Downloaded: 979 file(s) [attempted 979/8459 = 11%, 487 KB/s], Decompressed: 843
Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 178 KB/s], Decompressed: 925
Downloaded: 1065 file(s) [attempted 1065/8459 = 12%, 394 KB/s], Decompressed: 925
Downloaded: 1113 file(s) [attempted 1113/8459 = 13%, 347 KB/s], Decompressed: 1010
Downloaded: 1157 file(s) [attempted 1157/8459 = 13%, 1942 KB/s], Decompressed: 1010
Downloaded: 1192 file(s) [attempted 1192/8459 = 14%, 175 KB/s], Decompressed: 1010
Downloaded: 1229 file(s) [attempted 1229/8459 = 14%, 299 KB/s], Decompressed: 1010
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 46 KB/s], Decompressed: 1113
Downloaded: 1311 file(s) [attempted 1311/8459 = 15%, 266 KB/s], Decompressed: 1113
Downloaded: 1352 file(s) [attempted 1352/8459 = 15%, 347 KB/s], Decompressed: 1113
Downloaded: 1397 file(s) [attempted 1397/8459 = 16%, 41 KB/s], Decompressed: 1113
Downloaded: 1434 file(s) [attempted 1434/8459 = 16%, 672 KB/s], Decompressed: 1113
Downloaded: 1479 file(s) [attempted 1479/8459 = 17%, 1486 KB/s], Decompressed: 1256
Downloaded: 1523 file(s) [attempted 1523/8459 = 18%, 70 KB/s], Decompressed: 1256
Downloaded: 1564 file(s) [attempted 1564/8459 = 18%, 57 KB/s], Decompressed: 1256
Downloaded: 1602 file(s) [attempted 1602/8459 = 18%, 462 KB/s], Decompressed: 1256
Downloaded: 1639 file(s) [attempted 1639/8459 = 19%, 411 KB/s], Decompressed: 1256
Downloaded: 1684 file(s) [attempted 1684/8459 = 19%, 142 KB/s], Decompressed: 1479
Downloaded: 1728 file(s) [attempted 1728/8459 = 20%, 293 KB/s], Decompressed: 1479
Downloaded: 1769 file(s) [attempted 1769/8459 = 20%, 1062 KB/s], Decompressed: 1479
Downloaded: 1810 file(s) [attempted 1810/8459 = 21%, 45 KB/s], Decompressed: 1479
Downloaded: 1851 file(s) [attempted 1851/8459 = 21%, 647 KB/s], Decompressed: 1479
Downloaded: 1889 file(s) [attempted 1889/8459 = 22%, 736 KB/s], Decompressed: 1684
Downloaded: 1940 file(s) [attempted 1940/8459 = 22%, 42 KB/s], Decompressed: 1684
Downloaded: 1985 file(s) [attempted 1985/8459 = 23%, 992 KB/s], Decompressed: 1684
Downloaded: 2033 file(s) [attempted 2033/8459 = 24%, 626 KB/s], Decompressed: 1886
Downloaded: 2081 file(s) [attempted 2081/8459 = 24%, 30 KB/s], Decompressed: 1886
Downloaded: 2125 file(s) [attempted 2125/8459 = 25%, 1322 KB/s], Decompressed: 1886
Downloaded: 2173 file(s) [attempted 2173/8459 = 25%, 1150 KB/s], Decompressed: 1886
Downloaded: 2221 file(s) [attempted 2221/8459 = 26%, 302 KB/s], Decompressed: 2033
Downloaded: 2265 file(s) [attempted 2265/8459 = 26%, 538 KB/s], Decompressed: 2033
Downloaded: 2310 file(s) [attempted 2310/8459 = 27%, 197 KB/s], Decompressed: 2033
Downloaded: 2351 file(s) [attempted 2351/8459 = 27%, 633 KB/s], Decompressed: 2033
Downloaded: 2388 file(s) [attempted 2388/8459 = 28%, 88 KB/s], Decompressed: 2033
Downloaded: 2429 file(s) [attempted 2429/8459 = 28%, 609 KB/s], Decompressed: 2221
Downloaded: 2470 file(s) [attempted 2470/8459 = 29%, 425 KB/s], Decompressed: 2221
Downloaded: 2511 file(s) [attempted 2511/8459 = 29%, 274 KB/s], Decompressed: 2221
Downloaded: 2552 file(s) [attempted 2552/8459 = 30%, 106 KB/s], Decompressed: 2221
Downloaded: 2597 file(s) [attempted 2597/8459 = 30%, 123 KB/s], Decompressed: 2402
Downloaded: 2638 file(s) [attempted 2638/8459 = 31%, 35 KB/s], Decompressed: 2402
Downloaded: 2682 file(s) [attempted 2682/8459 = 31%, 189 KB/s], Decompressed: 2402
Downloaded: 2723 file(s) [attempted 2723/8459 = 32%, 254 KB/s], Decompressed: 2402
Downloaded: 2761 file(s) [attempted 2761/8459 = 32%, 169 KB/s], Decompressed: 2580
Downloaded: 2806 file(s) [attempted 2806/8459 = 33%, 473 KB/s], Decompressed: 2580
Downloaded: 2847 file(s) [attempted 2847/8459 = 33%, 489 KB/s], Decompressed: 2580
Downloaded: 2881 file(s) [attempted 2881/8459 = 34%, 627 KB/s], Decompressed: 2580
Downloaded: 2922 file(s) [attempted 2922/8459 = 34%, 651 KB/s], Decompressed: 2754
Downloaded: 2959 file(s) [attempted 2959/8459 = 34%, 229 KB/s], Decompressed: 2754
Downloaded: 2997 file(s) [attempted 2997/8459 = 35%, 99 KB/s], Decompressed: 2754
Downloaded: 3035 file(s) [attempted 3035/8459 = 35%, 148 KB/s], Decompressed: 2754
Downloaded: 3072 file(s) [attempted 3072/8459 = 36%, 131 KB/s], Decompressed: 2754
Downloaded: 3117 file(s) [attempted 3117/8459 = 36%, 78 KB/s], Decompressed: 2919
Downloaded: 3161 file(s) [attempted 3161/8459 = 37%, 1591 KB/s], Decompressed: 2919
Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 422 KB/s], Decompressed: 2919
Downloaded: 3233 file(s) [attempted 3233/8459 = 38%, 113 KB/s], Decompressed: 2919
Downloaded: 3274 file(s) [attempted 3274/8459 = 38%, 65 KB/s], Decompressed: 3082
Downloaded: 3322 file(s) [attempted 3322/8459 = 39%, 87 KB/s], Decompressed: 3082
Downloaded: 3366 file(s) [attempted 3366/8459 = 39%, 888 KB/s], Decompressed: 3082
Downloaded: 3407 file(s) [attempted 3407/8459 = 40%, 56 KB/s], Decompressed: 3243
Downloaded: 3442 file(s) [attempted 3442/8459 = 40%, 70 KB/s], Decompressed: 3243
Downloaded: 3483 file(s) [attempted 3483/8459 = 41%, 585 KB/s], Decompressed: 3243
Downloaded: 3527 file(s) [attempted 3527/8459 = 41%, 132 KB/s], Decompressed: 3243
Downloaded: 3570 file(s) [attempted 3570/8459 = 42%, 508 KB/s], Decompressed: 3390
Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 177 KB/s], Decompressed: 3390
Downloaded: 3654 file(s) [attempted 3654/8459 = 43%, 1406 KB/s], Decompressed: 3390
Downloaded: 3695 file(s) [attempted 3695/8459 = 43%, 294 KB/s], Decompressed: 3390
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 340 KB/s], Decompressed: 3541
Downloaded: 3773 file(s) [attempted 3773/8459 = 44%, 182 KB/s], Decompressed: 3541
Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 528 KB/s], Decompressed: 3541
Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 85 KB/s], Decompressed: 3541
Downloaded: 3900 file(s) [attempted 3900/8459 = 46%, 243 KB/s], Decompressed: 3719
Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 306 KB/s], Decompressed: 3719
Downloaded: 3975 file(s) [attempted 3975/8459 = 46%, 404 KB/s], Decompressed: 3719
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 49 KB/s], Decompressed: 3719
Downloaded: 4054 file(s) [attempted 4054/8459 = 47%, 655 KB/s], Decompressed: 3889
Downloaded: 4095 file(s) [attempted 4095/8459 = 48%, 191 KB/s], Decompressed: 3889
Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 79 KB/s], Decompressed: 3889
Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 192 KB/s], Decompressed: 3889
Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 408 KB/s], Decompressed: 4050
Downloaded: 4259 file(s) [attempted 4259/8459 = 50%, 48 KB/s], Decompressed: 4050
Downloaded: 4296 file(s) [attempted 4296/8459 = 50%, 272 KB/s], Decompressed: 4050
Downloaded: 4339 file(s) [attempted 4339/8459 = 51%, 66 KB/s], Decompressed: 4050
Downloaded: 4378 file(s) [attempted 4378/8459 = 51%, 174 KB/s], Decompressed: 4218
Downloaded: 4423 file(s) [attempted 4423/8459 = 52%, 271 KB/s], Decompressed: 4218
Downloaded: 4461 file(s) [attempted 4461/8459 = 52%, 35 KB/s], Decompressed: 4218
Downloaded: 4498 file(s) [attempted 4498/8459 = 53%, 135 KB/s], Decompressed: 4218
Downloaded: 4539 file(s) [attempted 4539/8459 = 53%, 549 KB/s], Decompressed: 4378
Downloaded: 4580 file(s) [attempted 4580/8459 = 54%, 426 KB/s], Decompressed: 4378
Downloaded: 4628 file(s) [attempted 4628/8459 = 54%, 256 KB/s], Decompressed: 4378
Downloaded: 4673 file(s) [attempted 4673/8459 = 55%, 664 KB/s], Decompressed: 4378
Downloaded: 4710 file(s) [attempted 4710/8459 = 55%, 177 KB/s], Decompressed: 4529
Downloaded: 4751 file(s) [attempted 4751/8459 = 56%, 109 KB/s], Decompressed: 4529
Downloaded: 4792 file(s) [attempted 4792/8459 = 56%, 379 KB/s], Decompressed: 4529
Downloaded: 4833 file(s) [attempted 4833/8459 = 57%, 49 KB/s], Decompressed: 4683
Downloaded: 4874 file(s) [attempted 4874/8459 = 57%, 109 KB/s], Decompressed: 4683
Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 711 KB/s], Decompressed: 4683
Downloaded: 4956 file(s) [attempted 4956/8459 = 58%, 1351 KB/s], Decompressed: 4826
Downloaded: 4997 file(s) [attempted 4997/8459 = 59%, 1122 KB/s], Decompressed: 4826
Downloaded: 5042 file(s) [attempted 5042/8459 = 59%, 255 KB/s], Decompressed: 4826
Downloaded: 5079 file(s) [attempted 5079/8459 = 60%, 143 KB/s], Decompressed: 4950
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 1944 KB/s], Decompressed: 4950
Downloaded: 5158 file(s) [attempted 5158/8459 = 60%, 632 KB/s], Decompressed: 4950
Downloaded: 5203 file(s) [attempted 5203/8459 = 61%, 119 KB/s], Decompressed: 5076
Downloaded: 5244 file(s) [attempted 5244/8459 = 61%, 75 KB/s], Decompressed: 5076
Downloaded: 5285 file(s) [attempted 5285/8459 = 62%, 283 KB/s], Decompressed: 5076
Downloaded: 5322 file(s) [attempted 5322/8459 = 62%, 219 KB/s], Decompressed: 5196
Downloaded: 5360 file(s) [attempted 5360/8459 = 63%, 221 KB/s], Decompressed: 5196
Downloaded: 5404 file(s) [attempted 5404/8459 = 63%, 62 KB/s], Decompressed: 5302
Downloaded: 5452 file(s) [attempted 5452/8459 = 64%, 319 KB/s], Decompressed: 5302
Downloaded: 5500 file(s) [attempted 5500/8459 = 65%, 63 KB/s], Decompressed: 5398
Downloaded: 5541 file(s) [attempted 5541/8459 = 65%, 296 KB/s], Decompressed: 5398
Downloaded: 5582 file(s) [attempted 5582/8459 = 65%, 1111 KB/s], Decompressed: 5480
Downloaded: 5623 file(s) [attempted 5623/8459 = 66%, 122 KB/s], Decompressed: 5480
Downloaded: 5664 file(s) [attempted 5664/8459 = 66%, 235 KB/s], Decompressed: 5568
Downloaded: 5705 file(s) [attempted 5705/8459 = 67%, 466 KB/s], Decompressed: 5568
Downloaded: 5746 file(s) [attempted 5746/8459 = 67%, 368 KB/s], Decompressed: 5654
Downloaded: 5791 file(s) [attempted 5791/8459 = 68%, 136 KB/s], Decompressed: 5654
Downloaded: 5832 file(s) [attempted 5832/8459 = 68%, 1499 KB/s], Decompressed: 5739
Downloaded: 5873 file(s) [attempted 5873/8459 = 69%, 220 KB/s], Decompressed: 5739
Downloaded: 5907 file(s) [attempted 5907/8459 = 69%, 352 KB/s], Decompressed: 5739
Downloaded: 5948 file(s) [attempted 5948/8459 = 70%, 299 KB/s], Decompressed: 5832
Downloaded: 5992 file(s) [attempted 5992/8459 = 70%, 142 KB/s], Decompressed: 5832
Downloaded: 6034 file(s) [attempted 6034/8459 = 71%, 378 KB/s], Decompressed: 5924
Downloaded: 6081 file(s) [attempted 6081/8459 = 71%, 105 KB/s], Decompressed: 5924
Downloaded: 6119 file(s) [attempted 6119/8459 = 72%, 2219 KB/s], Decompressed: 5924
Downloaded: 6153 file(s) [attempted 6153/8459 = 72%, 1199 KB/s], Decompressed: 6030
Downloaded: 6194 file(s) [attempted 6194/8459 = 73%, 329 KB/s], Decompressed: 6030
Downloaded: 6235 file(s) [attempted 6235/8459 = 73%, 241 KB/s], Decompressed: 6030
Downloaded: 6280 file(s) [attempted 6280/8459 = 74%, 58 KB/s], Decompressed: 6133
Downloaded: 6317 file(s) [attempted 6317/8459 = 74%, 475 KB/s], Decompressed: 6133
Downloaded: 6355 file(s) [attempted 6355/8459 = 75%, 1028 KB/s], Decompressed: 6239
Downloaded: 6399 file(s) [attempted 6399/8459 = 75%, 36 KB/s], Decompressed: 6239
Downloaded: 6437 file(s) [attempted 6437/8459 = 76%, 632 KB/s], Decompressed: 6239
Downloaded: 6478 file(s) [attempted 6478/8459 = 76%, 319 KB/s], Decompressed: 6341
Downloaded: 6522 file(s) [attempted 6522/8459 = 77%, 113 KB/s], Decompressed: 6341
Downloaded: 6560 file(s) [attempted 6560/8459 = 77%, 785 KB/s], Decompressed: 6341
Downloaded: 6601 file(s) [attempted 6601/8459 = 78%, 72 KB/s], Decompressed: 6471
Downloaded: 6642 file(s) [attempted 6642/8459 = 78%, 223 KB/s], Decompressed: 6471
Downloaded: 6676 file(s) [attempted 6676/8459 = 78%, 57 KB/s], Decompressed: 6471
Downloaded: 6721 file(s) [attempted 6721/8459 = 79%, 171 KB/s], Decompressed: 6471
Downloaded: 6765 file(s) [attempted 6765/8459 = 79%, 433 KB/s], Decompressed: 6601
Downloaded: 6810 file(s) [attempted 6810/8459 = 80%, 873 KB/s], Decompressed: 6601
Downloaded: 6850 file(s) [attempted 6850/8459 = 80%, 217 KB/s], Decompressed: 6724
Downloaded: 6885 file(s) [attempted 6885/8459 = 81%, 411 KB/s], Decompressed: 6724
Downloaded: 6926 file(s) [attempted 6926/8459 = 81%, 307 KB/s], Decompressed: 6724
Downloaded: 6970 file(s) [attempted 6970/8459 = 82%, 29 KB/s], Decompressed: 6844
Downloaded: 7018 file(s) [attempted 7018/8459 = 82%, 211 KB/s], Decompressed: 6844
Downloaded: 7063 file(s) [attempted 7063/8459 = 83%, 89 KB/s], Decompressed: 6953
Downloaded: 7100 file(s) [attempted 7100/8459 = 83%, 531 KB/s], Decompressed: 6953
Downloaded: 7135 file(s) [attempted 7135/8459 = 84%, 267 KB/s], Decompressed: 7037
Downloaded: 7179 file(s) [attempted 7179/8459 = 84%, 1673 KB/s], Decompressed: 7037
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 1860 KB/s], Decompressed: 7117
Downloaded: 7268 file(s) [attempted 7268/8459 = 85%, 695 KB/s], Decompressed: 7193
Downloaded: 7306 file(s) [attempted 7306/8459 = 86%, 137 KB/s], Decompressed: 7193
Downloaded: 7347 file(s) [attempted 7347/8459 = 86%, 109 KB/s], Decompressed: 7268
Downloaded: 7384 file(s) [attempted 7384/8459 = 87%, 380 KB/s], Decompressed: 7268
Downloaded: 7425 file(s) [attempted 7425/8459 = 87%, 499 KB/s], Decompressed: 7333
Downloaded: 7470 file(s) [attempted 7470/8459 = 88%, 157 KB/s], Decompressed: 7401
Downloaded: 7511 file(s) [attempted 7511/8459 = 88%, 236 KB/s], Decompressed: 7401
Downloaded: 7548 file(s) [attempted 7548/8459 = 89%, 655 KB/s], Decompressed: 7463
Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 143 KB/s], Decompressed: 7521
Downloaded: 7630 file(s) [attempted 7630/8459 = 90%, 1269 KB/s], Decompressed: 7521
Downloaded: 7668 file(s) [attempted 7668/8459 = 90%, 40 KB/s], Decompressed: 7579
Downloaded: 7702 file(s) [attempted 7702/8459 = 91%, 426 KB/s], Decompressed: 7634
Downloaded: 7747 file(s) [attempted 7747/8459 = 91%, 479 KB/s], Decompressed: 7682
Downloaded: 7791 file(s) [attempted 7791/8459 = 92%, 297 KB/s], Decompressed: 7682
Downloaded: 7829 file(s) [attempted 7829/8459 = 92%, 1855 KB/s], Decompressed: 7733
Downloaded: 7870 file(s) [attempted 7870/8459 = 93%, 647 KB/s], Decompressed: 7733
Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 232 KB/s], Decompressed: 7733
Downloaded: 7945 file(s) [attempted 7945/8459 = 93%, 36 KB/s], Decompressed: 7805
Downloaded: 7989 file(s) [attempted 7989/8459 = 94%, 619 KB/s], Decompressed: 7805
Downloaded: 8030 file(s) [attempted 8030/8459 = 94%, 428 KB/s], Decompressed: 7805
Downloaded: 8071 file(s) [attempted 8071/8459 = 95%, 103 KB/s], Decompressed: 7805
Downloaded: 8109 file(s) [attempted 8109/8459 = 95%, 128 KB/s], Decompressed: 7918
Downloaded: 8147 file(s) [attempted 8147/8459 = 96%, 345 KB/s], Decompressed: 7918
Downloaded: 8188 file(s) [attempted 8188/8459 = 96%, 269 KB/s], Decompressed: 7918
Downloaded: 8232 file(s) [attempted 8232/8459 = 97%, 484 KB/s], Decompressed: 7918
Downloaded: 8273 file(s) [attempted 8273/8459 = 97%, 526 KB/s], Decompressed: 7918
Downloaded: 8314 file(s) [attempted 8314/8459 = 98%, 541 KB/s], Decompressed: 7918
Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 541 KB/s], Decompressed: 8102
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 90 KB/s], Decompressed: 8102
Downloaded: 8437 file(s) [attempted 8437/8459 = 99%, 322 KB/s], Decompressed: 8102
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 279 KB/s], Decompressed: 8102
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 279 KB/s], Decompressed: 8102

apx-runtime-resource-v1	apx-verifier-job-1733-runtime-lake_cache-4060749-1787670439593654145-0	3960832	4100096	21474836480	0	0	0	0	0	0	6075846656	6480429056	21474836480	0	0	0	0	0	0

lean_checkerexit -duration 2h 0m · created 8/25/2026, 5:10:50 PM

lake build

✔ [500/502] Built Iut.Foundations.Species (78s)
✔ [501/506] Built Iut.Foundations.SourceGameplanSpeciesMutation (83s)
✔ [784/791] Built Iut.Foundations.RealLineCopy (103s)
✔ [785/791] Built Iut.Foundations.TransportDiagram (86s)
✔ [786/791] Built Iut.Foundations.IndeterminacyRelation (97s)
✔ [787/791] Built Iut.Foundations.RegionMeasure (194s)
✔ [788/791] Built Iut.Foundations.CommonTargetBound (302s)
✔ [789/791] Built Iut.Foundations.TransportedRegionFamily (238s)
✔ [790/794] Built Iut.Foundations.QualitativeData (236s)
✔ [3508/3513] Built Iut.Foundations.EtaleThetaQuotient (441s)
✔ [3509/3513] Built Iut.Foundations.Orbicurve (1346s)
✔ [3956/3959] Built Iut.Foundations.InitialThetaData (1185s)
✔ [3962/3966] Built Iut.Foundations.OrbicurvePullback (1182s)
✔ [3965/3968] Built Iut.Foundations.EtaleThetaCovers (360s)
✔ [3974/3982] Built Iut.Foundations.SourceTateCurve (319s)
✔ [3981/3986] Built Iut.Foundations.GaloisImage (230s)

/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1733-runtime-lean_checker-4060749-1787670625944459414-1 on attempt 1

blueprint_buildexit 1duration 16s · created 8/25/2026, 5:10:50 PM

lake build :blueprint

error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1733-runtime-blueprint_build-4060749-1787677833037015955-2	950272	1462272	21474836480	0	0	0	0	0	0	880103424	983916544	21474836480	0	0	0	0	0	0