Verification run

Run 9

ImperialCollegeLondon/FLT branch main triggered via poller

failed commit 47d88774aa2b toolchain lean-v4-31-0-rc1 prover lean took 3h 52m · 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 983 ms · created 6/3/2026, 9:26:46 PM

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

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

git_checkout exit 0 duration 17 ms · created 6/3/2026, 9:26:46 PM

git checkout 47d88774aa2b4372161e63599c212d4dc00b42cb

Note: switching to '47d88774aa2b4372161e63599c212d4dc00b42cb'.

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 47d8877 FLT final lecture (#1000)

lake_cache exit 0 duration 1m 25s · created 6/3/2026, 9:26:46 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 'f3c1871faf2d0368482578ad56ccdf6aeb3f72f4'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'd575be693add4fe9cb996968968ce42ce75c5ccd'
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 (491ms)
✔ [5/24] Built Cache.Lean (499ms)
✔ [6/24] Built Batteries.Data.Array.Match (721ms)
✔ [7/24] Built Cache.Init (275ms)
✔ [8/24] Built Batteries.Tactic.OpenPrivate (993ms)
✔ [9/24] Built Batteries.Data.Array.Match:c.o (235ms)
✔ [10/24] Built Batteries.Data.String.Basic:c.o (472ms)
✔ [11/24] Built Cache.Lean:c.o (249ms)
✔ [12/24] Built Cache.Init:c.o (75ms)
✔ [13/24] Built Batteries.Data.String.Matcher (302ms)
✔ [14/24] Built Batteries.Data.String.Matcher:c.o (153ms)
✔ [15/24] Built Batteries.Tactic.OpenPrivate:c.o (937ms)
✔ [16/24] Built Cache.IO (1.5s)
✔ [17/24] Built Cache.Hashing (783ms)
✔ [18/24] Built Cache.Hashing:c.o (344ms)
✔ [19/24] Built Cache.IO:c.o (1.2s)
✔ [20/24] Built Cache.Requests (1.9s)
✔ [21/24] Built Cache.Main (930ms)
✔ [22/24] Built Cache.Main:c.o (495ms)
✔ [23/24] Built Cache.Requests:c.o (1.8s)
✔ [24/24] Built cache:exe (2.3s)

Downloaded: 1 file(s) [attempted 1/8477 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8477 = 0%, 1 KB/s], Decompressed: 11
Downloaded: 38 file(s) [attempted 38/8477 = 0%, 14 KB/s], Decompressed: 22
Downloaded: 64 file(s) [attempted 64/8477 = 0%, 26 KB/s], Decompressed: 58
Downloaded: 93 file(s) [attempted 93/8477 = 1%, 351 KB/s], Decompressed: 83
Downloaded: 131 file(s) [attempted 131/8477 = 1%, 380 KB/s], Decompressed: 110
Downloaded: 162 file(s) [attempted 162/8477 = 1%, 422 KB/s], Decompressed: 138
Downloaded: 199 file(s) [attempted 199/8477 = 2%, 455 KB/s], Decompressed: 169
Downloaded: 240 file(s) [attempted 240/8477 = 2%, 502 KB/s], Decompressed: 210
Downloaded: 275 file(s) [attempted 275/8477 = 3%, 153 KB/s], Decompressed: 247
Downloaded: 319 file(s) [attempted 319/8477 = 3%, 150 KB/s], Decompressed: 275
Downloaded: 360 file(s) [attempted 360/8477 = 4%, 213 KB/s], Decompressed: 305
Downloaded: 395 file(s) [attempted 395/8477 = 4%, 119 KB/s], Decompressed: 340
Downloaded: 436 file(s) [attempted 436/8477 = 5%, 536 KB/s], Decompressed: 398
Downloaded: 474 file(s) [attempted 474/8477 = 5%, 337 KB/s], Decompressed: 422
Downloaded: 511 file(s) [attempted 511/8477 = 6%, 624 KB/s], Decompressed: 477
Downloaded: 549 file(s) [attempted 549/8477 = 6%, 28 KB/s], Decompressed: 504
Downloaded: 590 file(s) [attempted 590/8477 = 6%, 292 KB/s], Decompressed: 539
Downloaded: 635 file(s) [attempted 635/8477 = 7%, 57 KB/s], Decompressed: 539
Downloaded: 676 file(s) [attempted 676/8477 = 7%, 109 KB/s], Decompressed: 587
Downloaded: 713 file(s) [attempted 713/8477 = 8%, 288 KB/s], Decompressed: 638
Downloaded: 751 file(s) [attempted 751/8477 = 8%, 62 KB/s], Decompressed: 689
Downloaded: 789 file(s) [attempted 789/8477 = 9%, 337 KB/s], Decompressed: 737
Downloaded: 833 file(s) [attempted 833/8477 = 9%, 349 KB/s], Decompressed: 737
Downloaded: 874 file(s) [attempted 874/8477 = 10%, 42 KB/s], Decompressed: 785
Downloaded: 915 file(s) [attempted 915/8477 = 10%, 296 KB/s], Decompressed: 840
Downloaded: 950 file(s) [attempted 950/8477 = 11%, 168 KB/s], Decompressed: 891
Downloaded: 991 file(s) [attempted 991/8477 = 11%, 395 KB/s], Decompressed: 939
Downloaded: 1032 file(s) [attempted 1032/8477 = 12%, 678 KB/s], Decompressed: 939
Downloaded: 1069 file(s) [attempted 1069/8477 = 12%, 253 KB/s], Decompressed: 991
Downloaded: 1107 file(s) [attempted 1107/8477 = 13%, 72 KB/s], Decompressed: 1042
Downloaded: 1148 file(s) [attempted 1148/8477 = 13%, 84 KB/s], Decompressed: 1093
Downloaded: 1189 file(s) [attempted 1189/8477 = 14%, 570 KB/s], Decompressed: 1093
Downloaded: 1234 file(s) [attempted 1234/8477 = 14%, 97 KB/s], Decompressed: 1145
Downloaded: 1271 file(s) [attempted 1271/8477 = 14%, 96 KB/s], Decompressed: 1196
Downloaded: 1309 file(s) [attempted 1309/8477 = 15%, 123 KB/s], Decompressed: 1247
Downloaded: 1350 file(s) [attempted 1350/8477 = 15%, 219 KB/s], Decompressed: 1299
Downloaded: 1391 file(s) [attempted 1391/8477 = 16%, 178 KB/s], Decompressed: 1299
Downloaded: 1432 file(s) [attempted 1432/8477 = 16%, 395 KB/s], Decompressed: 1350
Downloaded: 1473 file(s) [attempted 1473/8477 = 17%, 109 KB/s], Decompressed: 1415
Downloaded: 1514 file(s) [attempted 1514/8477 = 17%, 137 KB/s], Decompressed: 1415
Downloaded: 1552 file(s) [attempted 1552/8477 = 18%, 167 KB/s], Decompressed: 1473
Downloaded: 1593 file(s) [attempted 1593/8477 = 18%, 35 KB/s], Decompressed: 1535
Downloaded: 1638 file(s) [attempted 1638/8477 = 19%, 59 KB/s], Decompressed: 1535
Downloaded: 1682 file(s) [attempted 1682/8477 = 19%, 161 KB/s], Decompressed: 1593
Downloaded: 1713 file(s) [attempted 1713/8477 = 20%, 200 KB/s], Decompressed: 1593
Downloaded: 1754 file(s) [attempted 1754/8477 = 20%, 294 KB/s], Decompressed: 1655
Downloaded: 1802 file(s) [attempted 1802/8477 = 21%, 36 KB/s], Decompressed: 1723
Downloaded: 1846 file(s) [attempted 1846/8477 = 21%, 41 KB/s], Decompressed: 1723
Downloaded: 1887 file(s) [attempted 1887/8477 = 22%, 3428 KB/s], Decompressed: 1792
Downloaded: 1932 file(s) [attempted 1932/8477 = 22%, 72 KB/s], Decompressed: 1853
Downloaded: 1966 file(s) [attempted 1966/8477 = 23%, 306 KB/s], Decompressed: 1853
Downloaded: 2007 file(s) [attempted 2007/8477 = 23%, 375 KB/s], Decompressed: 1908
Downloaded: 2041 file(s) [attempted 2041/8477 = 24%, 476 KB/s], Decompressed: 1977
Downloaded: 2086 file(s) [attempted 2086/8477 = 24%, 237 KB/s], Decompressed: 1977
Downloaded: 2124 file(s) [attempted 2124/8477 = 25%, 469 KB/s], Decompressed: 2041
Downloaded: 2158 file(s) [attempted 2158/8477 = 25%, 177 KB/s], Decompressed: 2041
Downloaded: 2202 file(s) [attempted 2202/8477 = 25%, 454 KB/s], Decompressed: 2110
Downloaded: 2240 file(s) [attempted 2240/8477 = 26%, 325 KB/s], Decompressed: 2110
Downloaded: 2278 file(s) [attempted 2278/8477 = 26%, 72 KB/s], Decompressed: 2182
Downloaded: 2319 file(s) [attempted 2319/8477 = 27%, 306 KB/s], Decompressed: 2182
Downloaded: 2360 file(s) [attempted 2360/8477 = 27%, 896 KB/s], Decompressed: 2257
Downloaded: 2397 file(s) [attempted 2397/8477 = 28%, 79 KB/s], Decompressed: 2257
Downloaded: 2438 file(s) [attempted 2438/8477 = 28%, 229 KB/s], Decompressed: 2329
Downloaded: 2479 file(s) [attempted 2479/8477 = 29%, 331 KB/s], Decompressed: 2329
Downloaded: 2517 file(s) [attempted 2517/8477 = 29%, 477 KB/s], Decompressed: 2408
Downloaded: 2558 file(s) [attempted 2558/8477 = 30%, 219 KB/s], Decompressed: 2408
Downloaded: 2603 file(s) [attempted 2603/8477 = 30%, 129 KB/s], Decompressed: 2490
Downloaded: 2647 file(s) [attempted 2647/8477 = 31%, 151 KB/s], Decompressed: 2490
Downloaded: 2692 file(s) [attempted 2692/8477 = 31%, 140 KB/s], Decompressed: 2575
Downloaded: 2726 file(s) [attempted 2726/8477 = 32%, 196 KB/s], Decompressed: 2575
Downloaded: 2767 file(s) [attempted 2767/8477 = 32%, 471 KB/s], Decompressed: 2654
Downloaded: 2801 file(s) [attempted 2801/8477 = 33%, 819 KB/s], Decompressed: 2729
Downloaded: 2846 file(s) [attempted 2846/8477 = 33%, 103 KB/s], Decompressed: 2729
Downloaded: 2890 file(s) [attempted 2890/8477 = 34%, 79 KB/s], Decompressed: 2794
Downloaded: 2935 file(s) [attempted 2935/8477 = 34%, 104 KB/s], Decompressed: 2794
Downloaded: 2976 file(s) [attempted 2976/8477 = 35%, 149 KB/s], Decompressed: 2866
Downloaded: 3013 file(s) [attempted 3013/8477 = 35%, 1754 KB/s], Decompressed: 2938
Downloaded: 3054 file(s) [attempted 3054/8477 = 36%, 154 KB/s], Decompressed: 2938
Downloaded: 3095 file(s) [attempted 3095/8477 = 36%, 544 KB/s], Decompressed: 3007
Downloaded: 3140 file(s) [attempted 3140/8477 = 37%, 103 KB/s], Decompressed: 3007
Downloaded: 3178 file(s) [attempted 3178/8477 = 37%, 303 KB/s], Decompressed: 3085
Downloaded: 3219 file(s) [attempted 3219/8477 = 37%, 169 KB/s], Decompressed: 3085
Downloaded: 3253 file(s) [attempted 3253/8477 = 38%, 1506 KB/s], Decompressed: 3085
Downloaded: 3297 file(s) [attempted 3297/8477 = 38%, 266 KB/s], Decompressed: 3171
Downloaded: 3342 file(s) [attempted 3342/8477 = 39%, 107 KB/s], Decompressed: 3171
Downloaded: 3383 file(s) [attempted 3383/8477 = 39%, 664 KB/s], Decompressed: 3280
Downloaded: 3427 file(s) [attempted 3427/8477 = 40%, 577 KB/s], Decompressed: 3280
Downloaded: 3465 file(s) [attempted 3465/8477 = 40%, 454 KB/s], Decompressed: 3280
Downloaded: 3510 file(s) [attempted 3510/8477 = 41%, 107 KB/s], Decompressed: 3383
Downloaded: 3540 file(s) [attempted 3540/8477 = 41%, 568 KB/s], Decompressed: 3383
Downloaded: 3585 file(s) [attempted 3585/8477 = 42%, 787 KB/s], Decompressed: 3472
Downloaded: 3623 file(s) [attempted 3623/8477 = 42%, 444 KB/s], Decompressed: 3544
Downloaded: 3664 file(s) [attempted 3664/8477 = 43%, 322 KB/s], Decompressed: 3544
Downloaded: 3705 file(s) [attempted 3705/8477 = 43%, 661 KB/s], Decompressed: 3616
Downloaded: 3742 file(s) [attempted 3742/8477 = 44%, 301 KB/s], Decompressed: 3616
Downloaded: 3783 file(s) [attempted 3783/8477 = 44%, 88 KB/s], Decompressed: 3677
Downloaded: 3824 file(s) [attempted 3824/8477 = 45%, 68 KB/s], Decompressed: 3749
Downloaded: 3862 file(s) [attempted 3862/8477 = 45%, 126 KB/s], Decompressed: 3749
Downloaded: 3903 file(s) [attempted 3903/8477 = 46%, 213 KB/s], Decompressed: 3811
Downloaded: 3944 file(s) [attempted 3944/8477 = 46%, 239 KB/s], Decompressed: 3879
Downloaded: 3985 file(s) [attempted 3985/8477 = 47%, 654 KB/s], Decompressed: 3879
Downloaded: 4020 file(s) [attempted 4020/8477 = 47%, 296 KB/s], Decompressed: 3944
Downloaded: 4064 file(s) [attempted 4064/8477 = 47%, 278 KB/s], Decompressed: 3944
Downloaded: 4102 file(s) [attempted 4102/8477 = 48%, 471 KB/s], Decompressed: 4009
Downloaded: 4146 file(s) [attempted 4146/8477 = 48%, 658 KB/s], Decompressed: 4067
Downloaded: 4187 file(s) [attempted 4187/8477 = 49%, 1095 KB/s], Decompressed: 4067
Downloaded: 4228 file(s) [attempted 4228/8477 = 49%, 91 KB/s], Decompressed: 4067
Downloaded: 4273 file(s) [attempted 4273/8477 = 50%, 46 KB/s], Decompressed: 4143
Downloaded: 4314 file(s) [attempted 4314/8477 = 50%, 1179 KB/s], Decompressed: 4143
Downloaded: 4352 file(s) [attempted 4352/8477 = 51%, 222 KB/s], Decompressed: 4232
Downloaded: 4396 file(s) [attempted 4396/8477 = 51%, 184 KB/s], Decompressed: 4232
Downloaded: 4434 file(s) [attempted 4434/8477 = 52%, 794 KB/s], Decompressed: 4321
Downloaded: 4478 file(s) [attempted 4478/8477 = 52%, 407 KB/s], Decompressed: 4321
Downloaded: 4523 file(s) [attempted 4523/8477 = 53%, 404 KB/s], Decompressed: 4399
Downloaded: 4560 file(s) [attempted 4560/8477 = 53%, 171 KB/s], Decompressed: 4399
Downloaded: 4601 file(s) [attempted 4601/8477 = 54%, 582 KB/s], Decompressed: 4488
Downloaded: 4646 file(s) [attempted 4646/8477 = 54%, 1137 KB/s], Decompressed: 4488
Downloaded: 4680 file(s) [attempted 4680/8477 = 55%, 538 KB/s], Decompressed: 4577
Downloaded: 4725 file(s) [attempted 4725/8477 = 55%, 364 KB/s], Decompressed: 4577
Downloaded: 4769 file(s) [attempted 4769/8477 = 56%, 132 KB/s], Decompressed: 4577
Downloaded: 4807 file(s) [attempted 4807/8477 = 56%, 1015 KB/s], Decompressed: 4670
Downloaded: 4844 file(s) [attempted 4844/8477 = 57%, 269 KB/s], Decompressed: 4670
Downloaded: 4879 file(s) [attempted 4879/8477 = 57%, 188 KB/s], Decompressed: 4772
Downloaded: 4926 file(s) [attempted 4926/8477 = 58%, 586 KB/s], Decompressed: 4772
Downloaded: 4971 file(s) [attempted 4971/8477 = 58%, 115 KB/s], Decompressed: 4872
Downloaded: 5015 file(s) [attempted 5015/8477 = 59%, 692 KB/s], Decompressed: 4872
Downloaded: 5053 file(s) [attempted 5053/8477 = 59%, 94 KB/s], Decompressed: 4872
Downloaded: 5091 file(s) [attempted 5091/8477 = 60%, 146 KB/s], Decompressed: 4964
Downloaded: 5131 file(s) [attempted 5131/8477 = 60%, 330 KB/s], Decompressed: 4964
Downloaded: 5169 file(s) [attempted 5169/8477 = 60%, 66 KB/s], Decompressed: 5070
Downloaded: 5214 file(s) [attempted 5214/8477 = 61%, 91 KB/s], Decompressed: 5070
Downloaded: 5252 file(s) [attempted 5252/8477 = 61%, 410 KB/s], Decompressed: 5070
Downloaded: 5294 file(s) [attempted 5294/8477 = 62%, 623 KB/s], Decompressed: 5163
Downloaded: 5330 file(s) [attempted 5330/8477 = 62%, 229 KB/s], Decompressed: 5163
Downloaded: 5368 file(s) [attempted 5368/8477 = 63%, 176 KB/s], Decompressed: 5258
Downloaded: 5412 file(s) [attempted 5412/8477 = 63%, 86 KB/s], Decompressed: 5258
Downloaded: 5454 file(s) [attempted 5454/8477 = 64%, 236 KB/s], Decompressed: 5351
Downloaded: 5495 file(s) [attempted 5495/8477 = 64%, 66 KB/s], Decompressed: 5351
Downloaded: 5532 file(s) [attempted 5532/8477 = 65%, 197 KB/s], Decompressed: 5351
Downloaded: 5570 file(s) [attempted 5570/8477 = 65%, 967 KB/s], Decompressed: 5443
Downloaded: 5614 file(s) [attempted 5614/8477 = 66%, 653 KB/s], Decompressed: 5443
Downloaded: 5655 file(s) [attempted 5655/8477 = 66%, 48 KB/s], Decompressed: 5536
Downloaded: 5693 file(s) [attempted 5693/8477 = 67%, 56 KB/s], Decompressed: 5536
Downloaded: 5731 file(s) [attempted 5731/8477 = 67%, 176 KB/s], Decompressed: 5618
Downloaded: 5775 file(s) [attempted 5775/8477 = 68%, 449 KB/s], Decompressed: 5618
Downloaded: 5820 file(s) [attempted 5820/8477 = 68%, 288 KB/s], Decompressed: 5710
Downloaded: 5864 file(s) [attempted 5864/8477 = 69%, 1044 KB/s], Decompressed: 5710
Downloaded: 5902 file(s) [attempted 5902/8477 = 69%, 250 KB/s], Decompressed: 5809
Downloaded: 5939 file(s) [attempted 5939/8477 = 70%, 408 KB/s], Decompressed: 5809
Downloaded: 5981 file(s) [attempted 5981/8477 = 70%, 92 KB/s], Decompressed: 5901
Downloaded: 6025 file(s) [attempted 6025/8477 = 71%, 403 KB/s], Decompressed: 5901
Downloaded: 6066 file(s) [attempted 6066/8477 = 71%, 365 KB/s], Decompressed: 5981
Downloaded: 6107 file(s) [attempted 6107/8477 = 72%, 350 KB/s], Decompressed: 5981
Downloaded: 6141 file(s) [attempted 6141/8477 = 72%, 126 KB/s], Decompressed: 5981
Downloaded: 6182 file(s) [attempted 6182/8477 = 72%, 657 KB/s], Decompressed: 6066
Downloaded: 6224 file(s) [attempted 6224/8477 = 73%, 757 KB/s], Decompressed: 6066
Downloaded: 6268 file(s) [attempted 6268/8477 = 73%, 91 KB/s], Decompressed: 6145
Downloaded: 6306 file(s) [attempted 6306/8477 = 74%, 228 KB/s], Decompressed: 6145
Downloaded: 6343 file(s) [attempted 6343/8477 = 74%, 846 KB/s], Decompressed: 6237
Downloaded: 6384 file(s) [attempted 6384/8477 = 75%, 203 KB/s], Decompressed: 6237
Downloaded: 6422 file(s) [attempted 6422/8477 = 75%, 224 KB/s], Decompressed: 6330
Downloaded: 6467 file(s) [attempted 6467/8477 = 76%, 243 KB/s], Decompressed: 6330
Downloaded: 6511 file(s) [attempted 6511/8477 = 76%, 79 KB/s], Decompressed: 6330
Downloaded: 6545 file(s) [attempted 6545/8477 = 77%, 59 KB/s], Decompressed: 6419
Downloaded: 6586 file(s) [attempted 6586/8477 = 77%, 89 KB/s], Decompressed: 6419
Downloaded: 6623 file(s) [attempted 6623/8477 = 78%, 2881 KB/s], Decompressed: 6514
Downloaded: 6665 file(s) [attempted 6665/8477 = 78%, 24 KB/s], Decompressed: 6514
Downloaded: 6710 file(s) [attempted 6710/8477 = 79%, 63 KB/s], Decompressed: 6610
Downloaded: 6747 file(s) [attempted 6747/8477 = 79%, 1514 KB/s], Decompressed: 6610
Downloaded: 6785 file(s) [attempted 6785/8477 = 80%, 623 KB/s], Decompressed: 6610
Downloaded: 6829 file(s) [attempted 6829/8477 = 80%, 1025 KB/s], Decompressed: 6706
Downloaded: 6870 file(s) [attempted 6870/8477 = 81%, 118 KB/s], Decompressed: 6706
Downloaded: 6915 file(s) [attempted 6915/8477 = 81%, 1779 KB/s], Decompressed: 6809
Downloaded: 6953 file(s) [attempted 6953/8477 = 82%, 282 KB/s], Decompressed: 6809
Downloaded: 6990 file(s) [attempted 6990/8477 = 82%, 527 KB/s], Decompressed: 6901
Downloaded: 7031 file(s) [attempted 7031/8477 = 82%, 285 KB/s], Decompressed: 6901
Downloaded: 7072 file(s) [attempted 7072/8477 = 83%, 1285 KB/s], Decompressed: 6976
Downloaded: 7117 file(s) [attempted 7117/8477 = 83%, 1038 KB/s], Decompressed: 6976
Downloaded: 7158 file(s) [attempted 7158/8477 = 84%, 101 KB/s], Decompressed: 7055
Downloaded: 7198 file(s) [attempted 7198/8477 = 84%, 280 KB/s], Decompressed: 7055
Downloaded: 7226 file(s) [attempted 7226/8477 = 85%, 657 KB/s], Decompressed: 7130
Downloaded: 7271 file(s) [attempted 7271/8477 = 85%, 38 KB/s], Decompressed: 7130
Downloaded: 7315 file(s) [attempted 7315/8477 = 86%, 178 KB/s], Decompressed: 7216
Downloaded: 7356 file(s) [attempted 7356/8477 = 86%, 382 KB/s], Decompressed: 7284
Downloaded: 7391 file(s) [attempted 7391/8477 = 87%, 357 KB/s], Decompressed: 7284
Downloaded: 7428 file(s) [attempted 7428/8477 = 87%, 5251 KB/s], Decompressed: 7350
Downloaded: 7469 file(s) [attempted 7469/8477 = 88%, 294 KB/s], Decompressed: 7411
Downloaded: 7514 file(s) [attempted 7514/8477 = 88%, 766 KB/s], Decompressed: 7411
Downloaded: 7558 file(s) [attempted 7558/8477 = 89%, 169 KB/s], Decompressed: 7466
Downloaded: 7596 file(s) [attempted 7596/8477 = 89%, 239 KB/s], Decompressed: 7521
Downloaded: 7630 file(s) [attempted 7630/8477 = 90%, 341 KB/s], Decompressed: 7572
Downloaded: 7671 file(s) [attempted 7671/8477 = 90%, 258 KB/s], Decompressed: 7572
Downloaded: 7716 file(s) [attempted 7716/8477 = 91%, 657 KB/s], Decompressed: 7627
Downloaded: 7760 file(s) [attempted 7760/8477 = 91%, 150 KB/s], Decompressed: 7675
Downloaded: 7812 file(s) [attempted 7812/8477 = 92%, 149 KB/s], Decompressed: 7764
Downloaded: 7863 file(s) [attempted 7863/8477 = 92%, 291 KB/s], Decompressed: 7812
Downloaded: 7911 file(s) [attempted 7911/8477 = 93%, 873 KB/s], Decompressed: 7812
Downloaded: 7962 file(s) [attempted 7962/8477 = 93%, 37 KB/s], Decompressed: 7863
Downloaded: 8010 file(s) [attempted 8010/8477 = 94%, 76 KB/s], Decompressed: 7924
Downloaded: 8047 file(s) [attempted 8047/8477 = 94%, 605 KB/s], Decompressed: 7924
Downloaded: 8078 file(s) [attempted 8078/8477 = 95%, 64 KB/s], Decompressed: 7924
Downloaded: 8126 file(s) [attempted 8126/8477 = 95%, 172 KB/s], Decompressed: 8010
Downloaded: 8171 file(s) [attempted 8171/8477 = 96%, 80 KB/s], Decompressed: 8010
Downloaded: 8215 file(s) [attempted 8215/8477 = 96%, 134 KB/s], Decompressed: 8092
Downloaded: 8256 file(s) [attempted 8256/8477 = 97%, 76 KB/s], Decompressed: 8092
Downloaded: 8291 file(s) [attempted 8291/8477 = 97%, 117 KB/s], Decompressed: 8191
Downloaded: 8325 file(s) [attempted 8325/8477 = 98%, 475 KB/s], Decompressed: 8191
Downloaded: 8369 file(s) [attempted 8369/8477 = 98%, 284 KB/s], Decompressed: 8280
Downloaded: 8417 file(s) [attempted 8417/8477 = 99%, 343 KB/s], Decompressed: 8280
Downloaded: 8462 file(s) [attempted 8462/8477 = 99%, 966 KB/s], Decompressed: 8366
Downloaded: 8477 file(s) [attempted 8477/8477 = 100%, 966 KB/s], Decompressed: 8366

lean_checker exit 0 duration 4m 56s · created 6/3/2026, 9:26:46 PM

lake build

✔ [402/683] Built FLT.Assumptions.KnownIn1980s (303ms)
✔ [2945/2983] Built FLT.Assumptions.Mazur (3.7s)
✔ [3075/3147] Built FLT.Assumptions.Odlyzko (3.7s)
✔ [3076/3147] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (3.7s)
✔ [3138/3283] Built FLT.Mathlib.Algebra.Algebra.Tower (3.8s)
✔ [3295/3316] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (2.0s)
✔ [3296/3316] Built FLT.Mathlib.Algebra.FixedPoints.Basic (3.0s)
✔ [3297/3316] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (4.1s)
✔ [3298/3316] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (2.3s)
✔ [3299/3316] Built FLT.Mathlib.Topology.Algebra.Group.Units (1.7s)
✔ [3302/3316] Built FLT.Mathlib.Order.Filter.Cofinite (1.0s)
✔ [3304/3316] Built FLT.Mathlib.Topology.Bases (1.1s)
✔ [3305/3316] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (6.2s)
✔ [3306/3316] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (1.5s)
✔ [3308/3317] Built FLT.Mathlib.MeasureTheory.Group.Action (2.7s)
✔ [3309/3317] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (1.9s)
✔ [3310/3330] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (4.6s)
✔ [3316/3337] Built FLT.Mathlib.MeasureTheory.Group.Measure (1.6s)
✔ [3320/3337] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.4s)
✔ [3322/3337] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.4s)
✔ [3323/3338] Built FLT.Hacks.RightActionInstances (4.7s)
✔ [3326/3342] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (6.6s)
✔ [3328/3342] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (2.3s)
✔ [3330/3342] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (1.5s)
✔ [3332/3348] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (2.3s)
✔ [3339/3353] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (1.2s)
✔ [3343/3359] Built FLT.Mathlib.LinearAlgebra.Countable (1.6s)
✔ [3348/3375] Built FLT.AutomorphicForm.QuaternionAlgebra.Defs (5.5s)
✔ [3357/3375] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (6.6s)
✔ [3360/3375] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (3.7s)
✔ [3363/3375] Built FLT.Mathlib.RingTheory.Localization.BaseChange (2.0s)
✔ [3364/3377] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (3.0s)
✔ [3365/3379] Built FLT.HaarMeasure.HaarChar.AddEquiv (9.4s)
✔ [3369/3384] Built FLT.DedekindDomain.AdicValuation (13s)
✔ [3372/3393] Built FLT.NumberField.Completion.Finite (2.0s)
✔ [3375/3393] Built FLT.DedekindDomain.IntegralClosure (8.3s)
✔ [3376/3393] Built FLT.HaarMeasure.HaarChar.Ring (3.9s)
✔ [3377/3393] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (1.7s)
✔ [3378/3393] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (1.1s)
✔ [3379/3403] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (14s)
✔ [3383/3403] Built FLT.Mathlib.Algebra.Algebra.Hom (2.6s)
✔ [3384/3403] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (1.8s)
✔ [3385/3407] Built FLT.NumberField.HeightOneSpectrum (1.7s)
✔ [3388/3407] Built FLT.Mathlib.Algebra.IsDirectLimit (2.4s)
✔ [3389/3407] Built FLT.Mathlib.Topology.Algebra.MulAction (1.4s)
✔ [3390/3407] Built FLT.Mathlib.LinearAlgebra.Pi (1.7s)
✔ [3391/3407] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (1.9s)
✔ [3393/3407] Built FLT.Mathlib.Topology.Algebra.UniformRing (1.4s)
✔ [3396/3407] Built FLT.Mathlib.Algebra.Algebra.Pi (1.5s)
✔ [3397/3407] Built FLT.Mathlib.Algebra.Algebra.Bilinear (2.4s)
✔ [3398/3422] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (1.9s)
✔ [3400/3422] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (3.3s)
✔ [3401/3423] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (3.5s)
✔ [3404/3423] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (1.9s)
✔ [3405/3423] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (2.3s)
✔ [3406/3423] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (1.0s)
✔ [3407/3423] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (10s)
✔ [3408/3423] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (2.1s)
✔ [3409/3423] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (1.9s)
✔ [3410/3426] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (10s)
✔ [3412/3426] Built FLT.Mathlib.Topology.Constructions (1.2s)
✔ [3414/3426] Built FLT.NumberField.InfinitePlace.Extension (3.3s)
✔ [3415/3433] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (2.4s)
✔ [3418/3435] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (2.0s)
✔ [3420/3435] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (3.2s)
✔ [3421/3435] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (2.8s)
✔ [3422/3435] Built FLT.Mathlib.Data.Real.Archimedean (2.1s)
✔ [3425/3435] Built FLT.NumberField.Padics.RestrictedProduct (4.6s)
✔ [3426/3438] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (2.8s)
✔ [3427/3438] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (3.7s)
✔ [3429/3454] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (2.2s)
✔ [3436/3460] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (3.0s)
✔ [3438/3463] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (9.1s)
✔ [3440/3463] Built FLT.HaarMeasure.MeasurableSpacePadics (4.1s)
✔ [3442/3463] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (5.7s)
✔ [3443/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (2.1s)
✔ [3445/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (1.9s)
✔ [3447/3466] Built FLT.HaarMeasure.HaarChar.RealComplex (4.5s)
✔ [3448/3466] Built FLT.HaarMeasure.HaarChar.Padic (4.7s)
✔ [3450/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.5s)
✔ [3452/3466] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (3.2s)
✔ [3453/3466] Built FLT.Mathlib.GroupTheory.DoubleCoset (2.3s)
✔ [3455/3468] Built FLT.Mathlib.Algebra.Central.TensorProduct (3.4s)
✔ [3456/3471] Built FLT.NumberField.Completion.Infinite (28s)
✔ [3459/3472] Built FLT.Mathlib.LinearAlgebra.Determinant (5.1s)
✔ [3461/3475] Built FLT.DedekindDomain.Completion.BaseChange (53s)
✔ [3464/3485] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (10s)
✔ [3470/3485] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (4.0s)
✔ [3471/3485] Built FLT.Mathlib.Topology.HomToDiscrete (1.8s)
✔ [3473/3496] Built FLT.Mathlib.Topology.Polish (1.8s)
✔ [3474/3497] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (2.6s)
✔ [3476/3497] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (1.9s)
✔ [3477/3497] Built FLT.Mathlib.Topology.Instances.Matrix (1.6s)
✔ [3478/3497] Built FLT.NumberField.InfiniteAdeleRing (17s)
✔ [3483/3500] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (1.8s)
✔ [3485/3500] Built FLT.Mathlib.MeasureTheory.Haar.Extension (2.8s)
✔ [3487/3513] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (4.5s)
✔ [3652/3704] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (1.0s)
✔ [3698/3713] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (2.3s)
✔ [3701/3731] Built FLT.Basic.FreyPackage (6.2s)
✔ [3719/3736] Built FLT.QuaternionAlgebra.NumberField (13s)
✔ [3722/3737] Built FLT.Deformations.Lemmas (6.6s)
✔ [3725/3738] Built FLT.Deformations.RepresentationTheory.IntegralClosure (3.8s)
✔ [3728/3752] Built FLT.Deformations.RepresentationTheory.Frobenius (5.4s)
✔ [3743/3754] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (12s)
✔ [3744/3767] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (48s)
✔ [3755/3767] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (12s)
✔ [3772/3803] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (2.2s)
✔ [3778/3803] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (18s)
✔ [3779/3803] Built FLT.Data.Hurwitz (6.0s)
✔ [3780/3803] Built FLT.Deformations.RepresentationTheory.Etale (12s)
✔ [3782/3805] Built FLT.Patching.Utils.InverseLimit (2.1s)
✔ [3785/3806] Built FLT.Data.QHat (9.2s)
✔ [3786/3806] Built FLT.Deformations.Algebra.InverseLimit.Basic (7.4s)
✔ [3789/3825] Built FLT.Data.HurwitzRatHat (2.9s)
✔ [3792/3825] Built FLT.Patching.Utils.Lemmas (6.2s)
✔ [3795/3825] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.6s)
✔ [3797/3825] Built FLT.Deformations.Algebra.InverseLimit.Topology (3.0s)
✔ [3799/3825] Built FLT.Mathlib.RepresentationTheory.Basic (2.5s)
✔ [3800/3825] Built FLT.GaloisRepresentation.Cyclotomic (2.2s)
✔ [3801/3825] Built FLT.Deformations.IsResidueAlgebra (2.5s)
✔ [3802/3825] Built FLT.Deformations.RepresentationTheory.GaloisRep (15s)
✔ [3803/3830] Built FLT.Patching.Utils.AdicTopology (4.3s)
✔ [3804/3830] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (82s)
✔ [3805/3830] Built FLT.Deformations.Subfunctor (1.0s)
✔ [3806/3830] Built FLT.Deformations.RepresentationTheory.Irreducible (1.5s)
✔ [3807/3830] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (2.1s)
✔ [3808/3831] Built FLT.GaloisRepresentation.Automorphic (2.8s)
✔ [3810/3873] Built FLT.EllipticCurve.Torsion (2.7s)
✔ [3911/3966] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.6s)
✔ [3933/3966] Built FLT.GroupScheme.FiniteFlat (280ms)
✔ [3934/3966] Built FLT.Deformations.IsProartinian (2.2s)
✔ [3935/3966] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (1.7s)
✔ [3936/3966] Built FLT.Mathlib.Data.Fin.Basic (1.2s)
✔ [3937/3966] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.8s)
✔ [3938/3966] Built FLT.Mathlib.Data.Set.Prod (577ms)
✔ [3939/3966] Built FLT.Mathlib.GroupTheory.Index (1.3s)
✔ [3940/3966] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.3s)
✔ [3942/3966] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.4s)
✔ [3944/3966] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.5s)
✔ [3945/3966] Built FLT.Mathlib.Topology.Algebra.Monoid (1.3s)
✔ [3946/3966] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (2.0s)
✔ [3947/3966] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (2.2s)
✔ [3948/3966] Built FLT.GaloisRepresentation.HardlyRamified.Lift (2.4s)
✔ [3949/3966] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.4s)
✔ [3950/3969] Built FLT.GaloisRepresentation.HardlyRamified.Frey (2.3s)
✔ [3952/3971] Built FLT.Deformations.Categories (3.8s)
✔ [3958/3980] Built FLT.Mathlib.Topology.Algebra.Order.Field (3.1s)
✔ [3964/3980] Built FLT.Basic.Reductions (2.5s)
✔ [3966/3983] Built FLT.Patching.Utils.TopologicallyFG (1.8s)
✔ [3968/3985] Built FLT.Deformations.LiftFunctor (4.6s)
✔ [3970/3985] Built FLT.NumberField.DiscriminantBounds (4.6s)
✔ [3971/3985] Built FLT.Patching.Utils.StructureFiniteness (5.1s)
✔ [3973/4002] Built FLT.Deformations.Representable (3.4s)
✔ [3991/4009] Built FLT.TateCurve.TateCurve (248ms)
✔ [3992/4009] Built FLT.GlobalLanglandsConjectures.GLnDefs (10s)
✔ [3993/4009] Built FLT.Patching.Utils.CompactHausdorffRings (3.1s)
✔ [3994/4009] Built FLT.Patching.Utils.Depth (5.5s)
✔ [3995/4009] Built FLT.GlobalLanglandsConjectures.GLzero (3.5s)
✔ [3996/4009] Built FLT.Patching.Ultraproduct (11s)
✔ [3997/4009] Built FLT.NumberField.AdeleRing (33s)
✔ [3998/4009] Built FLT.Patching.VanishingFilter (3.8s)
✔ [3999/4009] Built FLT.Patching.Algebra (13s)
✔ [4000/4009] Built FLT.HaarMeasure.HaarChar.AdeleRing (13s)
✔ [4001/4009] Built FLT.Patching.Module (15s)
✔ [4002/4009] Built FLT.Patching.Over (13s)
✔ [4003/4009] Built FLT.Patching.System (10s)
✔ [4004/4009] Built FLT.Patching.REqualsT (4.3s)
✔ [4005/4009] Built FLT.DivisionAlgebra.Finiteness (41s)
✔ [4006/4009] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (2.3s)
✔ [4007/4009] Built FLT (1.9s)
✔ [4008/4009] Built FermatsLastTheorem (15s)
Build completed successfully (4009 jobs).

blueprint_build exit 1 duration 1s · created 6/3/2026, 9:26:46 PM

lake build :blueprint

error: unknown package facet `blueprint`

semantic_extract exit - duration 3h 44m · created 6/3/2026, 9:26:46 PM

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

lean semantic helper: restored compiled static runner cache 818813c2350d2209c35f675d001e3c6a50e2a150f68d5d473e09e6b301a8f5e6
podman cleanup removed verifier container apx-verifier-job-57-runtime-semantic_extract-3537272-1780508436557006904-3