Verification run
Run 1290
failedcommit
302b7f081583toolchain lean-v4-30-0prover leantook 2h 50m · finished 3w agolake 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)
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-1744-source
exit_code=Some(128) duration_ms=249
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1744-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=4247
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1744-source'...
$ git checkout 302b7f081583ca4df1e4f706b3586257e1bf6c95
exit_code=Some(0) duration_ms=284
stderr:
Note: switching to '302b7f081583ca4df1e4f706b3586257e1bf6c95'.
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 302b7f0 Merge pull request #976 from promachina/e23-3n-example63-bad-place-common-rho
Resolved source revision: 302b7f081583ca4df1e4f706b3586257e1bf6c95
Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=302b7f081583ca4df1e4f706b3586257e1bf6c95 provenance={"branch":"master","checked_out_revision":"302b7f081583ca4df1e4f706b3586257e1bf6c95","clone_url_hash":"cf9e8d307ee63ecd911d8bcd90069d4fc8cf0babed43714369c40d2e79f23390","credential_mode":"github_installation","local_clone":false,"requested_commit_sha":"302b7f081583ca4df1e4f706b3586257e1bf6c95","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=5769 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=2928508
stdout:
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)
stderr:
✔ [8/25] Built Cache.Lean (1.1s)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (1.2s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (101ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (154ms)
✔ [13/25] Built Cache.Lean:c.o (136ms)
✔ [15/25] Built Cache.Init (357ms)
✔ [16/25] Built Cache.IO (2.4s)
✔ [17/25] Built Cache.Init:c.o (102ms)
✔ [18/25] Built Cache.IO:c.o (1.2s)
✔ [19/25] Built Cache.Hashing (959ms)
✔ [20/25] Built Cache.Hashing:c.o (363ms)
✔ [21/25] Built Cache.Requests (2.2s)
✔ [22/25] Built Cache.Requests:c.o (72s)
✔ [23/25] Built Cache.Main (15s)
✔ [24/25] Built Cache.Main:c.o (1.1s)
✔ [25/25] Built cache:exe (4.7s)
Downloaded: 1 file(s) [attempted 1/8459 = 0%, 15 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 4 KB/s], Decompressed: 8
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 27 KB/s], Decompressed: 19
Downloaded: 61 file(s) [attempted 61/8459 = 0%, 37 KB/s], Decompressed: 32
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 282 KB/s], Decompressed: 54
Downloaded: 114 file(s) [attempted 114/8459 = 1%, 271 KB/s], Decompressed: 93
Downloaded: 141 file(s) [attempted 141/8459 = 1%, 380 KB/s], Decompressed: 110
Downloaded: 175 file(s) [attempted 175/8459 = 2%, 87 KB/s], Decompressed: 157
Downloaded: 209 file(s) [attempted 209/8459 = 2%, 206 KB/s], Decompressed: 175
Downloaded: 240 file(s) [attempted 240/8459 = 2%, 23 KB/s], Decompressed: 199
Downloaded: 278 file(s) [attempted 278/8459 = 3%, 622 KB/s], Decompressed: 233
Downloaded: 319 file(s) [attempted 319/8459 = 3%, 722 KB/s], Decompressed: 271
Downloaded: 357 file(s) [attempted 357/8459 = 4%, 558 KB/s], Decompressed: 271
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 192 KB/s], Decompressed: 319
Downloaded: 428 file(s) [attempted 428/8459 = 5%, 251 KB/s], Decompressed: 370
Downloaded: 466 file(s) [attempted 466/8459 = 5%, 856 KB/s], Decompressed: 370
Downloaded: 507 file(s) [attempted 507/8459 = 5%, 653 KB/s], Decompressed: 418
Downloaded: 545 file(s) [attempted 545/8459 = 6%, 64 KB/s], Decompressed: 470
Downloaded: 582 file(s) [attempted 582/8459 = 6%, 320 KB/s], Decompressed: 521
Downloaded: 621 file(s) [attempted 621/8459 = 7%, 317 KB/s], Decompressed: 521
Downloaded: 661 file(s) [attempted 661/8459 = 7%, 155 KB/s], Decompressed: 582
Downloaded: 702 file(s) [attempted 702/8459 = 8%, 230 KB/s], Decompressed: 641
Downloaded: 743 file(s) [attempted 743/8459 = 8%, 348 KB/s], Decompressed: 641
Downloaded: 784 file(s) [attempted 784/8459 = 9%, 115 KB/s], Decompressed: 699
Downloaded: 825 file(s) [attempted 825/8459 = 9%, 117 KB/s], Decompressed: 754
Downloaded: 863 file(s) [attempted 863/8459 = 10%, 281 KB/s], Decompressed: 754
Downloaded: 901 file(s) [attempted 901/8459 = 10%, 213 KB/s], Decompressed: 808
Downloaded: 945 file(s) [attempted 945/8459 = 11%, 201 KB/s], Decompressed: 808
Downloaded: 983 file(s) [attempted 983/8459 = 11%, 261 KB/s], Decompressed: 891
Downloaded: 1024 file(s) [attempted 1024/8459 = 12%, 423 KB/s], Decompressed: 891
Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 39 KB/s], Decompressed: 973
Downloaded: 1099 file(s) [attempted 1099/8459 = 12%, 681 KB/s], Decompressed: 973
Downloaded: 1139 file(s) [attempted 1139/8459 = 13%, 66 KB/s], Decompressed: 1048
Downloaded: 1181 file(s) [attempted 1181/8459 = 13%, 355 KB/s], Decompressed: 1048
Downloaded: 1222 file(s) [attempted 1222/8459 = 14%, 946 KB/s], Decompressed: 1130
Downloaded: 1263 file(s) [attempted 1263/8459 = 14%, 142 KB/s], Decompressed: 1130
Downloaded: 1304 file(s) [attempted 1304/8459 = 15%, 121 KB/s], Decompressed: 1205
Downloaded: 1342 file(s) [attempted 1342/8459 = 15%, 382 KB/s], Decompressed: 1205
Downloaded: 1380 file(s) [attempted 1380/8459 = 16%, 256 KB/s], Decompressed: 1280
Downloaded: 1424 file(s) [attempted 1424/8459 = 16%, 682 KB/s], Decompressed: 1280
Downloaded: 1462 file(s) [attempted 1462/8459 = 17%, 671 KB/s], Decompressed: 1352
Downloaded: 1499 file(s) [attempted 1499/8459 = 17%, 41 KB/s], Decompressed: 1427
Downloaded: 1537 file(s) [attempted 1537/8459 = 18%, 161 KB/s], Decompressed: 1427
Downloaded: 1578 file(s) [attempted 1578/8459 = 18%, 314 KB/s], Decompressed: 1499
Downloaded: 1622 file(s) [attempted 1622/8459 = 19%, 565 KB/s], Decompressed: 1499
Downloaded: 1663 file(s) [attempted 1663/8459 = 19%, 350 KB/s], Decompressed: 1574
Downloaded: 1701 file(s) [attempted 1701/8459 = 20%, 515 KB/s], Decompressed: 1574
Downloaded: 1739 file(s) [attempted 1739/8459 = 20%, 318 KB/s], Decompressed: 1639
Downloaded: 1783 file(s) [attempted 1783/8459 = 21%, 476 KB/s], Decompressed: 1711
Downloaded: 1824 file(s) [attempted 1824/8459 = 21%, 461 KB/s], Decompressed: 1711
Downloaded: 1869 file(s) [attempted 1869/8459 = 22%, 278 KB/s], Decompressed: 1773
Downloaded: 1910 file(s) [attempted 1910/8459 = 22%, 495 KB/s], Decompressed: 1834
Downloaded: 1947 file(s) [attempted 1947/8459 = 23%, 423 KB/s], Decompressed: 1834
Downloaded: 1985 file(s) [attempted 1985/8459 = 23%, 1216 KB/s], Decompressed: 1896
Downloaded: 2026 file(s) [attempted 2026/8459 = 23%, 295 KB/s], Decompressed: 1896
Downloaded: 2067 file(s) [attempted 2067/8459 = 24%, 349 KB/s], Decompressed: 1968
Downloaded: 2105 file(s) [attempted 2105/8459 = 24%, 884 KB/s], Decompressed: 1968
Downloaded: 2146 file(s) [attempted 2146/8459 = 25%, 671 KB/s], Decompressed: 2040
Downloaded: 2187 file(s) [attempted 2187/8459 = 25%, 517 KB/s], Decompressed: 2040
Downloaded: 2228 file(s) [attempted 2228/8459 = 26%, 156 KB/s], Decompressed: 2128
Downloaded: 2269 file(s) [attempted 2269/8459 = 26%, 122 KB/s], Decompressed: 2128
Downloaded: 2306 file(s) [attempted 2306/8459 = 27%, 171 KB/s], Decompressed: 2211
Downloaded: 2347 file(s) [attempted 2347/8459 = 27%, 804 KB/s], Decompressed: 2211
Downloaded: 2388 file(s) [attempted 2388/8459 = 28%, 229 KB/s], Decompressed: 2289
Downloaded: 2433 file(s) [attempted 2433/8459 = 28%, 23 KB/s], Decompressed: 2354
Downloaded: 2477 file(s) [attempted 2477/8459 = 29%, 158 KB/s], Decompressed: 2354
Downloaded: 2515 file(s) [attempted 2515/8459 = 29%, 240 KB/s], Decompressed: 2419
Downloaded: 2556 file(s) [attempted 2556/8459 = 30%, 160 KB/s], Decompressed: 2481
Downloaded: 2593 file(s) [attempted 2593/8459 = 30%, 155 KB/s], Decompressed: 2539
Downloaded: 2632 file(s) [attempted 2632/8459 = 31%, 330 KB/s], Decompressed: 2539
Downloaded: 2676 file(s) [attempted 2676/8459 = 31%, 417 KB/s], Decompressed: 2587
Downloaded: 2713 file(s) [attempted 2713/8459 = 32%, 176 KB/s], Decompressed: 2641
Downloaded: 2753 file(s) [attempted 2753/8459 = 32%, 49 KB/s], Decompressed: 2696
Downloaded: 2792 file(s) [attempted 2792/8459 = 33%, 462 KB/s], Decompressed: 2696
Downloaded: 2829 file(s) [attempted 2829/8459 = 33%, 36 KB/s], Decompressed: 2751
Downloaded: 2870 file(s) [attempted 2870/8459 = 33%, 1047 KB/s], Decompressed: 2751
Downloaded: 2915 file(s) [attempted 2915/8459 = 34%, 50 KB/s], Decompressed: 2816
Downloaded: 2959 file(s) [attempted 2959/8459 = 34%, 329 KB/s], Decompressed: 2884
Downloaded: 2997 file(s) [attempted 2997/8459 = 35%, 939 KB/s], Decompressed: 2884
Downloaded: 3035 file(s) [attempted 3035/8459 = 35%, 153 KB/s], Decompressed: 2953
Downloaded: 3076 file(s) [attempted 3076/8459 = 36%, 211 KB/s], Decompressed: 2953
Downloaded: 3117 file(s) [attempted 3117/8459 = 36%, 167 KB/s], Decompressed: 3028
Downloaded: 3158 file(s) [attempted 3158/8459 = 37%, 312 KB/s], Decompressed: 3028
Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 86 KB/s], Decompressed: 3103
Downloaded: 3236 file(s) [attempted 3236/8459 = 38%, 153 KB/s], Decompressed: 3103
Downloaded: 3281 file(s) [attempted 3281/8459 = 38%, 154 KB/s], Decompressed: 3178
Downloaded: 3318 file(s) [attempted 3318/8459 = 39%, 90 KB/s], Decompressed: 3178
Downloaded: 3359 file(s) [attempted 3359/8459 = 39%, 339 KB/s], Decompressed: 3264
Downloaded: 3400 file(s) [attempted 3400/8459 = 40%, 429 KB/s], Decompressed: 3264
Downloaded: 3435 file(s) [attempted 3435/8459 = 40%, 96 KB/s], Decompressed: 3264
Downloaded: 3476 file(s) [attempted 3476/8459 = 41%, 800 KB/s], Decompressed: 3359
Downloaded: 3513 file(s) [attempted 3513/8459 = 41%, 277 KB/s], Decompressed: 3359
Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 496 KB/s], Decompressed: 3359
Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 565 KB/s], Decompressed: 3465
Downloaded: 3636 file(s) [attempted 3636/8459 = 42%, 567 KB/s], Decompressed: 3465
Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 386 KB/s], Decompressed: 3568
Downloaded: 3715 file(s) [attempted 3715/8459 = 43%, 63 KB/s], Decompressed: 3568
Downloaded: 3756 file(s) [attempted 3756/8459 = 44%, 74 KB/s], Decompressed: 3568
Downloaded: 3794 file(s) [attempted 3794/8459 = 44%, 124 KB/s], Decompressed: 3667
Downloaded: 3838 file(s) [attempted 3838/8459 = 45%, 611 KB/s], Decompressed: 3667
Downloaded: 3879 file(s) [attempted 3879/8459 = 45%, 82 KB/s], Decompressed: 3766
Downloaded: 3917 file(s) [attempted 3917/8459 = 46%, 355 KB/s], Decompressed: 3766
Downloaded: 3958 file(s) [attempted 3958/8459 = 46%, 90 KB/s], Decompressed: 3766
Downloaded: 3996 file(s) [attempted 3996/8459 = 47%, 122 KB/s], Decompressed: 3872
Downloaded: 4037 file(s) [attempted 4037/8459 = 47%, 249 KB/s], Decompressed: 3872
Downloaded: 4074 file(s) [attempted 4074/8459 = 48%, 127 KB/s], Decompressed: 3975
Downloaded: 4119 file(s) [attempted 4119/8459 = 48%, 313 KB/s], Decompressed: 3975
Downloaded: 4160 file(s) [attempted 4160/8459 = 49%, 105 KB/s], Decompressed: 4067
Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 180 KB/s], Decompressed: 4067
Downloaded: 4245 file(s) [attempted 4245/8459 = 50%, 78 KB/s], Decompressed: 4160
Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 330 KB/s], Decompressed: 4160
Downloaded: 4320 file(s) [attempted 4320/8459 = 51%, 777 KB/s], Decompressed: 4160
Downloaded: 4365 file(s) [attempted 4365/8459 = 51%, 380 KB/s], Decompressed: 4245
Downloaded: 4409 file(s) [attempted 4409/8459 = 52%, 385 KB/s], Decompressed: 4245
Downloaded: 4443 file(s) [attempted 4443/8459 = 52%, 532 KB/s], Decompressed: 4334
Downloaded: 4484 file(s) [attempted 4484/8459 = 53%, 1574 KB/s], Decompressed: 4334
Downloaded: 4526 file(s) [attempted 4526/8459 = 53%, 3374 KB/s], Decompressed: 4334
Downloaded: 4567 file(s) [attempted 4567/8459 = 53%, 34 KB/s], Decompressed: 4437
Downloaded: 4608 file(s) [attempted 4608/8459 = 54%, 152 KB/s], Decompressed: 4437
Downloaded: 4645 file(s) [attempted 4645/8459 = 54%, 397 KB/s], Decompressed: 4539
Downloaded: 4683 file(s) [attempted 4683/8459 = 55%, 990 KB/s], Decompressed: 4539
Downloaded: 4727 file(s) [attempted 4727/8459 = 55%, 666 KB/s], Decompressed: 4539
Downloaded: 4768 file(s) [attempted 4768/8459 = 56%, 686 KB/s], Decompressed: 4539
Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 238 KB/s], Decompressed: 4638
Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 264 KB/s], Decompressed: 4638
Downloaded: 4891 file(s) [attempted 4891/8459 = 57%, 44 KB/s], Decompressed: 4638
Downloaded: 4932 file(s) [attempted 4932/8459 = 58%, 511 KB/s], Decompressed: 4638
Downloaded: 4977 file(s) [attempted 4977/8459 = 58%, 633 KB/s], Decompressed: 4789
Downloaded: 5021 file(s) [attempted 5021/8459 = 59%, 151 KB/s], Decompressed: 4789
Downloaded: 5059 file(s) [attempted 5059/8459 = 59%, 95 KB/s], Decompressed: 4789
Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 509 KB/s], Decompressed: 4936
Downloaded: 5134 file(s) [attempted 5134/8459 = 60%, 33 KB/s], Decompressed: 4936
Downloaded: 5179 file(s) [attempted 5179/8459 = 61%, 85 KB/s], Decompressed: 4936
Downloaded: 5223 file(s) [attempted 5223/8459 = 61%, 75 KB/s], Decompressed: 5080
Downloaded: 5261 file(s) [attempted 5261/8459 = 62%, 36 KB/s], Decompressed: 5080
Downloaded: 5298 file(s) [attempted 5298/8459 = 62%, 752 KB/s], Decompressed: 5080
Downloaded: 5339 file(s) [attempted 5339/8459 = 63%, 397 KB/s], Decompressed: 5213
Downloaded: 5380 file(s) [attempted 5380/8459 = 63%, 379 KB/s], Decompressed: 5213
Downloaded: 5425 file(s) [attempted 5425/8459 = 64%, 113 KB/s], Decompressed: 5213
Downloaded: 5462 file(s) [attempted 5462/8459 = 64%, 196 KB/s], Decompressed: 5329
Downloaded: 5500 file(s) [attempted 5500/8459 = 65%, 62 KB/s], Decompressed: 5329
Downloaded: 5541 file(s) [attempted 5541/8459 = 65%, 38 KB/s], Decompressed: 5442
Downloaded: 5582 file(s) [attempted 5582/8459 = 65%, 1086 KB/s], Decompressed: 5442
Downloaded: 5627 file(s) [attempted 5627/8459 = 66%, 43 KB/s], Decompressed: 5442
Downloaded: 5661 file(s) [attempted 5661/8459 = 66%, 151 KB/s], Decompressed: 5541
Downloaded: 5698 file(s) [attempted 5698/8459 = 67%, 823 KB/s], Decompressed: 5541
Downloaded: 5739 file(s) [attempted 5739/8459 = 67%, 573 KB/s], Decompressed: 5633
Downloaded: 5787 file(s) [attempted 5787/8459 = 68%, 950 KB/s], Decompressed: 5633
Downloaded: 5828 file(s) [attempted 5828/8459 = 68%, 1498 KB/s], Decompressed: 5716
Downloaded: 5866 file(s) [attempted 5866/8459 = 69%, 4764 KB/s], Decompressed: 5716
Downloaded: 5904 file(s) [attempted 5904/8459 = 69%, 346 KB/s], Decompressed: 5794
Downloaded: 5945 file(s) [attempted 5945/8459 = 70%, 80 KB/s], Decompressed: 5794
Downloaded: 5986 file(s) [attempted 5986/8459 = 70%, 1510 KB/s], Decompressed: 5869
Downloaded: 6030 file(s) [attempted 6030/8459 = 71%, 324 KB/s], Decompressed: 5869
Downloaded: 6071 file(s) [attempted 6071/8459 = 71%, 87 KB/s], Decompressed: 5955
Downloaded: 6112 file(s) [attempted 6112/8459 = 72%, 382 KB/s], Decompressed: 5955
Downloaded: 6150 file(s) [attempted 6150/8459 = 72%, 339 KB/s], Decompressed: 6040
Downloaded: 6194 file(s) [attempted 6194/8459 = 73%, 949 KB/s], Decompressed: 6040
Downloaded: 6235 file(s) [attempted 6235/8459 = 73%, 256 KB/s], Decompressed: 6126
Downloaded: 6280 file(s) [attempted 6280/8459 = 74%, 184 KB/s], Decompressed: 6126
Downloaded: 6317 file(s) [attempted 6317/8459 = 74%, 410 KB/s], Decompressed: 6208
Downloaded: 6358 file(s) [attempted 6358/8459 = 75%, 834 KB/s], Decompressed: 6208
Downloaded: 6396 file(s) [attempted 6396/8459 = 75%, 375 KB/s], Decompressed: 6290
Downloaded: 6437 file(s) [attempted 6437/8459 = 76%, 1269 KB/s], Decompressed: 6290
Downloaded: 6481 file(s) [attempted 6481/8459 = 76%, 333 KB/s], Decompressed: 6290
Downloaded: 6523 file(s) [attempted 6523/8459 = 77%, 87 KB/s], Decompressed: 6389
Downloaded: 6560 file(s) [attempted 6560/8459 = 77%, 161 KB/s], Decompressed: 6389
Downloaded: 6601 file(s) [attempted 6601/8459 = 78%, 152 KB/s], Decompressed: 6492
Downloaded: 6642 file(s) [attempted 6642/8459 = 78%, 226 KB/s], Decompressed: 6492
Downloaded: 6683 file(s) [attempted 6683/8459 = 79%, 1918 KB/s], Decompressed: 6492
Downloaded: 6724 file(s) [attempted 6724/8459 = 79%, 176 KB/s], Decompressed: 6492
Downloaded: 6765 file(s) [attempted 6765/8459 = 79%, 109 KB/s], Decompressed: 6587
Downloaded: 6806 file(s) [attempted 6806/8459 = 80%, 224 KB/s], Decompressed: 6587
Downloaded: 6844 file(s) [attempted 6844/8459 = 80%, 982 KB/s], Decompressed: 6587
Downloaded: 6882 file(s) [attempted 6882/8459 = 81%, 220 KB/s], Decompressed: 6587
Downloaded: 6923 file(s) [attempted 6923/8459 = 81%, 178 KB/s], Decompressed: 6587
Downloaded: 6967 file(s) [attempted 6967/8459 = 82%, 53 KB/s], Decompressed: 6587
Downloaded: 7008 file(s) [attempted 7008/8459 = 82%, 110 KB/s], Decompressed: 6587
Downloaded: 7046 file(s) [attempted 7046/8459 = 83%, 570 KB/s], Decompressed: 6587
Downloaded: 7083 file(s) [attempted 7083/8459 = 83%, 116 KB/s], Decompressed: 6765
Downloaded: 7124 file(s) [attempted 7124/8459 = 84%, 118 KB/s], Decompressed: 6765
Downloaded: 7172 file(s) [attempted 7172/8459 = 84%, 649 KB/s], Decompressed: 6765
Downloaded: 7217 file(s) [attempted 7217/8459 = 85%, 1993 KB/s], Decompressed: 6765
Downloaded: 7254 file(s) [attempted 7254/8459 = 85%, 286 KB/s], Decompressed: 6765
Downloaded: 7288 file(s) [attempted 7288/8459 = 86%, 98 KB/s], Decompressed: 6765
Downloaded: 7333 file(s) [attempted 7333/8459 = 86%, 77 KB/s], Decompressed: 6765
Downloaded: 7374 file(s) [attempted 7374/8459 = 87%, 67 KB/s], Decompressed: 6765
Downloaded: 7415 file(s) [attempted 7415/8459 = 87%, 348 KB/s], Decompressed: 6765
Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 115 KB/s], Decompressed: 7054
Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 283 KB/s], Decompressed: 7054
Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 577 KB/s], Decompressed: 7054
Downloaded: 7576 file(s) [attempted 7576/8459 = 89%, 169 KB/s], Decompressed: 7054
Downloaded: 7620 file(s) [attempted 7620/8459 = 90%, 162 KB/s], Decompressed: 7054
Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 665 KB/s], Decompressed: 7054
Downloaded: 7692 file(s) [attempted 7692/8459 = 90%, 108 KB/s], Decompressed: 7054
Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 125 KB/s], Decompressed: 7054
Downloaded: 7777 file(s) [attempted 7777/8459 = 91%, 179 KB/s], Decompressed: 7054
Downloaded: 7822 file(s) [attempted 7822/8459 = 92%, 692 KB/s], Decompressed: 7054
Downloaded: 7860 file(s) [attempted 7860/8459 = 92%, 2042 KB/s], Decompressed: 7054
Downloaded: 7897 file(s) [attempted 7897/8459 = 93%, 62 KB/s], Decompressed: 7054
Downloaded: 7938 file(s) [attempted 7938/8459 = 93%, 83 KB/s], Decompressed: 7054
Downloaded: 7983 file(s) [attempted 7983/8459 = 94%, 342 KB/s], Decompressed: 7054
Downloaded: 8024 file(s) [attempted 8024/8459 = 94%, 161 KB/s], Decompressed: 7442
Downloaded: 8068 file(s) [attempted 8068/8459 = 95%, 1800 KB/s], Decompressed: 7442
Downloaded: 8109 file(s) [attempted 8109/8459 = 95%, 130 KB/s], Decompressed: 7442
Downloaded: 8150 file(s) [attempted 8150/8459 = 96%, 174 KB/s], Decompressed: 7442
Downloaded: 8184 file(s) [attempted 8184/8459 = 96%, 356 KB/s], Decompressed: 7442
Downloaded: 8229 file(s) [attempted 8229/8459 = 97%, 542 KB/s], Decompressed: 7442
Downloaded: 8270 file(s) [attempted 8270/8459 = 97%, 151 KB/s], Decompressed: 7442
Downloaded: 8314 file(s) [attempted 8314/8459 = 98%, 179 KB/s], Decompressed: 7442
Downloaded: 8355 file(s) [attempted 8355/8459 = 98%, 195 KB/s], Decompressed: 7442
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 85 KB/s], Decompressed: 7442
Downloaded: 8434 file(s) [attempted 8434/8459 = 99%, 751 KB/s], Decompressed: 7442
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 751 KB/s], Decompressed: 7442
apx-runtime-resource-v1 apx-verifier-job-1744-runtime-lake_cache-32972-1787752053658812677-0 4014080 4149248 21474836480 0 0 0 0 0 0 543666176 5505404928 21474836480 0 0 0 0 0 0
$ lake build
exit_code=None duration_ms=7202122
stdout:
✔ [500/502] Built Iut.Foundations.Species (223s)
✔ [501/506] Built Iut.Foundations.SourceGameplanSpeciesMutation (151s)
✔ [784/791] Built Iut.Foundations.RealLineCopy (236s)
✔ [785/791] Built Iut.Foundations.TransportDiagram (97s)
✔ [786/791] Built Iut.Foundations.IndeterminacyRelation (305s)
✔ [787/791] Built Iut.Foundations.RegionMeasure (265s)
✔ [788/791] Built Iut.Foundations.CommonTargetBound (340s)
✔ [789/791] Built Iut.Foundations.TransportedRegionFamily (280s)
✔ [790/794] Built Iut.Foundations.QualitativeData (90s)
✔ [3508/3513] Built Iut.Foundations.EtaleThetaQuotient (445s)
✔ [3509/3513] Built Iut.Foundations.Orbicurve (1180s)
✔ [3956/3959] Built Iut.Foundations.InitialThetaData (1084s)
✔ [3964/3966] Built Iut.Foundations.OrbicurvePullback (1058s)
✔ [3965/3966] Built Iut.Foundations.EtaleThetaCovers (340s)
✔ [3975/3982] Built Iut.Foundations.SourceTateCurve (329s)
✔ [3981/3984] Built Iut.Foundations.GaloisImage (211s)
stderr:
/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1744-runtime-lean_checker-32972-1787754982173401635-1 on attempt 2
$ lake build :blueprint
exit_code=Some(1) duration_ms=15635
stderr:
error: unknown package facet `blueprint`
apx-runtime-resource-v1 apx-verifier-job-1744-runtime-blueprint_build-32972-1787762250800858665-2 1159168 1417216 21474836480 0 0 0 0 0 0 882814976 986849280 21474836480 0 0 0 0 0 0
blueprint_build failed; continuing (non-fatal phase).
Command runs
git_cloneexit 128
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1744-source
Cloning into '/var/lib/apodeixis/repos/job-1744-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 0
git clone (github installation auth fallback)
Cloning into '/var/lib/apodeixis/repos/job-1744-source'...
git_checkoutexit 0
git checkout 302b7f081583ca4df1e4f706b3586257e1bf6c95
Note: switching to '302b7f081583ca4df1e4f706b3586257e1bf6c95'. 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 302b7f0 Merge pull request #976 from promachina/e23-3n-example63-bad-place-common-rho
lake_cacheexit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache Decompressed 8459 file(s) Already decompressed 8459 file(s)
✔ [8/25] Built Cache.Lean (1.1s) ✔ [10/25] Built Batteries.Data.Array.Match:c.o (1.2s) ✔ [11/25] Built Batteries.Data.String.Basic:c.o (101ms) ✔ [12/25] Built Batteries.Data.String.Matcher:c.o (154ms) ✔ [13/25] Built Cache.Lean:c.o (136ms) ✔ [15/25] Built Cache.Init (357ms) ✔ [16/25] Built Cache.IO (2.4s) ✔ [17/25] Built Cache.Init:c.o (102ms) ✔ [18/25] Built Cache.IO:c.o (1.2s) ✔ [19/25] Built Cache.Hashing (959ms) ✔ [20/25] Built Cache.Hashing:c.o (363ms) ✔ [21/25] Built Cache.Requests (2.2s) ✔ [22/25] Built Cache.Requests:c.o (72s) ✔ [23/25] Built Cache.Main (15s) ✔ [24/25] Built Cache.Main:c.o (1.1s) ✔ [25/25] Built cache:exe (4.7s) Downloaded: 1 file(s) [attempted 1/8459 = 0%, 15 KB/s], Decompressed: 0 Downloaded: 15 file(s) [attempted 15/8459 = 0%, 4 KB/s], Decompressed: 8 Downloaded: 39 file(s) [attempted 39/8459 = 0%, 27 KB/s], Decompressed: 19 Downloaded: 61 file(s) [attempted 61/8459 = 0%, 37 KB/s], Decompressed: 32 Downloaded: 86 file(s) [attempted 86/8459 = 1%, 282 KB/s], Decompressed: 54 Downloaded: 114 file(s) [attempted 114/8459 = 1%, 271 KB/s], Decompressed: 93 Downloaded: 141 file(s) [attempted 141/8459 = 1%, 380 KB/s], Decompressed: 110 Downloaded: 175 file(s) [attempted 175/8459 = 2%, 87 KB/s], Decompressed: 157 Downloaded: 209 file(s) [attempted 209/8459 = 2%, 206 KB/s], Decompressed: 175 Downloaded: 240 file(s) [attempted 240/8459 = 2%, 23 KB/s], Decompressed: 199 Downloaded: 278 file(s) [attempted 278/8459 = 3%, 622 KB/s], Decompressed: 233 Downloaded: 319 file(s) [attempted 319/8459 = 3%, 722 KB/s], Decompressed: 271 Downloaded: 357 file(s) [attempted 357/8459 = 4%, 558 KB/s], Decompressed: 271 Downloaded: 391 file(s) [attempted 391/8459 = 4%, 192 KB/s], Decompressed: 319 Downloaded: 428 file(s) [attempted 428/8459 = 5%, 251 KB/s], Decompressed: 370 Downloaded: 466 file(s) [attempted 466/8459 = 5%, 856 KB/s], Decompressed: 370 Downloaded: 507 file(s) [attempted 507/8459 = 5%, 653 KB/s], Decompressed: 418 Downloaded: 545 file(s) [attempted 545/8459 = 6%, 64 KB/s], Decompressed: 470 Downloaded: 582 file(s) [attempted 582/8459 = 6%, 320 KB/s], Decompressed: 521 Downloaded: 621 file(s) [attempted 621/8459 = 7%, 317 KB/s], Decompressed: 521 Downloaded: 661 file(s) [attempted 661/8459 = 7%, 155 KB/s], Decompressed: 582 Downloaded: 702 file(s) [attempted 702/8459 = 8%, 230 KB/s], Decompressed: 641 Downloaded: 743 file(s) [attempted 743/8459 = 8%, 348 KB/s], Decompressed: 641 Downloaded: 784 file(s) [attempted 784/8459 = 9%, 115 KB/s], Decompressed: 699 Downloaded: 825 file(s) [attempted 825/8459 = 9%, 117 KB/s], Decompressed: 754 Downloaded: 863 file(s) [attempted 863/8459 = 10%, 281 KB/s], Decompressed: 754 Downloaded: 901 file(s) [attempted 901/8459 = 10%, 213 KB/s], Decompressed: 808 Downloaded: 945 file(s) [attempted 945/8459 = 11%, 201 KB/s], Decompressed: 808 Downloaded: 983 file(s) [attempted 983/8459 = 11%, 261 KB/s], Decompressed: 891 Downloaded: 1024 file(s) [attempted 1024/8459 = 12%, 423 KB/s], Decompressed: 891 Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 39 KB/s], Decompressed: 973 Downloaded: 1099 file(s) [attempted 1099/8459 = 12%, 681 KB/s], Decompressed: 973 Downloaded: 1139 file(s) [attempted 1139/8459 = 13%, 66 KB/s], Decompressed: 1048 Downloaded: 1181 file(s) [attempted 1181/8459 = 13%, 355 KB/s], Decompressed: 1048 Downloaded: 1222 file(s) [attempted 1222/8459 = 14%, 946 KB/s], Decompressed: 1130 Downloaded: 1263 file(s) [attempted 1263/8459 = 14%, 142 KB/s], Decompressed: 1130 Downloaded: 1304 file(s) [attempted 1304/8459 = 15%, 121 KB/s], Decompressed: 1205 Downloaded: 1342 file(s) [attempted 1342/8459 = 15%, 382 KB/s], Decompressed: 1205 Downloaded: 1380 file(s) [attempted 1380/8459 = 16%, 256 KB/s], Decompressed: 1280 Downloaded: 1424 file(s) [attempted 1424/8459 = 16%, 682 KB/s], Decompressed: 1280 Downloaded: 1462 file(s) [attempted 1462/8459 = 17%, 671 KB/s], Decompressed: 1352 Downloaded: 1499 file(s) [attempted 1499/8459 = 17%, 41 KB/s], Decompressed: 1427 Downloaded: 1537 file(s) [attempted 1537/8459 = 18%, 161 KB/s], Decompressed: 1427 Downloaded: 1578 file(s) [attempted 1578/8459 = 18%, 314 KB/s], Decompressed: 1499 Downloaded: 1622 file(s) [attempted 1622/8459 = 19%, 565 KB/s], Decompressed: 1499 Downloaded: 1663 file(s) [attempted 1663/8459 = 19%, 350 KB/s], Decompressed: 1574 Downloaded: 1701 file(s) [attempted 1701/8459 = 20%, 515 KB/s], Decompressed: 1574 Downloaded: 1739 file(s) [attempted 1739/8459 = 20%, 318 KB/s], Decompressed: 1639 Downloaded: 1783 file(s) [attempted 1783/8459 = 21%, 476 KB/s], Decompressed: 1711 Downloaded: 1824 file(s) [attempted 1824/8459 = 21%, 461 KB/s], Decompressed: 1711 Downloaded: 1869 file(s) [attempted 1869/8459 = 22%, 278 KB/s], Decompressed: 1773 Downloaded: 1910 file(s) [attempted 1910/8459 = 22%, 495 KB/s], Decompressed: 1834 Downloaded: 1947 file(s) [attempted 1947/8459 = 23%, 423 KB/s], Decompressed: 1834 Downloaded: 1985 file(s) [attempted 1985/8459 = 23%, 1216 KB/s], Decompressed: 1896 Downloaded: 2026 file(s) [attempted 2026/8459 = 23%, 295 KB/s], Decompressed: 1896 Downloaded: 2067 file(s) [attempted 2067/8459 = 24%, 349 KB/s], Decompressed: 1968 Downloaded: 2105 file(s) [attempted 2105/8459 = 24%, 884 KB/s], Decompressed: 1968 Downloaded: 2146 file(s) [attempted 2146/8459 = 25%, 671 KB/s], Decompressed: 2040 Downloaded: 2187 file(s) [attempted 2187/8459 = 25%, 517 KB/s], Decompressed: 2040 Downloaded: 2228 file(s) [attempted 2228/8459 = 26%, 156 KB/s], Decompressed: 2128 Downloaded: 2269 file(s) [attempted 2269/8459 = 26%, 122 KB/s], Decompressed: 2128 Downloaded: 2306 file(s) [attempted 2306/8459 = 27%, 171 KB/s], Decompressed: 2211 Downloaded: 2347 file(s) [attempted 2347/8459 = 27%, 804 KB/s], Decompressed: 2211 Downloaded: 2388 file(s) [attempted 2388/8459 = 28%, 229 KB/s], Decompressed: 2289 Downloaded: 2433 file(s) [attempted 2433/8459 = 28%, 23 KB/s], Decompressed: 2354 Downloaded: 2477 file(s) [attempted 2477/8459 = 29%, 158 KB/s], Decompressed: 2354 Downloaded: 2515 file(s) [attempted 2515/8459 = 29%, 240 KB/s], Decompressed: 2419 Downloaded: 2556 file(s) [attempted 2556/8459 = 30%, 160 KB/s], Decompressed: 2481 Downloaded: 2593 file(s) [attempted 2593/8459 = 30%, 155 KB/s], Decompressed: 2539 Downloaded: 2632 file(s) [attempted 2632/8459 = 31%, 330 KB/s], Decompressed: 2539 Downloaded: 2676 file(s) [attempted 2676/8459 = 31%, 417 KB/s], Decompressed: 2587 Downloaded: 2713 file(s) [attempted 2713/8459 = 32%, 176 KB/s], Decompressed: 2641 Downloaded: 2753 file(s) [attempted 2753/8459 = 32%, 49 KB/s], Decompressed: 2696 Downloaded: 2792 file(s) [attempted 2792/8459 = 33%, 462 KB/s], Decompressed: 2696 Downloaded: 2829 file(s) [attempted 2829/8459 = 33%, 36 KB/s], Decompressed: 2751 Downloaded: 2870 file(s) [attempted 2870/8459 = 33%, 1047 KB/s], Decompressed: 2751 Downloaded: 2915 file(s) [attempted 2915/8459 = 34%, 50 KB/s], Decompressed: 2816 Downloaded: 2959 file(s) [attempted 2959/8459 = 34%, 329 KB/s], Decompressed: 2884 Downloaded: 2997 file(s) [attempted 2997/8459 = 35%, 939 KB/s], Decompressed: 2884 Downloaded: 3035 file(s) [attempted 3035/8459 = 35%, 153 KB/s], Decompressed: 2953 Downloaded: 3076 file(s) [attempted 3076/8459 = 36%, 211 KB/s], Decompressed: 2953 Downloaded: 3117 file(s) [attempted 3117/8459 = 36%, 167 KB/s], Decompressed: 3028 Downloaded: 3158 file(s) [attempted 3158/8459 = 37%, 312 KB/s], Decompressed: 3028 Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 86 KB/s], Decompressed: 3103 Downloaded: 3236 file(s) [attempted 3236/8459 = 38%, 153 KB/s], Decompressed: 3103 Downloaded: 3281 file(s) [attempted 3281/8459 = 38%, 154 KB/s], Decompressed: 3178 Downloaded: 3318 file(s) [attempted 3318/8459 = 39%, 90 KB/s], Decompressed: 3178 Downloaded: 3359 file(s) [attempted 3359/8459 = 39%, 339 KB/s], Decompressed: 3264 Downloaded: 3400 file(s) [attempted 3400/8459 = 40%, 429 KB/s], Decompressed: 3264 Downloaded: 3435 file(s) [attempted 3435/8459 = 40%, 96 KB/s], Decompressed: 3264 Downloaded: 3476 file(s) [attempted 3476/8459 = 41%, 800 KB/s], Decompressed: 3359 Downloaded: 3513 file(s) [attempted 3513/8459 = 41%, 277 KB/s], Decompressed: 3359 Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 496 KB/s], Decompressed: 3359 Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 565 KB/s], Decompressed: 3465 Downloaded: 3636 file(s) [attempted 3636/8459 = 42%, 567 KB/s], Decompressed: 3465 Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 386 KB/s], Decompressed: 3568 Downloaded: 3715 file(s) [attempted 3715/8459 = 43%, 63 KB/s], Decompressed: 3568 Downloaded: 3756 file(s) [attempted 3756/8459 = 44%, 74 KB/s], Decompressed: 3568 Downloaded: 3794 file(s) [attempted 3794/8459 = 44%, 124 KB/s], Decompressed: 3667 Downloaded: 3838 file(s) [attempted 3838/8459 = 45%, 611 KB/s], Decompressed: 3667 Downloaded: 3879 file(s) [attempted 3879/8459 = 45%, 82 KB/s], Decompressed: 3766 Downloaded: 3917 file(s) [attempted 3917/8459 = 46%, 355 KB/s], Decompressed: 3766 Downloaded: 3958 file(s) [attempted 3958/8459 = 46%, 90 KB/s], Decompressed: 3766 Downloaded: 3996 file(s) [attempted 3996/8459 = 47%, 122 KB/s], Decompressed: 3872 Downloaded: 4037 file(s) [attempted 4037/8459 = 47%, 249 KB/s], Decompressed: 3872 Downloaded: 4074 file(s) [attempted 4074/8459 = 48%, 127 KB/s], Decompressed: 3975 Downloaded: 4119 file(s) [attempted 4119/8459 = 48%, 313 KB/s], Decompressed: 3975 Downloaded: 4160 file(s) [attempted 4160/8459 = 49%, 105 KB/s], Decompressed: 4067 Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 180 KB/s], Decompressed: 4067 Downloaded: 4245 file(s) [attempted 4245/8459 = 50%, 78 KB/s], Decompressed: 4160 Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 330 KB/s], Decompressed: 4160 Downloaded: 4320 file(s) [attempted 4320/8459 = 51%, 777 KB/s], Decompressed: 4160 Downloaded: 4365 file(s) [attempted 4365/8459 = 51%, 380 KB/s], Decompressed: 4245 Downloaded: 4409 file(s) [attempted 4409/8459 = 52%, 385 KB/s], Decompressed: 4245 Downloaded: 4443 file(s) [attempted 4443/8459 = 52%, 532 KB/s], Decompressed: 4334 Downloaded: 4484 file(s) [attempted 4484/8459 = 53%, 1574 KB/s], Decompressed: 4334 Downloaded: 4526 file(s) [attempted 4526/8459 = 53%, 3374 KB/s], Decompressed: 4334 Downloaded: 4567 file(s) [attempted 4567/8459 = 53%, 34 KB/s], Decompressed: 4437 Downloaded: 4608 file(s) [attempted 4608/8459 = 54%, 152 KB/s], Decompressed: 4437 Downloaded: 4645 file(s) [attempted 4645/8459 = 54%, 397 KB/s], Decompressed: 4539 Downloaded: 4683 file(s) [attempted 4683/8459 = 55%, 990 KB/s], Decompressed: 4539 Downloaded: 4727 file(s) [attempted 4727/8459 = 55%, 666 KB/s], Decompressed: 4539 Downloaded: 4768 file(s) [attempted 4768/8459 = 56%, 686 KB/s], Decompressed: 4539 Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 238 KB/s], Decompressed: 4638 Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 264 KB/s], Decompressed: 4638 Downloaded: 4891 file(s) [attempted 4891/8459 = 57%, 44 KB/s], Decompressed: 4638 Downloaded: 4932 file(s) [attempted 4932/8459 = 58%, 511 KB/s], Decompressed: 4638 Downloaded: 4977 file(s) [attempted 4977/8459 = 58%, 633 KB/s], Decompressed: 4789 Downloaded: 5021 file(s) [attempted 5021/8459 = 59%, 151 KB/s], Decompressed: 4789 Downloaded: 5059 file(s) [attempted 5059/8459 = 59%, 95 KB/s], Decompressed: 4789 Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 509 KB/s], Decompressed: 4936 Downloaded: 5134 file(s) [attempted 5134/8459 = 60%, 33 KB/s], Decompressed: 4936 Downloaded: 5179 file(s) [attempted 5179/8459 = 61%, 85 KB/s], Decompressed: 4936 Downloaded: 5223 file(s) [attempted 5223/8459 = 61%, 75 KB/s], Decompressed: 5080 Downloaded: 5261 file(s) [attempted 5261/8459 = 62%, 36 KB/s], Decompressed: 5080 Downloaded: 5298 file(s) [attempted 5298/8459 = 62%, 752 KB/s], Decompressed: 5080 Downloaded: 5339 file(s) [attempted 5339/8459 = 63%, 397 KB/s], Decompressed: 5213 Downloaded: 5380 file(s) [attempted 5380/8459 = 63%, 379 KB/s], Decompressed: 5213 Downloaded: 5425 file(s) [attempted 5425/8459 = 64%, 113 KB/s], Decompressed: 5213 Downloaded: 5462 file(s) [attempted 5462/8459 = 64%, 196 KB/s], Decompressed: 5329 Downloaded: 5500 file(s) [attempted 5500/8459 = 65%, 62 KB/s], Decompressed: 5329 Downloaded: 5541 file(s) [attempted 5541/8459 = 65%, 38 KB/s], Decompressed: 5442 Downloaded: 5582 file(s) [attempted 5582/8459 = 65%, 1086 KB/s], Decompressed: 5442 Downloaded: 5627 file(s) [attempted 5627/8459 = 66%, 43 KB/s], Decompressed: 5442 Downloaded: 5661 file(s) [attempted 5661/8459 = 66%, 151 KB/s], Decompressed: 5541 Downloaded: 5698 file(s) [attempted 5698/8459 = 67%, 823 KB/s], Decompressed: 5541 Downloaded: 5739 file(s) [attempted 5739/8459 = 67%, 573 KB/s], Decompressed: 5633 Downloaded: 5787 file(s) [attempted 5787/8459 = 68%, 950 KB/s], Decompressed: 5633 Downloaded: 5828 file(s) [attempted 5828/8459 = 68%, 1498 KB/s], Decompressed: 5716 Downloaded: 5866 file(s) [attempted 5866/8459 = 69%, 4764 KB/s], Decompressed: 5716 Downloaded: 5904 file(s) [attempted 5904/8459 = 69%, 346 KB/s], Decompressed: 5794 Downloaded: 5945 file(s) [attempted 5945/8459 = 70%, 80 KB/s], Decompressed: 5794 Downloaded: 5986 file(s) [attempted 5986/8459 = 70%, 1510 KB/s], Decompressed: 5869 Downloaded: 6030 file(s) [attempted 6030/8459 = 71%, 324 KB/s], Decompressed: 5869 Downloaded: 6071 file(s) [attempted 6071/8459 = 71%, 87 KB/s], Decompressed: 5955 Downloaded: 6112 file(s) [attempted 6112/8459 = 72%, 382 KB/s], Decompressed: 5955 Downloaded: 6150 file(s) [attempted 6150/8459 = 72%, 339 KB/s], Decompressed: 6040 Downloaded: 6194 file(s) [attempted 6194/8459 = 73%, 949 KB/s], Decompressed: 6040 Downloaded: 6235 file(s) [attempted 6235/8459 = 73%, 256 KB/s], Decompressed: 6126 Downloaded: 6280 file(s) [attempted 6280/8459 = 74%, 184 KB/s], Decompressed: 6126 Downloaded: 6317 file(s) [attempted 6317/8459 = 74%, 410 KB/s], Decompressed: 6208 Downloaded: 6358 file(s) [attempted 6358/8459 = 75%, 834 KB/s], Decompressed: 6208 Downloaded: 6396 file(s) [attempted 6396/8459 = 75%, 375 KB/s], Decompressed: 6290 Downloaded: 6437 file(s) [attempted 6437/8459 = 76%, 1269 KB/s], Decompressed: 6290 Downloaded: 6481 file(s) [attempted 6481/8459 = 76%, 333 KB/s], Decompressed: 6290 Downloaded: 6523 file(s) [attempted 6523/8459 = 77%, 87 KB/s], Decompressed: 6389 Downloaded: 6560 file(s) [attempted 6560/8459 = 77%, 161 KB/s], Decompressed: 6389 Downloaded: 6601 file(s) [attempted 6601/8459 = 78%, 152 KB/s], Decompressed: 6492 Downloaded: 6642 file(s) [attempted 6642/8459 = 78%, 226 KB/s], Decompressed: 6492 Downloaded: 6683 file(s) [attempted 6683/8459 = 79%, 1918 KB/s], Decompressed: 6492 Downloaded: 6724 file(s) [attempted 6724/8459 = 79%, 176 KB/s], Decompressed: 6492 Downloaded: 6765 file(s) [attempted 6765/8459 = 79%, 109 KB/s], Decompressed: 6587 Downloaded: 6806 file(s) [attempted 6806/8459 = 80%, 224 KB/s], Decompressed: 6587 Downloaded: 6844 file(s) [attempted 6844/8459 = 80%, 982 KB/s], Decompressed: 6587 Downloaded: 6882 file(s) [attempted 6882/8459 = 81%, 220 KB/s], Decompressed: 6587 Downloaded: 6923 file(s) [attempted 6923/8459 = 81%, 178 KB/s], Decompressed: 6587 Downloaded: 6967 file(s) [attempted 6967/8459 = 82%, 53 KB/s], Decompressed: 6587 Downloaded: 7008 file(s) [attempted 7008/8459 = 82%, 110 KB/s], Decompressed: 6587 Downloaded: 7046 file(s) [attempted 7046/8459 = 83%, 570 KB/s], Decompressed: 6587 Downloaded: 7083 file(s) [attempted 7083/8459 = 83%, 116 KB/s], Decompressed: 6765 Downloaded: 7124 file(s) [attempted 7124/8459 = 84%, 118 KB/s], Decompressed: 6765 Downloaded: 7172 file(s) [attempted 7172/8459 = 84%, 649 KB/s], Decompressed: 6765 Downloaded: 7217 file(s) [attempted 7217/8459 = 85%, 1993 KB/s], Decompressed: 6765 Downloaded: 7254 file(s) [attempted 7254/8459 = 85%, 286 KB/s], Decompressed: 6765 Downloaded: 7288 file(s) [attempted 7288/8459 = 86%, 98 KB/s], Decompressed: 6765 Downloaded: 7333 file(s) [attempted 7333/8459 = 86%, 77 KB/s], Decompressed: 6765 Downloaded: 7374 file(s) [attempted 7374/8459 = 87%, 67 KB/s], Decompressed: 6765 Downloaded: 7415 file(s) [attempted 7415/8459 = 87%, 348 KB/s], Decompressed: 6765 Downloaded: 7449 file(s) [attempted 7449/8459 = 88%, 115 KB/s], Decompressed: 7054 Downloaded: 7490 file(s) [attempted 7490/8459 = 88%, 283 KB/s], Decompressed: 7054 Downloaded: 7531 file(s) [attempted 7531/8459 = 89%, 577 KB/s], Decompressed: 7054 Downloaded: 7576 file(s) [attempted 7576/8459 = 89%, 169 KB/s], Decompressed: 7054 Downloaded: 7620 file(s) [attempted 7620/8459 = 90%, 162 KB/s], Decompressed: 7054 Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 665 KB/s], Decompressed: 7054 Downloaded: 7692 file(s) [attempted 7692/8459 = 90%, 108 KB/s], Decompressed: 7054 Downloaded: 7733 file(s) [attempted 7733/8459 = 91%, 125 KB/s], Decompressed: 7054 Downloaded: 7777 file(s) [attempted 7777/8459 = 91%, 179 KB/s], Decompressed: 7054 Downloaded: 7822 file(s) [attempted 7822/8459 = 92%, 692 KB/s], Decompressed: 7054 Downloaded: 7860 file(s) [attempted 7860/8459 = 92%, 2042 KB/s], Decompressed: 7054 Downloaded: 7897 file(s) [attempted 7897/8459 = 93%, 62 KB/s], Decompressed: 7054 Downloaded: 7938 file(s) [attempted 7938/8459 = 93%, 83 KB/s], Decompressed: 7054 Downloaded: 7983 file(s) [attempted 7983/8459 = 94%, 342 KB/s], Decompressed: 7054 Downloaded: 8024 file(s) [attempted 8024/8459 = 94%, 161 KB/s], Decompressed: 7442 Downloaded: 8068 file(s) [attempted 8068/8459 = 95%, 1800 KB/s], Decompressed: 7442 Downloaded: 8109 file(s) [attempted 8109/8459 = 95%, 130 KB/s], Decompressed: 7442 Downloaded: 8150 file(s) [attempted 8150/8459 = 96%, 174 KB/s], Decompressed: 7442 Downloaded: 8184 file(s) [attempted 8184/8459 = 96%, 356 KB/s], Decompressed: 7442 Downloaded: 8229 file(s) [attempted 8229/8459 = 97%, 542 KB/s], Decompressed: 7442 Downloaded: 8270 file(s) [attempted 8270/8459 = 97%, 151 KB/s], Decompressed: 7442 Downloaded: 8314 file(s) [attempted 8314/8459 = 98%, 179 KB/s], Decompressed: 7442 Downloaded: 8355 file(s) [attempted 8355/8459 = 98%, 195 KB/s], Decompressed: 7442 Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 85 KB/s], Decompressed: 7442 Downloaded: 8434 file(s) [attempted 8434/8459 = 99%, 751 KB/s], Decompressed: 7442 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 751 KB/s], Decompressed: 7442 apx-runtime-resource-v1 apx-verifier-job-1744-runtime-lake_cache-32972-1787752053658812677-0 4014080 4149248 21474836480 0 0 0 0 0 0 543666176 5505404928 21474836480 0 0 0 0 0 0
lean_checkerexit -
lake build
✔ [500/502] Built Iut.Foundations.Species (223s) ✔ [501/506] Built Iut.Foundations.SourceGameplanSpeciesMutation (151s) ✔ [784/791] Built Iut.Foundations.RealLineCopy (236s) ✔ [785/791] Built Iut.Foundations.TransportDiagram (97s) ✔ [786/791] Built Iut.Foundations.IndeterminacyRelation (305s) ✔ [787/791] Built Iut.Foundations.RegionMeasure (265s) ✔ [788/791] Built Iut.Foundations.CommonTargetBound (340s) ✔ [789/791] Built Iut.Foundations.TransportedRegionFamily (280s) ✔ [790/794] Built Iut.Foundations.QualitativeData (90s) ✔ [3508/3513] Built Iut.Foundations.EtaleThetaQuotient (445s) ✔ [3509/3513] Built Iut.Foundations.Orbicurve (1180s) ✔ [3956/3959] Built Iut.Foundations.InitialThetaData (1084s) ✔ [3964/3966] Built Iut.Foundations.OrbicurvePullback (1058s) ✔ [3965/3966] Built Iut.Foundations.EtaleThetaCovers (340s) ✔ [3975/3982] Built Iut.Foundations.SourceTateCurve (329s) ✔ [3981/3984] Built Iut.Foundations.GaloisImage (211s)
/usr/bin/podman timed out after 7200s podman cleanup removed verifier container apx-verifier-job-1744-runtime-lean_checker-32972-1787754982173401635-1 on attempt 2
blueprint_buildexit 1
lake build :blueprint
error: unknown package facet `blueprint` apx-runtime-resource-v1 apx-verifier-job-1744-runtime-blueprint_build-32972-1787762250800858665-2 1159168 1417216 21474836480 0 0 0 0 0 0 882814976 986849280 21474836480 0 0 0 0 0 0