Verification run

Run 2

ImperialCollegeLondon/FLT branch main triggered via poller

failed commit 5cb37b0416d2 toolchain lean-v4-31-0-rc1 prover lean took 21m 55s · finished 6w ago

./.apodeixis/tools/lean-semantic-extract.sh failed with exit code 1 (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 767 ms · created 6/2/2026, 12:15:21 PM

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

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

git_checkout exit 0 duration 25 ms · created 6/2/2026, 12:15:21 PM

git checkout 5cb37b0416d2953c97dc2445326d2a3323ca5d4d

Note: switching to '5cb37b0416d2953c97dc2445326d2a3323ca5d4d'.

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 5cb37b0 chore: bump mathlib to d568c8c, fix breaking changes (#993)

lake_cache exit 0 duration 1m 28s · created 6/2/2026, 12:15:21 PM

lake exe cache get

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

info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git
info: checkdecls: checking out revision '3d425859e73fcfbef85b9638c2a91708ef4a22d4'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'd568c8c09630de097a046763c17b9ea99f95f950'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'd575be693add4fe9cb996968968ce42ce75c5ccd'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'c5d5b8fe6e5158def25cd28eb94e4141ad97c843'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '6db47de43aa7f516708053ae2fdadd29dd9baaaa'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '85bb7e7637e84a7d9803be7d954579fdae42c64b'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'fafca80479ff95e041d84373dda7122adf1295f2'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '8d33324ee877e9735d2829bc6f1f439e60cf98b1'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '708b057842c4cd0845fba132bd94b08493f6fc42'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '48bdcff4c5fa27e09028f9f330e59baa0d4640cf'
✔ [4/24] Built Batteries.Data.String.Basic (624ms)
✔ [5/24] Built Cache.Lean (834ms)
✔ [6/24] Built Batteries.Data.Array.Match (1.1s)
✔ [7/24] Built Batteries.Data.String.Basic:c.o (499ms)
✔ [8/24] Built Cache.Lean:c.o (134ms)
✔ [9/24] Built Cache.Init (466ms)
✔ [10/24] Built Batteries.Data.Array.Match:c.o (275ms)
✔ [11/24] Built Cache.Init:c.o (102ms)
✔ [12/24] Built Batteries.Tactic.OpenPrivate (1.6s)
✔ [13/24] Built Batteries.Data.String.Matcher (488ms)
✔ [14/24] Built Batteries.Data.String.Matcher:c.o (154ms)
✔ [15/24] Built Batteries.Tactic.OpenPrivate:c.o (967ms)
✔ [16/24] Built Cache.IO (1.7s)
✔ [17/24] Built Cache.Hashing (1.0s)
✔ [18/24] Built Cache.IO:c.o (1.2s)
✔ [19/24] Built Cache.Hashing:c.o (368ms)
✔ [20/24] Built Cache.Requests (2.1s)
✔ [21/24] Built Cache.Main (1.1s)
✔ [22/24] Built Cache.Main:c.o (576ms)
✔ [23/24] Built Cache.Requests:c.o (1.8s)
✔ [24/24] Built cache:exe (2.3s)

Downloaded: 1 file(s) [attempted 1/8477 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8477 = 0%, 11 KB/s], Decompressed: 11
Downloaded: 37 file(s) [attempted 37/8477 = 0%, 15 KB/s], Decompressed: 28
Downloaded: 62 file(s) [attempted 62/8477 = 0%, 30 KB/s], Decompressed: 61
Downloaded: 93 file(s) [attempted 93/8477 = 1%, 60 KB/s], Decompressed: 83
Downloaded: 127 file(s) [attempted 127/8477 = 1%, 251 KB/s], Decompressed: 107
Downloaded: 165 file(s) [attempted 165/8477 = 1%, 506 KB/s], Decompressed: 141
Downloaded: 206 file(s) [attempted 206/8477 = 2%, 441 KB/s], Decompressed: 165
Downloaded: 244 file(s) [attempted 244/8477 = 2%, 776 KB/s], Decompressed: 192
Downloaded: 288 file(s) [attempted 288/8477 = 3%, 78 KB/s], Decompressed: 230
Downloaded: 329 file(s) [attempted 329/8477 = 3%, 363 KB/s], Decompressed: 268
Downloaded: 367 file(s) [attempted 367/8477 = 4%, 88 KB/s], Decompressed: 268
Downloaded: 405 file(s) [attempted 405/8477 = 4%, 109 KB/s], Decompressed: 316
Downloaded: 446 file(s) [attempted 446/8477 = 5%, 722 KB/s], Decompressed: 371
Downloaded: 487 file(s) [attempted 487/8477 = 5%, 82 KB/s], Decompressed: 422
Downloaded: 525 file(s) [attempted 525/8477 = 6%, 614 KB/s], Decompressed: 422
Downloaded: 566 file(s) [attempted 566/8477 = 6%, 548 KB/s], Decompressed: 480
Downloaded: 610 file(s) [attempted 610/8477 = 7%, 541 KB/s], Decompressed: 480
Downloaded: 651 file(s) [attempted 651/8477 = 7%, 130 KB/s], Decompressed: 480
Downloaded: 689 file(s) [attempted 689/8477 = 8%, 156 KB/s], Decompressed: 555
Downloaded: 734 file(s) [attempted 734/8477 = 8%, 123 KB/s], Decompressed: 555
Downloaded: 775 file(s) [attempted 775/8477 = 9%, 1940 KB/s], Decompressed: 555
Downloaded: 819 file(s) [attempted 819/8477 = 9%, 95 KB/s], Decompressed: 658
Downloaded: 860 file(s) [attempted 860/8477 = 10%, 512 KB/s], Decompressed: 658
Downloaded: 898 file(s) [attempted 898/8477 = 10%, 432 KB/s], Decompressed: 658
Downloaded: 936 file(s) [attempted 936/8477 = 11%, 131 KB/s], Decompressed: 782
Downloaded: 980 file(s) [attempted 980/8477 = 11%, 602 KB/s], Decompressed: 782
Downloaded: 1021 file(s) [attempted 1021/8477 = 12%, 186 KB/s], Decompressed: 782
Downloaded: 1066 file(s) [attempted 1066/8477 = 12%, 704 KB/s], Decompressed: 782
Downloaded: 1100 file(s) [attempted 1100/8477 = 12%, 566 KB/s], Decompressed: 925
Downloaded: 1134 file(s) [attempted 1134/8477 = 13%, 301 KB/s], Decompressed: 925
Downloaded: 1179 file(s) [attempted 1179/8477 = 13%, 125 KB/s], Decompressed: 925
Downloaded: 1223 file(s) [attempted 1223/8477 = 14%, 383 KB/s], Decompressed: 925
Downloaded: 1261 file(s) [attempted 1261/8477 = 14%, 285 KB/s], Decompressed: 925
Downloaded: 1299 file(s) [attempted 1299/8477 = 15%, 334 KB/s], Decompressed: 1083
Downloaded: 1340 file(s) [attempted 1340/8477 = 15%, 411 KB/s], Decompressed: 1083
Downloaded: 1384 file(s) [attempted 1384/8477 = 16%, 268 KB/s], Decompressed: 1083
Downloaded: 1425 file(s) [attempted 1425/8477 = 16%, 75 KB/s], Decompressed: 1083
Downloaded: 1466 file(s) [attempted 1466/8477 = 17%, 505 KB/s], Decompressed: 1268
Downloaded: 1511 file(s) [attempted 1511/8477 = 17%, 87 KB/s], Decompressed: 1268
Downloaded: 1548 file(s) [attempted 1548/8477 = 18%, 251 KB/s], Decompressed: 1268
Downloaded: 1589 file(s) [attempted 1589/8477 = 18%, 173 KB/s], Decompressed: 1268
Downloaded: 1631 file(s) [attempted 1631/8477 = 19%, 704 KB/s], Decompressed: 1268
Downloaded: 1668 file(s) [attempted 1668/8477 = 19%, 247 KB/s], Decompressed: 1268
Downloaded: 1709 file(s) [attempted 1709/8477 = 20%, 283 KB/s], Decompressed: 1466
Downloaded: 1750 file(s) [attempted 1750/8477 = 20%, 175 KB/s], Decompressed: 1466
Downloaded: 1791 file(s) [attempted 1791/8477 = 21%, 794 KB/s], Decompressed: 1466
Downloaded: 1829 file(s) [attempted 1829/8477 = 21%, 208 KB/s], Decompressed: 1466
Downloaded: 1870 file(s) [attempted 1870/8477 = 22%, 287 KB/s], Decompressed: 1466
Downloaded: 1915 file(s) [attempted 1915/8477 = 22%, 276 KB/s], Decompressed: 1466
Downloaded: 1952 file(s) [attempted 1952/8477 = 23%, 39 KB/s], Decompressed: 1466
Downloaded: 1990 file(s) [attempted 1990/8477 = 23%, 1278 KB/s], Decompressed: 1702
Downloaded: 2034 file(s) [attempted 2034/8477 = 23%, 685 KB/s], Decompressed: 1702
Downloaded: 2072 file(s) [attempted 2072/8477 = 24%, 39 KB/s], Decompressed: 1702
Downloaded: 2117 file(s) [attempted 2117/8477 = 24%, 80 KB/s], Decompressed: 1702
Downloaded: 2154 file(s) [attempted 2154/8477 = 25%, 179 KB/s], Decompressed: 1702
Downloaded: 2195 file(s) [attempted 2195/8477 = 25%, 504 KB/s], Decompressed: 1702
Downloaded: 2236 file(s) [attempted 2236/8477 = 26%, 488 KB/s], Decompressed: 1702
Downloaded: 2277 file(s) [attempted 2277/8477 = 26%, 2124 KB/s], Decompressed: 1702
Downloaded: 2312 file(s) [attempted 2312/8477 = 27%, 604 KB/s], Decompressed: 1973
Downloaded: 2346 file(s) [attempted 2346/8477 = 27%, 166 KB/s], Decompressed: 1973
Downloaded: 2390 file(s) [attempted 2390/8477 = 28%, 282 KB/s], Decompressed: 1973
Downloaded: 2438 file(s) [attempted 2438/8477 = 28%, 233 KB/s], Decompressed: 1973
Downloaded: 2483 file(s) [attempted 2483/8477 = 29%, 156 KB/s], Decompressed: 1973
Downloaded: 2517 file(s) [attempted 2517/8477 = 29%, 253 KB/s], Decompressed: 1973
Downloaded: 2555 file(s) [attempted 2555/8477 = 30%, 113 KB/s], Decompressed: 1973
Downloaded: 2599 file(s) [attempted 2599/8477 = 30%, 39 KB/s], Decompressed: 1973
Downloaded: 2640 file(s) [attempted 2640/8477 = 31%, 123 KB/s], Decompressed: 1973
Downloaded: 2681 file(s) [attempted 2681/8477 = 31%, 416 KB/s], Decompressed: 2294
Downloaded: 2719 file(s) [attempted 2719/8477 = 32%, 501 KB/s], Decompressed: 2294
Downloaded: 2760 file(s) [attempted 2760/8477 = 32%, 234 KB/s], Decompressed: 2294
Downloaded: 2804 file(s) [attempted 2804/8477 = 33%, 160 KB/s], Decompressed: 2294
Downloaded: 2845 file(s) [attempted 2845/8477 = 33%, 103 KB/s], Decompressed: 2294
Downloaded: 2876 file(s) [attempted 2876/8477 = 33%, 24 KB/s], Decompressed: 2294
Downloaded: 2917 file(s) [attempted 2917/8477 = 34%, 293 KB/s], Decompressed: 2294
Downloaded: 2965 file(s) [attempted 2965/8477 = 34%, 42 KB/s], Decompressed: 2294
Downloaded: 3010 file(s) [attempted 3010/8477 = 35%, 394 KB/s], Decompressed: 2294
Downloaded: 3047 file(s) [attempted 3047/8477 = 35%, 122 KB/s], Decompressed: 2294
Downloaded: 3088 file(s) [attempted 3088/8477 = 36%, 115 KB/s], Decompressed: 2294
Downloaded: 3126 file(s) [attempted 3126/8477 = 36%, 195 KB/s], Decompressed: 2661
Downloaded: 3167 file(s) [attempted 3167/8477 = 37%, 1575 KB/s], Decompressed: 2661
Downloaded: 3205 file(s) [attempted 3205/8477 = 37%, 235 KB/s], Decompressed: 2661
Downloaded: 3246 file(s) [attempted 3246/8477 = 38%, 282 KB/s], Decompressed: 2661
Downloaded: 3290 file(s) [attempted 3290/8477 = 38%, 409 KB/s], Decompressed: 2661
Downloaded: 3328 file(s) [attempted 3328/8477 = 39%, 41 KB/s], Decompressed: 2661
Downloaded: 3372 file(s) [attempted 3372/8477 = 39%, 56 KB/s], Decompressed: 2661
Downloaded: 3410 file(s) [attempted 3410/8477 = 40%, 419 KB/s], Decompressed: 2661
Downloaded: 3451 file(s) [attempted 3451/8477 = 40%, 57 KB/s], Decompressed: 2661
Downloaded: 3492 file(s) [attempted 3492/8477 = 41%, 240 KB/s], Decompressed: 2661
Downloaded: 3533 file(s) [attempted 3533/8477 = 41%, 416 KB/s], Decompressed: 2661
Downloaded: 3574 file(s) [attempted 3574/8477 = 42%, 119 KB/s], Decompressed: 2661
Downloaded: 3615 file(s) [attempted 3615/8477 = 42%, 1144 KB/s], Decompressed: 2661
Downloaded: 3653 file(s) [attempted 3653/8477 = 43%, 389 KB/s], Decompressed: 2661
Downloaded: 3694 file(s) [attempted 3694/8477 = 43%, 53 KB/s], Decompressed: 2661
Downloaded: 3742 file(s) [attempted 3742/8477 = 44%, 330 KB/s], Decompressed: 3126
Downloaded: 3787 file(s) [attempted 3787/8477 = 44%, 393 KB/s], Decompressed: 3126
Downloaded: 3828 file(s) [attempted 3828/8477 = 45%, 164 KB/s], Decompressed: 3126
Downloaded: 3872 file(s) [attempted 3872/8477 = 45%, 450 KB/s], Decompressed: 3126
Downloaded: 3917 file(s) [attempted 3917/8477 = 46%, 53 KB/s], Decompressed: 3126
Downloaded: 3954 file(s) [attempted 3954/8477 = 46%, 856 KB/s], Decompressed: 3126
Downloaded: 3995 file(s) [attempted 3995/8477 = 47%, 53 KB/s], Decompressed: 3126
Downloaded: 4036 file(s) [attempted 4036/8477 = 47%, 88 KB/s], Decompressed: 3126
Downloaded: 4074 file(s) [attempted 4074/8477 = 48%, 65 KB/s], Decompressed: 3126
Downloaded: 4115 file(s) [attempted 4115/8477 = 48%, 448 KB/s], Decompressed: 3126
Downloaded: 4156 file(s) [attempted 4156/8477 = 49%, 49 KB/s], Decompressed: 3126
Downloaded: 4197 file(s) [attempted 4197/8477 = 49%, 342 KB/s], Decompressed: 3126
Downloaded: 4238 file(s) [attempted 4238/8477 = 49%, 556 KB/s], Decompressed: 3126
Downloaded: 4279 file(s) [attempted 4279/8477 = 50%, 406 KB/s], Decompressed: 3126
Downloaded: 4317 file(s) [attempted 4317/8477 = 50%, 344 KB/s], Decompressed: 3126
Downloaded: 4355 file(s) [attempted 4355/8477 = 51%, 174 KB/s], Decompressed: 3126
Downloaded: 4396 file(s) [attempted 4396/8477 = 51%, 868 KB/s], Decompressed: 3126
Downloaded: 4440 file(s) [attempted 4440/8477 = 52%, 321 KB/s], Decompressed: 3126
Downloaded: 4485 file(s) [attempted 4485/8477 = 52%, 302 KB/s], Decompressed: 3732
Downloaded: 4526 file(s) [attempted 4526/8477 = 53%, 119 KB/s], Decompressed: 3732
Downloaded: 4550 file(s) [attempted 4550/8477 = 53%, 42 KB/s], Decompressed: 3732
Downloaded: 4598 file(s) [attempted 4598/8477 = 54%, 529 KB/s], Decompressed: 3732
Downloaded: 4642 file(s) [attempted 4642/8477 = 54%, 73 KB/s], Decompressed: 3732
Downloaded: 4683 file(s) [attempted 4683/8477 = 55%, 420 KB/s], Decompressed: 3732
Downloaded: 4721 file(s) [attempted 4721/8477 = 55%, 358 KB/s], Decompressed: 3732
Downloaded: 4755 file(s) [attempted 4755/8477 = 56%, 251 KB/s], Decompressed: 3732
Downloaded: 4796 file(s) [attempted 4796/8477 = 56%, 684 KB/s], Decompressed: 3732
Downloaded: 4844 file(s) [attempted 4844/8477 = 57%, 97 KB/s], Decompressed: 3732
Downloaded: 4892 file(s) [attempted 4892/8477 = 57%, 268 KB/s], Decompressed: 3732
Downloaded: 4937 file(s) [attempted 4937/8477 = 58%, 77 KB/s], Decompressed: 3732
Downloaded: 4978 file(s) [attempted 4978/8477 = 58%, 88 KB/s], Decompressed: 3732
Downloaded: 5022 file(s) [attempted 5022/8477 = 59%, 313 KB/s], Decompressed: 3732
Downloaded: 5056 file(s) [attempted 5056/8477 = 59%, 97 KB/s], Decompressed: 3732
Downloaded: 5101 file(s) [attempted 5101/8477 = 60%, 208 KB/s], Decompressed: 3732
Downloaded: 5138 file(s) [attempted 5138/8477 = 60%, 46 KB/s], Decompressed: 3732
Downloaded: 5180 file(s) [attempted 5180/8477 = 61%, 483 KB/s], Decompressed: 3732
Downloaded: 5221 file(s) [attempted 5221/8477 = 61%, 292 KB/s], Decompressed: 3732
Downloaded: 5258 file(s) [attempted 5258/8477 = 62%, 792 KB/s], Decompressed: 3732
Downloaded: 5299 file(s) [attempted 5299/8477 = 62%, 436 KB/s], Decompressed: 4444
Downloaded: 5340 file(s) [attempted 5340/8477 = 62%, 243 KB/s], Decompressed: 4444
Downloaded: 5381 file(s) [attempted 5381/8477 = 63%, 1129 KB/s], Decompressed: 4444
Downloaded: 5423 file(s) [attempted 5423/8477 = 63%, 483 KB/s], Decompressed: 4444
Downloaded: 5464 file(s) [attempted 5464/8477 = 64%, 891 KB/s], Decompressed: 4444
Downloaded: 5501 file(s) [attempted 5501/8477 = 64%, 202 KB/s], Decompressed: 4444
Downloaded: 5539 file(s) [attempted 5539/8477 = 65%, 634 KB/s], Decompressed: 4444
Downloaded: 5580 file(s) [attempted 5580/8477 = 65%, 96 KB/s], Decompressed: 4444
Downloaded: 5618 file(s) [attempted 5618/8477 = 66%, 1148 KB/s], Decompressed: 4444
Downloaded: 5659 file(s) [attempted 5659/8477 = 66%, 231 KB/s], Decompressed: 4444
Downloaded: 5696 file(s) [attempted 5696/8477 = 67%, 866 KB/s], Decompressed: 4444
Downloaded: 5737 file(s) [attempted 5737/8477 = 67%, 163 KB/s], Decompressed: 4444
Downloaded: 5778 file(s) [attempted 5778/8477 = 68%, 1948 KB/s], Decompressed: 4444
Downloaded: 5820 file(s) [attempted 5820/8477 = 68%, 122 KB/s], Decompressed: 4444
Downloaded: 5861 file(s) [attempted 5861/8477 = 69%, 458 KB/s], Decompressed: 4444
Downloaded: 5905 file(s) [attempted 5905/8477 = 69%, 486 KB/s], Decompressed: 4444
Downloaded: 5943 file(s) [attempted 5943/8477 = 70%, 1269 KB/s], Decompressed: 4444
Downloaded: 5980 file(s) [attempted 5980/8477 = 70%, 91 KB/s], Decompressed: 4444
Downloaded: 6025 file(s) [attempted 6025/8477 = 71%, 92 KB/s], Decompressed: 4444
Downloaded: 6059 file(s) [attempted 6059/8477 = 71%, 673 KB/s], Decompressed: 4444
Downloaded: 6100 file(s) [attempted 6100/8477 = 71%, 117 KB/s], Decompressed: 4444
Downloaded: 6145 file(s) [attempted 6145/8477 = 72%, 150 KB/s], Decompressed: 4444
Downloaded: 6182 file(s) [attempted 6182/8477 = 72%, 305 KB/s], Decompressed: 4444
Downloaded: 6217 file(s) [attempted 6217/8477 = 73%, 245 KB/s], Decompressed: 4444
Downloaded: 6261 file(s) [attempted 6261/8477 = 73%, 72 KB/s], Decompressed: 4444
Downloaded: 6296 file(s) [attempted 6296/8477 = 74%, 205 KB/s], Decompressed: 4444
Downloaded: 6329 file(s) [attempted 6329/8477 = 74%, 88 KB/s], Decompressed: 5299
Downloaded: 6371 file(s) [attempted 6371/8477 = 75%, 82 KB/s], Decompressed: 5299
Downloaded: 6415 file(s) [attempted 6415/8477 = 75%, 385 KB/s], Decompressed: 5299
Downloaded: 6453 file(s) [attempted 6453/8477 = 76%, 205 KB/s], Decompressed: 5299
Downloaded: 6494 file(s) [attempted 6494/8477 = 76%, 242 KB/s], Decompressed: 5299
Downloaded: 6535 file(s) [attempted 6535/8477 = 77%, 504 KB/s], Decompressed: 5299
Downloaded: 6572 file(s) [attempted 6572/8477 = 77%, 294 KB/s], Decompressed: 5299
Downloaded: 6610 file(s) [attempted 6610/8477 = 77%, 472 KB/s], Decompressed: 5299
Downloaded: 6648 file(s) [attempted 6648/8477 = 78%, 839 KB/s], Decompressed: 5299
Downloaded: 6689 file(s) [attempted 6689/8477 = 78%, 396 KB/s], Decompressed: 5299
Downloaded: 6730 file(s) [attempted 6730/8477 = 79%, 172 KB/s], Decompressed: 5299
Downloaded: 6764 file(s) [attempted 6764/8477 = 79%, 153 KB/s], Decompressed: 5299
Downloaded: 6805 file(s) [attempted 6805/8477 = 80%, 310 KB/s], Decompressed: 5299
Downloaded: 6846 file(s) [attempted 6846/8477 = 80%, 334 KB/s], Decompressed: 5299
Downloaded: 6887 file(s) [attempted 6887/8477 = 81%, 992 KB/s], Decompressed: 5299
Downloaded: 6925 file(s) [attempted 6925/8477 = 81%, 425 KB/s], Decompressed: 5299
Downloaded: 6952 file(s) [attempted 6952/8477 = 82%, 412 KB/s], Decompressed: 5299
Downloaded: 6983 file(s) [attempted 6983/8477 = 82%, 565 KB/s], Decompressed: 5299
Downloaded: 7021 file(s) [attempted 7021/8477 = 82%, 288 KB/s], Decompressed: 5299
Downloaded: 7045 file(s) [attempted 7045/8477 = 83%, 127 KB/s], Decompressed: 5299
Downloaded: 7096 file(s) [attempted 7096/8477 = 83%, 663 KB/s], Decompressed: 5299
Downloaded: 7144 file(s) [attempted 7144/8477 = 84%, 1262 KB/s], Decompressed: 5299
Downloaded: 7192 file(s) [attempted 7192/8477 = 84%, 102 KB/s], Decompressed: 5299
Downloaded: 7233 file(s) [attempted 7233/8477 = 85%, 19 KB/s], Decompressed: 5299
Downloaded: 7277 file(s) [attempted 7277/8477 = 85%, 595 KB/s], Decompressed: 5299
Downloaded: 7322 file(s) [attempted 7322/8477 = 86%, 46 KB/s], Decompressed: 5299
Downloaded: 7366 file(s) [attempted 7366/8477 = 86%, 908 KB/s], Decompressed: 5299
Downloaded: 7407 file(s) [attempted 7407/8477 = 87%, 103 KB/s], Decompressed: 5299
Downloaded: 7445 file(s) [attempted 7445/8477 = 87%, 107 KB/s], Decompressed: 5299
Downloaded: 7486 file(s) [attempted 7486/8477 = 88%, 485 KB/s], Decompressed: 5299
Downloaded: 7527 file(s) [attempted 7527/8477 = 88%, 205 KB/s], Decompressed: 5299
Downloaded: 7565 file(s) [attempted 7565/8477 = 89%, 671 KB/s], Decompressed: 6319
Downloaded: 7609 file(s) [attempted 7609/8477 = 89%, 149 KB/s], Decompressed: 6319
Downloaded: 7654 file(s) [attempted 7654/8477 = 90%, 1202 KB/s], Decompressed: 6319
Downloaded: 7698 file(s) [attempted 7698/8477 = 90%, 229 KB/s], Decompressed: 6319
Downloaded: 7733 file(s) [attempted 7733/8477 = 91%, 80 KB/s], Decompressed: 6319
Downloaded: 7777 file(s) [attempted 7777/8477 = 91%, 930 KB/s], Decompressed: 6319
Downloaded: 7822 file(s) [attempted 7822/8477 = 92%, 181 KB/s], Decompressed: 6319
Downloaded: 7859 file(s) [attempted 7859/8477 = 92%, 1122 KB/s], Decompressed: 6319
Downloaded: 7897 file(s) [attempted 7897/8477 = 93%, 77 KB/s], Decompressed: 6319
Downloaded: 7945 file(s) [attempted 7945/8477 = 93%, 212 KB/s], Decompressed: 6319
Downloaded: 7989 file(s) [attempted 7989/8477 = 94%, 404 KB/s], Decompressed: 6319
Downloaded: 8030 file(s) [attempted 8030/8477 = 94%, 341 KB/s], Decompressed: 6319
Downloaded: 8068 file(s) [attempted 8068/8477 = 95%, 143 KB/s], Decompressed: 6319
Downloaded: 8106 file(s) [attempted 8106/8477 = 95%, 349 KB/s], Decompressed: 6319
Downloaded: 8147 file(s) [attempted 8147/8477 = 96%, 192 KB/s], Decompressed: 6319
Downloaded: 8188 file(s) [attempted 8188/8477 = 96%, 109 KB/s], Decompressed: 6319
Downloaded: 8232 file(s) [attempted 8232/8477 = 97%, 140 KB/s], Decompressed: 6319
Downloaded: 8277 file(s) [attempted 8277/8477 = 97%, 112 KB/s], Decompressed: 6319
Downloaded: 8318 file(s) [attempted 8318/8477 = 98%, 92 KB/s], Decompressed: 6319
Downloaded: 8355 file(s) [attempted 8355/8477 = 98%, 1151 KB/s], Decompressed: 6319
Downloaded: 8397 file(s) [attempted 8397/8477 = 99%, 202 KB/s], Decompressed: 6319
Downloaded: 8444 file(s) [attempted 8444/8477 = 99%, 263 KB/s], Decompressed: 6319
Downloaded: 8475 file(s) [attempted 8475/8477 = 99%, 116 KB/s], Decompressed: 6319
Downloaded: 8477 file(s) [attempted 8477/8477 = 100%, 116 KB/s], Decompressed: 6319

lean_checker exit 0 duration 6m 35s · created 6/2/2026, 12:15:21 PM

lake build

✔ [591/768] Built FLT.Assumptions.KnownIn1980s (472ms)
✔ [2949/2957] Built FLT.Assumptions.Mazur (4.5s)
✔ [3097/3138] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (4.6s)
✔ [3134/3238] Built FLT.Mathlib.Algebra.Algebra.Tower (4.6s)
✔ [3227/3311] Built FLT.Assumptions.Odlyzko (4.7s)
✔ [3294/3316] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (2.5s)
✔ [3295/3316] Built FLT.Mathlib.Algebra.FixedPoints.Basic (3.2s)
✔ [3296/3316] Built FLT.Mathlib.Topology.Algebra.Group.Units (1.6s)
✔ [3299/3316] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (5.4s)
✔ [3301/3316] Built FLT.Mathlib.Order.Filter.Cofinite (2.4s)
✔ [3302/3316] Built FLT.Mathlib.Topology.Bases (2.1s)
✔ [3303/3316] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (2.3s)
✔ [3304/3316] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (8.7s)
✔ [3305/3316] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (2.4s)
✔ [3307/3317] Built FLT.Mathlib.MeasureTheory.Group.Action (3.6s)
✔ [3308/3317] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (3.0s)
✔ [3310/3330] Built FLT.Mathlib.MeasureTheory.Group.Measure (2.8s)
✔ [3316/3337] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (6.9s)
✔ [3322/3337] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.8s)
✔ [3323/3337] Built FLT.Hacks.RightActionInstances (7.6s)
✔ [3324/3338] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (3.2s)
✔ [3325/3338] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (9.4s)
✔ [3327/3338] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (2.0s)
✔ [3330/3342] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (3.5s)
✔ [3332/3348] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (2.2s)
✔ [3338/3353] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (1.7s)
✔ [3343/3359] Built FLT.Mathlib.LinearAlgebra.Countable (2.3s)
✔ [3348/3359] Built FLT.AutomorphicForm.QuaternionAlgebra.Defs (6.9s)
✔ [3356/3375] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (5.3s)
✔ [3360/3375] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (9.7s)
✔ [3363/3375] Built FLT.Mathlib.RingTheory.Localization.BaseChange (4.7s)
✔ [3366/3377] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (3.8s)
✔ [3367/3379] Built FLT.DedekindDomain.AdicValuation (18s)
✔ [3369/3379] Built FLT.HaarMeasure.HaarChar.AddEquiv (12s)
✔ [3372/3393] Built FLT.DedekindDomain.IntegralClosure (11s)
✔ [3374/3393] Built FLT.NumberField.Completion.Finite (4.1s)
✔ [3376/3393] Built FLT.NumberField.HeightOneSpectrum (3.0s)
✔ [3377/3393] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (19s)
✔ [3378/3393] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (3.0s)
✔ [3379/3403] Built FLT.HaarMeasure.HaarChar.Ring (5.7s)
✔ [3381/3403] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (1.9s)
✔ [3383/3403] Built FLT.Mathlib.Algebra.Algebra.Hom (3.2s)
✔ [3384/3403] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (2.5s)
✔ [3385/3404] Built FLT.Mathlib.Topology.Algebra.MulAction (2.1s)
✔ [3388/3407] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (4.6s)
✔ [3389/3407] Built FLT.Mathlib.Algebra.IsDirectLimit (3.2s)
✔ [3390/3407] Built FLT.Mathlib.LinearAlgebra.Pi (3.0s)
✔ [3392/3407] Built FLT.Mathlib.Algebra.Algebra.Pi (2.2s)
✔ [3393/3407] Built FLT.Mathlib.Topology.Algebra.UniformRing (2.4s)
✔ [3397/3409] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (2.8s)
✔ [3398/3422] Built FLT.Mathlib.Algebra.Algebra.Bilinear (3.1s)
✔ [3401/3423] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (2.4s)
✔ [3403/3423] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (2.8s)
✔ [3404/3423] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (5.0s)
✔ [3405/3423] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (2.6s)
✔ [3406/3423] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (2.0s)
✔ [3407/3423] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (2.1s)
✔ [3408/3423] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (2.9s)
✔ [3409/3426] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (13s)
✔ [3411/3426] Built FLT.NumberField.InfinitePlace.Extension (4.0s)
✔ [3413/3426] Built FLT.Mathlib.Topology.Constructions (1.7s)
✔ [3414/3433] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (3.2s)
✔ [3417/3435] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (3.7s)
✔ [3418/3435] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (3.5s)
✔ [3420/3435] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (3.0s)
✔ [3421/3435] Built FLT.Mathlib.Data.Real.Archimedean (4.1s)
✔ [3422/3435] Built FLT.NumberField.Padics.RestrictedProduct (7.4s)
✔ [3424/3435] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (17s)
✔ [3426/3438] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (4.3s)
✔ [3427/3438] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (3.9s)
✔ [3429/3438] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (2.0s)
✔ [3436/3463] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (11s)
✔ [3438/3463] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (4.2s)
✔ [3441/3463] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (3.8s)
✔ [3442/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (3.9s)
✔ [3443/3466] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (9.3s)
✔ [3445/3466] Built FLT.HaarMeasure.HaarChar.RealComplex (5.7s)
✔ [3447/3466] Built FLT.HaarMeasure.MeasurableSpacePadics (4.7s)
✔ [3449/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.9s)
✔ [3451/3466] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (4.3s)
✔ [3452/3466] Built FLT.Mathlib.Algebra.Central.TensorProduct (4.2s)
✔ [3453/3466] Built FLT.Mathlib.GroupTheory.DoubleCoset (2.5s)
✔ [3455/3468] Built FLT.HaarMeasure.HaarChar.Padic (5.3s)
✔ [3456/3471] Built FLT.NumberField.Completion.Infinite (38s)
✔ [3459/3471] Built FLT.Mathlib.LinearAlgebra.Determinant (8.5s)
✔ [3461/3475] Built FLT.DedekindDomain.Completion.BaseChange (73s)
✔ [3463/3485] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (12s)
✔ [3470/3485] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (6.4s)
✔ [3471/3485] Built FLT.Mathlib.Topology.HomToDiscrete (3.7s)
✔ [3473/3496] Built FLT.Mathlib.Topology.Polish (2.3s)
✔ [3475/3497] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (3.7s)
✔ [3477/3497] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (2.3s)
✔ [3478/3497] Built FLT.Mathlib.Topology.Instances.Matrix (2.3s)
✔ [3479/3497] Built FLT.NumberField.InfiniteAdeleRing (24s)
✔ [3482/3497] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (2.7s)
✔ [3484/3500] Built FLT.Mathlib.MeasureTheory.Haar.Extension (3.8s)
✔ [3487/3519] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (6.2s)
✔ [3584/3628] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (2.6s)
✔ [3698/3713] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (3.1s)
✔ [3702/3713] Built FLT.Basic.FreyPackage (7.2s)
✔ [3719/3736] Built FLT.QuaternionAlgebra.NumberField (18s)
✔ [3722/3737] Built FLT.Deformations.Lemmas (8.8s)
✔ [3725/3739] Built FLT.Deformations.RepresentationTheory.IntegralClosure (4.9s)
✔ [3729/3747] Built FLT.Deformations.RepresentationTheory.Frobenius (6.4s)
✔ [3743/3754] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (15s)
✔ [3745/3763] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (65s)
✔ [3755/3773] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (17s)
✔ [3772/3803] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (2.6s)
✔ [3778/3803] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (25s)
✔ [3779/3803] Built FLT.Data.Hurwitz (9.5s)
✔ [3780/3803] Built FLT.Deformations.RepresentationTheory.Etale (18s)
✔ [3782/3805] Built FLT.Data.QHat (12s)
✔ [3784/3805] Built FLT.Patching.Utils.InverseLimit (1.7s)
✔ [3786/3806] Built FLT.Data.HurwitzRatHat (3.3s)
✔ [3788/3825] Built FLT.Deformations.Algebra.InverseLimit.Basic (9.8s)
✔ [3791/3825] Built FLT.Deformations.Algebra.InverseLimit.Topology (7.3s)
✔ [3795/3825] Built FLT.Patching.Utils.Lemmas (8.8s)
✔ [3797/3825] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.6s)
✔ [3798/3825] Built FLT.GaloisRepresentation.Cyclotomic (2.8s)
✔ [3799/3825] Built FLT.Mathlib.RepresentationTheory.Basic (3.2s)
✔ [3801/3825] Built FLT.Deformations.Subfunctor (1.7s)
✔ [3802/3825] Built FLT.Deformations.RepresentationTheory.GaloisRep (20s)
✔ [3803/3825] Built FLT.Patching.Utils.AdicTopology (5.2s)
✔ [3804/3830] Built FLT.Deformations.IsResidueAlgebra (3.7s)
✔ [3805/3830] Built FLT.Deformations.RepresentationTheory.Irreducible (1.0s)
✔ [3806/3830] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (115s)
✔ [3807/3830] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (2.0s)
✔ [3808/3831] Built FLT.GaloisRepresentation.Automorphic (4.1s)
✔ [3810/3853] Built FLT.EllipticCurve.Torsion (3.6s)
✔ [3932/3966] Built FLT.GaloisRepresentation.HardlyRamified.Defs (3.4s)
✔ [3933/3966] Built FLT.GroupScheme.FiniteFlat (520ms)
✔ [3934/3966] Built FLT.Deformations.IsProartinian (2.6s)
✔ [3935/3966] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (2.2s)
✔ [3936/3966] Built FLT.Mathlib.Data.Fin.Basic (1.6s)
✔ [3937/3966] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (2.6s)
✔ [3938/3966] Built FLT.Mathlib.Data.Set.Prod (828ms)
✔ [3939/3966] Built FLT.Mathlib.GroupTheory.Index (1.5s)
✔ [3940/3966] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.0s)
✔ [3941/3966] Built FLT.Mathlib.MeasureTheory.Measure.Regular (2.2s)
✔ [3944/3966] Built FLT.Mathlib.NumberTheory.NumberField.Completion (2.2s)
✔ [3945/3966] Built FLT.Mathlib.Topology.Algebra.Monoid (1.8s)
✔ [3946/3966] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (2.8s)
✔ [3947/3966] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (2.8s)
✔ [3948/3966] Built FLT.GaloisRepresentation.HardlyRamified.Lift (3.3s)
✔ [3949/3966] Built FLT.GaloisRepresentation.HardlyRamified.Family (3.6s)
✔ [3950/3969] Built FLT.GaloisRepresentation.HardlyRamified.Frey (3.6s)
✔ [3952/3971] Built FLT.Deformations.Categories (5.2s)
✔ [3958/3980] Built FLT.Mathlib.Topology.Algebra.Order.Field (3.9s)
✔ [3964/3983] Built FLT.Basic.Reductions (3.3s)
✔ [3966/3985] Built FLT.Patching.Utils.TopologicallyFG (2.7s)
✔ [3969/3985] Built FLT.Deformations.LiftFunctor (6.6s)
✔ [3970/3985] Built FLT.NumberField.DiscriminantBounds (6.1s)
✔ [3972/3985] Built FLT.Patching.Utils.StructureFiniteness (6.2s)
✔ [3974/3994] Built FLT.Deformations.Representable (4.5s)
✔ [3991/4009] Built FLT.TateCurve.TateCurve (381ms)
✔ [3992/4009] Built FLT.GlobalLanglandsConjectures.GLnDefs (14s)
✔ [3993/4009] Built FLT.Patching.Utils.CompactHausdorffRings (3.7s)
✔ [3994/4009] Built FLT.Patching.Utils.Depth (7.3s)
✔ [3995/4009] Built FLT.GlobalLanglandsConjectures.GLzero (5.5s)
✔ [3996/4009] Built FLT.Patching.Ultraproduct (15s)
✔ [3997/4009] Built FLT.NumberField.AdeleRing (45s)
✔ [3998/4009] Built FLT.Patching.VanishingFilter (4.6s)
✔ [3999/4009] Built FLT.Patching.Algebra (18s)
✔ [4000/4009] Built FLT.HaarMeasure.HaarChar.AdeleRing (18s)
✔ [4001/4009] Built FLT.Patching.Module (20s)
✔ [4002/4009] Built FLT.Patching.Over (15s)
✔ [4003/4009] Built FLT.Patching.System (12s)
✔ [4004/4009] Built FLT.Patching.REqualsT (4.0s)
✔ [4005/4009] Built FLT.DivisionAlgebra.Finiteness (48s)
✔ [4006/4009] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (2.2s)
✔ [4007/4009] Built FLT (1.0s)
✔ [4008/4009] Built FermatsLastTheorem (22s)
Build completed successfully (4009 jobs).

blueprint_build exit 1 duration 4s · created 6/2/2026, 12:15:21 PM

lake build :blueprint

error: unknown package facet `blueprint`

semantic_extract exit 1 duration 12m 24s · created 6/2/2026, 12:15:21 PM

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

lean semantic helper failed: generated static runner exited non-zero
remediation: inspect the generated repository runner and imported root modules