Verification run

Run 1292

promachina/iut-leanbranch e21-924-checkpoint-quotienttriggered via github_push
failedcommit f5e1b02c8e78toolchain lean-v4-30-0prover leantook 2h 8m · finished 2w 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 e21-924-checkpoint-quotient --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1751-source
exit_code=Some(128) duration_ms=224
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1751-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=4768
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1751-source'...


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

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 f5e1b02 link raw and unit descent comparison leaders

Resolved source revision: f5e1b02c8e78f92adeeed7e317f97a50dbf30393

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=f5e1b02c8e78f92adeeed7e317f97a50dbf30393 provenance={"branch":"e21-924-checkpoint-quotient","checked_out_revision":"f5e1b02c8e78f92adeeed7e317f97a50dbf30393","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"github_installation","local_clone":false,"requested_commit_sha":"f5e1b02c8e78f92adeeed7e317f97a50dbf30393","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=71714 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=418366
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:
✔ [7/22] Built Cache.Lean (9.8s)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (1.4s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (140ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (165ms)
✔ [13/25] Built Cache.Lean:c.o (146ms)
✔ [15/25] Built Cache.Init (295ms)
✔ [16/25] Built Cache.IO (7.8s)
✔ [17/25] Built Cache.Init:c.o (97ms)
✔ [18/25] Built Cache.IO:c.o (1.1s)
✔ [19/25] Built Cache.Hashing (889ms)
✔ [20/25] Built Cache.Hashing:c.o (352ms)
✔ [21/25] Built Cache.Requests (2.2s)
✔ [22/25] Built Cache.Requests:c.o (1.9s)
✔ [23/25] Built Cache.Main (1.0s)
✔ [24/25] Built Cache.Main:c.o (578ms)
✔ [25/25] Built cache:exe (231s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 9 KB/s], Decompressed: 9
Downloaded: 34 file(s) [attempted 34/8459 = 0%, 27 KB/s], Decompressed: 21
Downloaded: 58 file(s) [attempted 58/8459 = 0%, 230 KB/s], Decompressed: 38
Downloaded: 82 file(s) [attempted 82/8459 = 0%, 255 KB/s], Decompressed: 38
Downloaded: 110 file(s) [attempted 110/8459 = 1%, 114 KB/s], Decompressed: 57
Downloaded: 144 file(s) [attempted 144/8459 = 1%, 221 KB/s], Decompressed: 87
Downloaded: 175 file(s) [attempted 175/8459 = 2%, 290 KB/s], Decompressed: 127
Downloaded: 213 file(s) [attempted 213/8459 = 2%, 91 KB/s], Decompressed: 168
Downloaded: 247 file(s) [attempted 247/8459 = 2%, 563 KB/s], Decompressed: 206
Downloaded: 281 file(s) [attempted 281/8459 = 3%, 95 KB/s], Decompressed: 240
Downloaded: 319 file(s) [attempted 319/8459 = 3%, 463 KB/s], Decompressed: 274
Downloaded: 357 file(s) [attempted 357/8459 = 4%, 213 KB/s], Decompressed: 309
Downloaded: 394 file(s) [attempted 394/8459 = 4%, 594 KB/s], Decompressed: 339
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 528 KB/s], Decompressed: 374
Downloaded: 470 file(s) [attempted 470/8459 = 5%, 752 KB/s], Decompressed: 435
Downloaded: 507 file(s) [attempted 507/8459 = 5%, 360 KB/s], Decompressed: 466
Downloaded: 548 file(s) [attempted 548/8459 = 6%, 555 KB/s], Decompressed: 500
Downloaded: 589 file(s) [attempted 589/8459 = 6%, 43 KB/s], Decompressed: 541
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 343 KB/s], Decompressed: 541
Downloaded: 668 file(s) [attempted 668/8459 = 7%, 62 KB/s], Decompressed: 589
Downloaded: 706 file(s) [attempted 706/8459 = 8%, 268 KB/s], Decompressed: 637
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 247 KB/s], Decompressed: 637
Downloaded: 791 file(s) [attempted 791/8459 = 9%, 216 KB/s], Decompressed: 695
Downloaded: 832 file(s) [attempted 832/8459 = 9%, 348 KB/s], Decompressed: 757
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 379 KB/s], Decompressed: 812
Downloaded: 908 file(s) [attempted 908/8459 = 10%, 500 KB/s], Decompressed: 812
Downloaded: 952 file(s) [attempted 952/8459 = 11%, 867 KB/s], Decompressed: 865
Downloaded: 993 file(s) [attempted 993/8459 = 11%, 223 KB/s], Decompressed: 914
Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 538 KB/s], Decompressed: 962
Downloaded: 1075 file(s) [attempted 1075/8459 = 12%, 73 KB/s], Decompressed: 1010
Downloaded: 1109 file(s) [attempted 1109/8459 = 13%, 408 KB/s], Decompressed: 1010
Downloaded: 1154 file(s) [attempted 1154/8459 = 13%, 312 KB/s], Decompressed: 1062
Downloaded: 1195 file(s) [attempted 1195/8459 = 14%, 27 KB/s], Decompressed: 1116
Downloaded: 1239 file(s) [attempted 1239/8459 = 14%, 628 KB/s], Decompressed: 1171
Downloaded: 1284 file(s) [attempted 1284/8459 = 15%, 1624 KB/s], Decompressed: 1171
Downloaded: 1321 file(s) [attempted 1321/8459 = 15%, 755 KB/s], Decompressed: 1239
Downloaded: 1362 file(s) [attempted 1362/8459 = 16%, 216 KB/s], Decompressed: 1239
Downloaded: 1400 file(s) [attempted 1400/8459 = 16%, 180 KB/s], Decompressed: 1239
Downloaded: 1441 file(s) [attempted 1441/8459 = 17%, 164 KB/s], Decompressed: 1315
Downloaded: 1482 file(s) [attempted 1482/8459 = 17%, 414 KB/s], Decompressed: 1315
Downloaded: 1518 file(s) [attempted 1518/8459 = 17%, 345 KB/s], Decompressed: 1410
Downloaded: 1561 file(s) [attempted 1561/8459 = 18%, 45 KB/s], Decompressed: 1410
Downloaded: 1595 file(s) [attempted 1595/8459 = 18%, 21 KB/s], Decompressed: 1410
Downloaded: 1636 file(s) [attempted 1636/8459 = 19%, 479 KB/s], Decompressed: 1410
Downloaded: 1674 file(s) [attempted 1674/8459 = 19%, 58 KB/s], Decompressed: 1410
Downloaded: 1711 file(s) [attempted 1711/8459 = 20%, 215 KB/s], Decompressed: 1516
Downloaded: 1752 file(s) [attempted 1752/8459 = 20%, 268 KB/s], Decompressed: 1516
Downloaded: 1790 file(s) [attempted 1790/8459 = 21%, 247 KB/s], Decompressed: 1516
Downloaded: 1828 file(s) [attempted 1828/8459 = 21%, 138 KB/s], Decompressed: 1516
Downloaded: 1865 file(s) [attempted 1865/8459 = 22%, 288 KB/s], Decompressed: 1689
Downloaded: 1906 file(s) [attempted 1906/8459 = 22%, 233 KB/s], Decompressed: 1689
Downloaded: 1947 file(s) [attempted 1947/8459 = 23%, 1552 KB/s], Decompressed: 1689
Downloaded: 1981 file(s) [attempted 1981/8459 = 23%, 38 KB/s], Decompressed: 1834
Downloaded: 2022 file(s) [attempted 2022/8459 = 23%, 173 KB/s], Decompressed: 1834
Downloaded: 2063 file(s) [attempted 2063/8459 = 24%, 143 KB/s], Decompressed: 1834
Downloaded: 2108 file(s) [attempted 2108/8459 = 24%, 132 KB/s], Decompressed: 1957
Downloaded: 2149 file(s) [attempted 2149/8459 = 25%, 77 KB/s], Decompressed: 1957
Downloaded: 2187 file(s) [attempted 2187/8459 = 25%, 473 KB/s], Decompressed: 1957
Downloaded: 2231 file(s) [attempted 2231/8459 = 26%, 108 KB/s], Decompressed: 2077
Downloaded: 2265 file(s) [attempted 2265/8459 = 26%, 469 KB/s], Decompressed: 2077
Downloaded: 2306 file(s) [attempted 2306/8459 = 27%, 173 KB/s], Decompressed: 2077
Downloaded: 2347 file(s) [attempted 2347/8459 = 27%, 792 KB/s], Decompressed: 2204
Downloaded: 2388 file(s) [attempted 2388/8459 = 28%, 114 KB/s], Decompressed: 2204
Downloaded: 2433 file(s) [attempted 2433/8459 = 28%, 82 KB/s], Decompressed: 2204
Downloaded: 2470 file(s) [attempted 2470/8459 = 29%, 1547 KB/s], Decompressed: 2330
Downloaded: 2511 file(s) [attempted 2511/8459 = 29%, 673 KB/s], Decompressed: 2330
Downloaded: 2556 file(s) [attempted 2556/8459 = 30%, 1432 KB/s], Decompressed: 2443
Downloaded: 2597 file(s) [attempted 2597/8459 = 30%, 37 KB/s], Decompressed: 2443
Downloaded: 2635 file(s) [attempted 2635/8459 = 31%, 294 KB/s], Decompressed: 2443
Downloaded: 2676 file(s) [attempted 2676/8459 = 31%, 233 KB/s], Decompressed: 2556
Downloaded: 2713 file(s) [attempted 2713/8459 = 32%, 1060 KB/s], Decompressed: 2556
Downloaded: 2758 file(s) [attempted 2758/8459 = 32%, 682 KB/s], Decompressed: 2556
Downloaded: 2802 file(s) [attempted 2802/8459 = 33%, 749 KB/s], Decompressed: 2676
Downloaded: 2836 file(s) [attempted 2836/8459 = 33%, 86 KB/s], Decompressed: 2676
Downloaded: 2877 file(s) [attempted 2877/8459 = 34%, 163 KB/s], Decompressed: 2676
Downloaded: 2918 file(s) [attempted 2918/8459 = 34%, 48 KB/s], Decompressed: 2676
Downloaded: 2959 file(s) [attempted 2959/8459 = 34%, 1242 KB/s], Decompressed: 2799
Downloaded: 2997 file(s) [attempted 2997/8459 = 35%, 333 KB/s], Decompressed: 2799
Downloaded: 3038 file(s) [attempted 3038/8459 = 35%, 1067 KB/s], Decompressed: 2799
Downloaded: 3076 file(s) [attempted 3076/8459 = 36%, 904 KB/s], Decompressed: 2799
Downloaded: 3103 file(s) [attempted 3103/8459 = 36%, 663 KB/s], Decompressed: 2799
Downloaded: 3105 file(s) [attempted 3105/8459 = 36%, 297 KB/s], Decompressed: 2929
Downloaded: 3106 file(s) [attempted 3106/8459 = 36%, 1153 KB/s], Decompressed: 2929
Downloaded: 3154 file(s) [attempted 3154/8459 = 37%, 0 KB/s], Decompressed: 2929
Downloaded: 3202 file(s) [attempted 3202/8459 = 37%, 166 KB/s], Decompressed: 2929
Downloaded: 3253 file(s) [attempted 3253/8459 = 38%, 185 KB/s], Decompressed: 2929
Downloaded: 3301 file(s) [attempted 3301/8459 = 39%, 153 KB/s], Decompressed: 3105
Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 681 KB/s], Decompressed: 3105
Downloaded: 3401 file(s) [attempted 3401/8459 = 40%, 68 KB/s], Decompressed: 3105
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 336 KB/s], Decompressed: 3284
Downloaded: 3500 file(s) [attempted 3500/8459 = 41%, 99 KB/s], Decompressed: 3284
Downloaded: 3548 file(s) [attempted 3548/8459 = 41%, 967 KB/s], Decompressed: 3284
Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 243 KB/s], Decompressed: 3284
Downloaded: 3636 file(s) [attempted 3636/8459 = 42%, 541 KB/s], Decompressed: 3448
Downloaded: 3671 file(s) [attempted 3671/8459 = 43%, 519 KB/s], Decompressed: 3448
Downloaded: 3708 file(s) [attempted 3708/8459 = 43%, 172 KB/s], Decompressed: 3448
Downloaded: 3746 file(s) [attempted 3746/8459 = 44%, 97 KB/s], Decompressed: 3448
Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 350 KB/s], Decompressed: 3623
Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 125 KB/s], Decompressed: 3623
Downloaded: 3862 file(s) [attempted 3862/8459 = 45%, 1018 KB/s], Decompressed: 3623
Downloaded: 3907 file(s) [attempted 3907/8459 = 46%, 62 KB/s], Decompressed: 3623
Downloaded: 3951 file(s) [attempted 3951/8459 = 46%, 326 KB/s], Decompressed: 3780
Downloaded: 3996 file(s) [attempted 3996/8459 = 47%, 196 KB/s], Decompressed: 3780
Downloaded: 4033 file(s) [attempted 4033/8459 = 47%, 925 KB/s], Decompressed: 3910
Downloaded: 4071 file(s) [attempted 4071/8459 = 48%, 465 KB/s], Decompressed: 3910
Downloaded: 4108 file(s) [attempted 4108/8459 = 48%, 156 KB/s], Decompressed: 3910
Downloaded: 4153 file(s) [attempted 4153/8459 = 49%, 43 KB/s], Decompressed: 4016
Downloaded: 4197 file(s) [attempted 4197/8459 = 49%, 310 KB/s], Decompressed: 4016
Downloaded: 4235 file(s) [attempted 4235/8459 = 50%, 82 KB/s], Decompressed: 4112
Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 88 KB/s], Decompressed: 4112
Downloaded: 4310 file(s) [attempted 4310/8459 = 50%, 87 KB/s], Decompressed: 4208
Downloaded: 4355 file(s) [attempted 4355/8459 = 51%, 350 KB/s], Decompressed: 4208
Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 34 KB/s], Decompressed: 4296
Downloaded: 4437 file(s) [attempted 4437/8459 = 52%, 706 KB/s], Decompressed: 4365
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 880 KB/s], Decompressed: 4365
Downloaded: 4515 file(s) [attempted 4515/8459 = 53%, 998 KB/s], Decompressed: 4433
Downloaded: 4556 file(s) [attempted 4556/8459 = 53%, 45 KB/s], Decompressed: 4433
Downloaded: 4597 file(s) [attempted 4597/8459 = 54%, 555 KB/s], Decompressed: 4498
Downloaded: 4638 file(s) [attempted 4638/8459 = 54%, 193 KB/s], Decompressed: 4560
Downloaded: 4683 file(s) [attempted 4683/8459 = 55%, 593 KB/s], Decompressed: 4611
Downloaded: 4720 file(s) [attempted 4720/8459 = 55%, 169 KB/s], Decompressed: 4662
Downloaded: 4761 file(s) [attempted 4761/8459 = 56%, 1333 KB/s], Decompressed: 4710
Downloaded: 4803 file(s) [attempted 4803/8459 = 56%, 175 KB/s], Decompressed: 4755
Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 228 KB/s], Decompressed: 4755
Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 1060 KB/s], Decompressed: 4803
Downloaded: 4929 file(s) [attempted 4929/8459 = 58%, 472 KB/s], Decompressed: 4857
Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 118 KB/s], Decompressed: 4857
Downloaded: 5008 file(s) [attempted 5008/8459 = 59%, 129 KB/s], Decompressed: 4915
Downloaded: 5045 file(s) [attempted 5045/8459 = 59%, 460 KB/s], Decompressed: 4970
Downloaded: 5090 file(s) [attempted 5090/8459 = 60%, 83 KB/s], Decompressed: 5018
Downloaded: 5138 file(s) [attempted 5138/8459 = 60%, 418 KB/s], Decompressed: 5018
Downloaded: 5179 file(s) [attempted 5179/8459 = 61%, 331 KB/s], Decompressed: 5086
Downloaded: 5213 file(s) [attempted 5213/8459 = 61%, 463 KB/s], Decompressed: 5148
Downloaded: 5247 file(s) [attempted 5247/8459 = 62%, 269 KB/s], Decompressed: 5148
Downloaded: 5292 file(s) [attempted 5292/8459 = 62%, 1482 KB/s], Decompressed: 5209
Downloaded: 5339 file(s) [attempted 5339/8459 = 63%, 192 KB/s], Decompressed: 5268
Downloaded: 5384 file(s) [attempted 5384/8459 = 63%, 454 KB/s], Decompressed: 5268
Downloaded: 5418 file(s) [attempted 5418/8459 = 64%, 29 KB/s], Decompressed: 5336
Downloaded: 5452 file(s) [attempted 5452/8459 = 64%, 343 KB/s], Decompressed: 5394
Downloaded: 5497 file(s) [attempted 5497/8459 = 64%, 233 KB/s], Decompressed: 5394
Downloaded: 5545 file(s) [attempted 5545/8459 = 65%, 70 KB/s], Decompressed: 5449
Downloaded: 5592 file(s) [attempted 5592/8459 = 66%, 395 KB/s], Decompressed: 5500
Downloaded: 5633 file(s) [attempted 5633/8459 = 66%, 524 KB/s], Decompressed: 5551
Downloaded: 5671 file(s) [attempted 5671/8459 = 67%, 569 KB/s], Decompressed: 5599
Downloaded: 5705 file(s) [attempted 5705/8459 = 67%, 142 KB/s], Decompressed: 5647
Downloaded: 5746 file(s) [attempted 5746/8459 = 67%, 376 KB/s], Decompressed: 5698
Downloaded: 5787 file(s) [attempted 5787/8459 = 68%, 64 KB/s], Decompressed: 5698
Downloaded: 5835 file(s) [attempted 5835/8459 = 68%, 671 KB/s], Decompressed: 5746
Downloaded: 5876 file(s) [attempted 5876/8459 = 69%, 161 KB/s], Decompressed: 5798
Downloaded: 5907 file(s) [attempted 5907/8459 = 69%, 113 KB/s], Decompressed: 5845
Downloaded: 5948 file(s) [attempted 5948/8459 = 70%, 72 KB/s], Decompressed: 5845
Downloaded: 5993 file(s) [attempted 5993/8459 = 70%, 612 KB/s], Decompressed: 5900
Downloaded: 6037 file(s) [attempted 6037/8459 = 71%, 482 KB/s], Decompressed: 5958
Downloaded: 6081 file(s) [attempted 6081/8459 = 71%, 158 KB/s], Decompressed: 5958
Downloaded: 6122 file(s) [attempted 6122/8459 = 72%, 154 KB/s], Decompressed: 6023
Downloaded: 6153 file(s) [attempted 6153/8459 = 72%, 549 KB/s], Decompressed: 6023
Downloaded: 6198 file(s) [attempted 6198/8459 = 73%, 76 KB/s], Decompressed: 6092
Downloaded: 6239 file(s) [attempted 6239/8459 = 73%, 656 KB/s], Decompressed: 6092
Downloaded: 6283 file(s) [attempted 6283/8459 = 74%, 197 KB/s], Decompressed: 6181
Downloaded: 6328 file(s) [attempted 6328/8459 = 74%, 316 KB/s], Decompressed: 6181
Downloaded: 6366 file(s) [attempted 6366/8459 = 75%, 267 KB/s], Decompressed: 6276
Downloaded: 6403 file(s) [attempted 6403/8459 = 75%, 116 KB/s], Decompressed: 6276
Downloaded: 6444 file(s) [attempted 6444/8459 = 76%, 701 KB/s], Decompressed: 6276
Downloaded: 6485 file(s) [attempted 6485/8459 = 76%, 152 KB/s], Decompressed: 6365
Downloaded: 6529 file(s) [attempted 6529/8459 = 77%, 347 KB/s], Decompressed: 6365
Downloaded: 6574 file(s) [attempted 6574/8459 = 77%, 461 KB/s], Decompressed: 6454
Downloaded: 6608 file(s) [attempted 6608/8459 = 78%, 164 KB/s], Decompressed: 6454
Downloaded: 6652 file(s) [attempted 6652/8459 = 78%, 953 KB/s], Decompressed: 6546
Downloaded: 6694 file(s) [attempted 6694/8459 = 79%, 891 KB/s], Decompressed: 6546
Downloaded: 6731 file(s) [attempted 6731/8459 = 79%, 967 KB/s], Decompressed: 6546
Downloaded: 6772 file(s) [attempted 6772/8459 = 80%, 1353 KB/s], Decompressed: 6652
Downloaded: 6810 file(s) [attempted 6810/8459 = 80%, 851 KB/s], Decompressed: 6652
Downloaded: 6851 file(s) [attempted 6851/8459 = 80%, 61 KB/s], Decompressed: 6741
Downloaded: 6895 file(s) [attempted 6895/8459 = 81%, 1896 KB/s], Decompressed: 6741
Downloaded: 6936 file(s) [attempted 6936/8459 = 81%, 304 KB/s], Decompressed: 6741
Downloaded: 6975 file(s) [attempted 6975/8459 = 82%, 52 KB/s], Decompressed: 6844
Downloaded: 7015 file(s) [attempted 7015/8459 = 82%, 133 KB/s], Decompressed: 6844
Downloaded: 7049 file(s) [attempted 7049/8459 = 83%, 1707 KB/s], Decompressed: 6943
Downloaded: 7094 file(s) [attempted 7094/8459 = 83%, 654 KB/s], Decompressed: 6943
Downloaded: 7131 file(s) [attempted 7131/8459 = 84%, 84 KB/s], Decompressed: 7039
Downloaded: 7172 file(s) [attempted 7172/8459 = 84%, 36 KB/s], Decompressed: 7039
Downloaded: 7213 file(s) [attempted 7213/8459 = 85%, 43 KB/s], Decompressed: 7039
Downloaded: 7251 file(s) [attempted 7251/8459 = 85%, 427 KB/s], Decompressed: 7128
Downloaded: 7295 file(s) [attempted 7295/8459 = 86%, 35 KB/s], Decompressed: 7128
Downloaded: 7336 file(s) [attempted 7336/8459 = 86%, 23 KB/s], Decompressed: 7220
Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 377 KB/s], Decompressed: 7220
Downloaded: 7412 file(s) [attempted 7412/8459 = 87%, 146 KB/s], Decompressed: 7316
Downloaded: 7453 file(s) [attempted 7453/8459 = 88%, 447 KB/s], Decompressed: 7316
Downloaded: 7497 file(s) [attempted 7497/8459 = 88%, 22 KB/s], Decompressed: 7401
Downloaded: 7538 file(s) [attempted 7538/8459 = 89%, 501 KB/s], Decompressed: 7401
Downloaded: 7576 file(s) [attempted 7576/8459 = 89%, 114 KB/s], Decompressed: 7401
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 341 KB/s], Decompressed: 7487
Downloaded: 7657 file(s) [attempted 7657/8459 = 90%, 471 KB/s], Decompressed: 7487
Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 448 KB/s], Decompressed: 7579
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 1632 KB/s], Decompressed: 7579
Downloaded: 7774 file(s) [attempted 7774/8459 = 91%, 306 KB/s], Decompressed: 7661
Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 1030 KB/s], Decompressed: 7661
Downloaded: 7863 file(s) [attempted 7863/8459 = 92%, 704 KB/s], Decompressed: 7743
Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 220 KB/s], Decompressed: 7743
Downloaded: 7945 file(s) [attempted 7945/8459 = 93%, 975 KB/s], Decompressed: 7743
Downloaded: 7983 file(s) [attempted 7983/8459 = 94%, 1716 KB/s], Decompressed: 7743
Downloaded: 8020 file(s) [attempted 8020/8459 = 94%, 245 KB/s], Decompressed: 7743
Downloaded: 8061 file(s) [attempted 8061/8459 = 95%, 180 KB/s], Decompressed: 7863
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 151 KB/s], Decompressed: 7863
Downloaded: 8137 file(s) [attempted 8137/8459 = 96%, 65 KB/s], Decompressed: 7863
Downloaded: 8178 file(s) [attempted 8178/8459 = 96%, 52 KB/s], Decompressed: 7863
Downloaded: 8222 file(s) [attempted 8222/8459 = 97%, 77 KB/s], Decompressed: 7863
Downloaded: 8263 file(s) [attempted 8263/8459 = 97%, 134 KB/s], Decompressed: 7863
Downloaded: 8301 file(s) [attempted 8301/8459 = 98%, 87 KB/s], Decompressed: 8037
Downloaded: 8342 file(s) [attempted 8342/8459 = 98%, 79 KB/s], Decompressed: 8037
Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 326 KB/s], Decompressed: 8037
Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 644 KB/s], Decompressed: 8037
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 678 KB/s], Decompressed: 8037
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 678 KB/s], Decompressed: 8037

apx-runtime-resource-v1	apx-verifier-job-1751-runtime-lake_cache-711490-1788189032380519916-0	3825664	4337664	21474836480	0	0	0	0	0	0	5198471168	5437927424	21474836480	0	0	0	0	0	0


$ lake build
exit_code=None duration_ms=7200007
stdout:
✔ [500/502] Built Iut.Foundations.Species (77s)
✔ [501/506] Built Iut.Foundations.SourceGameplanSpeciesMutation (141s)
✔ [784/791] Built Iut.Foundations.RealLineCopy (170s)
✔ [785/791] Built Iut.Foundations.TransportDiagram (110s)
✔ [786/791] Built Iut.Foundations.IndeterminacyRelation (137s)
✔ [787/791] Built Iut.Foundations.RegionMeasure (172s)
✔ [788/791] Built Iut.Foundations.CommonTargetBound (183s)
✔ [789/791] Built Iut.Foundations.TransportedRegionFamily (150s)
✔ [790/791] Built Iut.Foundations.QualitativeData (144s)
✔ [3508/3513] Built Iut.Foundations.EtaleThetaQuotient (504s)
✔ [3509/3513] Built Iut.Foundations.Orbicurve (1378s)
✔ [3956/3959] Built Iut.Foundations.InitialThetaData (1083s)
✔ [3962/3966] Built Iut.Foundations.OrbicurvePullback (1072s)
✔ [3965/3966] Built Iut.Foundations.EtaleThetaCovers (572s)
✔ [3971/3990] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverMapHomotopy (1199s)

stderr:
/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1751-runtime-lean_checker-711490-1788189450753716204-1 on attempt 1

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

apx-runtime-resource-v1	apx-verifier-job-1751-runtime-blueprint_build-711490-1788196651366420278-2	831488	1343488	21474836480	0	0	0	0	0	0	816369664	919945216	21474836480	0	0	0	0	0	0


blueprint_build failed; continuing (non-fatal phase).

Command runs

git_cloneexit 0duration 5s · created
git clone (github installation auth fallback)
Cloning into '/var/lib/apodeixis/repos/job-1751-source'...
git_cloneexit 128duration 224 ms · created
git clone --depth 1 --branch e21-924-checkpoint-quotient --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1751-source
Cloning into '/var/lib/apodeixis/repos/job-1751-source'...
error: unable to read askpass response from '/usr/bin/false'
fatal: could not read Username for 'https://github.com': terminal prompts disabled
git_checkoutexit 0duration 334 ms · created
git checkout f5e1b02c8e78f92adeeed7e317f97a50dbf30393
Note: switching to 'f5e1b02c8e78f92adeeed7e317f97a50dbf30393'.

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 f5e1b02 link raw and unit descent comparison leaders
lake_cacheexit 0duration 6m 58s · created
lake exe cache get
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)
✔ [7/22] Built Cache.Lean (9.8s)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (1.4s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (140ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (165ms)
✔ [13/25] Built Cache.Lean:c.o (146ms)
✔ [15/25] Built Cache.Init (295ms)
✔ [16/25] Built Cache.IO (7.8s)
✔ [17/25] Built Cache.Init:c.o (97ms)
✔ [18/25] Built Cache.IO:c.o (1.1s)
✔ [19/25] Built Cache.Hashing (889ms)
✔ [20/25] Built Cache.Hashing:c.o (352ms)
✔ [21/25] Built Cache.Requests (2.2s)
✔ [22/25] Built Cache.Requests:c.o (1.9s)
✔ [23/25] Built Cache.Main (1.0s)
✔ [24/25] Built Cache.Main:c.o (578ms)
✔ [25/25] Built cache:exe (231s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 9 KB/s], Decompressed: 9
Downloaded: 34 file(s) [attempted 34/8459 = 0%, 27 KB/s], Decompressed: 21
Downloaded: 58 file(s) [attempted 58/8459 = 0%, 230 KB/s], Decompressed: 38
Downloaded: 82 file(s) [attempted 82/8459 = 0%, 255 KB/s], Decompressed: 38
Downloaded: 110 file(s) [attempted 110/8459 = 1%, 114 KB/s], Decompressed: 57
Downloaded: 144 file(s) [attempted 144/8459 = 1%, 221 KB/s], Decompressed: 87
Downloaded: 175 file(s) [attempted 175/8459 = 2%, 290 KB/s], Decompressed: 127
Downloaded: 213 file(s) [attempted 213/8459 = 2%, 91 KB/s], Decompressed: 168
Downloaded: 247 file(s) [attempted 247/8459 = 2%, 563 KB/s], Decompressed: 206
Downloaded: 281 file(s) [attempted 281/8459 = 3%, 95 KB/s], Decompressed: 240
Downloaded: 319 file(s) [attempted 319/8459 = 3%, 463 KB/s], Decompressed: 274
Downloaded: 357 file(s) [attempted 357/8459 = 4%, 213 KB/s], Decompressed: 309
Downloaded: 394 file(s) [attempted 394/8459 = 4%, 594 KB/s], Decompressed: 339
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 528 KB/s], Decompressed: 374
Downloaded: 470 file(s) [attempted 470/8459 = 5%, 752 KB/s], Decompressed: 435
Downloaded: 507 file(s) [attempted 507/8459 = 5%, 360 KB/s], Decompressed: 466
Downloaded: 548 file(s) [attempted 548/8459 = 6%, 555 KB/s], Decompressed: 500
Downloaded: 589 file(s) [attempted 589/8459 = 6%, 43 KB/s], Decompressed: 541
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 343 KB/s], Decompressed: 541
Downloaded: 668 file(s) [attempted 668/8459 = 7%, 62 KB/s], Decompressed: 589
Downloaded: 706 file(s) [attempted 706/8459 = 8%, 268 KB/s], Decompressed: 637
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 247 KB/s], Decompressed: 637
Downloaded: 791 file(s) [attempted 791/8459 = 9%, 216 KB/s], Decompressed: 695
Downloaded: 832 file(s) [attempted 832/8459 = 9%, 348 KB/s], Decompressed: 757
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 379 KB/s], Decompressed: 812
Downloaded: 908 file(s) [attempted 908/8459 = 10%, 500 KB/s], Decompressed: 812
Downloaded: 952 file(s) [attempted 952/8459 = 11%, 867 KB/s], Decompressed: 865
Downloaded: 993 file(s) [attempted 993/8459 = 11%, 223 KB/s], Decompressed: 914
Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 538 KB/s], Decompressed: 962
Downloaded: 1075 file(s) [attempted 1075/8459 = 12%, 73 KB/s], Decompressed: 1010
Downloaded: 1109 file(s) [attempted 1109/8459 = 13%, 408 KB/s], Decompressed: 1010
Downloaded: 1154 file(s) [attempted 1154/8459 = 13%, 312 KB/s], Decompressed: 1062
Downloaded: 1195 file(s) [attempted 1195/8459 = 14%, 27 KB/s], Decompressed: 1116
Downloaded: 1239 file(s) [attempted 1239/8459 = 14%, 628 KB/s], Decompressed: 1171
Downloaded: 1284 file(s) [attempted 1284/8459 = 15%, 1624 KB/s], Decompressed: 1171
Downloaded: 1321 file(s) [attempted 1321/8459 = 15%, 755 KB/s], Decompressed: 1239
Downloaded: 1362 file(s) [attempted 1362/8459 = 16%, 216 KB/s], Decompressed: 1239
Downloaded: 1400 file(s) [attempted 1400/8459 = 16%, 180 KB/s], Decompressed: 1239
Downloaded: 1441 file(s) [attempted 1441/8459 = 17%, 164 KB/s], Decompressed: 1315
Downloaded: 1482 file(s) [attempted 1482/8459 = 17%, 414 KB/s], Decompressed: 1315
Downloaded: 1518 file(s) [attempted 1518/8459 = 17%, 345 KB/s], Decompressed: 1410
Downloaded: 1561 file(s) [attempted 1561/8459 = 18%, 45 KB/s], Decompressed: 1410
Downloaded: 1595 file(s) [attempted 1595/8459 = 18%, 21 KB/s], Decompressed: 1410
Downloaded: 1636 file(s) [attempted 1636/8459 = 19%, 479 KB/s], Decompressed: 1410
Downloaded: 1674 file(s) [attempted 1674/8459 = 19%, 58 KB/s], Decompressed: 1410
Downloaded: 1711 file(s) [attempted 1711/8459 = 20%, 215 KB/s], Decompressed: 1516
Downloaded: 1752 file(s) [attempted 1752/8459 = 20%, 268 KB/s], Decompressed: 1516
Downloaded: 1790 file(s) [attempted 1790/8459 = 21%, 247 KB/s], Decompressed: 1516
Downloaded: 1828 file(s) [attempted 1828/8459 = 21%, 138 KB/s], Decompressed: 1516
Downloaded: 1865 file(s) [attempted 1865/8459 = 22%, 288 KB/s], Decompressed: 1689
Downloaded: 1906 file(s) [attempted 1906/8459 = 22%, 233 KB/s], Decompressed: 1689
Downloaded: 1947 file(s) [attempted 1947/8459 = 23%, 1552 KB/s], Decompressed: 1689
Downloaded: 1981 file(s) [attempted 1981/8459 = 23%, 38 KB/s], Decompressed: 1834
Downloaded: 2022 file(s) [attempted 2022/8459 = 23%, 173 KB/s], Decompressed: 1834
Downloaded: 2063 file(s) [attempted 2063/8459 = 24%, 143 KB/s], Decompressed: 1834
Downloaded: 2108 file(s) [attempted 2108/8459 = 24%, 132 KB/s], Decompressed: 1957
Downloaded: 2149 file(s) [attempted 2149/8459 = 25%, 77 KB/s], Decompressed: 1957
Downloaded: 2187 file(s) [attempted 2187/8459 = 25%, 473 KB/s], Decompressed: 1957
Downloaded: 2231 file(s) [attempted 2231/8459 = 26%, 108 KB/s], Decompressed: 2077
Downloaded: 2265 file(s) [attempted 2265/8459 = 26%, 469 KB/s], Decompressed: 2077
Downloaded: 2306 file(s) [attempted 2306/8459 = 27%, 173 KB/s], Decompressed: 2077
Downloaded: 2347 file(s) [attempted 2347/8459 = 27%, 792 KB/s], Decompressed: 2204
Downloaded: 2388 file(s) [attempted 2388/8459 = 28%, 114 KB/s], Decompressed: 2204
Downloaded: 2433 file(s) [attempted 2433/8459 = 28%, 82 KB/s], Decompressed: 2204
Downloaded: 2470 file(s) [attempted 2470/8459 = 29%, 1547 KB/s], Decompressed: 2330
Downloaded: 2511 file(s) [attempted 2511/8459 = 29%, 673 KB/s], Decompressed: 2330
Downloaded: 2556 file(s) [attempted 2556/8459 = 30%, 1432 KB/s], Decompressed: 2443
Downloaded: 2597 file(s) [attempted 2597/8459 = 30%, 37 KB/s], Decompressed: 2443
Downloaded: 2635 file(s) [attempted 2635/8459 = 31%, 294 KB/s], Decompressed: 2443
Downloaded: 2676 file(s) [attempted 2676/8459 = 31%, 233 KB/s], Decompressed: 2556
Downloaded: 2713 file(s) [attempted 2713/8459 = 32%, 1060 KB/s], Decompressed: 2556
Downloaded: 2758 file(s) [attempted 2758/8459 = 32%, 682 KB/s], Decompressed: 2556
Downloaded: 2802 file(s) [attempted 2802/8459 = 33%, 749 KB/s], Decompressed: 2676
Downloaded: 2836 file(s) [attempted 2836/8459 = 33%, 86 KB/s], Decompressed: 2676
Downloaded: 2877 file(s) [attempted 2877/8459 = 34%, 163 KB/s], Decompressed: 2676
Downloaded: 2918 file(s) [attempted 2918/8459 = 34%, 48 KB/s], Decompressed: 2676
Downloaded: 2959 file(s) [attempted 2959/8459 = 34%, 1242 KB/s], Decompressed: 2799
Downloaded: 2997 file(s) [attempted 2997/8459 = 35%, 333 KB/s], Decompressed: 2799
Downloaded: 3038 file(s) [attempted 3038/8459 = 35%, 1067 KB/s], Decompressed: 2799
Downloaded: 3076 file(s) [attempted 3076/8459 = 36%, 904 KB/s], Decompressed: 2799
Downloaded: 3103 file(s) [attempted 3103/8459 = 36%, 663 KB/s], Decompressed: 2799
Downloaded: 3105 file(s) [attempted 3105/8459 = 36%, 297 KB/s], Decompressed: 2929
Downloaded: 3106 file(s) [attempted 3106/8459 = 36%, 1153 KB/s], Decompressed: 2929
Downloaded: 3154 file(s) [attempted 3154/8459 = 37%, 0 KB/s], Decompressed: 2929
Downloaded: 3202 file(s) [attempted 3202/8459 = 37%, 166 KB/s], Decompressed: 2929
Downloaded: 3253 file(s) [attempted 3253/8459 = 38%, 185 KB/s], Decompressed: 2929
Downloaded: 3301 file(s) [attempted 3301/8459 = 39%, 153 KB/s], Decompressed: 3105
Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 681 KB/s], Decompressed: 3105
Downloaded: 3401 file(s) [attempted 3401/8459 = 40%, 68 KB/s], Decompressed: 3105
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 336 KB/s], Decompressed: 3284
Downloaded: 3500 file(s) [attempted 3500/8459 = 41%, 99 KB/s], Decompressed: 3284
Downloaded: 3548 file(s) [attempted 3548/8459 = 41%, 967 KB/s], Decompressed: 3284
Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 243 KB/s], Decompressed: 3284
Downloaded: 3636 file(s) [attempted 3636/8459 = 42%, 541 KB/s], Decompressed: 3448
Downloaded: 3671 file(s) [attempted 3671/8459 = 43%, 519 KB/s], Decompressed: 3448
Downloaded: 3708 file(s) [attempted 3708/8459 = 43%, 172 KB/s], Decompressed: 3448
Downloaded: 3746 file(s) [attempted 3746/8459 = 44%, 97 KB/s], Decompressed: 3448
Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 350 KB/s], Decompressed: 3623
Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 125 KB/s], Decompressed: 3623
Downloaded: 3862 file(s) [attempted 3862/8459 = 45%, 1018 KB/s], Decompressed: 3623
Downloaded: 3907 file(s) [attempted 3907/8459 = 46%, 62 KB/s], Decompressed: 3623
Downloaded: 3951 file(s) [attempted 3951/8459 = 46%, 326 KB/s], Decompressed: 3780
Downloaded: 3996 file(s) [attempted 3996/8459 = 47%, 196 KB/s], Decompressed: 3780
Downloaded: 4033 file(s) [attempted 4033/8459 = 47%, 925 KB/s], Decompressed: 3910
Downloaded: 4071 file(s) [attempted 4071/8459 = 48%, 465 KB/s], Decompressed: 3910
Downloaded: 4108 file(s) [attempted 4108/8459 = 48%, 156 KB/s], Decompressed: 3910
Downloaded: 4153 file(s) [attempted 4153/8459 = 49%, 43 KB/s], Decompressed: 4016
Downloaded: 4197 file(s) [attempted 4197/8459 = 49%, 310 KB/s], Decompressed: 4016
Downloaded: 4235 file(s) [attempted 4235/8459 = 50%, 82 KB/s], Decompressed: 4112
Downloaded: 4276 file(s) [attempted 4276/8459 = 50%, 88 KB/s], Decompressed: 4112
Downloaded: 4310 file(s) [attempted 4310/8459 = 50%, 87 KB/s], Decompressed: 4208
Downloaded: 4355 file(s) [attempted 4355/8459 = 51%, 350 KB/s], Decompressed: 4208
Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 34 KB/s], Decompressed: 4296
Downloaded: 4437 file(s) [attempted 4437/8459 = 52%, 706 KB/s], Decompressed: 4365
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 880 KB/s], Decompressed: 4365
Downloaded: 4515 file(s) [attempted 4515/8459 = 53%, 998 KB/s], Decompressed: 4433
Downloaded: 4556 file(s) [attempted 4556/8459 = 53%, 45 KB/s], Decompressed: 4433
Downloaded: 4597 file(s) [attempted 4597/8459 = 54%, 555 KB/s], Decompressed: 4498
Downloaded: 4638 file(s) [attempted 4638/8459 = 54%, 193 KB/s], Decompressed: 4560
Downloaded: 4683 file(s) [attempted 4683/8459 = 55%, 593 KB/s], Decompressed: 4611
Downloaded: 4720 file(s) [attempted 4720/8459 = 55%, 169 KB/s], Decompressed: 4662
Downloaded: 4761 file(s) [attempted 4761/8459 = 56%, 1333 KB/s], Decompressed: 4710
Downloaded: 4803 file(s) [attempted 4803/8459 = 56%, 175 KB/s], Decompressed: 4755
Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 228 KB/s], Decompressed: 4755
Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 1060 KB/s], Decompressed: 4803
Downloaded: 4929 file(s) [attempted 4929/8459 = 58%, 472 KB/s], Decompressed: 4857
Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 118 KB/s], Decompressed: 4857
Downloaded: 5008 file(s) [attempted 5008/8459 = 59%, 129 KB/s], Decompressed: 4915
Downloaded: 5045 file(s) [attempted 5045/8459 = 59%, 460 KB/s], Decompressed: 4970
Downloaded: 5090 file(s) [attempted 5090/8459 = 60%, 83 KB/s], Decompressed: 5018
Downloaded: 5138 file(s) [attempted 5138/8459 = 60%, 418 KB/s], Decompressed: 5018
Downloaded: 5179 file(s) [attempted 5179/8459 = 61%, 331 KB/s], Decompressed: 5086
Downloaded: 5213 file(s) [attempted 5213/8459 = 61%, 463 KB/s], Decompressed: 5148
Downloaded: 5247 file(s) [attempted 5247/8459 = 62%, 269 KB/s], Decompressed: 5148
Downloaded: 5292 file(s) [attempted 5292/8459 = 62%, 1482 KB/s], Decompressed: 5209
Downloaded: 5339 file(s) [attempted 5339/8459 = 63%, 192 KB/s], Decompressed: 5268
Downloaded: 5384 file(s) [attempted 5384/8459 = 63%, 454 KB/s], Decompressed: 5268
Downloaded: 5418 file(s) [attempted 5418/8459 = 64%, 29 KB/s], Decompressed: 5336
Downloaded: 5452 file(s) [attempted 5452/8459 = 64%, 343 KB/s], Decompressed: 5394
Downloaded: 5497 file(s) [attempted 5497/8459 = 64%, 233 KB/s], Decompressed: 5394
Downloaded: 5545 file(s) [attempted 5545/8459 = 65%, 70 KB/s], Decompressed: 5449
Downloaded: 5592 file(s) [attempted 5592/8459 = 66%, 395 KB/s], Decompressed: 5500
Downloaded: 5633 file(s) [attempted 5633/8459 = 66%, 524 KB/s], Decompressed: 5551
Downloaded: 5671 file(s) [attempted 5671/8459 = 67%, 569 KB/s], Decompressed: 5599
Downloaded: 5705 file(s) [attempted 5705/8459 = 67%, 142 KB/s], Decompressed: 5647
Downloaded: 5746 file(s) [attempted 5746/8459 = 67%, 376 KB/s], Decompressed: 5698
Downloaded: 5787 file(s) [attempted 5787/8459 = 68%, 64 KB/s], Decompressed: 5698
Downloaded: 5835 file(s) [attempted 5835/8459 = 68%, 671 KB/s], Decompressed: 5746
Downloaded: 5876 file(s) [attempted 5876/8459 = 69%, 161 KB/s], Decompressed: 5798
Downloaded: 5907 file(s) [attempted 5907/8459 = 69%, 113 KB/s], Decompressed: 5845
Downloaded: 5948 file(s) [attempted 5948/8459 = 70%, 72 KB/s], Decompressed: 5845
Downloaded: 5993 file(s) [attempted 5993/8459 = 70%, 612 KB/s], Decompressed: 5900
Downloaded: 6037 file(s) [attempted 6037/8459 = 71%, 482 KB/s], Decompressed: 5958
Downloaded: 6081 file(s) [attempted 6081/8459 = 71%, 158 KB/s], Decompressed: 5958
Downloaded: 6122 file(s) [attempted 6122/8459 = 72%, 154 KB/s], Decompressed: 6023
Downloaded: 6153 file(s) [attempted 6153/8459 = 72%, 549 KB/s], Decompressed: 6023
Downloaded: 6198 file(s) [attempted 6198/8459 = 73%, 76 KB/s], Decompressed: 6092
Downloaded: 6239 file(s) [attempted 6239/8459 = 73%, 656 KB/s], Decompressed: 6092
Downloaded: 6283 file(s) [attempted 6283/8459 = 74%, 197 KB/s], Decompressed: 6181
Downloaded: 6328 file(s) [attempted 6328/8459 = 74%, 316 KB/s], Decompressed: 6181
Downloaded: 6366 file(s) [attempted 6366/8459 = 75%, 267 KB/s], Decompressed: 6276
Downloaded: 6403 file(s) [attempted 6403/8459 = 75%, 116 KB/s], Decompressed: 6276
Downloaded: 6444 file(s) [attempted 6444/8459 = 76%, 701 KB/s], Decompressed: 6276
Downloaded: 6485 file(s) [attempted 6485/8459 = 76%, 152 KB/s], Decompressed: 6365
Downloaded: 6529 file(s) [attempted 6529/8459 = 77%, 347 KB/s], Decompressed: 6365
Downloaded: 6574 file(s) [attempted 6574/8459 = 77%, 461 KB/s], Decompressed: 6454
Downloaded: 6608 file(s) [attempted 6608/8459 = 78%, 164 KB/s], Decompressed: 6454
Downloaded: 6652 file(s) [attempted 6652/8459 = 78%, 953 KB/s], Decompressed: 6546
Downloaded: 6694 file(s) [attempted 6694/8459 = 79%, 891 KB/s], Decompressed: 6546
Downloaded: 6731 file(s) [attempted 6731/8459 = 79%, 967 KB/s], Decompressed: 6546
Downloaded: 6772 file(s) [attempted 6772/8459 = 80%, 1353 KB/s], Decompressed: 6652
Downloaded: 6810 file(s) [attempted 6810/8459 = 80%, 851 KB/s], Decompressed: 6652
Downloaded: 6851 file(s) [attempted 6851/8459 = 80%, 61 KB/s], Decompressed: 6741
Downloaded: 6895 file(s) [attempted 6895/8459 = 81%, 1896 KB/s], Decompressed: 6741
Downloaded: 6936 file(s) [attempted 6936/8459 = 81%, 304 KB/s], Decompressed: 6741
Downloaded: 6975 file(s) [attempted 6975/8459 = 82%, 52 KB/s], Decompressed: 6844
Downloaded: 7015 file(s) [attempted 7015/8459 = 82%, 133 KB/s], Decompressed: 6844
Downloaded: 7049 file(s) [attempted 7049/8459 = 83%, 1707 KB/s], Decompressed: 6943
Downloaded: 7094 file(s) [attempted 7094/8459 = 83%, 654 KB/s], Decompressed: 6943
Downloaded: 7131 file(s) [attempted 7131/8459 = 84%, 84 KB/s], Decompressed: 7039
Downloaded: 7172 file(s) [attempted 7172/8459 = 84%, 36 KB/s], Decompressed: 7039
Downloaded: 7213 file(s) [attempted 7213/8459 = 85%, 43 KB/s], Decompressed: 7039
Downloaded: 7251 file(s) [attempted 7251/8459 = 85%, 427 KB/s], Decompressed: 7128
Downloaded: 7295 file(s) [attempted 7295/8459 = 86%, 35 KB/s], Decompressed: 7128
Downloaded: 7336 file(s) [attempted 7336/8459 = 86%, 23 KB/s], Decompressed: 7220
Downloaded: 7377 file(s) [attempted 7377/8459 = 87%, 377 KB/s], Decompressed: 7220
Downloaded: 7412 file(s) [attempted 7412/8459 = 87%, 146 KB/s], Decompressed: 7316
Downloaded: 7453 file(s) [attempted 7453/8459 = 88%, 447 KB/s], Decompressed: 7316
Downloaded: 7497 file(s) [attempted 7497/8459 = 88%, 22 KB/s], Decompressed: 7401
Downloaded: 7538 file(s) [attempted 7538/8459 = 89%, 501 KB/s], Decompressed: 7401
Downloaded: 7576 file(s) [attempted 7576/8459 = 89%, 114 KB/s], Decompressed: 7401
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 341 KB/s], Decompressed: 7487
Downloaded: 7657 file(s) [attempted 7657/8459 = 90%, 471 KB/s], Decompressed: 7487
Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 448 KB/s], Decompressed: 7579
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 1632 KB/s], Decompressed: 7579
Downloaded: 7774 file(s) [attempted 7774/8459 = 91%, 306 KB/s], Decompressed: 7661
Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 1030 KB/s], Decompressed: 7661
Downloaded: 7863 file(s) [attempted 7863/8459 = 92%, 704 KB/s], Decompressed: 7743
Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 220 KB/s], Decompressed: 7743
Downloaded: 7945 file(s) [attempted 7945/8459 = 93%, 975 KB/s], Decompressed: 7743
Downloaded: 7983 file(s) [attempted 7983/8459 = 94%, 1716 KB/s], Decompressed: 7743
Downloaded: 8020 file(s) [attempted 8020/8459 = 94%, 245 KB/s], Decompressed: 7743
Downloaded: 8061 file(s) [attempted 8061/8459 = 95%, 180 KB/s], Decompressed: 7863
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 151 KB/s], Decompressed: 7863
Downloaded: 8137 file(s) [attempted 8137/8459 = 96%, 65 KB/s], Decompressed: 7863
Downloaded: 8178 file(s) [attempted 8178/8459 = 96%, 52 KB/s], Decompressed: 7863
Downloaded: 8222 file(s) [attempted 8222/8459 = 97%, 77 KB/s], Decompressed: 7863
Downloaded: 8263 file(s) [attempted 8263/8459 = 97%, 134 KB/s], Decompressed: 7863
Downloaded: 8301 file(s) [attempted 8301/8459 = 98%, 87 KB/s], Decompressed: 8037
Downloaded: 8342 file(s) [attempted 8342/8459 = 98%, 79 KB/s], Decompressed: 8037
Downloaded: 8383 file(s) [attempted 8383/8459 = 99%, 326 KB/s], Decompressed: 8037
Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 644 KB/s], Decompressed: 8037
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 678 KB/s], Decompressed: 8037
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 678 KB/s], Decompressed: 8037

apx-runtime-resource-v1	apx-verifier-job-1751-runtime-lake_cache-711490-1788189032380519916-0	3825664	4337664	21474836480	0	0	0	0	0	0	5198471168	5437927424	21474836480	0	0	0	0	0	0
lean_checkerexit -duration 2h 0m · created
lake build
✔ [500/502] Built Iut.Foundations.Species (77s)
✔ [501/506] Built Iut.Foundations.SourceGameplanSpeciesMutation (141s)
✔ [784/791] Built Iut.Foundations.RealLineCopy (170s)
✔ [785/791] Built Iut.Foundations.TransportDiagram (110s)
✔ [786/791] Built Iut.Foundations.IndeterminacyRelation (137s)
✔ [787/791] Built Iut.Foundations.RegionMeasure (172s)
✔ [788/791] Built Iut.Foundations.CommonTargetBound (183s)
✔ [789/791] Built Iut.Foundations.TransportedRegionFamily (150s)
✔ [790/791] Built Iut.Foundations.QualitativeData (144s)
✔ [3508/3513] Built Iut.Foundations.EtaleThetaQuotient (504s)
✔ [3509/3513] Built Iut.Foundations.Orbicurve (1378s)
✔ [3956/3959] Built Iut.Foundations.InitialThetaData (1083s)
✔ [3962/3966] Built Iut.Foundations.OrbicurvePullback (1072s)
✔ [3965/3966] Built Iut.Foundations.EtaleThetaCovers (572s)
✔ [3971/3990] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverMapHomotopy (1199s)
/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1751-runtime-lean_checker-711490-1788189450753716204-1 on attempt 1
blueprint_buildexit 1duration 14s · created
lake build :blueprint
error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1751-runtime-blueprint_build-711490-1788196651366420278-2	831488	1343488	21474836480	0	0	0	0	0	0	816369664	919945216	21474836480	0	0	0	0	0	0

Keyboard shortcuts