Verification run

Run 14

ImperialCollegeLondon/FLT branch main triggered via poller

failed commit f30ec5dc256d toolchain lean-v4-31-0-rc1 prover lean took 4h 9m · finished 6w ago

./.apodeixis/tools/lean-semantic-extract.sh failed with exit code none (process did not exit cleanly) (toolchain lean-v4-31-0-rc1, command: elan run leanprover/lean4:v4.31.0-rc1 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase ./.apodeixis/tools/lean-semantic-extract.sh)

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

(no log excerpt)

Command runs

git_clone exit 0 duration 759 ms · created 6/6/2026, 11:08:24 AM

git clone --depth 1 --branch main --single-branch https://github.com/ImperialCollegeLondon/FLT.git /var/lib/apodeixis/repos/job-129-source

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

git_checkout exit 0 duration 18 ms · created 6/6/2026, 11:08:24 AM

git checkout f30ec5dc256df9d259e3470ea7bcbce83be9b3f4

Note: switching to 'f30ec5dc256df9d259e3470ea7bcbce83be9b3f4'.

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 f30ec5d chore: rename files (#1003)

lake_cache exit 0 duration 1m 19s · created 6/6/2026, 11:08:24 AM

lake exe cache get

Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8500 file(s) from leanprover-community/mathlib4 cache
Decompressed 8500 file(s)
Already decompressed 8500 file(s)

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '859caf703c2ec80952bad6c1cd102b3f14eabf5b'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '9196a81145e1e291a1469288e77392b0e1b9a493'
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
✔ [11/23] Built Cache.Init (628ms)
✔ [12/23] Built Cache.Lean (696ms)
✔ [13/23] Built Cache.Init:c.o (399ms)
✔ [14/23] Built Cache.Lean:c.o (374ms)
✔ [15/23] Built Cache.IO (1.9s)
✔ [16/23] Built Cache.Hashing (952ms)
✔ [17/23] Built Cache.IO:c.o (1.2s)
✔ [18/23] Built Cache.Hashing:c.o (361ms)
✔ [19/23] Built Cache.Requests (2.1s)
✔ [20/23] Built Cache.Main (1.0s)
✔ [21/23] Built Cache.Main:c.o (503ms)
✔ [22/23] Built Cache.Requests:c.o (1.8s)
✔ [23/23] Built cache:exe (2.6s)

Downloaded: 1 file(s) [attempted 1/8500 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8500 = 0%, 5 KB/s], Decompressed: 11
Downloaded: 38 file(s) [attempted 38/8500 = 0%, 14 KB/s], Decompressed: 35
Downloaded: 68 file(s) [attempted 68/8500 = 0%, 96 KB/s], Decompressed: 57
Downloaded: 96 file(s) [attempted 96/8500 = 1%, 469 KB/s], Decompressed: 83
Downloaded: 131 file(s) [attempted 131/8500 = 1%, 392 KB/s], Decompressed: 103
Downloaded: 169 file(s) [attempted 169/8500 = 1%, 275 KB/s], Decompressed: 127
Downloaded: 206 file(s) [attempted 206/8500 = 2%, 847 KB/s], Decompressed: 158
Downloaded: 240 file(s) [attempted 240/8500 = 2%, 180 KB/s], Decompressed: 192
Downloaded: 282 file(s) [attempted 282/8500 = 3%, 186 KB/s], Decompressed: 192
Downloaded: 326 file(s) [attempted 326/8500 = 3%, 146 KB/s], Decompressed: 234
Downloaded: 371 file(s) [attempted 371/8500 = 4%, 609 KB/s], Decompressed: 234
Downloaded: 408 file(s) [attempted 408/8500 = 4%, 147 KB/s], Decompressed: 305
Downloaded: 453 file(s) [attempted 453/8500 = 5%, 105 KB/s], Decompressed: 305
Downloaded: 494 file(s) [attempted 494/8500 = 5%, 1458 KB/s], Decompressed: 384
Downloaded: 532 file(s) [attempted 532/8500 = 6%, 77 KB/s], Decompressed: 384
Downloaded: 569 file(s) [attempted 569/8500 = 6%, 344 KB/s], Decompressed: 384
Downloaded: 614 file(s) [attempted 614/8500 = 7%, 753 KB/s], Decompressed: 384
Downloaded: 658 file(s) [attempted 658/8500 = 7%, 1451 KB/s], Decompressed: 490
Downloaded: 699 file(s) [attempted 699/8500 = 8%, 96 KB/s], Decompressed: 490
Downloaded: 741 file(s) [attempted 741/8500 = 8%, 524 KB/s], Decompressed: 490
Downloaded: 775 file(s) [attempted 775/8500 = 9%, 879 KB/s], Decompressed: 490
Downloaded: 819 file(s) [attempted 819/8500 = 9%, 114 KB/s], Decompressed: 617
Downloaded: 867 file(s) [attempted 867/8500 = 10%, 567 KB/s], Decompressed: 617
Downloaded: 912 file(s) [attempted 912/8500 = 10%, 54 KB/s], Decompressed: 617
Downloaded: 956 file(s) [attempted 956/8500 = 11%, 849 KB/s], Decompressed: 617
Downloaded: 1001 file(s) [attempted 1001/8500 = 11%, 108 KB/s], Decompressed: 617
Downloaded: 1045 file(s) [attempted 1045/8500 = 12%, 110 KB/s], Decompressed: 799
Downloaded: 1083 file(s) [attempted 1083/8500 = 12%, 128 KB/s], Decompressed: 799
Downloaded: 1124 file(s) [attempted 1124/8500 = 13%, 228 KB/s], Decompressed: 799
Downloaded: 1169 file(s) [attempted 1169/8500 = 13%, 347 KB/s], Decompressed: 799
Downloaded: 1206 file(s) [attempted 1206/8500 = 14%, 36 KB/s], Decompressed: 799
Downloaded: 1247 file(s) [attempted 1247/8500 = 14%, 34 KB/s], Decompressed: 1004
Downloaded: 1292 file(s) [attempted 1292/8500 = 15%, 865 KB/s], Decompressed: 1004
Downloaded: 1336 file(s) [attempted 1336/8500 = 15%, 80 KB/s], Decompressed: 1004
Downloaded: 1384 file(s) [attempted 1384/8500 = 16%, 37 KB/s], Decompressed: 1004
Downloaded: 1432 file(s) [attempted 1432/8500 = 16%, 410 KB/s], Decompressed: 1004
Downloaded: 1473 file(s) [attempted 1473/8500 = 17%, 533 KB/s], Decompressed: 1004
Downloaded: 1518 file(s) [attempted 1518/8500 = 17%, 1303 KB/s], Decompressed: 1004
Downloaded: 1555 file(s) [attempted 1555/8500 = 18%, 215 KB/s], Decompressed: 1247
Downloaded: 1600 file(s) [attempted 1600/8500 = 18%, 144 KB/s], Decompressed: 1247
Downloaded: 1637 file(s) [attempted 1637/8500 = 19%, 1672 KB/s], Decompressed: 1247
Downloaded: 1675 file(s) [attempted 1675/8500 = 19%, 228 KB/s], Decompressed: 1247
Downloaded: 1716 file(s) [attempted 1716/8500 = 20%, 465 KB/s], Decompressed: 1247
Downloaded: 1761 file(s) [attempted 1761/8500 = 20%, 289 KB/s], Decompressed: 1247
Downloaded: 1798 file(s) [attempted 1798/8500 = 21%, 437 KB/s], Decompressed: 1247
Downloaded: 1839 file(s) [attempted 1839/8500 = 21%, 118 KB/s], Decompressed: 1247
Downloaded: 1880 file(s) [attempted 1880/8500 = 22%, 234 KB/s], Decompressed: 1247
Downloaded: 1921 file(s) [attempted 1921/8500 = 22%, 674 KB/s], Decompressed: 1555
Downloaded: 1962 file(s) [attempted 1962/8500 = 23%, 355 KB/s], Decompressed: 1555
Downloaded: 2007 file(s) [attempted 2007/8500 = 23%, 140 KB/s], Decompressed: 1555
Downloaded: 2051 file(s) [attempted 2051/8500 = 24%, 347 KB/s], Decompressed: 1555
Downloaded: 2093 file(s) [attempted 2093/8500 = 24%, 94 KB/s], Decompressed: 1555
Downloaded: 2134 file(s) [attempted 2134/8500 = 25%, 198 KB/s], Decompressed: 1555
Downloaded: 2175 file(s) [attempted 2175/8500 = 25%, 319 KB/s], Decompressed: 1555
Downloaded: 2219 file(s) [attempted 2219/8500 = 26%, 278 KB/s], Decompressed: 1555
Downloaded: 2264 file(s) [attempted 2264/8500 = 26%, 27 KB/s], Decompressed: 1555
Downloaded: 2298 file(s) [attempted 2298/8500 = 27%, 708 KB/s], Decompressed: 1555
Downloaded: 2339 file(s) [attempted 2339/8500 = 27%, 107 KB/s], Decompressed: 1918
Downloaded: 2390 file(s) [attempted 2390/8500 = 28%, 102 KB/s], Decompressed: 1918
Downloaded: 2435 file(s) [attempted 2435/8500 = 28%, 667 KB/s], Decompressed: 1918
Downloaded: 2472 file(s) [attempted 2472/8500 = 29%, 65 KB/s], Decompressed: 1918
Downloaded: 2517 file(s) [attempted 2517/8500 = 29%, 228 KB/s], Decompressed: 1918
Downloaded: 2555 file(s) [attempted 2555/8500 = 30%, 499 KB/s], Decompressed: 1918
Downloaded: 2592 file(s) [attempted 2592/8500 = 30%, 374 KB/s], Decompressed: 1918
Downloaded: 2637 file(s) [attempted 2637/8500 = 31%, 2108 KB/s], Decompressed: 1918
Downloaded: 2675 file(s) [attempted 2675/8500 = 31%, 270 KB/s], Decompressed: 1918
Downloaded: 2722 file(s) [attempted 2722/8500 = 32%, 1109 KB/s], Decompressed: 1918
Downloaded: 2763 file(s) [attempted 2763/8500 = 32%, 211 KB/s], Decompressed: 1918
Downloaded: 2811 file(s) [attempted 2811/8500 = 33%, 161 KB/s], Decompressed: 1918
Downloaded: 2859 file(s) [attempted 2859/8500 = 33%, 139 KB/s], Decompressed: 1918
Downloaded: 2893 file(s) [attempted 2893/8500 = 34%, 85 KB/s], Decompressed: 2339
Downloaded: 2931 file(s) [attempted 2931/8500 = 34%, 618 KB/s], Decompressed: 2339
Downloaded: 2976 file(s) [attempted 2976/8500 = 35%, 161 KB/s], Decompressed: 2339
Downloaded: 3020 file(s) [attempted 3020/8500 = 35%, 1714 KB/s], Decompressed: 2339
Downloaded: 3064 file(s) [attempted 3064/8500 = 36%, 413 KB/s], Decompressed: 2339
Downloaded: 3106 file(s) [attempted 3106/8500 = 36%, 183 KB/s], Decompressed: 2339
Downloaded: 3140 file(s) [attempted 3140/8500 = 36%, 109 KB/s], Decompressed: 2339
Downloaded: 3184 file(s) [attempted 3184/8500 = 37%, 162 KB/s], Decompressed: 2339
Downloaded: 3229 file(s) [attempted 3229/8500 = 37%, 164 KB/s], Decompressed: 2339
Downloaded: 3270 file(s) [attempted 3270/8500 = 38%, 433 KB/s], Decompressed: 2339
Downloaded: 3314 file(s) [attempted 3314/8500 = 38%, 108 KB/s], Decompressed: 2339
Downloaded: 3359 file(s) [attempted 3359/8500 = 39%, 174 KB/s], Decompressed: 2339
Downloaded: 3403 file(s) [attempted 3403/8500 = 40%, 658 KB/s], Decompressed: 2339
Downloaded: 3444 file(s) [attempted 3444/8500 = 40%, 424 KB/s], Decompressed: 2339
Downloaded: 3482 file(s) [attempted 3482/8500 = 40%, 50 KB/s], Decompressed: 2863
Downloaded: 3526 file(s) [attempted 3526/8500 = 41%, 297 KB/s], Decompressed: 2863
Downloaded: 3564 file(s) [attempted 3564/8500 = 41%, 225 KB/s], Decompressed: 2863
Downloaded: 3609 file(s) [attempted 3609/8500 = 42%, 36 KB/s], Decompressed: 2863
Downloaded: 3657 file(s) [attempted 3657/8500 = 43%, 117 KB/s], Decompressed: 2863
Downloaded: 3704 file(s) [attempted 3704/8500 = 43%, 209 KB/s], Decompressed: 2863
Downloaded: 3742 file(s) [attempted 3742/8500 = 44%, 301 KB/s], Decompressed: 2863
Downloaded: 3793 file(s) [attempted 3793/8500 = 44%, 108 KB/s], Decompressed: 2863
Downloaded: 3841 file(s) [attempted 3841/8500 = 45%, 406 KB/s], Decompressed: 2863
Downloaded: 3886 file(s) [attempted 3886/8500 = 45%, 559 KB/s], Decompressed: 2863
Downloaded: 3923 file(s) [attempted 3923/8500 = 46%, 162 KB/s], Decompressed: 2863
Downloaded: 3965 file(s) [attempted 3965/8500 = 46%, 372 KB/s], Decompressed: 2863
Downloaded: 4009 file(s) [attempted 4009/8500 = 47%, 783 KB/s], Decompressed: 2863
Downloaded: 4047 file(s) [attempted 4047/8500 = 47%, 81 KB/s], Decompressed: 2863
Downloaded: 4084 file(s) [attempted 4084/8500 = 48%, 972 KB/s], Decompressed: 2863
Downloaded: 4129 file(s) [attempted 4129/8500 = 48%, 159 KB/s], Decompressed: 2863
Downloaded: 4163 file(s) [attempted 4163/8500 = 48%, 45 KB/s], Decompressed: 2863
Downloaded: 4204 file(s) [attempted 4204/8500 = 49%, 452 KB/s], Decompressed: 3465
Downloaded: 4252 file(s) [attempted 4252/8500 = 50%, 550 KB/s], Decompressed: 3465
Downloaded: 4300 file(s) [attempted 4300/8500 = 50%, 71 KB/s], Decompressed: 3465
Downloaded: 4348 file(s) [attempted 4348/8500 = 51%, 2046 KB/s], Decompressed: 3465
Downloaded: 4396 file(s) [attempted 4396/8500 = 51%, 114 KB/s], Decompressed: 3465
Downloaded: 4440 file(s) [attempted 4440/8500 = 52%, 144 KB/s], Decompressed: 3465
Downloaded: 4485 file(s) [attempted 4485/8500 = 52%, 241 KB/s], Decompressed: 3465
Downloaded: 4533 file(s) [attempted 4533/8500 = 53%, 290 KB/s], Decompressed: 3465
Downloaded: 4574 file(s) [attempted 4574/8500 = 53%, 1051 KB/s], Decompressed: 3465
Downloaded: 4611 file(s) [attempted 4611/8500 = 54%, 51 KB/s], Decompressed: 3465
Downloaded: 4656 file(s) [attempted 4656/8500 = 54%, 60 KB/s], Decompressed: 3465
Downloaded: 4697 file(s) [attempted 4697/8500 = 55%, 247 KB/s], Decompressed: 3465
Downloaded: 4733 file(s) [attempted 4733/8500 = 55%, 202 KB/s], Decompressed: 3465
Downloaded: 4776 file(s) [attempted 4776/8500 = 56%, 102 KB/s], Decompressed: 3465
Downloaded: 4817 file(s) [attempted 4817/8500 = 56%, 404 KB/s], Decompressed: 3465
Downloaded: 4858 file(s) [attempted 4858/8500 = 57%, 198 KB/s], Decompressed: 3465
Downloaded: 4902 file(s) [attempted 4902/8500 = 57%, 106 KB/s], Decompressed: 3465
Downloaded: 4947 file(s) [attempted 4947/8500 = 58%, 162 KB/s], Decompressed: 3465
Downloaded: 4988 file(s) [attempted 4988/8500 = 58%, 481 KB/s], Decompressed: 3465
Downloaded: 5022 file(s) [attempted 5022/8500 = 59%, 290 KB/s], Decompressed: 3465
Downloaded: 5063 file(s) [attempted 5063/8500 = 59%, 458 KB/s], Decompressed: 4197
Downloaded: 5111 file(s) [attempted 5111/8500 = 60%, 106 KB/s], Decompressed: 4197
Downloaded: 5156 file(s) [attempted 5156/8500 = 60%, 1035 KB/s], Decompressed: 4197
Downloaded: 5197 file(s) [attempted 5197/8500 = 61%, 117 KB/s], Decompressed: 4197
Downloaded: 5238 file(s) [attempted 5238/8500 = 61%, 23 KB/s], Decompressed: 4197
Downloaded: 5279 file(s) [attempted 5279/8500 = 62%, 148 KB/s], Decompressed: 4197
Downloaded: 5316 file(s) [attempted 5316/8500 = 62%, 127 KB/s], Decompressed: 4197
Downloaded: 5361 file(s) [attempted 5361/8500 = 63%, 476 KB/s], Decompressed: 4197
Downloaded: 5402 file(s) [attempted 5402/8500 = 63%, 393 KB/s], Decompressed: 4197
Downloaded: 5443 file(s) [attempted 5443/8500 = 64%, 292 KB/s], Decompressed: 4197
Downloaded: 5481 file(s) [attempted 5481/8500 = 64%, 875 KB/s], Decompressed: 4197
Downloaded: 5525 file(s) [attempted 5525/8500 = 65%, 658 KB/s], Decompressed: 4197
Downloaded: 5566 file(s) [attempted 5566/8500 = 65%, 41 KB/s], Decompressed: 4197
Downloaded: 5611 file(s) [attempted 5611/8500 = 66%, 69 KB/s], Decompressed: 4197
Downloaded: 5655 file(s) [attempted 5655/8500 = 66%, 114 KB/s], Decompressed: 4197
Downloaded: 5696 file(s) [attempted 5696/8500 = 67%, 442 KB/s], Decompressed: 4197
Downloaded: 5730 file(s) [attempted 5730/8500 = 67%, 769 KB/s], Decompressed: 4197
Downloaded: 5778 file(s) [attempted 5778/8500 = 67%, 485 KB/s], Decompressed: 4197
Downloaded: 5826 file(s) [attempted 5826/8500 = 68%, 113 KB/s], Decompressed: 4197
Downloaded: 5874 file(s) [attempted 5874/8500 = 69%, 1064 KB/s], Decompressed: 4197
Downloaded: 5919 file(s) [attempted 5919/8500 = 69%, 100 KB/s], Decompressed: 4197
Downloaded: 5960 file(s) [attempted 5960/8500 = 70%, 1183 KB/s], Decompressed: 4197
Downloaded: 6001 file(s) [attempted 6001/8500 = 70%, 486 KB/s], Decompressed: 4197
Downloaded: 6042 file(s) [attempted 6042/8500 = 71%, 554 KB/s], Decompressed: 5046
Downloaded: 6086 file(s) [attempted 6086/8500 = 71%, 234 KB/s], Decompressed: 5046
Downloaded: 6127 file(s) [attempted 6127/8500 = 72%, 182 KB/s], Decompressed: 5046
Downloaded: 6162 file(s) [attempted 6162/8500 = 72%, 236 KB/s], Decompressed: 5046
Downloaded: 6210 file(s) [attempted 6210/8500 = 73%, 47 KB/s], Decompressed: 5046
Downloaded: 6254 file(s) [attempted 6254/8500 = 73%, 97 KB/s], Decompressed: 5046
Downloaded: 6295 file(s) [attempted 6295/8500 = 74%, 400 KB/s], Decompressed: 5046
Downloaded: 6336 file(s) [attempted 6336/8500 = 74%, 525 KB/s], Decompressed: 5046
Downloaded: 6370 file(s) [attempted 6370/8500 = 74%, 346 KB/s], Decompressed: 5046
Downloaded: 6418 file(s) [attempted 6418/8500 = 75%, 241 KB/s], Decompressed: 5046
Downloaded: 6456 file(s) [attempted 6456/8500 = 75%, 93 KB/s], Decompressed: 5046
Downloaded: 6497 file(s) [attempted 6497/8500 = 76%, 132 KB/s], Decompressed: 5046
Downloaded: 6542 file(s) [attempted 6542/8500 = 76%, 158 KB/s], Decompressed: 5046
Downloaded: 6586 file(s) [attempted 6586/8500 = 77%, 103 KB/s], Decompressed: 5046
Downloaded: 6617 file(s) [attempted 6617/8500 = 77%, 351 KB/s], Decompressed: 5046
Downloaded: 6665 file(s) [attempted 6665/8500 = 78%, 196 KB/s], Decompressed: 5046
Downloaded: 6704 file(s) [attempted 6704/8500 = 78%, 90 KB/s], Decompressed: 5046
Downloaded: 6743 file(s) [attempted 6743/8500 = 79%, 469 KB/s], Decompressed: 5046
Downloaded: 6785 file(s) [attempted 6785/8500 = 79%, 80 KB/s], Decompressed: 5046
Downloaded: 6822 file(s) [attempted 6822/8500 = 80%, 241 KB/s], Decompressed: 5046
Downloaded: 6867 file(s) [attempted 6867/8500 = 80%, 294 KB/s], Decompressed: 5046
Downloaded: 6904 file(s) [attempted 6904/8500 = 81%, 195 KB/s], Decompressed: 5046
Downloaded: 6950 file(s) [attempted 6950/8500 = 81%, 951 KB/s], Decompressed: 5046
Downloaded: 6986 file(s) [attempted 6986/8500 = 82%, 879 KB/s], Decompressed: 5046
Downloaded: 7028 file(s) [attempted 7028/8500 = 82%, 253 KB/s], Decompressed: 5046
Downloaded: 7072 file(s) [attempted 7072/8500 = 83%, 937 KB/s], Decompressed: 5046
Downloaded: 7110 file(s) [attempted 7110/8500 = 83%, 252 KB/s], Decompressed: 5046
Downloaded: 7154 file(s) [attempted 7154/8500 = 84%, 116 KB/s], Decompressed: 5046
Downloaded: 7195 file(s) [attempted 7195/8500 = 84%, 80 KB/s], Decompressed: 6028
Downloaded: 7229 file(s) [attempted 7229/8500 = 85%, 25 KB/s], Decompressed: 6028
Downloaded: 7270 file(s) [attempted 7270/8500 = 85%, 1069 KB/s], Decompressed: 6028
Downloaded: 7312 file(s) [attempted 7312/8500 = 86%, 60 KB/s], Decompressed: 6028
Downloaded: 7356 file(s) [attempted 7356/8500 = 86%, 106 KB/s], Decompressed: 6028
Downloaded: 7397 file(s) [attempted 7397/8500 = 87%, 1518 KB/s], Decompressed: 6028
Downloaded: 7435 file(s) [attempted 7435/8500 = 87%, 460 KB/s], Decompressed: 6028
Downloaded: 7476 file(s) [attempted 7476/8500 = 87%, 115 KB/s], Decompressed: 6028
Downloaded: 7517 file(s) [attempted 7517/8500 = 88%, 330 KB/s], Decompressed: 6028
Downloaded: 7561 file(s) [attempted 7561/8500 = 88%, 131 KB/s], Decompressed: 6028
Downloaded: 7602 file(s) [attempted 7602/8500 = 89%, 294 KB/s], Decompressed: 6028
Downloaded: 7644 file(s) [attempted 7644/8500 = 89%, 146 KB/s], Decompressed: 6028
Downloaded: 7685 file(s) [attempted 7685/8500 = 90%, 91 KB/s], Decompressed: 6028
Downloaded: 7726 file(s) [attempted 7726/8500 = 90%, 49 KB/s], Decompressed: 6028
Downloaded: 7770 file(s) [attempted 7770/8500 = 91%, 126 KB/s], Decompressed: 6028
Downloaded: 7811 file(s) [attempted 7811/8500 = 91%, 479 KB/s], Decompressed: 6028
Downloaded: 7849 file(s) [attempted 7849/8500 = 92%, 621 KB/s], Decompressed: 6028
Downloaded: 7893 file(s) [attempted 7893/8500 = 92%, 309 KB/s], Decompressed: 6028
Downloaded: 7938 file(s) [attempted 7938/8500 = 93%, 1581 KB/s], Decompressed: 6028
Downloaded: 7979 file(s) [attempted 7979/8500 = 93%, 93 KB/s], Decompressed: 6028
Downloaded: 8017 file(s) [attempted 8017/8500 = 94%, 90 KB/s], Decompressed: 6028
Downloaded: 8058 file(s) [attempted 8058/8500 = 94%, 192 KB/s], Decompressed: 6028
Downloaded: 8106 file(s) [attempted 8106/8500 = 95%, 83 KB/s], Decompressed: 6028
Downloaded: 8147 file(s) [attempted 8147/8500 = 95%, 911 KB/s], Decompressed: 6028
Downloaded: 8184 file(s) [attempted 8184/8500 = 96%, 98 KB/s], Decompressed: 6028
Downloaded: 8229 file(s) [attempted 8229/8500 = 96%, 516 KB/s], Decompressed: 6028
Downloaded: 8266 file(s) [attempted 8266/8500 = 97%, 314 KB/s], Decompressed: 6028
Downloaded: 8304 file(s) [attempted 8304/8500 = 97%, 46 KB/s], Decompressed: 6028
Downloaded: 8352 file(s) [attempted 8352/8500 = 98%, 179 KB/s], Decompressed: 6028
Downloaded: 8396 file(s) [attempted 8396/8500 = 98%, 1164 KB/s], Decompressed: 6028
Downloaded: 8437 file(s) [attempted 8437/8500 = 99%, 278 KB/s], Decompressed: 6028
Downloaded: 8475 file(s) [attempted 8475/8500 = 99%, 37 KB/s], Decompressed: 7161
Downloaded: 8499 file(s) [attempted 8499/8500 = 99%, 275 KB/s], Decompressed: 7161
Downloaded: 8500 file(s) [attempted 8500/8500 = 100%, 275 KB/s], Decompressed: 7161

lean_checker exit 0 duration 6m 25s · created 6/6/2026, 11:08:24 AM

lake build

✔ [2952/2980] Built FLT.Assumptions.Mazur (4.8s)
✔ [3079/3125] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (4.9s)
✔ [3080/3125] Built FLT.Mathlib.Algebra.Algebra.Tower (4.9s)
✔ [3276/3318] Built FLT.Assumptions.Odlyzko (5.3s)
✔ [3298/3318] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (2.4s)
✔ [3299/3318] Built FLT.Mathlib.Algebra.FixedPoints.Basic (3.7s)
✔ [3300/3318] Built FLT.Mathlib.Topology.Algebra.Group.Units (2.1s)
✔ [3301/3318] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (5.4s)
✔ [3303/3318] Built FLT.Mathlib.Order.Filter.Cofinite (2.4s)
✔ [3305/3318] Built FLT.Mathlib.Topology.Bases (2.0s)
✔ [3306/3318] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (2.2s)
✔ [3307/3318] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (7.9s)
✔ [3308/3318] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (2.2s)
✔ [3310/3319] Built FLT.Mathlib.MeasureTheory.Group.Action (4.2s)
✔ [3311/3319] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (2.6s)
✔ [3312/3332] Built FLT.Mathlib.MeasureTheory.Group.Measure (2.9s)
✔ [3318/3339] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (6.9s)
✔ [3324/3339] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (2.1s)
✔ [3325/3339] Built FLT.Hacks.RightActionInstances (7.2s)
✔ [3327/3340] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (2.2s)
✔ [3328/3340] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (9.3s)
✔ [3330/3343] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (3.7s)
✔ [3332/3344] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (2.8s)
✔ [3334/3350] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (3.5s)
✔ [3339/3350] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (1.9s)
✔ [3344/3357] Built FLT.Mathlib.LinearAlgebra.Countable (2.5s)
✔ [3350/3377] Built FLT.AutomorphicForm.QuaternionAlgebra.Defs (7.1s)
✔ [3358/3377] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (9.5s)
✔ [3359/3377] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (5.0s)
✔ [3363/3377] Built FLT.Mathlib.RingTheory.Localization.BaseChange (4.4s)
✔ [3364/3377] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (4.8s)
✔ [3365/3381] Built FLT.DedekindDomain.AdicValuation (18s)
✔ [3371/3381] Built FLT.HaarMeasure.HaarChar.AddEquiv (13s)
✔ [3374/3395] Built FLT.DedekindDomain.IntegralClosure (9.6s)
✔ [3377/3395] Built FLT.NumberField.Completion.Finite (4.2s)
✔ [3378/3395] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (18s)
✔ [3379/3395] Built FLT.HaarMeasure.HaarChar.Ring (5.0s)
✔ [3380/3395] Built FLT.NumberField.HeightOneSpectrum (3.4s)
✔ [3382/3395] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (3.2s)
✔ [3384/3405] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (1.0s)
✔ [3386/3405] Built FLT.Mathlib.Algebra.Algebra.Hom (3.6s)
✔ [3387/3405] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (3.1s)
✔ [3390/3409] Built FLT.Mathlib.Topology.Algebra.MulAction (2.3s)
✔ [3391/3409] Built FLT.Mathlib.LinearAlgebra.Pi (2.5s)
✔ [3392/3409] Built FLT.Mathlib.Algebra.IsDirectLimit (3.8s)
✔ [3393/3409] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (5.4s)
✔ [3394/3409] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (2.8s)
✔ [3396/3409] Built FLT.Mathlib.Topology.Algebra.UniformRing (2.5s)
✔ [3399/3409] Built FLT.Mathlib.Algebra.Algebra.Pi (2.6s)
✔ [3400/3424] Built FLT.Mathlib.Algebra.Algebra.Bilinear (3.0s)
✔ [3402/3425] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (3.1s)
✔ [3405/3425] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (5.5s)
✔ [3406/3425] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (2.7s)
✔ [3407/3425] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (2.7s)
✔ [3408/3425] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (3.1s)
✔ [3409/3425] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (2.5s)
✔ [3410/3425] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (13s)
✔ [3411/3425] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (2.7s)
✔ [3413/3428] Built FLT.NumberField.InfinitePlace.Extension (4.8s)
✔ [3416/3428] Built FLT.Mathlib.Topology.Constructions (2.8s)
✔ [3417/3435] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (3.7s)
✔ [3419/3437] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (4.2s)
✔ [3420/3437] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (3.9s)
✔ [3422/3437] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (4.5s)
✔ [3423/3437] Built FLT.Mathlib.Data.Real.Archimedean (3.1s)
✔ [3424/3437] Built FLT.NumberField.Padics.RestrictedProduct (7.0s)
✔ [3426/3437] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (15s)
✔ [3428/3440] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (3.1s)
✔ [3429/3440] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (3.6s)
✔ [3431/3453] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (3.6s)
✔ [3438/3462] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (3.8s)
✔ [3440/3465] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (12s)
✔ [3442/3465] Built FLT.HaarMeasure.MeasurableSpacePadics (6.3s)
✔ [3443/3465] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (8.7s)
✔ [3445/3468] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (2.3s)
✔ [3447/3468] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (2.4s)
✔ [3449/3468] Built FLT.HaarMeasure.HaarChar.RealComplex (3.0s)
✔ [3451/3468] Built FLT.HaarMeasure.HaarChar.Padic (4.6s)
✔ [3453/3468] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.0s)
✔ [3454/3468] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (3.8s)
✔ [3456/3468] Built FLT.Mathlib.Algebra.Central.TensorProduct (4.5s)
✔ [3457/3468] Built FLT.Mathlib.GroupTheory.DoubleCoset (2.1s)
✔ [3458/3469] Built FLT.DedekindDomain.Completion.BaseChange (60s)
✔ [3459/3473] Built FLT.NumberField.Completion.Infinite (36s)
✔ [3461/3473] Built FLT.Mathlib.LinearAlgebra.Determinant (8.3s)
✔ [3464/3474] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (12s)
✔ [3472/3487] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (6.5s)
✔ [3473/3487] Built FLT.Mathlib.Topology.HomToDiscrete (3.2s)
✔ [3475/3499] Built FLT.Mathlib.Topology.Polish (2.1s)
✔ [3477/3504] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (4.2s)
✔ [3479/3504] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (2.6s)
✔ [3480/3504] Built FLT.Mathlib.Topology.Instances.Matrix (2.7s)
✔ [3481/3504] Built FLT.NumberField.InfiniteAdeleRing (24s)
✔ [3482/3504] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (2.9s)
✔ [3486/3504] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (6.7s)
✔ [3487/3504] Built FLT.Deformations.Algebra.InverseLimit.Basic (9.9s)
✔ [3488/3504] Built FLT.Mathlib.MeasureTheory.Haar.Extension (5.7s)
✔ [3490/3504] Built FLT.Data.QHat (14s)
✔ [3491/3504] Built FLT.Deformations.Algebra.InverseLimit.Topology (6.7s)
✔ [3492/3511] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (3.5s)
✔ [3493/3513] Built FLT.Data.Hurwitz (10s)
✔ [3496/3513] Built FLT.Data.HurwitzRatHat (6.2s)
✔ [3502/3517] Built FLT.Patching.Utils.Lemmas (9.9s)
✔ [3505/3520] Built FLT.QuaternionAlgebra.NumberField (21s)
✔ [3508/3534] Built FLT.Patching.Utils.InverseLimit (2.2s)
✔ [3516/3534] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (65s)
✔ [3517/3534] Built FLT.Deformations.Lemmas (7.5s)
✔ [3520/3535] Built FLT.Mathlib.RingTheory.LocalRing.Defs (2.6s)
✔ [3521/3535] Built FLT.Deformations.Subfunctor (2.1s)
✔ [3522/3535] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (2.5s)
✔ [3523/3535] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (11s)
✔ [3525/3555] Built FLT.Deformations.IsResidueAlgebra (3.6s)
✔ [3572/3586] Built FLT.Patching.Utils.AdicTopology (6.1s)
✔ [3573/3586] Built FLT.Deformations.RepresentationTheory.IntegralClosure (3.8s)
✔ [3575/3586] Built FLT.Deformations.RepresentationTheory.Frobenius (4.6s)
✔ [3594/3606] Built FLT.Deformations.IsProartinian (3.5s)
✔ [3596/3614] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (14s)
✔ [3606/3638] Built FLT.Deformations.Categories (4.9s)
✔ [3625/3639] Built FLT.Mathlib.RepresentationTheory.Basic (3.3s)
✔ [3626/3639] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (107s)
✔ [3629/3649] Built FLT.Deformations.RepresentationTheory.Irreducible (2.4s)
✔ [3802/3827] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (3.3s)
✔ [3806/3832] Built FLT.GaloisRepresentation.Cyclotomic (3.2s)
✔ [3808/3833] Built FLT.Deformations.RepresentationTheory.Etale (14s)
✔ [3931/3968] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (20s)
✔ [3932/3968] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (2.7s)
✔ [3933/3968] Built FLT.FreyCurve.FreyPackage (5.3s)
✔ [3935/3968] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (3.4s)
✔ [3936/3968] Built FLT.Mathlib.Data.Fin.Basic (1.7s)
✔ [3937/3968] Built FLT.Mathlib.GroupTheory.Index (1.7s)
✔ [3938/3968] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.9s)
✔ [3940/3968] Built FLT.Mathlib.MeasureTheory.Measure.Regular (2.2s)
✔ [3945/3973] Built FLT.Mathlib.NumberTheory.NumberField.Completion (2.8s)
✔ [3946/3973] Built FLT.Mathlib.Topology.Algebra.Monoid (2.2s)
✔ [3953/3982] Built FLT.Mathlib.Topology.Algebra.Order.Field (4.5s)
✔ [3957/3985] Built FLT.Patching.Utils.TopologicallyFG (3.0s)
✔ [3959/3987] Built FLT.NumberField.DiscriminantBounds (5.7s)
✔ [3961/3987] Built FLT.GlobalLanglandsConjectures.GLnDefs (16s)
✔ [3964/4011] Built FLT.GlobalLanglandsConjectures.GLzero (5.1s)
✔ [3965/4011] Built FLT.Patching.Utils.StructureFiniteness (8.3s)
✔ [3983/4011] Built FLT.Deformations.RepresentationTheory.GaloisRep (23s)
✔ [3984/4011] Built FLT.Patching.Utils.CompactHausdorffRings (4.7s)
✔ [3985/4011] Built FLT.Patching.Utils.Depth (6.6s)
✔ [3986/4011] Built FLT.NumberField.AdeleRing (48s)
✔ [3987/4011] Built FLT.GaloisRepresentation.Automorphic (4.9s)
✔ [3988/4011] Built FLT.GaloisRepresentation.HardlyRamified.Defs (3.8s)
✔ [3989/4011] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (2.0s)
✔ [3990/4011] Built FLT.EllipticCurve.Torsion (3.7s)
✔ [3991/4011] Built FLT.Patching.Ultraproduct (16s)
✔ [3992/4011] Built FLT.Deformations.LiftFunctor (6.5s)
✔ [3993/4011] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (3.0s)
✔ [3994/4011] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (3.2s)
✔ [3995/4011] Built FLT.GaloisRepresentation.HardlyRamified.Lift (4.8s)
✔ [3996/4011] Built FLT.GaloisRepresentation.HardlyRamified.Family (5.2s)
✔ [3997/4011] Built FLT.GaloisRepresentation.HardlyRamified.Frey (4.6s)
✔ [3998/4011] Built FLT.Patching.VanishingFilter (5.6s)
✔ [3999/4011] Built FLT.Deformations.Representable (4.8s)
✔ [4000/4011] Built FLT.HaarMeasure.HaarChar.AdeleRing (20s)
✔ [4001/4011] Built FLT.FreyCurve.Contradiction (2.0s)
✔ [4002/4011] Built FLT.Patching.Algebra (17s)
✔ [4003/4011] Built FLT.Patching.Module (21s)
✔ [4004/4011] Built FLT.Patching.Over (15s)
✔ [4005/4011] Built FLT.Patching.System (12s)
✔ [4006/4011] Built FLT.Patching.REqualsT (4.7s)
✔ [4007/4011] Built FLT.DivisionAlgebra.Finiteness (52s)
✔ [4008/4011] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (2.3s)
✔ [4009/4011] Built FLT (1.9s)
✔ [4010/4011] Built FermatsLastTheorem (17s)
Build completed successfully (4011 jobs).

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

blueprint_build exit 1 duration 3s · created 6/6/2026, 11:08:24 AM

lake build :blueprint

warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: unknown package facet `blueprint`

semantic_extract exit - duration 4h 0m · created 6/6/2026, 11:08:24 AM

./.apodeixis/tools/lean-semantic-extract.sh

warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache c47fb553dff1df6e153b5315866e7078a3b2ede54e88a41ebfdb408259f9f93d
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
/usr/bin/podman timed out after 14400s
podman cleanup removed verifier container apx-verifier-job-129-runtime-semantic_extract-2608519-1780729625022123987-15