Login

Verification run

Run 27

ImperialCollegeLondon/FLT branch main triggered via manual
succeeded commit da43bbecb5da toolchain lean-v4-31-0 prover lean took 8m 25s · 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-538-source
exit_code=Some(0) duration_ms=1274
stderr:
Cloning into '/var/lib/apodeixis/repos/job-538-source'...


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

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 da43bbe chore: bump to v4.31 (#1026)

Resolved source revision: da43bbecb5dafc86686181188c69b16ef47895b5

Detected prover: lean
Detected requested toolchain: lean-v4-31-0
Materialized Lean semantic helper assets
Prepared source: revision=da43bbecb5dafc86686181188c69b16ef47895b5 provenance={"branch":"main","checked_out_revision":"da43bbecb5dafc86686181188c69b16ef47895b5","clone_url_hash":"26972c4fa07707e04a8d064eb61ea9ced3487bda0b6c5e8ecd8face933c5481e","credential_mode":"none","local_clone":false,"requested_commit_sha":"da43bbecb5dafc86686181188c69b16ef47895b5","used_missing_commit_fetch":false}
Resolved toolchain: lean-v4-31-0 (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=74925
stdout:
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8542 file(s) from leanprover-community/mathlib4 cache
Decompressed 8516 file(s)
Already decompressed 8516 file(s)

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

Downloaded: 1 file(s) [attempted 1/8542 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 17 file(s) [attempted 17/8542 = 0%, 5 KB/s], Decompressed: 14
Downloaded: 41 file(s) [attempted 41/8542 = 0%, 28 KB/s], Decompressed: 33
Downloaded: 68 file(s) [attempted 68/8542 = 0%, 104 KB/s], Decompressed: 62
Downloaded: 92 file(s) [attempted 93/8542 = 1%, 321 KB/s], Decompressed: 85
Downloaded: 119 file(s) [attempted 120/8542 = 1%, 292 KB/s], Decompressed: 116
Downloaded: 156 file(s) [attempted 157/8542 = 1%, 212 KB/s], Decompressed: 150
Downloaded: 189 file(s) [attempted 190/8542 = 2%, 46 KB/s], Decompressed: 184
Downloaded: 222 file(s) [attempted 223/8542 = 2%, 23 KB/s], Decompressed: 205
Downloaded: 260 file(s) [attempted 261/8542 = 3%, 325 KB/s], Decompressed: 253
Downloaded: 298 file(s) [attempted 299/8542 = 3%, 187 KB/s], Decompressed: 294
Downloaded: 337 file(s) [attempted 338/8542 = 3%, 187 KB/s], Decompressed: 332
Downloaded: 376 file(s) [attempted 377/8542 = 4%, 101 KB/s], Decompressed: 370
Downloaded: 407 file(s) [attempted 408/8542 = 4%, 462 KB/s], Decompressed: 404
Downloaded: 442 file(s) [attempted 443/8542 = 5%, 248 KB/s], Decompressed: 438
Downloaded: 479 file(s) [attempted 480/8542 = 5%, 410 KB/s], Decompressed: 462
Downloaded: 524 file(s) [attempted 525/8542 = 6%, 726 KB/s], Decompressed: 462
Downloaded: 555 file(s) [attempted 556/8542 = 6%, 1203 KB/s], Decompressed: 472
Downloaded: 599 file(s) [attempted 600/8542 = 7%, 894 KB/s], Decompressed: 596
Downloaded: 647 file(s) [attempted 648/8542 = 7%, 161 KB/s], Decompressed: 640
Downloaded: 685 file(s) [attempted 686/8542 = 8%, 103 KB/s], Decompressed: 681
Downloaded: 726 file(s) [attempted 727/8542 = 8%, 164 KB/s], Decompressed: 722
Downloaded: 761 file(s) [attempted 762/8542 = 8%, 125 KB/s], Decompressed: 753
Downloaded: 801 file(s) [attempted 802/8542 = 9%, 129 KB/s], Decompressed: 794
Downloaded: 842 file(s) [attempted 843/8542 = 9%, 316 KB/s], Decompressed: 839
Downloaded: 883 file(s) [attempted 885/8542 = 10%, 1107 KB/s], Decompressed: 877
Downloaded: 920 file(s) [attempted 922/8542 = 10%, 311 KB/s], Decompressed: 906
Downloaded: 958 file(s) [attempted 960/8542 = 11%, 188 KB/s], Decompressed: 954
Downloaded: 1001 file(s) [attempted 1003/8542 = 11%, 805 KB/s], Decompressed: 995
Downloaded: 1043 file(s) [attempted 1045/8542 = 12%, 1003 KB/s], Decompressed: 1040
Downloaded: 1084 file(s) [attempted 1086/8542 = 12%, 258 KB/s], Decompressed: 1081
Downloaded: 1123 file(s) [attempted 1125/8542 = 13%, 410 KB/s], Decompressed: 1115
Downloaded: 1156 file(s) [attempted 1158/8542 = 13%, 127 KB/s], Decompressed: 1149
Downloaded: 1197 file(s) [attempted 1199/8542 = 14%, 39 KB/s], Decompressed: 1190
Downloaded: 1245 file(s) [attempted 1247/8542 = 14%, 1193 KB/s], Decompressed: 1242
Downloaded: 1285 file(s) [attempted 1288/8542 = 15%, 1439 KB/s], Decompressed: 1282
Downloaded: 1326 file(s) [attempted 1329/8542 = 15%, 22 KB/s], Decompressed: 1316
Downloaded: 1357 file(s) [attempted 1360/8542 = 15%, 216 KB/s], Decompressed: 1350
Downloaded: 1400 file(s) [attempted 1403/8542 = 16%, 107 KB/s], Decompressed: 1395
Downloaded: 1443 file(s) [attempted 1446/8542 = 16%, 684 KB/s], Decompressed: 1439
Downloaded: 1484 file(s) [attempted 1487/8542 = 17%, 110 KB/s], Decompressed: 1467
Downloaded: 1519 file(s) [attempted 1524/8542 = 17%, 150 KB/s], Decompressed: 1514
Downloaded: 1561 file(s) [attempted 1566/8542 = 18%, 373 KB/s], Decompressed: 1557
Downloaded: 1598 file(s) [attempted 1603/8542 = 18%, 31 KB/s], Decompressed: 1595
Downloaded: 1641 file(s) [attempted 1646/8542 = 19%, 48 KB/s], Decompressed: 1632
Downloaded: 1680 file(s) [attempted 1685/8542 = 19%, 113 KB/s], Decompressed: 1674
Downloaded: 1718 file(s) [attempted 1723/8542 = 20%, 207 KB/s], Decompressed: 1711
Downloaded: 1759 file(s) [attempted 1764/8542 = 20%, 239 KB/s], Decompressed: 1728
Downloaded: 1800 file(s) [attempted 1805/8542 = 21%, 53 KB/s], Decompressed: 1728
Downloaded: 1841 file(s) [attempted 1846/8542 = 21%, 1049 KB/s], Decompressed: 1831
Downloaded: 1879 file(s) [attempted 1884/8542 = 22%, 274 KB/s], Decompressed: 1872
Downloaded: 1916 file(s) [attempted 1921/8542 = 22%, 692 KB/s], Decompressed: 1913
Downloaded: 1959 file(s) [attempted 1964/8542 = 22%, 740 KB/s], Decompressed: 1954
Downloaded: 2002 file(s) [attempted 2007/8542 = 23%, 36 KB/s], Decompressed: 1995
Downloaded: 2043 file(s) [attempted 2048/8542 = 23%, 99 KB/s], Decompressed: 2029
Downloaded: 2078 file(s) [attempted 2083/8542 = 24%, 132 KB/s], Decompressed: 2029
Downloaded: 2118 file(s) [attempted 2123/8542 = 24%, 53 KB/s], Decompressed: 2036
Downloaded: 2159 file(s) [attempted 2164/8542 = 25%, 244 KB/s], Decompressed: 2156
Downloaded: 2201 file(s) [attempted 2206/8542 = 25%, 1014 KB/s], Decompressed: 2190
Downloaded: 2245 file(s) [attempted 2250/8542 = 26%, 113 KB/s], Decompressed: 2238
Downloaded: 2283 file(s) [attempted 2288/8542 = 26%, 490 KB/s], Decompressed: 2276
Downloaded: 2317 file(s) [attempted 2322/8542 = 27%, 341 KB/s], Decompressed: 2279
Downloaded: 2361 file(s) [attempted 2366/8542 = 27%, 38 KB/s], Decompressed: 2279
Downloaded: 2406 file(s) [attempted 2411/8542 = 28%, 258 KB/s], Decompressed: 2399
Downloaded: 2447 file(s) [attempted 2452/8542 = 28%, 238 KB/s], Decompressed: 2440
Downloaded: 2490 file(s) [attempted 2495/8542 = 29%, 337 KB/s], Decompressed: 2478
Downloaded: 2520 file(s) [attempted 2525/8542 = 29%, 228 KB/s], Decompressed: 2515
Downloaded: 2562 file(s) [attempted 2567/8542 = 30%, 183 KB/s], Decompressed: 2556
Downloaded: 2604 file(s) [attempted 2609/8542 = 30%, 276 KB/s], Decompressed: 2601
Downloaded: 2649 file(s) [attempted 2654/8542 = 31%, 346 KB/s], Decompressed: 2621
Downloaded: 2687 file(s) [attempted 2692/8542 = 31%, 251 KB/s], Decompressed: 2676
Downloaded: 2721 file(s) [attempted 2726/8542 = 31%, 128 KB/s], Decompressed: 2714
Downloaded: 2762 file(s) [attempted 2767/8542 = 32%, 579 KB/s], Decompressed: 2755
Downloaded: 2803 file(s) [attempted 2808/8542 = 32%, 656 KB/s], Decompressed: 2799
Downloaded: 2851 file(s) [attempted 2856/8542 = 33%, 208 KB/s], Decompressed: 2823
Downloaded: 2885 file(s) [attempted 2890/8542 = 33%, 867 KB/s], Decompressed: 2823
Downloaded: 2926 file(s) [attempted 2931/8542 = 34%, 262 KB/s], Decompressed: 2834
Downloaded: 2964 file(s) [attempted 2969/8542 = 34%, 605 KB/s], Decompressed: 2960
Downloaded: 3004 file(s) [attempted 3010/8542 = 35%, 709 KB/s], Decompressed: 3000
Downloaded: 3051 file(s) [attempted 3058/8542 = 35%, 1113 KB/s], Decompressed: 3035
Downloaded: 3085 file(s) [attempted 3092/8542 = 36%, 252 KB/s], Decompressed: 3078
Downloaded: 3129 file(s) [attempted 3136/8542 = 36%, 60 KB/s], Decompressed: 3123
Downloaded: 3170 file(s) [attempted 3177/8542 = 37%, 80 KB/s], Decompressed: 3160
Downloaded: 3208 file(s) [attempted 3215/8542 = 37%, 379 KB/s], Decompressed: 3184
Downloaded: 3253 file(s) [attempted 3260/8542 = 38%, 193 KB/s], Decompressed: 3184
Downloaded: 3294 file(s) [attempted 3301/8542 = 38%, 158 KB/s], Decompressed: 3290
Downloaded: 3334 file(s) [attempted 3342/8542 = 39%, 20 KB/s], Decompressed: 3328
Downloaded: 3372 file(s) [attempted 3380/8542 = 39%, 66 KB/s], Decompressed: 3368
Downloaded: 3409 file(s) [attempted 3417/8542 = 40%, 49 KB/s], Decompressed: 3395
Downloaded: 3450 file(s) [attempted 3458/8542 = 40%, 384 KB/s], Decompressed: 3447
Downloaded: 3495 file(s) [attempted 3503/8542 = 41%, 633 KB/s], Decompressed: 3491
Downloaded: 3536 file(s) [attempted 3544/8542 = 41%, 397 KB/s], Decompressed: 3522
Downloaded: 3573 file(s) [attempted 3581/8542 = 41%, 86 KB/s], Decompressed: 3566
Downloaded: 3613 file(s) [attempted 3622/8542 = 42%, 197 KB/s], Decompressed: 3610
Downloaded: 3651 file(s) [attempted 3660/8542 = 42%, 235 KB/s], Decompressed: 3648
Downloaded: 3692 file(s) [attempted 3701/8542 = 43%, 517 KB/s], Decompressed: 3685
Downloaded: 3733 file(s) [attempted 3742/8542 = 43%, 62 KB/s], Decompressed: 3720
Downloaded: 3774 file(s) [attempted 3783/8542 = 44%, 79 KB/s], Decompressed: 3720
Downloaded: 3819 file(s) [attempted 3828/8542 = 44%, 311 KB/s], Decompressed: 3723
Downloaded: 3856 file(s) [attempted 3865/8542 = 45%, 119 KB/s], Decompressed: 3846
Downloaded: 3894 file(s) [attempted 3903/8542 = 45%, 88 KB/s], Decompressed: 3891
Downloaded: 3939 file(s) [attempted 3948/8542 = 46%, 113 KB/s], Decompressed: 3935
Downloaded: 3976 file(s) [attempted 3985/8542 = 46%, 397 KB/s], Decompressed: 3973
Downloaded: 4017 file(s) [attempted 4026/8542 = 47%, 192 KB/s], Decompressed: 4010
Downloaded: 4051 file(s) [attempted 4060/8542 = 47%, 908 KB/s], Decompressed: 4048
Downloaded: 4092 file(s) [attempted 4102/8542 = 48%, 1280 KB/s], Decompressed: 4088
Downloaded: 4133 file(s) [attempted 4143/8542 = 48%, 153 KB/s], Decompressed: 4105
Downloaded: 4177 file(s) [attempted 4187/8542 = 49%, 373 KB/s], Decompressed: 4105
Downloaded: 4221 file(s) [attempted 4232/8542 = 49%, 270 KB/s], Decompressed: 4210
Downloaded: 4259 file(s) [attempted 4270/8542 = 49%, 875 KB/s], Decompressed: 4255
Downloaded: 4299 file(s) [attempted 4310/8542 = 50%, 214 KB/s], Decompressed: 4296
Downloaded: 4340 file(s) [attempted 4351/8542 = 50%, 861 KB/s], Decompressed: 4334
Downloaded: 4385 file(s) [attempted 4396/8542 = 51%, 235 KB/s], Decompressed: 4358
Downloaded: 4423 file(s) [attempted 4434/8542 = 51%, 24 KB/s], Decompressed: 4358
Downloaded: 4460 file(s) [attempted 4471/8542 = 52%, 126 KB/s], Decompressed: 4443
Downloaded: 4501 file(s) [attempted 4512/8542 = 52%, 347 KB/s], Decompressed: 4494
Downloaded: 4542 file(s) [attempted 4553/8542 = 53%, 109 KB/s], Decompressed: 4539
Downloaded: 4587 file(s) [attempted 4598/8542 = 53%, 513 KB/s], Decompressed: 4556
Downloaded: 4621 file(s) [attempted 4632/8542 = 54%, 631 KB/s], Decompressed: 4614
Downloaded: 4662 file(s) [attempted 4673/8542 = 54%, 540 KB/s], Decompressed: 4659
Downloaded: 4699 file(s) [attempted 4711/8542 = 55%, 49 KB/s], Decompressed: 4692
Downloaded: 4740 file(s) [attempted 4752/8542 = 55%, 171 KB/s], Decompressed: 4733
Downloaded: 4784 file(s) [attempted 4796/8542 = 56%, 164 KB/s], Decompressed: 4771
Downloaded: 4819 file(s) [attempted 4831/8542 = 56%, 581 KB/s], Decompressed: 4812
Downloaded: 4863 file(s) [attempted 4875/8542 = 57%, 166 KB/s], Decompressed: 4856
Downloaded: 4902 file(s) [attempted 4914/8542 = 57%, 192 KB/s], Decompressed: 4897
Downloaded: 4938 file(s) [attempted 4950/8542 = 57%, 200 KB/s], Decompressed: 4925
Downloaded: 4982 file(s) [attempted 4995/8542 = 58%, 426 KB/s], Decompressed: 4925
Downloaded: 5016 file(s) [attempted 5029/8542 = 58%, 60 KB/s], Decompressed: 4931
Downloaded: 5057 file(s) [attempted 5070/8542 = 59%, 117 KB/s], Decompressed: 5050
Downloaded: 5098 file(s) [attempted 5111/8542 = 59%, 87 KB/s], Decompressed: 5095
Downloaded: 5143 file(s) [attempted 5156/8542 = 60%, 2151 KB/s], Decompressed: 5139
Downloaded: 5187 file(s) [attempted 5200/8542 = 60%, 244 KB/s], Decompressed: 5180
Downloaded: 5221 file(s) [attempted 5234/8542 = 61%, 321 KB/s], Decompressed: 5215
Downloaded: 5262 file(s) [attempted 5275/8542 = 61%, 1661 KB/s], Decompressed: 5256
Downloaded: 5307 file(s) [attempted 5320/8542 = 62%, 312 KB/s], Decompressed: 5300
Downloaded: 5348 file(s) [attempted 5361/8542 = 62%, 291 KB/s], Decompressed: 5345
Downloaded: 5390 file(s) [attempted 5403/8542 = 63%, 588 KB/s], Decompressed: 5386
Downloaded: 5427 file(s) [attempted 5440/8542 = 63%, 787 KB/s], Decompressed: 5413
Downloaded: 5468 file(s) [attempted 5481/8542 = 64%, 139 KB/s], Decompressed: 5464
Downloaded: 5505 file(s) [attempted 5518/8542 = 64%, 167 KB/s], Decompressed: 5499
Downloaded: 5550 file(s) [attempted 5563/8542 = 65%, 31 KB/s], Decompressed: 5547
Downloaded: 5594 file(s) [attempted 5607/8542 = 65%, 30 KB/s], Decompressed: 5585
Downloaded: 5634 file(s) [attempted 5647/8542 = 66%, 56 KB/s], Decompressed: 5625
Downloaded: 5670 file(s) [attempted 5683/8542 = 66%, 299 KB/s], Decompressed: 5666
Downloaded: 5711 file(s) [attempted 5724/8542 = 67%, 467 KB/s], Decompressed: 5704
Downloaded: 5749 file(s) [attempted 5762/8542 = 67%, 605 KB/s], Decompressed: 5745
Downloaded: 5790 file(s) [attempted 5803/8542 = 67%, 37 KB/s], Decompressed: 5786
Downloaded: 5828 file(s) [attempted 5844/8542 = 68%, 156 KB/s], Decompressed: 5825
Downloaded: 5869 file(s) [attempted 5885/8542 = 68%, 109 KB/s], Decompressed: 5865
Downloaded: 5906 file(s) [attempted 5922/8542 = 69%, 118 KB/s], Decompressed: 5899
Downloaded: 5947 file(s) [attempted 5963/8542 = 69%, 223 KB/s], Decompressed: 5941
Downloaded: 5988 file(s) [attempted 6004/8542 = 70%, 646 KB/s], Decompressed: 5947
Downloaded: 6029 file(s) [attempted 6046/8542 = 70%, 73 KB/s], Decompressed: 6022
Downloaded: 6066 file(s) [attempted 6083/8542 = 71%, 233 KB/s], Decompressed: 6059
Downloaded: 6107 file(s) [attempted 6124/8542 = 71%, 220 KB/s], Decompressed: 6100
Downloaded: 6145 file(s) [attempted 6162/8542 = 72%, 60 KB/s], Decompressed: 6144
Downloaded: 6189 file(s) [attempted 6206/8542 = 72%, 223 KB/s], Decompressed: 6186
Downloaded: 6230 file(s) [attempted 6247/8542 = 73%, 130 KB/s], Decompressed: 6227
Downloaded: 6268 file(s) [attempted 6285/8542 = 73%, 186 KB/s], Decompressed: 6261
Downloaded: 6302 file(s) [attempted 6319/8542 = 73%, 92 KB/s], Decompressed: 6295
Downloaded: 6344 file(s) [attempted 6361/8542 = 74%, 724 KB/s], Decompressed: 6340
Downloaded: 6383 file(s) [attempted 6401/8542 = 74%, 336 KB/s], Decompressed: 6374
Downloaded: 6425 file(s) [attempted 6443/8542 = 75%, 568 KB/s], Decompressed: 6413
Downloaded: 6459 file(s) [attempted 6478/8542 = 75%, 1 KB/s], Decompressed: 6452
Downloaded: 6497 file(s) [attempted 6516/8542 = 76%, 770 KB/s], Decompressed: 6489
Downloaded: 6543 file(s) [attempted 6562/8542 = 76%, 79 KB/s], Decompressed: 6540
Downloaded: 6583 file(s) [attempted 6603/8542 = 77%, 431 KB/s], Decompressed: 6580
Downloaded: 6620 file(s) [attempted 6640/8542 = 77%, 472 KB/s], Decompressed: 6611
Downloaded: 6652 file(s) [attempted 6672/8542 = 78%, 659 KB/s], Decompressed: 6648
Downloaded: 6696 file(s) [attempted 6716/8542 = 78%, 25 KB/s], Decompressed: 6693
Downloaded: 6739 file(s) [attempted 6759/8542 = 79%, 388 KB/s], Decompressed: 6731
Downloaded: 6778 file(s) [attempted 6798/8542 = 79%, 1539 KB/s], Decompressed: 6775
Downloaded: 6813 file(s) [attempted 6833/8542 = 79%, 415 KB/s], Decompressed: 6809
Downloaded: 6851 file(s) [attempted 6871/8542 = 80%, 140 KB/s], Decompressed: 6847
Downloaded: 6895 file(s) [attempted 6915/8542 = 80%, 55 KB/s], Decompressed: 6891
Downloaded: 6935 file(s) [attempted 6956/8542 = 81%, 655 KB/s], Decompressed: 6932
Downloaded: 6975 file(s) [attempted 6997/8542 = 81%, 261 KB/s], Decompressed: 6968
Downloaded: 7009 file(s) [attempted 7031/8542 = 82%, 1553 KB/s], Decompressed: 7002
Downloaded: 7046 file(s) [attempted 7069/8542 = 82%, 207 KB/s], Decompressed: 7042
Downloaded: 7090 file(s) [attempted 7113/8542 = 83%, 397 KB/s], Decompressed: 7087
Downloaded: 7138 file(s) [attempted 7161/8542 = 83%, 272 KB/s], Decompressed: 7131
Downloaded: 7183 file(s) [attempted 7206/8542 = 84%, 119 KB/s], Decompressed: 7179
Downloaded: 7221 file(s) [attempted 7244/8542 = 84%, 83 KB/s], Decompressed: 7217
Downloaded: 7256 file(s) [attempted 7279/8542 = 85%, 76 KB/s], Decompressed: 7251
Downloaded: 7294 file(s) [attempted 7317/8542 = 85%, 41 KB/s], Decompressed: 7285
Downloaded: 7334 file(s) [attempted 7357/8542 = 86%, 47 KB/s], Decompressed: 7330
Downloaded: 7378 file(s) [attempted 7401/8542 = 86%, 700 KB/s], Decompressed: 7368
Downloaded: 7413 file(s) [attempted 7436/8542 = 87%, 252 KB/s], Decompressed: 7409
Downloaded: 7453 file(s) [attempted 7476/8542 = 87%, 305 KB/s], Decompressed: 7446
Downloaded: 7493 file(s) [attempted 7517/8542 = 88%, 132 KB/s], Decompressed: 7490
Downloaded: 7536 file(s) [attempted 7560/8542 = 88%, 1382 KB/s], Decompressed: 7531
Downloaded: 7575 file(s) [attempted 7599/8542 = 88%, 127 KB/s], Decompressed: 7535
Downloaded: 7613 file(s) [attempted 7637/8542 = 89%, 223 KB/s], Decompressed: 7535
Downloaded: 7654 file(s) [attempted 7678/8542 = 89%, 450 KB/s], Decompressed: 7535
Downloaded: 7695 file(s) [attempted 7719/8542 = 90%, 287 KB/s], Decompressed: 7535
Downloaded: 7736 file(s) [attempted 7760/8542 = 90%, 438 KB/s], Decompressed: 7729
Downloaded: 7776 file(s) [attempted 7800/8542 = 91%, 758 KB/s], Decompressed: 7767
Downloaded: 7808 file(s) [attempted 7833/8542 = 91%, 147 KB/s], Decompressed: 7806
Downloaded: 7852 file(s) [attempted 7877/8542 = 92%, 158 KB/s], Decompressed: 7834
Downloaded: 7890 file(s) [attempted 7915/8542 = 92%, 1202 KB/s], Decompressed: 7886
Downloaded: 7927 file(s) [attempted 7952/8542 = 93%, 178 KB/s], Decompressed: 7923
Downloaded: 7962 file(s) [attempted 7987/8542 = 93%, 810 KB/s], Decompressed: 7958
Downloaded: 8006 file(s) [attempted 8031/8542 = 94%, 114 KB/s], Decompressed: 8002
Downloaded: 8050 file(s) [attempted 8075/8542 = 94%, 130 KB/s], Decompressed: 8047
Downloaded: 8089 file(s) [attempted 8114/8542 = 94%, 515 KB/s], Decompressed: 8077
Downloaded: 8129 file(s) [attempted 8154/8542 = 95%, 391 KB/s], Decompressed: 8122
Downloaded: 8170 file(s) [attempted 8195/8542 = 95%, 359 KB/s], Decompressed: 8166
Downloaded: 8213 file(s) [attempted 8238/8542 = 96%, 122 KB/s], Decompressed: 8204
Downloaded: 8252 file(s) [attempted 8277/8542 = 96%, 604 KB/s], Decompressed: 8245
Downloaded: 8292 file(s) [attempted 8317/8542 = 97%, 522 KB/s], Decompressed: 8276
Downloaded: 8334 file(s) [attempted 8359/8542 = 97%, 540 KB/s], Decompressed: 8327
Downloaded: 8377 file(s) [attempted 8403/8542 = 98%, 516 KB/s], Decompressed: 8371
Downloaded: 8415 file(s) [attempted 8441/8542 = 98%, 336 KB/s], Decompressed: 8412
Downloaded: 8453 file(s) [attempted 8479/8542 = 99%, 81 KB/s], Decompressed: 8449
Downloaded: 8493 file(s) [attempted 8519/8542 = 99%, 82 KB/s], Decompressed: 8487
Downloaded: 8516 file(s) [attempted 8542/8542 = 100%, 82 KB/s], Decompressed: 8508
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=37106
stdout:
Build completed successfully (4018 jobs).

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


$ lake build :blueprint
exit_code=Some(1) duration_ms=1500
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
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 1s · created 
git clone --depth 1 --branch main --single-branch https://github.com/ImperialCollegeLondon/FLT.git /var/lib/apodeixis/repos/job-538-source
Cloning into '/var/lib/apodeixis/repos/job-538-source'...
git_checkout exit 0 duration 39 ms · created 
git checkout da43bbecb5dafc86686181188c69b16ef47895b5
Note: switching to 'da43bbecb5dafc86686181188c69b16ef47895b5'.

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 da43bbe chore: bump to v4.31 (#1026)
lake_cache exit 0 duration 1m 15s · created 
lake exe cache get
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8542 file(s) from leanprover-community/mathlib4 cache
Decompressed 8516 file(s)
Already decompressed 8516 file(s)

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

Downloaded: 1 file(s) [attempted 1/8542 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 17 file(s) [attempted 17/8542 = 0%, 5 KB/s], Decompressed: 14
Downloaded: 41 file(s) [attempted 41/8542 = 0%, 28 KB/s], Decompressed: 33
Downloaded: 68 file(s) [attempted 68/8542 = 0%, 104 KB/s], Decompressed: 62
Downloaded: 92 file(s) [attempted 93/8542 = 1%, 321 KB/s], Decompressed: 85
Downloaded: 119 file(s) [attempted 120/8542 = 1%, 292 KB/s], Decompressed: 116
Downloaded: 156 file(s) [attempted 157/8542 = 1%, 212 KB/s], Decompressed: 150
Downloaded: 189 file(s) [attempted 190/8542 = 2%, 46 KB/s], Decompressed: 184
Downloaded: 222 file(s) [attempted 223/8542 = 2%, 23 KB/s], Decompressed: 205
Downloaded: 260 file(s) [attempted 261/8542 = 3%, 325 KB/s], Decompressed: 253
Downloaded: 298 file(s) [attempted 299/8542 = 3%, 187 KB/s], Decompressed: 294
Downloaded: 337 file(s) [attempted 338/8542 = 3%, 187 KB/s], Decompressed: 332
Downloaded: 376 file(s) [attempted 377/8542 = 4%, 101 KB/s], Decompressed: 370
Downloaded: 407 file(s) [attempted 408/8542 = 4%, 462 KB/s], Decompressed: 404
Downloaded: 442 file(s) [attempted 443/8542 = 5%, 248 KB/s], Decompressed: 438
Downloaded: 479 file(s) [attempted 480/8542 = 5%, 410 KB/s], Decompressed: 462
Downloaded: 524 file(s) [attempted 525/8542 = 6%, 726 KB/s], Decompressed: 462
Downloaded: 555 file(s) [attempted 556/8542 = 6%, 1203 KB/s], Decompressed: 472
Downloaded: 599 file(s) [attempted 600/8542 = 7%, 894 KB/s], Decompressed: 596
Downloaded: 647 file(s) [attempted 648/8542 = 7%, 161 KB/s], Decompressed: 640
Downloaded: 685 file(s) [attempted 686/8542 = 8%, 103 KB/s], Decompressed: 681
Downloaded: 726 file(s) [attempted 727/8542 = 8%, 164 KB/s], Decompressed: 722
Downloaded: 761 file(s) [attempted 762/8542 = 8%, 125 KB/s], Decompressed: 753
Downloaded: 801 file(s) [attempted 802/8542 = 9%, 129 KB/s], Decompressed: 794
Downloaded: 842 file(s) [attempted 843/8542 = 9%, 316 KB/s], Decompressed: 839
Downloaded: 883 file(s) [attempted 885/8542 = 10%, 1107 KB/s], Decompressed: 877
Downloaded: 920 file(s) [attempted 922/8542 = 10%, 311 KB/s], Decompressed: 906
Downloaded: 958 file(s) [attempted 960/8542 = 11%, 188 KB/s], Decompressed: 954
Downloaded: 1001 file(s) [attempted 1003/8542 = 11%, 805 KB/s], Decompressed: 995
Downloaded: 1043 file(s) [attempted 1045/8542 = 12%, 1003 KB/s], Decompressed: 1040
Downloaded: 1084 file(s) [attempted 1086/8542 = 12%, 258 KB/s], Decompressed: 1081
Downloaded: 1123 file(s) [attempted 1125/8542 = 13%, 410 KB/s], Decompressed: 1115
Downloaded: 1156 file(s) [attempted 1158/8542 = 13%, 127 KB/s], Decompressed: 1149
Downloaded: 1197 file(s) [attempted 1199/8542 = 14%, 39 KB/s], Decompressed: 1190
Downloaded: 1245 file(s) [attempted 1247/8542 = 14%, 1193 KB/s], Decompressed: 1242
Downloaded: 1285 file(s) [attempted 1288/8542 = 15%, 1439 KB/s], Decompressed: 1282
Downloaded: 1326 file(s) [attempted 1329/8542 = 15%, 22 KB/s], Decompressed: 1316
Downloaded: 1357 file(s) [attempted 1360/8542 = 15%, 216 KB/s], Decompressed: 1350
Downloaded: 1400 file(s) [attempted 1403/8542 = 16%, 107 KB/s], Decompressed: 1395
Downloaded: 1443 file(s) [attempted 1446/8542 = 16%, 684 KB/s], Decompressed: 1439
Downloaded: 1484 file(s) [attempted 1487/8542 = 17%, 110 KB/s], Decompressed: 1467
Downloaded: 1519 file(s) [attempted 1524/8542 = 17%, 150 KB/s], Decompressed: 1514
Downloaded: 1561 file(s) [attempted 1566/8542 = 18%, 373 KB/s], Decompressed: 1557
Downloaded: 1598 file(s) [attempted 1603/8542 = 18%, 31 KB/s], Decompressed: 1595
Downloaded: 1641 file(s) [attempted 1646/8542 = 19%, 48 KB/s], Decompressed: 1632
Downloaded: 1680 file(s) [attempted 1685/8542 = 19%, 113 KB/s], Decompressed: 1674
Downloaded: 1718 file(s) [attempted 1723/8542 = 20%, 207 KB/s], Decompressed: 1711
Downloaded: 1759 file(s) [attempted 1764/8542 = 20%, 239 KB/s], Decompressed: 1728
Downloaded: 1800 file(s) [attempted 1805/8542 = 21%, 53 KB/s], Decompressed: 1728
Downloaded: 1841 file(s) [attempted 1846/8542 = 21%, 1049 KB/s], Decompressed: 1831
Downloaded: 1879 file(s) [attempted 1884/8542 = 22%, 274 KB/s], Decompressed: 1872
Downloaded: 1916 file(s) [attempted 1921/8542 = 22%, 692 KB/s], Decompressed: 1913
Downloaded: 1959 file(s) [attempted 1964/8542 = 22%, 740 KB/s], Decompressed: 1954
Downloaded: 2002 file(s) [attempted 2007/8542 = 23%, 36 KB/s], Decompressed: 1995
Downloaded: 2043 file(s) [attempted 2048/8542 = 23%, 99 KB/s], Decompressed: 2029
Downloaded: 2078 file(s) [attempted 2083/8542 = 24%, 132 KB/s], Decompressed: 2029
Downloaded: 2118 file(s) [attempted 2123/8542 = 24%, 53 KB/s], Decompressed: 2036
Downloaded: 2159 file(s) [attempted 2164/8542 = 25%, 244 KB/s], Decompressed: 2156
Downloaded: 2201 file(s) [attempted 2206/8542 = 25%, 1014 KB/s], Decompressed: 2190
Downloaded: 2245 file(s) [attempted 2250/8542 = 26%, 113 KB/s], Decompressed: 2238
Downloaded: 2283 file(s) [attempted 2288/8542 = 26%, 490 KB/s], Decompressed: 2276
Downloaded: 2317 file(s) [attempted 2322/8542 = 27%, 341 KB/s], Decompressed: 2279
Downloaded: 2361 file(s) [attempted 2366/8542 = 27%, 38 KB/s], Decompressed: 2279
Downloaded: 2406 file(s) [attempted 2411/8542 = 28%, 258 KB/s], Decompressed: 2399
Downloaded: 2447 file(s) [attempted 2452/8542 = 28%, 238 KB/s], Decompressed: 2440
Downloaded: 2490 file(s) [attempted 2495/8542 = 29%, 337 KB/s], Decompressed: 2478
Downloaded: 2520 file(s) [attempted 2525/8542 = 29%, 228 KB/s], Decompressed: 2515
Downloaded: 2562 file(s) [attempted 2567/8542 = 30%, 183 KB/s], Decompressed: 2556
Downloaded: 2604 file(s) [attempted 2609/8542 = 30%, 276 KB/s], Decompressed: 2601
Downloaded: 2649 file(s) [attempted 2654/8542 = 31%, 346 KB/s], Decompressed: 2621
Downloaded: 2687 file(s) [attempted 2692/8542 = 31%, 251 KB/s], Decompressed: 2676
Downloaded: 2721 file(s) [attempted 2726/8542 = 31%, 128 KB/s], Decompressed: 2714
Downloaded: 2762 file(s) [attempted 2767/8542 = 32%, 579 KB/s], Decompressed: 2755
Downloaded: 2803 file(s) [attempted 2808/8542 = 32%, 656 KB/s], Decompressed: 2799
Downloaded: 2851 file(s) [attempted 2856/8542 = 33%, 208 KB/s], Decompressed: 2823
Downloaded: 2885 file(s) [attempted 2890/8542 = 33%, 867 KB/s], Decompressed: 2823
Downloaded: 2926 file(s) [attempted 2931/8542 = 34%, 262 KB/s], Decompressed: 2834
Downloaded: 2964 file(s) [attempted 2969/8542 = 34%, 605 KB/s], Decompressed: 2960
Downloaded: 3004 file(s) [attempted 3010/8542 = 35%, 709 KB/s], Decompressed: 3000
Downloaded: 3051 file(s) [attempted 3058/8542 = 35%, 1113 KB/s], Decompressed: 3035
Downloaded: 3085 file(s) [attempted 3092/8542 = 36%, 252 KB/s], Decompressed: 3078
Downloaded: 3129 file(s) [attempted 3136/8542 = 36%, 60 KB/s], Decompressed: 3123
Downloaded: 3170 file(s) [attempted 3177/8542 = 37%, 80 KB/s], Decompressed: 3160
Downloaded: 3208 file(s) [attempted 3215/8542 = 37%, 379 KB/s], Decompressed: 3184
Downloaded: 3253 file(s) [attempted 3260/8542 = 38%, 193 KB/s], Decompressed: 3184
Downloaded: 3294 file(s) [attempted 3301/8542 = 38%, 158 KB/s], Decompressed: 3290
Downloaded: 3334 file(s) [attempted 3342/8542 = 39%, 20 KB/s], Decompressed: 3328
Downloaded: 3372 file(s) [attempted 3380/8542 = 39%, 66 KB/s], Decompressed: 3368
Downloaded: 3409 file(s) [attempted 3417/8542 = 40%, 49 KB/s], Decompressed: 3395
Downloaded: 3450 file(s) [attempted 3458/8542 = 40%, 384 KB/s], Decompressed: 3447
Downloaded: 3495 file(s) [attempted 3503/8542 = 41%, 633 KB/s], Decompressed: 3491
Downloaded: 3536 file(s) [attempted 3544/8542 = 41%, 397 KB/s], Decompressed: 3522
Downloaded: 3573 file(s) [attempted 3581/8542 = 41%, 86 KB/s], Decompressed: 3566
Downloaded: 3613 file(s) [attempted 3622/8542 = 42%, 197 KB/s], Decompressed: 3610
Downloaded: 3651 file(s) [attempted 3660/8542 = 42%, 235 KB/s], Decompressed: 3648
Downloaded: 3692 file(s) [attempted 3701/8542 = 43%, 517 KB/s], Decompressed: 3685
Downloaded: 3733 file(s) [attempted 3742/8542 = 43%, 62 KB/s], Decompressed: 3720
Downloaded: 3774 file(s) [attempted 3783/8542 = 44%, 79 KB/s], Decompressed: 3720
Downloaded: 3819 file(s) [attempted 3828/8542 = 44%, 311 KB/s], Decompressed: 3723
Downloaded: 3856 file(s) [attempted 3865/8542 = 45%, 119 KB/s], Decompressed: 3846
Downloaded: 3894 file(s) [attempted 3903/8542 = 45%, 88 KB/s], Decompressed: 3891
Downloaded: 3939 file(s) [attempted 3948/8542 = 46%, 113 KB/s], Decompressed: 3935
Downloaded: 3976 file(s) [attempted 3985/8542 = 46%, 397 KB/s], Decompressed: 3973
Downloaded: 4017 file(s) [attempted 4026/8542 = 47%, 192 KB/s], Decompressed: 4010
Downloaded: 4051 file(s) [attempted 4060/8542 = 47%, 908 KB/s], Decompressed: 4048
Downloaded: 4092 file(s) [attempted 4102/8542 = 48%, 1280 KB/s], Decompressed: 4088
Downloaded: 4133 file(s) [attempted 4143/8542 = 48%, 153 KB/s], Decompressed: 4105
Downloaded: 4177 file(s) [attempted 4187/8542 = 49%, 373 KB/s], Decompressed: 4105
Downloaded: 4221 file(s) [attempted 4232/8542 = 49%, 270 KB/s], Decompressed: 4210
Downloaded: 4259 file(s) [attempted 4270/8542 = 49%, 875 KB/s], Decompressed: 4255
Downloaded: 4299 file(s) [attempted 4310/8542 = 50%, 214 KB/s], Decompressed: 4296
Downloaded: 4340 file(s) [attempted 4351/8542 = 50%, 861 KB/s], Decompressed: 4334
Downloaded: 4385 file(s) [attempted 4396/8542 = 51%, 235 KB/s], Decompressed: 4358
Downloaded: 4423 file(s) [attempted 4434/8542 = 51%, 24 KB/s], Decompressed: 4358
Downloaded: 4460 file(s) [attempted 4471/8542 = 52%, 126 KB/s], Decompressed: 4443
Downloaded: 4501 file(s) [attempted 4512/8542 = 52%, 347 KB/s], Decompressed: 4494
Downloaded: 4542 file(s) [attempted 4553/8542 = 53%, 109 KB/s], Decompressed: 4539
Downloaded: 4587 file(s) [attempted 4598/8542 = 53%, 513 KB/s], Decompressed: 4556
Downloaded: 4621 file(s) [attempted 4632/8542 = 54%, 631 KB/s], Decompressed: 4614
Downloaded: 4662 file(s) [attempted 4673/8542 = 54%, 540 KB/s], Decompressed: 4659
Downloaded: 4699 file(s) [attempted 4711/8542 = 55%, 49 KB/s], Decompressed: 4692
Downloaded: 4740 file(s) [attempted 4752/8542 = 55%, 171 KB/s], Decompressed: 4733
Downloaded: 4784 file(s) [attempted 4796/8542 = 56%, 164 KB/s], Decompressed: 4771
Downloaded: 4819 file(s) [attempted 4831/8542 = 56%, 581 KB/s], Decompressed: 4812
Downloaded: 4863 file(s) [attempted 4875/8542 = 57%, 166 KB/s], Decompressed: 4856
Downloaded: 4902 file(s) [attempted 4914/8542 = 57%, 192 KB/s], Decompressed: 4897
Downloaded: 4938 file(s) [attempted 4950/8542 = 57%, 200 KB/s], Decompressed: 4925
Downloaded: 4982 file(s) [attempted 4995/8542 = 58%, 426 KB/s], Decompressed: 4925
Downloaded: 5016 file(s) [attempted 5029/8542 = 58%, 60 KB/s], Decompressed: 4931
Downloaded: 5057 file(s) [attempted 5070/8542 = 59%, 117 KB/s], Decompressed: 5050
Downloaded: 5098 file(s) [attempted 5111/8542 = 59%, 87 KB/s], Decompressed: 5095
Downloaded: 5143 file(s) [attempted 5156/8542 = 60%, 2151 KB/s], Decompressed: 5139
Downloaded: 5187 file(s) [attempted 5200/8542 = 60%, 244 KB/s], Decompressed: 5180
Downloaded: 5221 file(s) [attempted 5234/8542 = 61%, 321 KB/s], Decompressed: 5215
Downloaded: 5262 file(s) [attempted 5275/8542 = 61%, 1661 KB/s], Decompressed: 5256
Downloaded: 5307 file(s) [attempted 5320/8542 = 62%, 312 KB/s], Decompressed: 5300
Downloaded: 5348 file(s) [attempted 5361/8542 = 62%, 291 KB/s], Decompressed: 5345
Downloaded: 5390 file(s) [attempted 5403/8542 = 63%, 588 KB/s], Decompressed: 5386
Downloaded: 5427 file(s) [attempted 5440/8542 = 63%, 787 KB/s], Decompressed: 5413
Downloaded: 5468 file(s) [attempted 5481/8542 = 64%, 139 KB/s], Decompressed: 5464
Downloaded: 5505 file(s) [attempted 5518/8542 = 64%, 167 KB/s], Decompressed: 5499
Downloaded: 5550 file(s) [attempted 5563/8542 = 65%, 31 KB/s], Decompressed: 5547
Downloaded: 5594 file(s) [attempted 5607/8542 = 65%, 30 KB/s], Decompressed: 5585
Downloaded: 5634 file(s) [attempted 5647/8542 = 66%, 56 KB/s], Decompressed: 5625
Downloaded: 5670 file(s) [attempted 5683/8542 = 66%, 299 KB/s], Decompressed: 5666
Downloaded: 5711 file(s) [attempted 5724/8542 = 67%, 467 KB/s], Decompressed: 5704
Downloaded: 5749 file(s) [attempted 5762/8542 = 67%, 605 KB/s], Decompressed: 5745
Downloaded: 5790 file(s) [attempted 5803/8542 = 67%, 37 KB/s], Decompressed: 5786
Downloaded: 5828 file(s) [attempted 5844/8542 = 68%, 156 KB/s], Decompressed: 5825
Downloaded: 5869 file(s) [attempted 5885/8542 = 68%, 109 KB/s], Decompressed: 5865
Downloaded: 5906 file(s) [attempted 5922/8542 = 69%, 118 KB/s], Decompressed: 5899
Downloaded: 5947 file(s) [attempted 5963/8542 = 69%, 223 KB/s], Decompressed: 5941
Downloaded: 5988 file(s) [attempted 6004/8542 = 70%, 646 KB/s], Decompressed: 5947
Downloaded: 6029 file(s) [attempted 6046/8542 = 70%, 73 KB/s], Decompressed: 6022
Downloaded: 6066 file(s) [attempted 6083/8542 = 71%, 233 KB/s], Decompressed: 6059
Downloaded: 6107 file(s) [attempted 6124/8542 = 71%, 220 KB/s], Decompressed: 6100
Downloaded: 6145 file(s) [attempted 6162/8542 = 72%, 60 KB/s], Decompressed: 6144
Downloaded: 6189 file(s) [attempted 6206/8542 = 72%, 223 KB/s], Decompressed: 6186
Downloaded: 6230 file(s) [attempted 6247/8542 = 73%, 130 KB/s], Decompressed: 6227
Downloaded: 6268 file(s) [attempted 6285/8542 = 73%, 186 KB/s], Decompressed: 6261
Downloaded: 6302 file(s) [attempted 6319/8542 = 73%, 92 KB/s], Decompressed: 6295
Downloaded: 6344 file(s) [attempted 6361/8542 = 74%, 724 KB/s], Decompressed: 6340
Downloaded: 6383 file(s) [attempted 6401/8542 = 74%, 336 KB/s], Decompressed: 6374
Downloaded: 6425 file(s) [attempted 6443/8542 = 75%, 568 KB/s], Decompressed: 6413
Downloaded: 6459 file(s) [attempted 6478/8542 = 75%, 1 KB/s], Decompressed: 6452
Downloaded: 6497 file(s) [attempted 6516/8542 = 76%, 770 KB/s], Decompressed: 6489
Downloaded: 6543 file(s) [attempted 6562/8542 = 76%, 79 KB/s], Decompressed: 6540
Downloaded: 6583 file(s) [attempted 6603/8542 = 77%, 431 KB/s], Decompressed: 6580
Downloaded: 6620 file(s) [attempted 6640/8542 = 77%, 472 KB/s], Decompressed: 6611
Downloaded: 6652 file(s) [attempted 6672/8542 = 78%, 659 KB/s], Decompressed: 6648
Downloaded: 6696 file(s) [attempted 6716/8542 = 78%, 25 KB/s], Decompressed: 6693
Downloaded: 6739 file(s) [attempted 6759/8542 = 79%, 388 KB/s], Decompressed: 6731
Downloaded: 6778 file(s) [attempted 6798/8542 = 79%, 1539 KB/s], Decompressed: 6775
Downloaded: 6813 file(s) [attempted 6833/8542 = 79%, 415 KB/s], Decompressed: 6809
Downloaded: 6851 file(s) [attempted 6871/8542 = 80%, 140 KB/s], Decompressed: 6847
Downloaded: 6895 file(s) [attempted 6915/8542 = 80%, 55 KB/s], Decompressed: 6891
Downloaded: 6935 file(s) [attempted 6956/8542 = 81%, 655 KB/s], Decompressed: 6932
Downloaded: 6975 file(s) [attempted 6997/8542 = 81%, 261 KB/s], Decompressed: 6968
Downloaded: 7009 file(s) [attempted 7031/8542 = 82%, 1553 KB/s], Decompressed: 7002
Downloaded: 7046 file(s) [attempted 7069/8542 = 82%, 207 KB/s], Decompressed: 7042
Downloaded: 7090 file(s) [attempted 7113/8542 = 83%, 397 KB/s], Decompressed: 7087
Downloaded: 7138 file(s) [attempted 7161/8542 = 83%, 272 KB/s], Decompressed: 7131
Downloaded: 7183 file(s) [attempted 7206/8542 = 84%, 119 KB/s], Decompressed: 7179
Downloaded: 7221 file(s) [attempted 7244/8542 = 84%, 83 KB/s], Decompressed: 7217
Downloaded: 7256 file(s) [attempted 7279/8542 = 85%, 76 KB/s], Decompressed: 7251
Downloaded: 7294 file(s) [attempted 7317/8542 = 85%, 41 KB/s], Decompressed: 7285
Downloaded: 7334 file(s) [attempted 7357/8542 = 86%, 47 KB/s], Decompressed: 7330
Downloaded: 7378 file(s) [attempted 7401/8542 = 86%, 700 KB/s], Decompressed: 7368
Downloaded: 7413 file(s) [attempted 7436/8542 = 87%, 252 KB/s], Decompressed: 7409
Downloaded: 7453 file(s) [attempted 7476/8542 = 87%, 305 KB/s], Decompressed: 7446
Downloaded: 7493 file(s) [attempted 7517/8542 = 88%, 132 KB/s], Decompressed: 7490
Downloaded: 7536 file(s) [attempted 7560/8542 = 88%, 1382 KB/s], Decompressed: 7531
Downloaded: 7575 file(s) [attempted 7599/8542 = 88%, 127 KB/s], Decompressed: 7535
Downloaded: 7613 file(s) [attempted 7637/8542 = 89%, 223 KB/s], Decompressed: 7535
Downloaded: 7654 file(s) [attempted 7678/8542 = 89%, 450 KB/s], Decompressed: 7535
Downloaded: 7695 file(s) [attempted 7719/8542 = 90%, 287 KB/s], Decompressed: 7535
Downloaded: 7736 file(s) [attempted 7760/8542 = 90%, 438 KB/s], Decompressed: 7729
Downloaded: 7776 file(s) [attempted 7800/8542 = 91%, 758 KB/s], Decompressed: 7767
Downloaded: 7808 file(s) [attempted 7833/8542 = 91%, 147 KB/s], Decompressed: 7806
Downloaded: 7852 file(s) [attempted 7877/8542 = 92%, 158 KB/s], Decompressed: 7834
Downloaded: 7890 file(s) [attempted 7915/8542 = 92%, 1202 KB/s], Decompressed: 7886
Downloaded: 7927 file(s) [attempted 7952/8542 = 93%, 178 KB/s], Decompressed: 7923
Downloaded: 7962 file(s) [attempted 7987/8542 = 93%, 810 KB/s], Decompressed: 7958
Downloaded: 8006 file(s) [attempted 8031/8542 = 94%, 114 KB/s], Decompressed: 8002
Downloaded: 8050 file(s) [attempted 8075/8542 = 94%, 130 KB/s], Decompressed: 8047
Downloaded: 8089 file(s) [attempted 8114/8542 = 94%, 515 KB/s], Decompressed: 8077
Downloaded: 8129 file(s) [attempted 8154/8542 = 95%, 391 KB/s], Decompressed: 8122
Downloaded: 8170 file(s) [attempted 8195/8542 = 95%, 359 KB/s], Decompressed: 8166
Downloaded: 8213 file(s) [attempted 8238/8542 = 96%, 122 KB/s], Decompressed: 8204
Downloaded: 8252 file(s) [attempted 8277/8542 = 96%, 604 KB/s], Decompressed: 8245
Downloaded: 8292 file(s) [attempted 8317/8542 = 97%, 522 KB/s], Decompressed: 8276
Downloaded: 8334 file(s) [attempted 8359/8542 = 97%, 540 KB/s], Decompressed: 8327
Downloaded: 8377 file(s) [attempted 8403/8542 = 98%, 516 KB/s], Decompressed: 8371
Downloaded: 8415 file(s) [attempted 8441/8542 = 98%, 336 KB/s], Decompressed: 8412
Downloaded: 8453 file(s) [attempted 8479/8542 = 99%, 81 KB/s], Decompressed: 8449
Downloaded: 8493 file(s) [attempted 8519/8542 = 99%, 82 KB/s], Decompressed: 8487
Downloaded: 8516 file(s) [attempted 8542/8542 = 100%, 82 KB/s], Decompressed: 8508
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 37s · created 
lake build
Build completed successfully (4018 jobs).

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

Keyboard shortcuts