Verification run

Run 12

ImperialCollegeLondon/FLT branch main triggered via poller

failed commit 1af7f843a5ee 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 863 ms · created 6/5/2026, 11:04:11 PM

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

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

git_checkout exit 0 duration 18 ms · created 6/5/2026, 11:04:11 PM

git checkout 1af7f843a5eeb53b201fc1f49ed8435478942e90

Note: switching to '1af7f843a5eeb53b201fc1f49ed8435478942e90'.

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 1af7f84 chore: Bump `mathlib` dependency to e577c16 (#1002)

lake_cache exit 0 duration 1m 35s · created 6/5/2026, 11:04:11 PM

lake exe cache get

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

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'e577c1669e6b5017b3486292968ea067efba92eb'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '373598f95357e173818035c8c835cd927a9d767f'
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 (653ms)
✔ [5/24] Built Cache.Lean (724ms)
✔ [6/24] Built Batteries.Data.Array.Match (1.1s)
✔ [7/24] Built Cache.Init (415ms)
✔ [8/24] Built Batteries.Data.String.Basic:c.o (643ms)
✔ [9/24] Built Cache.Lean:c.o (228ms)
✔ [10/24] Built Batteries.Tactic.OpenPrivate (1.3s)
✔ [11/24] Built Batteries.Data.Array.Match:c.o (236ms)
✔ [12/24] Built Cache.Init:c.o (129ms)
✔ [13/24] Built Batteries.Data.String.Matcher (408ms)
✔ [14/24] Built Batteries.Data.String.Matcher:c.o (156ms)
✔ [15/24] Built Batteries.Tactic.OpenPrivate:c.o (977ms)
✔ [16/24] Built Cache.IO (1.6s)
✔ [17/24] Built Cache.Hashing (956ms)
✔ [18/24] Built Cache.IO:c.o (1.2s)
✔ [19/24] Built Cache.Hashing:c.o (357ms)
✔ [20/24] Built Cache.Requests (1.0s)
✔ [21/24] Built Cache.Main (1.0s)
✔ [22/24] Built Cache.Main:c.o (518ms)
✔ [23/24] Built Cache.Requests:c.o (1.8s)
✔ [24/24] Built cache:exe (2.5s)

Downloaded: 1 file(s) [attempted 1/8495 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8495 = 0%, 11 KB/s], Decompressed: 8
Downloaded: 40 file(s) [attempted 40/8495 = 0%, 26 KB/s], Decompressed: 30
Downloaded: 65 file(s) [attempted 65/8495 = 0%, 164 KB/s], Decompressed: 61
Downloaded: 93 file(s) [attempted 93/8495 = 1%, 352 KB/s], Decompressed: 86
Downloaded: 134 file(s) [attempted 134/8495 = 1%, 359 KB/s], Decompressed: 110
Downloaded: 169 file(s) [attempted 169/8495 = 1%, 59 KB/s], Decompressed: 134
Downloaded: 206 file(s) [attempted 206/8495 = 2%, 116 KB/s], Decompressed: 162
Downloaded: 247 file(s) [attempted 247/8495 = 2%, 310 KB/s], Decompressed: 199
Downloaded: 285 file(s) [attempted 285/8495 = 3%, 575 KB/s], Decompressed: 199
Downloaded: 323 file(s) [attempted 323/8495 = 3%, 153 KB/s], Decompressed: 247
Downloaded: 367 file(s) [attempted 367/8495 = 4%, 1239 KB/s], Decompressed: 247
Downloaded: 411 file(s) [attempted 411/8495 = 4%, 496 KB/s], Decompressed: 309
Downloaded: 449 file(s) [attempted 449/8495 = 5%, 318 KB/s], Decompressed: 309
Downloaded: 480 file(s) [attempted 480/8495 = 5%, 96 KB/s], Decompressed: 377
Downloaded: 521 file(s) [attempted 521/8495 = 6%, 956 KB/s], Decompressed: 377
Downloaded: 566 file(s) [attempted 566/8495 = 6%, 575 KB/s], Decompressed: 377
Downloaded: 610 file(s) [attempted 610/8495 = 7%, 360 KB/s], Decompressed: 466
Downloaded: 651 file(s) [attempted 651/8495 = 7%, 226 KB/s], Decompressed: 466
Downloaded: 675 file(s) [attempted 675/8495 = 7%, 422 KB/s], Decompressed: 466
Downloaded: 723 file(s) [attempted 723/8495 = 8%, 118 KB/s], Decompressed: 466
Downloaded: 768 file(s) [attempted 768/8495 = 9%, 313 KB/s], Decompressed: 466
Downloaded: 809 file(s) [attempted 809/8495 = 9%, 501 KB/s], Decompressed: 590
Downloaded: 850 file(s) [attempted 850/8495 = 10%, 142 KB/s], Decompressed: 590
Downloaded: 884 file(s) [attempted 884/8495 = 10%, 150 KB/s], Decompressed: 590
Downloaded: 929 file(s) [attempted 929/8495 = 10%, 188 KB/s], Decompressed: 590
Downloaded: 970 file(s) [attempted 970/8495 = 11%, 63 KB/s], Decompressed: 590
Downloaded: 1008 file(s) [attempted 1008/8495 = 11%, 179 KB/s], Decompressed: 590
Downloaded: 1049 file(s) [attempted 1049/8495 = 12%, 23 KB/s], Decompressed: 590
Downloaded: 1090 file(s) [attempted 1090/8495 = 12%, 211 KB/s], Decompressed: 788
Downloaded: 1124 file(s) [attempted 1124/8495 = 13%, 499 KB/s], Decompressed: 788
Downloaded: 1168 file(s) [attempted 1168/8495 = 13%, 40 KB/s], Decompressed: 788
Downloaded: 1203 file(s) [attempted 1203/8495 = 14%, 184 KB/s], Decompressed: 788
Downloaded: 1244 file(s) [attempted 1244/8495 = 14%, 622 KB/s], Decompressed: 788
Downloaded: 1285 file(s) [attempted 1285/8495 = 15%, 94 KB/s], Decompressed: 788
Downloaded: 1323 file(s) [attempted 1323/8495 = 15%, 385 KB/s], Decompressed: 788
Downloaded: 1366 file(s) [attempted 1366/8495 = 16%, 65 KB/s], Decompressed: 788
Downloaded: 1401 file(s) [attempted 1401/8495 = 16%, 84 KB/s], Decompressed: 788
Downloaded: 1441 file(s) [attempted 1441/8495 = 16%, 168 KB/s], Decompressed: 788
Downloaded: 1478 file(s) [attempted 1478/8495 = 17%, 265 KB/s], Decompressed: 788
Downloaded: 1521 file(s) [attempted 1521/8495 = 17%, 247 KB/s], Decompressed: 788
Downloaded: 1562 file(s) [attempted 1562/8495 = 18%, 259 KB/s], Decompressed: 1076
Downloaded: 1603 file(s) [attempted 1603/8495 = 18%, 341 KB/s], Decompressed: 1076
Downloaded: 1641 file(s) [attempted 1641/8495 = 19%, 634 KB/s], Decompressed: 1076
Downloaded: 1678 file(s) [attempted 1678/8495 = 19%, 118 KB/s], Decompressed: 1076
Downloaded: 1723 file(s) [attempted 1723/8495 = 20%, 572 KB/s], Decompressed: 1076
Downloaded: 1767 file(s) [attempted 1767/8495 = 20%, 266 KB/s], Decompressed: 1076
Downloaded: 1802 file(s) [attempted 1802/8495 = 21%, 46 KB/s], Decompressed: 1076
Downloaded: 1843 file(s) [attempted 1843/8495 = 21%, 233 KB/s], Decompressed: 1076
Downloaded: 1877 file(s) [attempted 1877/8495 = 22%, 709 KB/s], Decompressed: 1076
Downloaded: 1921 file(s) [attempted 1921/8495 = 22%, 268 KB/s], Decompressed: 1076
Downloaded: 1963 file(s) [attempted 1963/8495 = 23%, 103 KB/s], Decompressed: 1076
Downloaded: 2004 file(s) [attempted 2004/8495 = 23%, 505 KB/s], Decompressed: 1076
Downloaded: 2048 file(s) [attempted 2048/8495 = 24%, 55 KB/s], Decompressed: 1076
Downloaded: 2086 file(s) [attempted 2086/8495 = 24%, 235 KB/s], Decompressed: 1076
Downloaded: 2120 file(s) [attempted 2120/8495 = 24%, 126 KB/s], Decompressed: 1076
Downloaded: 2161 file(s) [attempted 2161/8495 = 25%, 584 KB/s], Decompressed: 1076
Downloaded: 2199 file(s) [attempted 2199/8495 = 25%, 222 KB/s], Decompressed: 1076
Downloaded: 2240 file(s) [attempted 2240/8495 = 26%, 469 KB/s], Decompressed: 1076
Downloaded: 2288 file(s) [attempted 2288/8495 = 26%, 302 KB/s], Decompressed: 1076
Downloaded: 2332 file(s) [attempted 2332/8495 = 27%, 1019 KB/s], Decompressed: 1524
Downloaded: 2383 file(s) [attempted 2383/8495 = 28%, 1051 KB/s], Decompressed: 1524
Downloaded: 2428 file(s) [attempted 2428/8495 = 28%, 36 KB/s], Decompressed: 1524
Downloaded: 2462 file(s) [attempted 2462/8495 = 28%, 268 KB/s], Decompressed: 1524
Downloaded: 2503 file(s) [attempted 2503/8495 = 29%, 79 KB/s], Decompressed: 1524
Downloaded: 2551 file(s) [attempted 2551/8495 = 30%, 517 KB/s], Decompressed: 1524
Downloaded: 2599 file(s) [attempted 2599/8495 = 30%, 606 KB/s], Decompressed: 1524
Downloaded: 2644 file(s) [attempted 2644/8495 = 31%, 38 KB/s], Decompressed: 1524
Downloaded: 2691 file(s) [attempted 2691/8495 = 31%, 26 KB/s], Decompressed: 1524
Downloaded: 2733 file(s) [attempted 2733/8495 = 32%, 170 KB/s], Decompressed: 1524
Downloaded: 2767 file(s) [attempted 2767/8495 = 32%, 59 KB/s], Decompressed: 1524
Downloaded: 2808 file(s) [attempted 2808/8495 = 33%, 1138 KB/s], Decompressed: 1524
Downloaded: 2849 file(s) [attempted 2849/8495 = 33%, 214 KB/s], Decompressed: 1524
Downloaded: 2893 file(s) [attempted 2893/8495 = 34%, 602 KB/s], Decompressed: 1524
Downloaded: 2938 file(s) [attempted 2938/8495 = 34%, 398 KB/s], Decompressed: 1524
Downloaded: 2969 file(s) [attempted 2969/8495 = 34%, 253 KB/s], Decompressed: 1524
Downloaded: 3013 file(s) [attempted 3013/8495 = 35%, 906 KB/s], Decompressed: 1524
Downloaded: 3054 file(s) [attempted 3054/8495 = 35%, 1270 KB/s], Decompressed: 1524
Downloaded: 3095 file(s) [attempted 3095/8495 = 36%, 1673 KB/s], Decompressed: 1524
Downloaded: 3136 file(s) [attempted 3136/8495 = 36%, 184 KB/s], Decompressed: 1524
Downloaded: 3177 file(s) [attempted 3177/8495 = 37%, 67 KB/s], Decompressed: 1524
Downloaded: 3218 file(s) [attempted 3218/8495 = 37%, 545 KB/s], Decompressed: 1524
Downloaded: 3266 file(s) [attempted 3266/8495 = 38%, 619 KB/s], Decompressed: 1524
Downloaded: 3311 file(s) [attempted 3311/8495 = 38%, 192 KB/s], Decompressed: 1524
Downloaded: 3338 file(s) [attempted 3338/8495 = 39%, 401 KB/s], Decompressed: 1524
Downloaded: 3379 file(s) [attempted 3379/8495 = 39%, 173 KB/s], Decompressed: 1524
Downloaded: 3420 file(s) [attempted 3420/8495 = 40%, 204 KB/s], Decompressed: 1524
Downloaded: 3458 file(s) [attempted 3458/8495 = 40%, 191 KB/s], Decompressed: 1524
Downloaded: 3499 file(s) [attempted 3499/8495 = 41%, 75 KB/s], Decompressed: 2318
Downloaded: 3533 file(s) [attempted 3533/8495 = 41%, 405 KB/s], Decompressed: 2318
Downloaded: 3574 file(s) [attempted 3574/8495 = 42%, 708 KB/s], Decompressed: 2318
Downloaded: 3622 file(s) [attempted 3622/8495 = 42%, 39 KB/s], Decompressed: 2318
Downloaded: 3657 file(s) [attempted 3657/8495 = 43%, 408 KB/s], Decompressed: 2318
Downloaded: 3701 file(s) [attempted 3701/8495 = 43%, 713 KB/s], Decompressed: 2318
Downloaded: 3739 file(s) [attempted 3739/8495 = 44%, 143 KB/s], Decompressed: 2318
Downloaded: 3783 file(s) [attempted 3783/8495 = 44%, 65 KB/s], Decompressed: 2318
Downloaded: 3824 file(s) [attempted 3824/8495 = 45%, 450 KB/s], Decompressed: 2318
Downloaded: 3865 file(s) [attempted 3865/8495 = 45%, 132 KB/s], Decompressed: 2318
Downloaded: 3906 file(s) [attempted 3906/8495 = 45%, 438 KB/s], Decompressed: 2318
Downloaded: 3947 file(s) [attempted 3947/8495 = 46%, 96 KB/s], Decompressed: 2318
Downloaded: 3982 file(s) [attempted 3982/8495 = 46%, 229 KB/s], Decompressed: 2318
Downloaded: 4026 file(s) [attempted 4026/8495 = 47%, 311 KB/s], Decompressed: 2318
Downloaded: 4071 file(s) [attempted 4071/8495 = 47%, 678 KB/s], Decompressed: 2318
Downloaded: 4108 file(s) [attempted 4108/8495 = 48%, 1528 KB/s], Decompressed: 2318
Downloaded: 4149 file(s) [attempted 4149/8495 = 48%, 299 KB/s], Decompressed: 2318
Downloaded: 4194 file(s) [attempted 4194/8495 = 49%, 51 KB/s], Decompressed: 2318
Downloaded: 4232 file(s) [attempted 4232/8495 = 49%, 323 KB/s], Decompressed: 2318
Downloaded: 4278 file(s) [attempted 4278/8495 = 50%, 429 KB/s], Decompressed: 2318
Downloaded: 4317 file(s) [attempted 4317/8495 = 50%, 911 KB/s], Decompressed: 2318
Downloaded: 4344 file(s) [attempted 4344/8495 = 51%, 493 KB/s], Decompressed: 2318
Downloaded: 4396 file(s) [attempted 4396/8495 = 51%, 721 KB/s], Decompressed: 2318
Downloaded: 4440 file(s) [attempted 4440/8495 = 52%, 281 KB/s], Decompressed: 2318
Downloaded: 4481 file(s) [attempted 4481/8495 = 52%, 204 KB/s], Decompressed: 2318
Downloaded: 4526 file(s) [attempted 4526/8495 = 53%, 428 KB/s], Decompressed: 2318
Downloaded: 4563 file(s) [attempted 4563/8495 = 53%, 116 KB/s], Decompressed: 2318
Downloaded: 4608 file(s) [attempted 4608/8495 = 54%, 615 KB/s], Decompressed: 2318
Downloaded: 4652 file(s) [attempted 4652/8495 = 54%, 389 KB/s], Decompressed: 2318
Downloaded: 4694 file(s) [attempted 4694/8495 = 55%, 64 KB/s], Decompressed: 2318
Downloaded: 4728 file(s) [attempted 4728/8495 = 55%, 1403 KB/s], Decompressed: 2318
Downloaded: 4772 file(s) [attempted 4772/8495 = 56%, 140 KB/s], Decompressed: 2318
Downloaded: 4817 file(s) [attempted 4817/8495 = 56%, 180 KB/s], Decompressed: 2318
Downloaded: 4861 file(s) [attempted 4861/8495 = 57%, 318 KB/s], Decompressed: 2318
Downloaded: 4892 file(s) [attempted 4892/8495 = 57%, 35 KB/s], Decompressed: 2318
Downloaded: 4933 file(s) [attempted 4933/8495 = 58%, 232 KB/s], Decompressed: 2318
Downloaded: 4978 file(s) [attempted 4978/8495 = 58%, 128 KB/s], Decompressed: 2318
Downloaded: 5022 file(s) [attempted 5022/8495 = 59%, 730 KB/s], Decompressed: 2318
Downloaded: 5046 file(s) [attempted 5046/8495 = 59%, 132 KB/s], Decompressed: 2318
Downloaded: 5091 file(s) [attempted 5091/8495 = 59%, 60 KB/s], Decompressed: 2318
Downloaded: 5135 file(s) [attempted 5135/8495 = 60%, 560 KB/s], Decompressed: 2318
Downloaded: 5176 file(s) [attempted 5176/8495 = 60%, 164 KB/s], Decompressed: 2318
Downloaded: 5224 file(s) [attempted 5224/8495 = 61%, 840 KB/s], Decompressed: 2318
Downloaded: 5269 file(s) [attempted 5269/8495 = 62%, 253 KB/s], Decompressed: 2318
Downloaded: 5303 file(s) [attempted 5303/8495 = 62%, 638 KB/s], Decompressed: 2318
Downloaded: 5344 file(s) [attempted 5344/8495 = 62%, 70 KB/s], Decompressed: 2318
Downloaded: 5385 file(s) [attempted 5385/8495 = 63%, 868 KB/s], Decompressed: 2318
Downloaded: 5426 file(s) [attempted 5426/8495 = 63%, 225 KB/s], Decompressed: 2318
Downloaded: 5460 file(s) [attempted 5460/8495 = 64%, 649 KB/s], Decompressed: 2318
Downloaded: 5498 file(s) [attempted 5498/8495 = 64%, 138 KB/s], Decompressed: 2318
Downloaded: 5542 file(s) [attempted 5542/8495 = 65%, 426 KB/s], Decompressed: 2318
Downloaded: 5583 file(s) [attempted 5583/8495 = 65%, 126 KB/s], Decompressed: 2318
Downloaded: 5624 file(s) [attempted 5624/8495 = 66%, 776 KB/s], Decompressed: 2318
Downloaded: 5662 file(s) [attempted 5662/8495 = 66%, 173 KB/s], Decompressed: 2318
Downloaded: 5703 file(s) [attempted 5703/8495 = 67%, 118 KB/s], Decompressed: 3465
Downloaded: 5744 file(s) [attempted 5744/8495 = 67%, 1322 KB/s], Decompressed: 3465
Downloaded: 5792 file(s) [attempted 5792/8495 = 68%, 49 KB/s], Decompressed: 3465
Downloaded: 5826 file(s) [attempted 5826/8495 = 68%, 198 KB/s], Decompressed: 3465
Downloaded: 5871 file(s) [attempted 5871/8495 = 69%, 1008 KB/s], Decompressed: 3465
Downloaded: 5912 file(s) [attempted 5912/8495 = 69%, 48 KB/s], Decompressed: 3465
Downloaded: 5956 file(s) [attempted 5956/8495 = 70%, 1269 KB/s], Decompressed: 3465
Downloaded: 5980 file(s) [attempted 5980/8495 = 70%, 267 KB/s], Decompressed: 3465
Downloaded: 6025 file(s) [attempted 6025/8495 = 70%, 266 KB/s], Decompressed: 3465
Downloaded: 6069 file(s) [attempted 6069/8495 = 71%, 132 KB/s], Decompressed: 3465
Downloaded: 6114 file(s) [attempted 6114/8495 = 71%, 369 KB/s], Decompressed: 3465
Downloaded: 6158 file(s) [attempted 6158/8495 = 72%, 59 KB/s], Decompressed: 3465
Downloaded: 6203 file(s) [attempted 6203/8495 = 73%, 530 KB/s], Decompressed: 3465
Downloaded: 6240 file(s) [attempted 6240/8495 = 73%, 739 KB/s], Decompressed: 3465
Downloaded: 6281 file(s) [attempted 6281/8495 = 73%, 34 KB/s], Decompressed: 3465
Downloaded: 6329 file(s) [attempted 6329/8495 = 74%, 87 KB/s], Decompressed: 3465
Downloaded: 6370 file(s) [attempted 6370/8495 = 74%, 57 KB/s], Decompressed: 3465
Downloaded: 6412 file(s) [attempted 6412/8495 = 75%, 34 KB/s], Decompressed: 3465
Downloaded: 6446 file(s) [attempted 6446/8495 = 75%, 531 KB/s], Decompressed: 3465
Downloaded: 6487 file(s) [attempted 6487/8495 = 76%, 983 KB/s], Decompressed: 3465
Downloaded: 6528 file(s) [attempted 6528/8495 = 76%, 583 KB/s], Decompressed: 3465
Downloaded: 6576 file(s) [attempted 6576/8495 = 77%, 530 KB/s], Decompressed: 3465
Downloaded: 6613 file(s) [attempted 6613/8495 = 77%, 359 KB/s], Decompressed: 3465
Downloaded: 6648 file(s) [attempted 6648/8495 = 78%, 2689 KB/s], Decompressed: 3465
Downloaded: 6689 file(s) [attempted 6689/8495 = 78%, 158 KB/s], Decompressed: 3465
Downloaded: 6733 file(s) [attempted 6733/8495 = 79%, 254 KB/s], Decompressed: 3465
Downloaded: 6774 file(s) [attempted 6774/8495 = 79%, 700 KB/s], Decompressed: 3465
Downloaded: 6815 file(s) [attempted 6815/8495 = 80%, 75 KB/s], Decompressed: 3465
Downloaded: 6856 file(s) [attempted 6856/8495 = 80%, 977 KB/s], Decompressed: 3465
Downloaded: 6894 file(s) [attempted 6894/8495 = 81%, 160 KB/s], Decompressed: 3465
Downloaded: 6939 file(s) [attempted 6939/8495 = 81%, 581 KB/s], Decompressed: 3465
Downloaded: 6983 file(s) [attempted 6983/8495 = 82%, 93 KB/s], Decompressed: 3465
Downloaded: 7021 file(s) [attempted 7021/8495 = 82%, 102 KB/s], Decompressed: 3465
Downloaded: 7058 file(s) [attempted 7058/8495 = 83%, 465 KB/s], Decompressed: 3465
Downloaded: 7099 file(s) [attempted 7099/8495 = 83%, 150 KB/s], Decompressed: 3465
Downloaded: 7147 file(s) [attempted 7147/8495 = 84%, 182 KB/s], Decompressed: 3465
Downloaded: 7195 file(s) [attempted 7195/8495 = 84%, 87 KB/s], Decompressed: 3465
Downloaded: 7236 file(s) [attempted 7236/8495 = 85%, 2221 KB/s], Decompressed: 3465
Downloaded: 7281 file(s) [attempted 7281/8495 = 85%, 176 KB/s], Decompressed: 3465
Downloaded: 7318 file(s) [attempted 7318/8495 = 86%, 363 KB/s], Decompressed: 3465
Downloaded: 7370 file(s) [attempted 7370/8495 = 86%, 392 KB/s], Decompressed: 3465
Downloaded: 7418 file(s) [attempted 7418/8495 = 87%, 274 KB/s], Decompressed: 3465
Downloaded: 7466 file(s) [attempted 7466/8495 = 87%, 943 KB/s], Decompressed: 3465
Downloaded: 7507 file(s) [attempted 7507/8495 = 88%, 331 KB/s], Decompressed: 3465
Downloaded: 7551 file(s) [attempted 7551/8495 = 88%, 421 KB/s], Decompressed: 3465
Downloaded: 7582 file(s) [attempted 7582/8495 = 89%, 90 KB/s], Decompressed: 3465
Downloaded: 7623 file(s) [attempted 7623/8495 = 89%, 155 KB/s], Decompressed: 3465
Downloaded: 7668 file(s) [attempted 7668/8495 = 90%, 182 KB/s], Decompressed: 3465
Downloaded: 7709 file(s) [attempted 7709/8495 = 90%, 373 KB/s], Decompressed: 3465
Downloaded: 7753 file(s) [attempted 7753/8495 = 91%, 667 KB/s], Decompressed: 3465
Downloaded: 7794 file(s) [attempted 7794/8495 = 91%, 120 KB/s], Decompressed: 3465
Downloaded: 7835 file(s) [attempted 7835/8495 = 92%, 611 KB/s], Decompressed: 3465
Downloaded: 7873 file(s) [attempted 7873/8495 = 92%, 493 KB/s], Decompressed: 3465
Downloaded: 7914 file(s) [attempted 7914/8495 = 93%, 461 KB/s], Decompressed: 3465
Downloaded: 7958 file(s) [attempted 7958/8495 = 93%, 36 KB/s], Decompressed: 3465
Downloaded: 7999 file(s) [attempted 7999/8495 = 94%, 183 KB/s], Decompressed: 3465
Downloaded: 8034 file(s) [attempted 8034/8495 = 94%, 218 KB/s], Decompressed: 3465
Downloaded: 8075 file(s) [attempted 8075/8495 = 95%, 91 KB/s], Decompressed: 3465
Downloaded: 8116 file(s) [attempted 8116/8495 = 95%, 35 KB/s], Decompressed: 3465
Downloaded: 8160 file(s) [attempted 8160/8495 = 96%, 39 KB/s], Decompressed: 3465
Downloaded: 8201 file(s) [attempted 8201/8495 = 96%, 337 KB/s], Decompressed: 3465
Downloaded: 8239 file(s) [attempted 8239/8495 = 96%, 1596 KB/s], Decompressed: 3465
Downloaded: 8284 file(s) [attempted 8284/8495 = 97%, 322 KB/s], Decompressed: 3465
Downloaded: 8321 file(s) [attempted 8321/8495 = 97%, 141 KB/s], Decompressed: 3465
Downloaded: 8367 file(s) [attempted 8367/8495 = 98%, 60 KB/s], Decompressed: 3465
Downloaded: 8403 file(s) [attempted 8403/8495 = 98%, 754 KB/s], Decompressed: 3465
Downloaded: 8438 file(s) [attempted 8438/8495 = 99%, 240 KB/s], Decompressed: 3465
Downloaded: 8482 file(s) [attempted 8482/8495 = 99%, 21 KB/s], Decompressed: 3465
Downloaded: 8492 file(s) [attempted 8492/8495 = 99%, 278 KB/s], Decompressed: 3465
Downloaded: 8495 file(s) [attempted 8495/8495 = 100%, 278 KB/s], Decompressed: 3465

lean_checker exit 0 duration 6m 6s · created 6/5/2026, 11:04:11 PM

lake build

✔ [2952/2978] Built FLT.Assumptions.Mazur (5.2s)
✔ [3047/3107] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (4.9s)
✔ [3048/3107] Built FLT.Mathlib.Algebra.Algebra.Tower (4.0s)
✔ [3205/3256] Built FLT.Assumptions.Odlyzko (5.2s)
✔ [3298/3318] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (2.5s)
✔ [3299/3318] Built FLT.Mathlib.Algebra.FixedPoints.Basic (3.5s)
✔ [3300/3318] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (5.3s)
✔ [3301/3318] Built FLT.Mathlib.Topology.Algebra.Group.Units (2.2s)
✔ [3303/3318] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (3.0s)
✔ [3305/3318] Built FLT.Mathlib.Order.Filter.Cofinite (1.0s)
✔ [3306/3318] Built FLT.Mathlib.Topology.Bases (2.1s)
✔ [3307/3318] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (9.5s)
✔ [3308/3318] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (2.7s)
✔ [3310/3319] Built FLT.Mathlib.MeasureTheory.Group.Action (4.5s)
✔ [3311/3319] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (3.7s)
✔ [3312/3332] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (7.6s)
✔ [3318/3332] Built FLT.Mathlib.MeasureTheory.Group.Measure (2.8s)
✔ [3323/3339] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (2.2s)
✔ [3324/3339] Built FLT.Hacks.RightActionInstances (8.5s)
✔ [3325/3340] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (2.4s)
✔ [3328/3344] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (10s)
✔ [3330/3344] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (3.8s)
✔ [3332/3344] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (2.6s)
✔ [3334/3350] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (4.2s)
✔ [3341/3355] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (2.1s)
✔ [3344/3357] Built FLT.Mathlib.LinearAlgebra.Countable (2.9s)
✔ [3350/3367] Built FLT.AutomorphicForm.QuaternionAlgebra.Defs (9.4s)
✔ [3359/3377] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (10s)
✔ [3362/3377] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (5.9s)
✔ [3365/3377] Built FLT.Mathlib.RingTheory.Localization.BaseChange (4.8s)
✔ [3366/3377] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (5.2s)
✔ [3367/3377] Built FLT.HaarMeasure.HaarChar.AddEquiv (14s)
✔ [3370/3379] Built FLT.DedekindDomain.AdicValuation (21s)
✔ [3371/3395] Built FLT.NumberField.Completion.Finite (5.2s)
✔ [3378/3395] Built FLT.DedekindDomain.IntegralClosure (12s)
✔ [3379/3395] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (21s)
✔ [3380/3395] Built FLT.HaarMeasure.HaarChar.Ring (6.8s)
✔ [3382/3405] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (2.1s)
✔ [3383/3405] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (3.3s)
✔ [3385/3405] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (3.2s)
✔ [3386/3405] Built FLT.Mathlib.Algebra.Algebra.Hom (4.1s)
✔ [3387/3409] Built FLT.NumberField.HeightOneSpectrum (3.1s)
✔ [3390/3409] Built FLT.Mathlib.Topology.Algebra.MulAction (2.6s)
✔ [3391/3409] Built FLT.Mathlib.Algebra.IsDirectLimit (4.1s)
✔ [3392/3409] Built FLT.Mathlib.LinearAlgebra.Pi (2.9s)
✔ [3393/3409] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (3.2s)
✔ [3395/3409] Built FLT.Mathlib.Topology.Algebra.UniformRing (2.6s)
✔ [3397/3409] Built FLT.Mathlib.Algebra.Algebra.Pi (2.9s)
✔ [3399/3409] Built FLT.Mathlib.Algebra.Algebra.Bilinear (4.1s)
✔ [3400/3424] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (5.3s)
✔ [3402/3425] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (3.3s)
✔ [3405/3425] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (6.1s)
✔ [3406/3425] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (3.1s)
✔ [3407/3425] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (3.4s)
✔ [3408/3425] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (2.5s)
✔ [3409/3425] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (2.5s)
✔ [3410/3425] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (14s)
✔ [3411/3425] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (3.3s)
✔ [3413/3428] Built FLT.NumberField.InfinitePlace.Extension (5.3s)
✔ [3415/3428] Built FLT.Mathlib.Topology.Constructions (2.1s)
✔ [3416/3435] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (4.5s)
✔ [3419/3437] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (5.0s)
✔ [3420/3437] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (4.1s)
✔ [3422/3437] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (4.6s)
✔ [3423/3437] Built FLT.Mathlib.Data.Real.Archimedean (3.4s)
✔ [3424/3437] Built FLT.NumberField.Padics.RestrictedProduct (7.5s)
✔ [3426/3437] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (18s)
✔ [3428/3440] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (4.5s)
✔ [3429/3440] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (4.3s)
✔ [3431/3442] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (4.5s)
✔ [3438/3462] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (4.3s)
✔ [3440/3465] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (13s)
✔ [3442/3465] Built FLT.HaarMeasure.MeasurableSpacePadics (4.9s)
✔ [3444/3465] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (8.2s)
✔ [3445/3468] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (2.4s)
✔ [3447/3468] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (3.3s)
✔ [3449/3468] Built FLT.HaarMeasure.HaarChar.RealComplex (4.6s)
✔ [3450/3468] Built FLT.HaarMeasure.HaarChar.Padic (5.1s)
✔ [3452/3468] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (5.4s)
✔ [3454/3468] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (2.1s)
✔ [3455/3468] Built FLT.Mathlib.GroupTheory.DoubleCoset (3.0s)
✔ [3457/3469] Built FLT.Mathlib.Algebra.Central.TensorProduct (4.4s)
✔ [3458/3473] Built FLT.NumberField.Completion.Infinite (40s)
✔ [3460/3473] Built FLT.Mathlib.LinearAlgebra.Determinant (9.4s)
✔ [3463/3487] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (15s)
✔ [3471/3487] Built FLT.DedekindDomain.Completion.BaseChange (80s)
✔ [3472/3487] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (6.4s)
✔ [3474/3487] Built FLT.Mathlib.Topology.HomToDiscrete (2.9s)
✔ [3475/3498] Built FLT.Mathlib.Topology.Polish (2.3s)
✔ [3477/3499] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (3.4s)
✔ [3479/3499] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (2.5s)
✔ [3480/3499] Built FLT.Mathlib.Topology.Instances.Matrix (2.7s)
✔ [3481/3499] Built FLT.NumberField.InfiniteAdeleRing (22s)
✔ [3484/3501] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (3.3s)
✔ [3486/3502] Built FLT.Mathlib.MeasureTheory.Haar.Extension (4.5s)
✔ [3489/3511] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (7.1s)
✔ [3697/3712] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (3.1s)
✔ [3701/3715] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (3.5s)
✔ [3703/3715] Built FLT.Basic.FreyPackage (8.4s)
✔ [3721/3738] Built FLT.QuaternionAlgebra.NumberField (17s)
✔ [3724/3739] Built FLT.Deformations.Lemmas (8.2s)
✔ [3727/3741] Built FLT.Deformations.RepresentationTheory.IntegralClosure (4.1s)
✔ [3731/3754] Built FLT.Deformations.RepresentationTheory.Frobenius (7.7s)
✔ [3747/3760] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (13s)
✔ [3749/3764] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (59s)
✔ [3757/3784] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (13s)
✔ [3774/3805] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (2.2s)
✔ [3780/3805] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (18s)
✔ [3781/3805] Built FLT.Deformations.RepresentationTheory.Etale (13s)
✔ [3782/3805] Built FLT.Data.Hurwitz (7.2s)
✔ [3784/3805] Built FLT.Patching.Utils.InverseLimit (2.1s)
✔ [3787/3808] Built FLT.Data.QHat (9.7s)
✔ [3788/3808] Built FLT.Deformations.Algebra.InverseLimit.Basic (7.4s)
✔ [3790/3814] Built FLT.Patching.Utils.Lemmas (5.0s)
✔ [3794/3827] Built FLT.Data.HurwitzRatHat (3.3s)
✔ [3797/3827] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.8s)
✔ [3799/3827] Built FLT.Deformations.Algebra.InverseLimit.Topology (3.9s)
✔ [3801/3827] Built FLT.Mathlib.RepresentationTheory.Basic (2.5s)
✔ [3802/3827] Built FLT.GaloisRepresentation.Cyclotomic (2.2s)
✔ [3803/3827] Built FLT.Deformations.RepresentationTheory.GaloisRep (15s)
✔ [3805/3827] Built FLT.Deformations.IsResidueAlgebra (2.6s)
✔ [3806/3827] Built FLT.Patching.Utils.AdicTopology (4.5s)
✔ [3807/3827] Built FLT.Deformations.RepresentationTheory.Irreducible (1.7s)
✔ [3808/3827] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (92s)
✔ [3809/3832] Built FLT.GaloisRepresentation.Automorphic (3.1s)
✔ [3810/3832] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (2.5s)
✔ [3811/3837] Built FLT.EllipticCurve.Torsion (3.1s)
✔ [3816/3844] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.0s)
✔ [3828/3844] Built FLT.Deformations.IsProartinian (2.2s)
✔ [3829/3844] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (2.5s)
✔ [3830/3849] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (2.6s)
✔ [3832/3853] Built FLT.GaloisRepresentation.HardlyRamified.Lift (2.3s)
✔ [3833/3855] Built FLT.GaloisRepresentation.HardlyRamified.Frey (2.5s)
✔ [3836/3870] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.7s)
✔ [3942/3968] Built FLT.Basic.Reductions (2.3s)
✔ [3943/3968] Built FLT.Deformations.Categories (3.9s)
✔ [3946/3968] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (2.0s)
✔ [3947/3968] Built FLT.Mathlib.GroupTheory.Index (1.3s)
✔ [3948/3968] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.8s)
✔ [3949/3968] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.7s)
✔ [3951/3968] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.7s)
✔ [3957/3982] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.6s)
✔ [3958/3982] Built FLT.Mathlib.Topology.Algebra.Monoid (1.5s)
✔ [3967/3985] Built FLT.Patching.Utils.TopologicallyFG (1.9s)
✔ [3968/3987] Built FLT.Mathlib.Topology.Algebra.Order.Field (3.2s)
✔ [3971/3987] Built FLT.Deformations.LiftFunctor (4.6s)
✔ [3972/3987] Built FLT.NumberField.DiscriminantBounds (4.7s)
✔ [3974/3987] Built FLT.Patching.Utils.StructureFiniteness (5.0s)
✔ [3976/3990] Built FLT.Deformations.Representable (3.5s)
✔ [3994/4011] Built FLT.GlobalLanglandsConjectures.GLnDefs (11s)
✔ [3995/4011] Built FLT.Patching.Utils.CompactHausdorffRings (3.8s)
✔ [3996/4011] Built FLT.Patching.Utils.Depth (6.1s)
✔ [3997/4011] Built FLT.GlobalLanglandsConjectures.GLzero (4.1s)
✔ [3998/4011] Built FLT.Patching.Ultraproduct (12s)
✔ [3999/4011] Built FLT.NumberField.AdeleRing (34s)
✔ [4000/4011] Built FLT.Patching.VanishingFilter (3.0s)
✔ [4001/4011] Built FLT.Patching.Algebra (13s)
✔ [4002/4011] Built FLT.HaarMeasure.HaarChar.AdeleRing (13s)
✔ [4003/4011] Built FLT.Patching.Module (15s)
✔ [4004/4011] Built FLT.Patching.Over (12s)
✔ [4005/4011] Built FLT.Patching.System (10s)
✔ [4006/4011] Built FLT.Patching.REqualsT (4.1s)
✔ [4007/4011] Built FLT.DivisionAlgebra.Finiteness (42s)
✔ [4008/4011] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (2.3s)
✔ [4009/4011] Built FLT (1.9s)
✔ [4010/4011] Built FermatsLastTheorem (18s)
Build completed successfully (4011 jobs).

blueprint_build exit 1 duration 3s · created 6/5/2026, 11:04:11 PM

lake build :blueprint

error: unknown package facet `blueprint`

semantic_extract exit - duration 4h 0m · created 6/5/2026, 11:04:11 PM

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

lean semantic helper: restored compiled static runner cache cb3988123f413cb6eafb01f6df5887b718b750259daf2194d1ef9e1aa7478844
/usr/bin/podman timed out after 14400s
podman cleanup removed verifier container apx-verifier-job-67-runtime-semantic_extract-2608519-1780686170453981266-3