Login

Verification run

Run 24

ImperialCollegeLondon/FLT branch main triggered via manual
succeeded commit c541ddcef7c9 toolchain lean-v4-31-0-rc2 prover lean took 6m 51s · finished 4w ago
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

$ git clone --depth 1 --branch main --single-branch https://github.com/ImperialCollegeLondon/FLT.git /var/lib/apodeixis/repos/job-515-source
exit_code=Some(0) duration_ms=969
stderr:
Cloning into '/var/lib/apodeixis/repos/job-515-source'...


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

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 c541ddc chore: bump mathlib to 96fd0ff, fix breaking changes (#1022)

Resolved source revision: c541ddcef7c95308113bed83c0c9460926bcb706

Detected prover: lean
Detected requested toolchain: lean-v4-31-0-rc2
Materialized Lean semantic helper assets
Prepared source: revision=c541ddcef7c95308113bed83c0c9460926bcb706 provenance={"branch":"main","checked_out_revision":"c541ddcef7c95308113bed83c0c9460926bcb706","clone_url_hash":"26972c4fa07707e04a8d064eb61ea9ced3487bda0b6c5e8ecd8face933c5481e","credential_mode":"none","local_clone":false,"requested_commit_sha":"c541ddcef7c95308113bed83c0c9460926bcb706","used_missing_commit_fetch":false}
Resolved toolchain: lean-v4-31-0-rc2 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
Restored Lean workspace build cache
Restored Lean semantic extraction cache
Restored 10 Lean dependency package snapshot(s)
Prepared 10 shared Lean git mirror alias(es)
Lean semantic module cache: restored exact semantic artifact is valid; skipping semantic_extract

$ lake exe cache get
exit_code=Some(0) duration_ms=114002
stdout:
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8548 file(s) from leanprover-community/mathlib4 cache
Decompressed 8522 file(s)
Already decompressed 8522 file(s)

stderr:
info: mathlib: URL has changed; deleting '/apx/source/.lake/packages/mathlib' and cloning again
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '96fd0fff3b8837985ae21dd02e712cb5df72ec05'
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
✔ [6/23] Built Cache.Lean (441ms)
✔ [11/23] Built Cache.Lean:c.o (1.4s)
✔ [13/23] Built Cache.Init (309ms)
✔ [14/23] Built Cache.IO (2.1s)
✔ [15/23] Built Cache.Init:c.o (108ms)
✔ [16/23] Built Cache.IO:c.o (1.2s)
✔ [17/23] Built Cache.Hashing (984ms)
✔ [18/23] Built Cache.Hashing:c.o (356ms)
✔ [19/23] Built Cache.Requests (1.9s)
✔ [20/23] Built Cache.Requests:c.o (1.7s)
✔ [21/23] Built Cache.Main (913ms)
✔ [22/23] Built Cache.Main:c.o (490ms)
✔ [23/23] Built cache:exe (7.6s)

Downloaded: 1 file(s) [attempted 1/8548 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8548 = 0%, 5 KB/s], Decompressed: 9
Downloaded: 35 file(s) [attempted 35/8548 = 0%, 15 KB/s], Decompressed: 24
Downloaded: 63 file(s) [attempted 63/8548 = 0%, 44 KB/s], Decompressed: 54
Downloaded: 85 file(s) [attempted 86/8548 = 1%, 107 KB/s], Decompressed: 76
Downloaded: 123 file(s) [attempted 124/8548 = 1%, 51 KB/s], Decompressed: 100
Downloaded: 157 file(s) [attempted 158/8548 = 1%, 257 KB/s], Decompressed: 120
Downloaded: 191 file(s) [attempted 192/8548 = 2%, 685 KB/s], Decompressed: 164
Downloaded: 222 file(s) [attempted 223/8548 = 2%, 287 KB/s], Decompressed: 164
Downloaded: 253 file(s) [attempted 254/8548 = 2%, 84 KB/s], Decompressed: 191
Downloaded: 298 file(s) [attempted 299/8548 = 3%, 670 KB/s], Decompressed: 226
Downloaded: 332 file(s) [attempted 333/8548 = 3%, 306 KB/s], Decompressed: 260
Downloaded: 376 file(s) [attempted 377/8548 = 4%, 113 KB/s], Decompressed: 301
Downloaded: 418 file(s) [attempted 419/8548 = 4%, 437 KB/s], Decompressed: 346
Downloaded: 452 file(s) [attempted 453/8548 = 5%, 235 KB/s], Decompressed: 397
Downloaded: 496 file(s) [attempted 497/8548 = 5%, 1157 KB/s], Decompressed: 397
Downloaded: 537 file(s) [attempted 538/8548 = 6%, 687 KB/s], Decompressed: 452
Downloaded: 575 file(s) [attempted 576/8548 = 6%, 317 KB/s], Decompressed: 452
Downloaded: 613 file(s) [attempted 614/8548 = 7%, 609 KB/s], Decompressed: 513
Downloaded: 657 file(s) [attempted 658/8548 = 7%, 1471 KB/s], Decompressed: 513
Downloaded: 698 file(s) [attempted 699/8548 = 8%, 229 KB/s], Decompressed: 596
Downloaded: 740 file(s) [attempted 741/8548 = 8%, 522 KB/s], Decompressed: 596
Downloaded: 784 file(s) [attempted 785/8548 = 9%, 419 KB/s], Decompressed: 596
Downloaded: 822 file(s) [attempted 823/8548 = 9%, 494 KB/s], Decompressed: 688
Downloaded: 866 file(s) [attempted 867/8548 = 10%, 118 KB/s], Decompressed: 688
Downloaded: 906 file(s) [attempted 908/8548 = 10%, 200 KB/s], Decompressed: 688
Downloaded: 947 file(s) [attempted 949/8548 = 11%, 328 KB/s], Decompressed: 787
Downloaded: 989 file(s) [attempted 991/8548 = 11%, 609 KB/s], Decompressed: 787
Downloaded: 1026 file(s) [attempted 1028/8548 = 12%, 58 KB/s], Decompressed: 787
Downloaded: 1067 file(s) [attempted 1069/8548 = 12%, 722 KB/s], Decompressed: 913
Downloaded: 1112 file(s) [attempted 1114/8548 = 13%, 2052 KB/s], Decompressed: 913
Downloaded: 1149 file(s) [attempted 1151/8548 = 13%, 67 KB/s], Decompressed: 913
Downloaded: 1191 file(s) [attempted 1193/8548 = 13%, 88 KB/s], Decompressed: 1054
Downloaded: 1232 file(s) [attempted 1234/8548 = 14%, 171 KB/s], Decompressed: 1054
Downloaded: 1269 file(s) [attempted 1271/8548 = 14%, 69 KB/s], Decompressed: 1054
Downloaded: 1309 file(s) [attempted 1312/8548 = 15%, 757 KB/s], Decompressed: 1054
Downloaded: 1347 file(s) [attempted 1350/8548 = 15%, 334 KB/s], Decompressed: 1184
Downloaded: 1388 file(s) [attempted 1391/8548 = 16%, 336 KB/s], Decompressed: 1184
Downloaded: 1429 file(s) [attempted 1432/8548 = 16%, 384 KB/s], Decompressed: 1184
Downloaded: 1474 file(s) [attempted 1477/8548 = 17%, 108 KB/s], Decompressed: 1323
Downloaded: 1510 file(s) [attempted 1514/8548 = 17%, 182 KB/s], Decompressed: 1323
Downloaded: 1547 file(s) [attempted 1552/8548 = 18%, 73 KB/s], Decompressed: 1323
Downloaded: 1585 file(s) [attempted 1590/8548 = 18%, 488 KB/s], Decompressed: 1323
Downloaded: 1629 file(s) [attempted 1634/8548 = 19%, 481 KB/s], Decompressed: 1470
Downloaded: 1674 file(s) [attempted 1679/8548 = 19%, 225 KB/s], Decompressed: 1470
Downloaded: 1715 file(s) [attempted 1720/8548 = 20%, 151 KB/s], Decompressed: 1470
Downloaded: 1752 file(s) [attempted 1757/8548 = 20%, 194 KB/s], Decompressed: 1470
Downloaded: 1793 file(s) [attempted 1798/8548 = 21%, 187 KB/s], Decompressed: 1612
Downloaded: 1834 file(s) [attempted 1839/8548 = 21%, 164 KB/s], Decompressed: 1612
Downloaded: 1875 file(s) [attempted 1880/8548 = 21%, 1737 KB/s], Decompressed: 1612
Downloaded: 1920 file(s) [attempted 1925/8548 = 22%, 43 KB/s], Decompressed: 1766
Downloaded: 1958 file(s) [attempted 1963/8548 = 22%, 423 KB/s], Decompressed: 1766
Downloaded: 1995 file(s) [attempted 2000/8548 = 23%, 132 KB/s], Decompressed: 1766
Downloaded: 2033 file(s) [attempted 2038/8548 = 23%, 1573 KB/s], Decompressed: 1766
Downloaded: 2074 file(s) [attempted 2079/8548 = 24%, 40 KB/s], Decompressed: 1766
Downloaded: 2115 file(s) [attempted 2120/8548 = 24%, 52 KB/s], Decompressed: 1916
Downloaded: 2156 file(s) [attempted 2161/8548 = 25%, 131 KB/s], Decompressed: 1916
Downloaded: 2197 file(s) [attempted 2202/8548 = 25%, 923 KB/s], Decompressed: 1916
Downloaded: 2235 file(s) [attempted 2240/8548 = 26%, 387 KB/s], Decompressed: 1916
Downloaded: 2279 file(s) [attempted 2284/8548 = 26%, 214 KB/s], Decompressed: 2081
Downloaded: 2317 file(s) [attempted 2322/8548 = 27%, 150 KB/s], Decompressed: 2081
Downloaded: 2361 file(s) [attempted 2366/8548 = 27%, 243 KB/s], Decompressed: 2081
Downloaded: 2402 file(s) [attempted 2407/8548 = 28%, 483 KB/s], Decompressed: 2081
Downloaded: 2444 file(s) [attempted 2449/8548 = 28%, 131 KB/s], Decompressed: 2081
Downloaded: 2485 file(s) [attempted 2490/8548 = 29%, 58 KB/s], Decompressed: 2081
Downloaded: 2529 file(s) [attempted 2534/8548 = 29%, 144 KB/s], Decompressed: 2279
Downloaded: 2567 file(s) [attempted 2572/8548 = 30%, 1171 KB/s], Decompressed: 2279
Downloaded: 2604 file(s) [attempted 2609/8548 = 30%, 354 KB/s], Decompressed: 2279
Downloaded: 2645 file(s) [attempted 2650/8548 = 31%, 152 KB/s], Decompressed: 2279
Downloaded: 2687 file(s) [attempted 2692/8548 = 31%, 259 KB/s], Decompressed: 2279
Downloaded: 2728 file(s) [attempted 2733/8548 = 31%, 107 KB/s], Decompressed: 2279
Downloaded: 2765 file(s) [attempted 2770/8548 = 32%, 122 KB/s], Decompressed: 2279
Downloaded: 2806 file(s) [attempted 2811/8548 = 32%, 416 KB/s], Decompressed: 2502
Downloaded: 2847 file(s) [attempted 2852/8548 = 33%, 532 KB/s], Decompressed: 2502
Downloaded: 2889 file(s) [attempted 2894/8548 = 33%, 857 KB/s], Decompressed: 2502
Downloaded: 2926 file(s) [attempted 2931/8548 = 34%, 915 KB/s], Decompressed: 2502
Downloaded: 2967 file(s) [attempted 2972/8548 = 34%, 570 KB/s], Decompressed: 2502
Downloaded: 3007 file(s) [attempted 3013/8548 = 35%, 233 KB/s], Decompressed: 2502
Downloaded: 3044 file(s) [attempted 3051/8548 = 35%, 88 KB/s], Decompressed: 2502
Downloaded: 3088 file(s) [attempted 3095/8548 = 36%, 145 KB/s], Decompressed: 2769
Downloaded: 3126 file(s) [attempted 3133/8548 = 36%, 153 KB/s], Decompressed: 2769
Downloaded: 3167 file(s) [attempted 3174/8548 = 37%, 345 KB/s], Decompressed: 2769
Downloaded: 3208 file(s) [attempted 3215/8548 = 37%, 55 KB/s], Decompressed: 2769
Downloaded: 3253 file(s) [attempted 3260/8548 = 38%, 395 KB/s], Decompressed: 2769
Downloaded: 3290 file(s) [attempted 3297/8548 = 38%, 3142 KB/s], Decompressed: 2769
Downloaded: 3330 file(s) [attempted 3337/8548 = 39%, 144 KB/s], Decompressed: 2769
Downloaded: 3371 file(s) [attempted 3379/8548 = 39%, 248 KB/s], Decompressed: 2769
Downloaded: 3413 file(s) [attempted 3421/8548 = 40%, 543 KB/s], Decompressed: 2769
Downloaded: 3457 file(s) [attempted 3465/8548 = 40%, 109 KB/s], Decompressed: 3071
Downloaded: 3495 file(s) [attempted 3503/8548 = 40%, 348 KB/s], Decompressed: 3071
Downloaded: 3539 file(s) [attempted 3547/8548 = 41%, 61 KB/s], Decompressed: 3071
Downloaded: 3573 file(s) [attempted 3581/8548 = 41%, 237 KB/s], Decompressed: 3071
Downloaded: 3616 file(s) [attempted 3625/8548 = 42%, 267 KB/s], Decompressed: 3071
Downloaded: 3655 file(s) [attempted 3664/8548 = 42%, 235 KB/s], Decompressed: 3071
Downloaded: 3692 file(s) [attempted 3701/8548 = 43%, 234 KB/s], Decompressed: 3071
Downloaded: 3737 file(s) [attempted 3746/8548 = 43%, 171 KB/s], Decompressed: 3071
Downloaded: 3774 file(s) [attempted 3783/8548 = 44%, 282 KB/s], Decompressed: 3071
Downloaded: 3815 file(s) [attempted 3824/8548 = 44%, 466 KB/s], Decompressed: 3071
Downloaded: 3856 file(s) [attempted 3865/8548 = 45%, 24 KB/s], Decompressed: 3440
Downloaded: 3894 file(s) [attempted 3903/8548 = 45%, 569 KB/s], Decompressed: 3440
Downloaded: 3935 file(s) [attempted 3944/8548 = 46%, 385 KB/s], Decompressed: 3440
Downloaded: 3976 file(s) [attempted 3985/8548 = 46%, 340 KB/s], Decompressed: 3440
Downloaded: 4017 file(s) [attempted 4026/8548 = 47%, 1833 KB/s], Decompressed: 3440
Downloaded: 4052 file(s) [attempted 4061/8548 = 47%, 647 KB/s], Decompressed: 3440
Downloaded: 4089 file(s) [attempted 4098/8548 = 47%, 616 KB/s], Decompressed: 3440
Downloaded: 4133 file(s) [attempted 4143/8548 = 48%, 3424 KB/s], Decompressed: 3440
Downloaded: 4177 file(s) [attempted 4187/8548 = 48%, 49 KB/s], Decompressed: 3440
Downloaded: 4221 file(s) [attempted 4232/8548 = 49%, 322 KB/s], Decompressed: 3440
Downloaded: 4260 file(s) [attempted 4271/8548 = 49%, 497 KB/s], Decompressed: 3440
Downloaded: 4293 file(s) [attempted 4304/8548 = 50%, 312 KB/s], Decompressed: 3832
Downloaded: 4334 file(s) [attempted 4345/8548 = 50%, 168 KB/s], Decompressed: 3832
Downloaded: 4378 file(s) [attempted 4389/8548 = 51%, 870 KB/s], Decompressed: 3832
Downloaded: 4423 file(s) [attempted 4434/8548 = 51%, 192 KB/s], Decompressed: 3832
Downloaded: 4467 file(s) [attempted 4478/8548 = 52%, 720 KB/s], Decompressed: 3832
Downloaded: 4508 file(s) [attempted 4519/8548 = 52%, 880 KB/s], Decompressed: 3832
Downloaded: 4546 file(s) [attempted 4557/8548 = 53%, 73 KB/s], Decompressed: 3832
Downloaded: 4580 file(s) [attempted 4591/8548 = 53%, 23 KB/s], Decompressed: 3832
Downloaded: 4624 file(s) [attempted 4635/8548 = 54%, 336 KB/s], Decompressed: 3832
Downloaded: 4669 file(s) [attempted 4680/8548 = 54%, 1130 KB/s], Decompressed: 3832
Downloaded: 4713 file(s) [attempted 4725/8548 = 55%, 69 KB/s], Decompressed: 3832
Downloaded: 4750 file(s) [attempted 4762/8548 = 55%, 24 KB/s], Decompressed: 3832
Downloaded: 4791 file(s) [attempted 4803/8548 = 56%, 21 KB/s], Decompressed: 3832
Downloaded: 4829 file(s) [attempted 4841/8548 = 56%, 336 KB/s], Decompressed: 4275
Downloaded: 4873 file(s) [attempted 4885/8548 = 57%, 193 KB/s], Decompressed: 4275
Downloaded: 4914 file(s) [attempted 4926/8548 = 57%, 545 KB/s], Decompressed: 4275
Downloaded: 4955 file(s) [attempted 4967/8548 = 58%, 538 KB/s], Decompressed: 4275
Downloaded: 4992 file(s) [attempted 5005/8548 = 58%, 190 KB/s], Decompressed: 4275
Downloaded: 5030 file(s) [attempted 5043/8548 = 58%, 1102 KB/s], Decompressed: 4275
Downloaded: 5074 file(s) [attempted 5087/8548 = 59%, 327 KB/s], Decompressed: 4275
Downloaded: 5115 file(s) [attempted 5128/8548 = 59%, 150 KB/s], Decompressed: 4275
Downloaded: 5156 file(s) [attempted 5169/8548 = 60%, 90 KB/s], Decompressed: 4275
Downloaded: 5201 file(s) [attempted 5214/8548 = 60%, 1226 KB/s], Decompressed: 4275
Downloaded: 5245 file(s) [attempted 5258/8548 = 61%, 116 KB/s], Decompressed: 4275
Downloaded: 5286 file(s) [attempted 5299/8548 = 61%, 97 KB/s], Decompressed: 4275
Downloaded: 5331 file(s) [attempted 5344/8548 = 62%, 488 KB/s], Decompressed: 4275
Downloaded: 5372 file(s) [attempted 5385/8548 = 62%, 46 KB/s], Decompressed: 4275
Downloaded: 5410 file(s) [attempted 5423/8548 = 63%, 702 KB/s], Decompressed: 4275
Downloaded: 5447 file(s) [attempted 5460/8548 = 63%, 371 KB/s], Decompressed: 4825
Downloaded: 5492 file(s) [attempted 5505/8548 = 64%, 100 KB/s], Decompressed: 4825
Downloaded: 5536 file(s) [attempted 5549/8548 = 64%, 194 KB/s], Decompressed: 4825
Downloaded: 5577 file(s) [attempted 5590/8548 = 65%, 80 KB/s], Decompressed: 4825
Downloaded: 5618 file(s) [attempted 5631/8548 = 65%, 869 KB/s], Decompressed: 4825
Downloaded: 5656 file(s) [attempted 5669/8548 = 66%, 130 KB/s], Decompressed: 4825
Downloaded: 5694 file(s) [attempted 5707/8548 = 66%, 116 KB/s], Decompressed: 4825
Downloaded: 5738 file(s) [attempted 5751/8548 = 67%, 109 KB/s], Decompressed: 4825
Downloaded: 5786 file(s) [attempted 5799/8548 = 67%, 263 KB/s], Decompressed: 4825
Downloaded: 5831 file(s) [attempted 5847/8548 = 68%, 655 KB/s], Decompressed: 4825
Downloaded: 5869 file(s) [attempted 5885/8548 = 68%, 116 KB/s], Decompressed: 4825
Downloaded: 5910 file(s) [attempted 5926/8548 = 69%, 108 KB/s], Decompressed: 4825
Downloaded: 5944 file(s) [attempted 5960/8548 = 69%, 47 KB/s], Decompressed: 4825
Downloaded: 5985 file(s) [attempted 6001/8548 = 70%, 61 KB/s], Decompressed: 4825
Downloaded: 6025 file(s) [attempted 6042/8548 = 70%, 206 KB/s], Decompressed: 4825
Downloaded: 6070 file(s) [attempted 6087/8548 = 71%, 27 KB/s], Decompressed: 4825
Downloaded: 6111 file(s) [attempted 6128/8548 = 71%, 23 KB/s], Decompressed: 5427
Downloaded: 6148 file(s) [attempted 6165/8548 = 72%, 26 KB/s], Decompressed: 5427
Downloaded: 6189 file(s) [attempted 6206/8548 = 72%, 730 KB/s], Decompressed: 5427
Downloaded: 6237 file(s) [attempted 6254/8548 = 73%, 481 KB/s], Decompressed: 5427
Downloaded: 6277 file(s) [attempted 6294/8548 = 73%, 152 KB/s], Decompressed: 5427
Downloaded: 6316 file(s) [attempted 6333/8548 = 74%, 835 KB/s], Decompressed: 5427
Downloaded: 6350 file(s) [attempted 6367/8548 = 74%, 1064 KB/s], Decompressed: 5427
Downloaded: 6384 file(s) [attempted 6402/8548 = 74%, 337 KB/s], Decompressed: 5427
Downloaded: 6431 file(s) [attempted 6449/8548 = 75%, 283 KB/s], Decompressed: 5427
Downloaded: 6475 file(s) [attempted 6494/8548 = 75%, 84 KB/s], Decompressed: 5427
Downloaded: 6516 file(s) [attempted 6535/8548 = 76%, 1775 KB/s], Decompressed: 5427
Downloaded: 6553 file(s) [attempted 6573/8548 = 76%, 425 KB/s], Decompressed: 5427
Downloaded: 6590 file(s) [attempted 6610/8548 = 77%, 542 KB/s], Decompressed: 5427
Downloaded: 6631 file(s) [attempted 6651/8548 = 77%, 362 KB/s], Decompressed: 5427
Downloaded: 6676 file(s) [attempted 6696/8548 = 78%, 225 KB/s], Decompressed: 5427
Downloaded: 6717 file(s) [attempted 6737/8548 = 78%, 172 KB/s], Decompressed: 5427
Downloaded: 6755 file(s) [attempted 6775/8548 = 79%, 58 KB/s], Decompressed: 5427
Downloaded: 6796 file(s) [attempted 6816/8548 = 79%, 62 KB/s], Decompressed: 5427
Downloaded: 6840 file(s) [attempted 6860/8548 = 80%, 239 KB/s], Decompressed: 6080
Downloaded: 6874 file(s) [attempted 6894/8548 = 80%, 83 KB/s], Decompressed: 6080
Downloaded: 6914 file(s) [attempted 6935/8548 = 81%, 459 KB/s], Decompressed: 6080
Downloaded: 6952 file(s) [attempted 6973/8548 = 81%, 115 KB/s], Decompressed: 6080
Downloaded: 6992 file(s) [attempted 7014/8548 = 82%, 251 KB/s], Decompressed: 6080
Downloaded: 7033 file(s) [attempted 7055/8548 = 82%, 380 KB/s], Decompressed: 6080
Downloaded: 7073 file(s) [attempted 7096/8548 = 83%, 258 KB/s], Decompressed: 6080
Downloaded: 7110 file(s) [attempted 7133/8548 = 83%, 99 KB/s], Decompressed: 6080
Downloaded: 7149 file(s) [attempted 7172/8548 = 83%, 69 KB/s], Decompressed: 6080
Downloaded: 7186 file(s) [attempted 7209/8548 = 84%, 148 KB/s], Decompressed: 6080
Downloaded: 7231 file(s) [attempted 7254/8548 = 84%, 106 KB/s], Decompressed: 6080
Downloaded: 7272 file(s) [attempted 7295/8548 = 85%, 329 KB/s], Decompressed: 6080
Downloaded: 7309 file(s) [attempted 7332/8548 = 85%, 358 KB/s], Decompressed: 6080
Downloaded: 7354 file(s) [attempted 7377/8548 = 86%, 278 KB/s], Decompressed: 6080
Downloaded: 7395 file(s) [attempted 7418/8548 = 86%, 583 KB/s], Decompressed: 6080
Downloaded: 7436 file(s) [attempted 7459/8548 = 87%, 583 KB/s], Decompressed: 6080
Downloaded: 7476 file(s) [attempted 7500/8548 = 87%, 614 KB/s], Decompressed: 6080
Downloaded: 7510 file(s) [attempted 7534/8548 = 88%, 235 KB/s], Decompressed: 6080
Downloaded: 7551 file(s) [attempted 7575/8548 = 88%, 318 KB/s], Decompressed: 6080
Downloaded: 7593 file(s) [attempted 7617/8548 = 89%, 631 KB/s], Decompressed: 6802
Downloaded: 7634 file(s) [attempted 7658/8548 = 89%, 119 KB/s], Decompressed: 6802
Downloaded: 7669 file(s) [attempted 7693/8548 = 89%, 217 KB/s], Decompressed: 6802
Downloaded: 7709 file(s) [attempted 7733/8548 = 90%, 297 KB/s], Decompressed: 6802
Downloaded: 7747 file(s) [attempted 7771/8548 = 90%, 285 KB/s], Decompressed: 6802
Downloaded: 7791 file(s) [attempted 7815/8548 = 91%, 577 KB/s], Decompressed: 6802
Downloaded: 7828 file(s) [attempted 7853/8548 = 91%, 560 KB/s], Decompressed: 6802
Downloaded: 7869 file(s) [attempted 7894/8548 = 92%, 978 KB/s], Decompressed: 6802
Downloaded: 7910 file(s) [attempted 7935/8548 = 92%, 214 KB/s], Decompressed: 6802
Downloaded: 7954 file(s) [attempted 7979/8548 = 93%, 868 KB/s], Decompressed: 6802
Downloaded: 7995 file(s) [attempted 8020/8548 = 93%, 334 KB/s], Decompressed: 6802
Downloaded: 8033 file(s) [attempted 8058/8548 = 94%, 374 KB/s], Decompressed: 6802
Downloaded: 8078 file(s) [attempted 8103/8548 = 94%, 157 KB/s], Decompressed: 6802
Downloaded: 8122 file(s) [attempted 8147/8548 = 95%, 178 KB/s], Decompressed: 6802
Downloaded: 8163 file(s) [attempted 8188/8548 = 95%, 368 KB/s], Decompressed: 6802
Downloaded: 8204 file(s) [attempted 8229/8548 = 96%, 76 KB/s], Decompressed: 6802
Downloaded: 8245 file(s) [attempted 8270/8548 = 96%, 197 KB/s], Decompressed: 6802
Downloaded: 8279 file(s) [attempted 8304/8548 = 97%, 791 KB/s], Decompressed: 6802
Downloaded: 8324 file(s) [attempted 8349/8548 = 97%, 1626 KB/s], Decompressed: 6802
Downloaded: 8361 file(s) [attempted 8387/8548 = 98%, 628 KB/s], Decompressed: 6802
Downloaded: 8405 file(s) [attempted 8431/8548 = 98%, 80 KB/s], Decompressed: 6802
Downloaded: 8443 file(s) [attempted 8469/8548 = 99%, 335 KB/s], Decompressed: 6802
Downloaded: 8480 file(s) [attempted 8506/8548 = 99%, 65 KB/s], Decompressed: 7586
Downloaded: 8518 file(s) [attempted 8544/8548 = 99%, 503 KB/s], Decompressed: 7586
Downloaded: 8521 file(s) [attempted 8547/8548 = 99%, 715 KB/s], Decompressed: 7586
Downloaded: 8522 file(s) [attempted 8548/8548 = 100%, 715 KB/s], Decompressed: 7586
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.

  * If you push your commits to a PR to the mathlib4 repository
    (use a draft PR if it is not ready for review),
    then CI will build the oleans and they will be available later.
  * If you have already opened a PR, this may mean
    the CI build has failed part-way through building.


$ lake build
exit_code=Some(0) duration_ms=31479
stdout:
Build completed successfully (4011 jobs).

stderr:
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ lake build :blueprint
exit_code=Some(1) duration_ms=1270
stderr:
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: unknown package facet `blueprint`


blueprint_build failed; continuing (non-fatal phase).
Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

git_clone exit 0 duration 969 ms · created 
git clone --depth 1 --branch main --single-branch https://github.com/ImperialCollegeLondon/FLT.git /var/lib/apodeixis/repos/job-515-source
Cloning into '/var/lib/apodeixis/repos/job-515-source'...
git_checkout exit 0 duration 45 ms · created 
git checkout c541ddcef7c95308113bed83c0c9460926bcb706
Note: switching to 'c541ddcef7c95308113bed83c0c9460926bcb706'.

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 c541ddc chore: bump mathlib to 96fd0ff, fix breaking changes (#1022)
lake_cache exit 0 duration 1m 54s · created 
lake exe cache get
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8548 file(s) from leanprover-community/mathlib4 cache
Decompressed 8522 file(s)
Already decompressed 8522 file(s)

info: mathlib: URL has changed; deleting '/apx/source/.lake/packages/mathlib' and cloning again
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '96fd0fff3b8837985ae21dd02e712cb5df72ec05'
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
✔ [6/23] Built Cache.Lean (441ms)
✔ [11/23] Built Cache.Lean:c.o (1.4s)
✔ [13/23] Built Cache.Init (309ms)
✔ [14/23] Built Cache.IO (2.1s)
✔ [15/23] Built Cache.Init:c.o (108ms)
✔ [16/23] Built Cache.IO:c.o (1.2s)
✔ [17/23] Built Cache.Hashing (984ms)
✔ [18/23] Built Cache.Hashing:c.o (356ms)
✔ [19/23] Built Cache.Requests (1.9s)
✔ [20/23] Built Cache.Requests:c.o (1.7s)
✔ [21/23] Built Cache.Main (913ms)
✔ [22/23] Built Cache.Main:c.o (490ms)
✔ [23/23] Built cache:exe (7.6s)

Downloaded: 1 file(s) [attempted 1/8548 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8548 = 0%, 5 KB/s], Decompressed: 9
Downloaded: 35 file(s) [attempted 35/8548 = 0%, 15 KB/s], Decompressed: 24
Downloaded: 63 file(s) [attempted 63/8548 = 0%, 44 KB/s], Decompressed: 54
Downloaded: 85 file(s) [attempted 86/8548 = 1%, 107 KB/s], Decompressed: 76
Downloaded: 123 file(s) [attempted 124/8548 = 1%, 51 KB/s], Decompressed: 100
Downloaded: 157 file(s) [attempted 158/8548 = 1%, 257 KB/s], Decompressed: 120
Downloaded: 191 file(s) [attempted 192/8548 = 2%, 685 KB/s], Decompressed: 164
Downloaded: 222 file(s) [attempted 223/8548 = 2%, 287 KB/s], Decompressed: 164
Downloaded: 253 file(s) [attempted 254/8548 = 2%, 84 KB/s], Decompressed: 191
Downloaded: 298 file(s) [attempted 299/8548 = 3%, 670 KB/s], Decompressed: 226
Downloaded: 332 file(s) [attempted 333/8548 = 3%, 306 KB/s], Decompressed: 260
Downloaded: 376 file(s) [attempted 377/8548 = 4%, 113 KB/s], Decompressed: 301
Downloaded: 418 file(s) [attempted 419/8548 = 4%, 437 KB/s], Decompressed: 346
Downloaded: 452 file(s) [attempted 453/8548 = 5%, 235 KB/s], Decompressed: 397
Downloaded: 496 file(s) [attempted 497/8548 = 5%, 1157 KB/s], Decompressed: 397
Downloaded: 537 file(s) [attempted 538/8548 = 6%, 687 KB/s], Decompressed: 452
Downloaded: 575 file(s) [attempted 576/8548 = 6%, 317 KB/s], Decompressed: 452
Downloaded: 613 file(s) [attempted 614/8548 = 7%, 609 KB/s], Decompressed: 513
Downloaded: 657 file(s) [attempted 658/8548 = 7%, 1471 KB/s], Decompressed: 513
Downloaded: 698 file(s) [attempted 699/8548 = 8%, 229 KB/s], Decompressed: 596
Downloaded: 740 file(s) [attempted 741/8548 = 8%, 522 KB/s], Decompressed: 596
Downloaded: 784 file(s) [attempted 785/8548 = 9%, 419 KB/s], Decompressed: 596
Downloaded: 822 file(s) [attempted 823/8548 = 9%, 494 KB/s], Decompressed: 688
Downloaded: 866 file(s) [attempted 867/8548 = 10%, 118 KB/s], Decompressed: 688
Downloaded: 906 file(s) [attempted 908/8548 = 10%, 200 KB/s], Decompressed: 688
Downloaded: 947 file(s) [attempted 949/8548 = 11%, 328 KB/s], Decompressed: 787
Downloaded: 989 file(s) [attempted 991/8548 = 11%, 609 KB/s], Decompressed: 787
Downloaded: 1026 file(s) [attempted 1028/8548 = 12%, 58 KB/s], Decompressed: 787
Downloaded: 1067 file(s) [attempted 1069/8548 = 12%, 722 KB/s], Decompressed: 913
Downloaded: 1112 file(s) [attempted 1114/8548 = 13%, 2052 KB/s], Decompressed: 913
Downloaded: 1149 file(s) [attempted 1151/8548 = 13%, 67 KB/s], Decompressed: 913
Downloaded: 1191 file(s) [attempted 1193/8548 = 13%, 88 KB/s], Decompressed: 1054
Downloaded: 1232 file(s) [attempted 1234/8548 = 14%, 171 KB/s], Decompressed: 1054
Downloaded: 1269 file(s) [attempted 1271/8548 = 14%, 69 KB/s], Decompressed: 1054
Downloaded: 1309 file(s) [attempted 1312/8548 = 15%, 757 KB/s], Decompressed: 1054
Downloaded: 1347 file(s) [attempted 1350/8548 = 15%, 334 KB/s], Decompressed: 1184
Downloaded: 1388 file(s) [attempted 1391/8548 = 16%, 336 KB/s], Decompressed: 1184
Downloaded: 1429 file(s) [attempted 1432/8548 = 16%, 384 KB/s], Decompressed: 1184
Downloaded: 1474 file(s) [attempted 1477/8548 = 17%, 108 KB/s], Decompressed: 1323
Downloaded: 1510 file(s) [attempted 1514/8548 = 17%, 182 KB/s], Decompressed: 1323
Downloaded: 1547 file(s) [attempted 1552/8548 = 18%, 73 KB/s], Decompressed: 1323
Downloaded: 1585 file(s) [attempted 1590/8548 = 18%, 488 KB/s], Decompressed: 1323
Downloaded: 1629 file(s) [attempted 1634/8548 = 19%, 481 KB/s], Decompressed: 1470
Downloaded: 1674 file(s) [attempted 1679/8548 = 19%, 225 KB/s], Decompressed: 1470
Downloaded: 1715 file(s) [attempted 1720/8548 = 20%, 151 KB/s], Decompressed: 1470
Downloaded: 1752 file(s) [attempted 1757/8548 = 20%, 194 KB/s], Decompressed: 1470
Downloaded: 1793 file(s) [attempted 1798/8548 = 21%, 187 KB/s], Decompressed: 1612
Downloaded: 1834 file(s) [attempted 1839/8548 = 21%, 164 KB/s], Decompressed: 1612
Downloaded: 1875 file(s) [attempted 1880/8548 = 21%, 1737 KB/s], Decompressed: 1612
Downloaded: 1920 file(s) [attempted 1925/8548 = 22%, 43 KB/s], Decompressed: 1766
Downloaded: 1958 file(s) [attempted 1963/8548 = 22%, 423 KB/s], Decompressed: 1766
Downloaded: 1995 file(s) [attempted 2000/8548 = 23%, 132 KB/s], Decompressed: 1766
Downloaded: 2033 file(s) [attempted 2038/8548 = 23%, 1573 KB/s], Decompressed: 1766
Downloaded: 2074 file(s) [attempted 2079/8548 = 24%, 40 KB/s], Decompressed: 1766
Downloaded: 2115 file(s) [attempted 2120/8548 = 24%, 52 KB/s], Decompressed: 1916
Downloaded: 2156 file(s) [attempted 2161/8548 = 25%, 131 KB/s], Decompressed: 1916
Downloaded: 2197 file(s) [attempted 2202/8548 = 25%, 923 KB/s], Decompressed: 1916
Downloaded: 2235 file(s) [attempted 2240/8548 = 26%, 387 KB/s], Decompressed: 1916
Downloaded: 2279 file(s) [attempted 2284/8548 = 26%, 214 KB/s], Decompressed: 2081
Downloaded: 2317 file(s) [attempted 2322/8548 = 27%, 150 KB/s], Decompressed: 2081
Downloaded: 2361 file(s) [attempted 2366/8548 = 27%, 243 KB/s], Decompressed: 2081
Downloaded: 2402 file(s) [attempted 2407/8548 = 28%, 483 KB/s], Decompressed: 2081
Downloaded: 2444 file(s) [attempted 2449/8548 = 28%, 131 KB/s], Decompressed: 2081
Downloaded: 2485 file(s) [attempted 2490/8548 = 29%, 58 KB/s], Decompressed: 2081
Downloaded: 2529 file(s) [attempted 2534/8548 = 29%, 144 KB/s], Decompressed: 2279
Downloaded: 2567 file(s) [attempted 2572/8548 = 30%, 1171 KB/s], Decompressed: 2279
Downloaded: 2604 file(s) [attempted 2609/8548 = 30%, 354 KB/s], Decompressed: 2279
Downloaded: 2645 file(s) [attempted 2650/8548 = 31%, 152 KB/s], Decompressed: 2279
Downloaded: 2687 file(s) [attempted 2692/8548 = 31%, 259 KB/s], Decompressed: 2279
Downloaded: 2728 file(s) [attempted 2733/8548 = 31%, 107 KB/s], Decompressed: 2279
Downloaded: 2765 file(s) [attempted 2770/8548 = 32%, 122 KB/s], Decompressed: 2279
Downloaded: 2806 file(s) [attempted 2811/8548 = 32%, 416 KB/s], Decompressed: 2502
Downloaded: 2847 file(s) [attempted 2852/8548 = 33%, 532 KB/s], Decompressed: 2502
Downloaded: 2889 file(s) [attempted 2894/8548 = 33%, 857 KB/s], Decompressed: 2502
Downloaded: 2926 file(s) [attempted 2931/8548 = 34%, 915 KB/s], Decompressed: 2502
Downloaded: 2967 file(s) [attempted 2972/8548 = 34%, 570 KB/s], Decompressed: 2502
Downloaded: 3007 file(s) [attempted 3013/8548 = 35%, 233 KB/s], Decompressed: 2502
Downloaded: 3044 file(s) [attempted 3051/8548 = 35%, 88 KB/s], Decompressed: 2502
Downloaded: 3088 file(s) [attempted 3095/8548 = 36%, 145 KB/s], Decompressed: 2769
Downloaded: 3126 file(s) [attempted 3133/8548 = 36%, 153 KB/s], Decompressed: 2769
Downloaded: 3167 file(s) [attempted 3174/8548 = 37%, 345 KB/s], Decompressed: 2769
Downloaded: 3208 file(s) [attempted 3215/8548 = 37%, 55 KB/s], Decompressed: 2769
Downloaded: 3253 file(s) [attempted 3260/8548 = 38%, 395 KB/s], Decompressed: 2769
Downloaded: 3290 file(s) [attempted 3297/8548 = 38%, 3142 KB/s], Decompressed: 2769
Downloaded: 3330 file(s) [attempted 3337/8548 = 39%, 144 KB/s], Decompressed: 2769
Downloaded: 3371 file(s) [attempted 3379/8548 = 39%, 248 KB/s], Decompressed: 2769
Downloaded: 3413 file(s) [attempted 3421/8548 = 40%, 543 KB/s], Decompressed: 2769
Downloaded: 3457 file(s) [attempted 3465/8548 = 40%, 109 KB/s], Decompressed: 3071
Downloaded: 3495 file(s) [attempted 3503/8548 = 40%, 348 KB/s], Decompressed: 3071
Downloaded: 3539 file(s) [attempted 3547/8548 = 41%, 61 KB/s], Decompressed: 3071
Downloaded: 3573 file(s) [attempted 3581/8548 = 41%, 237 KB/s], Decompressed: 3071
Downloaded: 3616 file(s) [attempted 3625/8548 = 42%, 267 KB/s], Decompressed: 3071
Downloaded: 3655 file(s) [attempted 3664/8548 = 42%, 235 KB/s], Decompressed: 3071
Downloaded: 3692 file(s) [attempted 3701/8548 = 43%, 234 KB/s], Decompressed: 3071
Downloaded: 3737 file(s) [attempted 3746/8548 = 43%, 171 KB/s], Decompressed: 3071
Downloaded: 3774 file(s) [attempted 3783/8548 = 44%, 282 KB/s], Decompressed: 3071
Downloaded: 3815 file(s) [attempted 3824/8548 = 44%, 466 KB/s], Decompressed: 3071
Downloaded: 3856 file(s) [attempted 3865/8548 = 45%, 24 KB/s], Decompressed: 3440
Downloaded: 3894 file(s) [attempted 3903/8548 = 45%, 569 KB/s], Decompressed: 3440
Downloaded: 3935 file(s) [attempted 3944/8548 = 46%, 385 KB/s], Decompressed: 3440
Downloaded: 3976 file(s) [attempted 3985/8548 = 46%, 340 KB/s], Decompressed: 3440
Downloaded: 4017 file(s) [attempted 4026/8548 = 47%, 1833 KB/s], Decompressed: 3440
Downloaded: 4052 file(s) [attempted 4061/8548 = 47%, 647 KB/s], Decompressed: 3440
Downloaded: 4089 file(s) [attempted 4098/8548 = 47%, 616 KB/s], Decompressed: 3440
Downloaded: 4133 file(s) [attempted 4143/8548 = 48%, 3424 KB/s], Decompressed: 3440
Downloaded: 4177 file(s) [attempted 4187/8548 = 48%, 49 KB/s], Decompressed: 3440
Downloaded: 4221 file(s) [attempted 4232/8548 = 49%, 322 KB/s], Decompressed: 3440
Downloaded: 4260 file(s) [attempted 4271/8548 = 49%, 497 KB/s], Decompressed: 3440
Downloaded: 4293 file(s) [attempted 4304/8548 = 50%, 312 KB/s], Decompressed: 3832
Downloaded: 4334 file(s) [attempted 4345/8548 = 50%, 168 KB/s], Decompressed: 3832
Downloaded: 4378 file(s) [attempted 4389/8548 = 51%, 870 KB/s], Decompressed: 3832
Downloaded: 4423 file(s) [attempted 4434/8548 = 51%, 192 KB/s], Decompressed: 3832
Downloaded: 4467 file(s) [attempted 4478/8548 = 52%, 720 KB/s], Decompressed: 3832
Downloaded: 4508 file(s) [attempted 4519/8548 = 52%, 880 KB/s], Decompressed: 3832
Downloaded: 4546 file(s) [attempted 4557/8548 = 53%, 73 KB/s], Decompressed: 3832
Downloaded: 4580 file(s) [attempted 4591/8548 = 53%, 23 KB/s], Decompressed: 3832
Downloaded: 4624 file(s) [attempted 4635/8548 = 54%, 336 KB/s], Decompressed: 3832
Downloaded: 4669 file(s) [attempted 4680/8548 = 54%, 1130 KB/s], Decompressed: 3832
Downloaded: 4713 file(s) [attempted 4725/8548 = 55%, 69 KB/s], Decompressed: 3832
Downloaded: 4750 file(s) [attempted 4762/8548 = 55%, 24 KB/s], Decompressed: 3832
Downloaded: 4791 file(s) [attempted 4803/8548 = 56%, 21 KB/s], Decompressed: 3832
Downloaded: 4829 file(s) [attempted 4841/8548 = 56%, 336 KB/s], Decompressed: 4275
Downloaded: 4873 file(s) [attempted 4885/8548 = 57%, 193 KB/s], Decompressed: 4275
Downloaded: 4914 file(s) [attempted 4926/8548 = 57%, 545 KB/s], Decompressed: 4275
Downloaded: 4955 file(s) [attempted 4967/8548 = 58%, 538 KB/s], Decompressed: 4275
Downloaded: 4992 file(s) [attempted 5005/8548 = 58%, 190 KB/s], Decompressed: 4275
Downloaded: 5030 file(s) [attempted 5043/8548 = 58%, 1102 KB/s], Decompressed: 4275
Downloaded: 5074 file(s) [attempted 5087/8548 = 59%, 327 KB/s], Decompressed: 4275
Downloaded: 5115 file(s) [attempted 5128/8548 = 59%, 150 KB/s], Decompressed: 4275
Downloaded: 5156 file(s) [attempted 5169/8548 = 60%, 90 KB/s], Decompressed: 4275
Downloaded: 5201 file(s) [attempted 5214/8548 = 60%, 1226 KB/s], Decompressed: 4275
Downloaded: 5245 file(s) [attempted 5258/8548 = 61%, 116 KB/s], Decompressed: 4275
Downloaded: 5286 file(s) [attempted 5299/8548 = 61%, 97 KB/s], Decompressed: 4275
Downloaded: 5331 file(s) [attempted 5344/8548 = 62%, 488 KB/s], Decompressed: 4275
Downloaded: 5372 file(s) [attempted 5385/8548 = 62%, 46 KB/s], Decompressed: 4275
Downloaded: 5410 file(s) [attempted 5423/8548 = 63%, 702 KB/s], Decompressed: 4275
Downloaded: 5447 file(s) [attempted 5460/8548 = 63%, 371 KB/s], Decompressed: 4825
Downloaded: 5492 file(s) [attempted 5505/8548 = 64%, 100 KB/s], Decompressed: 4825
Downloaded: 5536 file(s) [attempted 5549/8548 = 64%, 194 KB/s], Decompressed: 4825
Downloaded: 5577 file(s) [attempted 5590/8548 = 65%, 80 KB/s], Decompressed: 4825
Downloaded: 5618 file(s) [attempted 5631/8548 = 65%, 869 KB/s], Decompressed: 4825
Downloaded: 5656 file(s) [attempted 5669/8548 = 66%, 130 KB/s], Decompressed: 4825
Downloaded: 5694 file(s) [attempted 5707/8548 = 66%, 116 KB/s], Decompressed: 4825
Downloaded: 5738 file(s) [attempted 5751/8548 = 67%, 109 KB/s], Decompressed: 4825
Downloaded: 5786 file(s) [attempted 5799/8548 = 67%, 263 KB/s], Decompressed: 4825
Downloaded: 5831 file(s) [attempted 5847/8548 = 68%, 655 KB/s], Decompressed: 4825
Downloaded: 5869 file(s) [attempted 5885/8548 = 68%, 116 KB/s], Decompressed: 4825
Downloaded: 5910 file(s) [attempted 5926/8548 = 69%, 108 KB/s], Decompressed: 4825
Downloaded: 5944 file(s) [attempted 5960/8548 = 69%, 47 KB/s], Decompressed: 4825
Downloaded: 5985 file(s) [attempted 6001/8548 = 70%, 61 KB/s], Decompressed: 4825
Downloaded: 6025 file(s) [attempted 6042/8548 = 70%, 206 KB/s], Decompressed: 4825
Downloaded: 6070 file(s) [attempted 6087/8548 = 71%, 27 KB/s], Decompressed: 4825
Downloaded: 6111 file(s) [attempted 6128/8548 = 71%, 23 KB/s], Decompressed: 5427
Downloaded: 6148 file(s) [attempted 6165/8548 = 72%, 26 KB/s], Decompressed: 5427
Downloaded: 6189 file(s) [attempted 6206/8548 = 72%, 730 KB/s], Decompressed: 5427
Downloaded: 6237 file(s) [attempted 6254/8548 = 73%, 481 KB/s], Decompressed: 5427
Downloaded: 6277 file(s) [attempted 6294/8548 = 73%, 152 KB/s], Decompressed: 5427
Downloaded: 6316 file(s) [attempted 6333/8548 = 74%, 835 KB/s], Decompressed: 5427
Downloaded: 6350 file(s) [attempted 6367/8548 = 74%, 1064 KB/s], Decompressed: 5427
Downloaded: 6384 file(s) [attempted 6402/8548 = 74%, 337 KB/s], Decompressed: 5427
Downloaded: 6431 file(s) [attempted 6449/8548 = 75%, 283 KB/s], Decompressed: 5427
Downloaded: 6475 file(s) [attempted 6494/8548 = 75%, 84 KB/s], Decompressed: 5427
Downloaded: 6516 file(s) [attempted 6535/8548 = 76%, 1775 KB/s], Decompressed: 5427
Downloaded: 6553 file(s) [attempted 6573/8548 = 76%, 425 KB/s], Decompressed: 5427
Downloaded: 6590 file(s) [attempted 6610/8548 = 77%, 542 KB/s], Decompressed: 5427
Downloaded: 6631 file(s) [attempted 6651/8548 = 77%, 362 KB/s], Decompressed: 5427
Downloaded: 6676 file(s) [attempted 6696/8548 = 78%, 225 KB/s], Decompressed: 5427
Downloaded: 6717 file(s) [attempted 6737/8548 = 78%, 172 KB/s], Decompressed: 5427
Downloaded: 6755 file(s) [attempted 6775/8548 = 79%, 58 KB/s], Decompressed: 5427
Downloaded: 6796 file(s) [attempted 6816/8548 = 79%, 62 KB/s], Decompressed: 5427
Downloaded: 6840 file(s) [attempted 6860/8548 = 80%, 239 KB/s], Decompressed: 6080
Downloaded: 6874 file(s) [attempted 6894/8548 = 80%, 83 KB/s], Decompressed: 6080
Downloaded: 6914 file(s) [attempted 6935/8548 = 81%, 459 KB/s], Decompressed: 6080
Downloaded: 6952 file(s) [attempted 6973/8548 = 81%, 115 KB/s], Decompressed: 6080
Downloaded: 6992 file(s) [attempted 7014/8548 = 82%, 251 KB/s], Decompressed: 6080
Downloaded: 7033 file(s) [attempted 7055/8548 = 82%, 380 KB/s], Decompressed: 6080
Downloaded: 7073 file(s) [attempted 7096/8548 = 83%, 258 KB/s], Decompressed: 6080
Downloaded: 7110 file(s) [attempted 7133/8548 = 83%, 99 KB/s], Decompressed: 6080
Downloaded: 7149 file(s) [attempted 7172/8548 = 83%, 69 KB/s], Decompressed: 6080
Downloaded: 7186 file(s) [attempted 7209/8548 = 84%, 148 KB/s], Decompressed: 6080
Downloaded: 7231 file(s) [attempted 7254/8548 = 84%, 106 KB/s], Decompressed: 6080
Downloaded: 7272 file(s) [attempted 7295/8548 = 85%, 329 KB/s], Decompressed: 6080
Downloaded: 7309 file(s) [attempted 7332/8548 = 85%, 358 KB/s], Decompressed: 6080
Downloaded: 7354 file(s) [attempted 7377/8548 = 86%, 278 KB/s], Decompressed: 6080
Downloaded: 7395 file(s) [attempted 7418/8548 = 86%, 583 KB/s], Decompressed: 6080
Downloaded: 7436 file(s) [attempted 7459/8548 = 87%, 583 KB/s], Decompressed: 6080
Downloaded: 7476 file(s) [attempted 7500/8548 = 87%, 614 KB/s], Decompressed: 6080
Downloaded: 7510 file(s) [attempted 7534/8548 = 88%, 235 KB/s], Decompressed: 6080
Downloaded: 7551 file(s) [attempted 7575/8548 = 88%, 318 KB/s], Decompressed: 6080
Downloaded: 7593 file(s) [attempted 7617/8548 = 89%, 631 KB/s], Decompressed: 6802
Downloaded: 7634 file(s) [attempted 7658/8548 = 89%, 119 KB/s], Decompressed: 6802
Downloaded: 7669 file(s) [attempted 7693/8548 = 89%, 217 KB/s], Decompressed: 6802
Downloaded: 7709 file(s) [attempted 7733/8548 = 90%, 297 KB/s], Decompressed: 6802
Downloaded: 7747 file(s) [attempted 7771/8548 = 90%, 285 KB/s], Decompressed: 6802
Downloaded: 7791 file(s) [attempted 7815/8548 = 91%, 577 KB/s], Decompressed: 6802
Downloaded: 7828 file(s) [attempted 7853/8548 = 91%, 560 KB/s], Decompressed: 6802
Downloaded: 7869 file(s) [attempted 7894/8548 = 92%, 978 KB/s], Decompressed: 6802
Downloaded: 7910 file(s) [attempted 7935/8548 = 92%, 214 KB/s], Decompressed: 6802
Downloaded: 7954 file(s) [attempted 7979/8548 = 93%, 868 KB/s], Decompressed: 6802
Downloaded: 7995 file(s) [attempted 8020/8548 = 93%, 334 KB/s], Decompressed: 6802
Downloaded: 8033 file(s) [attempted 8058/8548 = 94%, 374 KB/s], Decompressed: 6802
Downloaded: 8078 file(s) [attempted 8103/8548 = 94%, 157 KB/s], Decompressed: 6802
Downloaded: 8122 file(s) [attempted 8147/8548 = 95%, 178 KB/s], Decompressed: 6802
Downloaded: 8163 file(s) [attempted 8188/8548 = 95%, 368 KB/s], Decompressed: 6802
Downloaded: 8204 file(s) [attempted 8229/8548 = 96%, 76 KB/s], Decompressed: 6802
Downloaded: 8245 file(s) [attempted 8270/8548 = 96%, 197 KB/s], Decompressed: 6802
Downloaded: 8279 file(s) [attempted 8304/8548 = 97%, 791 KB/s], Decompressed: 6802
Downloaded: 8324 file(s) [attempted 8349/8548 = 97%, 1626 KB/s], Decompressed: 6802
Downloaded: 8361 file(s) [attempted 8387/8548 = 98%, 628 KB/s], Decompressed: 6802
Downloaded: 8405 file(s) [attempted 8431/8548 = 98%, 80 KB/s], Decompressed: 6802
Downloaded: 8443 file(s) [attempted 8469/8548 = 99%, 335 KB/s], Decompressed: 6802
Downloaded: 8480 file(s) [attempted 8506/8548 = 99%, 65 KB/s], Decompressed: 7586
Downloaded: 8518 file(s) [attempted 8544/8548 = 99%, 503 KB/s], Decompressed: 7586
Downloaded: 8521 file(s) [attempted 8547/8548 = 99%, 715 KB/s], Decompressed: 7586
Downloaded: 8522 file(s) [attempted 8548/8548 = 100%, 715 KB/s], Decompressed: 7586
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.

  * If you push your commits to a PR to the mathlib4 repository
    (use a draft PR if it is not ready for review),
    then CI will build the oleans and they will be available later.
  * If you have already opened a PR, this may mean
    the CI build has failed part-way through building.
lean_checker exit 0 duration 31s · created 
lake build
Build completed successfully (4011 jobs).

warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
blueprint_build exit 1 duration 1s · created 
lake build :blueprint
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: unknown package facet `blueprint`

Keyboard shortcuts