Verification run

Run 17

ImperialCollegeLondon/FLT branch main triggered via poller

failed commit f178a1fc94fd toolchain lean-v4-31-0-rc1 prover lean took 24m 56s · finished 5w ago

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003) failed with exit code 143 (toolchain lean-v4-31-0-rc1, command: <command argv unavailable>)

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 835 ms · created 6/10/2026, 2:36:12 PM

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

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

git_checkout exit 0 duration 35 ms · created 6/10/2026, 2:36:12 PM

git checkout f178a1fc94fd8054db53fdeee063c286f6dab329

Note: switching to 'f178a1fc94fd8054db53fdeee063c286f6dab329'.

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 f178a1f chore: bump mathlib to 1d78019, fix breaking changes (#1009)

lake_cache exit 0 duration 1m 13s · created 6/10/2026, 2:36:12 PM

lake exe cache get

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

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '1d7801990b62b5e70a7b3d2d3bb1b52b1c7ba4a8'
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
✔ [11/23] Built Cache.Lean (457ms)
✔ [12/23] Built Cache.Init (407ms)
✔ [13/23] Built Cache.Lean:c.o (416ms)
✔ [14/23] Built Cache.Init:c.o (450ms)
✔ [15/23] Built Cache.IO (1.8s)
✔ [16/23] Built Cache.Hashing (988ms)
✔ [17/23] Built Cache.IO:c.o (1.2s)
✔ [18/23] Built Cache.Hashing:c.o (344ms)
✔ [19/23] Built Cache.Requests (2.2s)
✔ [20/23] Built Cache.Main (1.1s)
✔ [21/23] Built Cache.Main:c.o (514ms)
✔ [22/23] Built Cache.Requests:c.o (1.8s)
✔ [23/23] Built cache:exe (2.4s)

Downloaded: 1 file(s) [attempted 1/8520 = 0%, 11 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8520 = 0%, 26 KB/s], Decompressed: 11
Downloaded: 37 file(s) [attempted 37/8520 = 0%, 12 KB/s], Decompressed: 28
Downloaded: 64 file(s) [attempted 64/8520 = 0%, 332 KB/s], Decompressed: 57
Downloaded: 93 file(s) [attempted 93/8520 = 1%, 191 KB/s], Decompressed: 79
Downloaded: 124 file(s) [attempted 124/8520 = 1%, 22 KB/s], Decompressed: 103
Downloaded: 158 file(s) [attempted 158/8520 = 1%, 253 KB/s], Decompressed: 138
Downloaded: 199 file(s) [attempted 199/8520 = 2%, 491 KB/s], Decompressed: 182
Downloaded: 240 file(s) [attempted 240/8520 = 2%, 256 KB/s], Decompressed: 223
Downloaded: 285 file(s) [attempted 285/8520 = 3%, 159 KB/s], Decompressed: 240
Downloaded: 323 file(s) [attempted 323/8520 = 3%, 765 KB/s], Decompressed: 292
Downloaded: 364 file(s) [attempted 364/8520 = 4%, 134 KB/s], Decompressed: 340
Downloaded: 401 file(s) [attempted 401/8520 = 4%, 113 KB/s], Decompressed: 381
Downloaded: 439 file(s) [attempted 439/8520 = 5%, 92 KB/s], Decompressed: 415
Downloaded: 480 file(s) [attempted 480/8520 = 5%, 1206 KB/s], Decompressed: 453
Downloaded: 518 file(s) [attempted 518/8520 = 6%, 1611 KB/s], Decompressed: 487
Downloaded: 559 file(s) [attempted 559/8520 = 6%, 1483 KB/s], Decompressed: 509
Downloaded: 600 file(s) [attempted 600/8520 = 7%, 851 KB/s], Decompressed: 562
Downloaded: 641 file(s) [attempted 641/8520 = 7%, 55 KB/s], Decompressed: 593
Downloaded: 682 file(s) [attempted 682/8520 = 8%, 228 KB/s], Decompressed: 655
Downloaded: 720 file(s) [attempted 720/8520 = 8%, 1108 KB/s], Decompressed: 703
Downloaded: 764 file(s) [attempted 764/8520 = 8%, 590 KB/s], Decompressed: 741
Downloaded: 802 file(s) [attempted 802/8520 = 9%, 543 KB/s], Decompressed: 771
Downloaded: 843 file(s) [attempted 843/8520 = 9%, 517 KB/s], Decompressed: 792
Downloaded: 884 file(s) [attempted 884/8520 = 10%, 301 KB/s], Decompressed: 819
Downloaded: 922 file(s) [attempted 922/8520 = 10%, 194 KB/s], Decompressed: 857
Downloaded: 963 file(s) [attempted 963/8520 = 11%, 154 KB/s], Decompressed: 908
Downloaded: 1001 file(s) [attempted 1001/8520 = 11%, 221 KB/s], Decompressed: 949
Downloaded: 1042 file(s) [attempted 1042/8520 = 12%, 142 KB/s], Decompressed: 1015
Downloaded: 1083 file(s) [attempted 1083/8520 = 12%, 364 KB/s], Decompressed: 1042
Downloaded: 1127 file(s) [attempted 1127/8520 = 13%, 175 KB/s], Decompressed: 1073
Downloaded: 1165 file(s) [attempted 1165/8520 = 13%, 336 KB/s], Decompressed: 1131
Downloaded: 1199 file(s) [attempted 1199/8520 = 14%, 512 KB/s], Decompressed: 1155
Downloaded: 1244 file(s) [attempted 1244/8520 = 14%, 90 KB/s], Decompressed: 1192
Downloaded: 1288 file(s) [attempted 1288/8520 = 15%, 247 KB/s], Decompressed: 1237
Downloaded: 1333 file(s) [attempted 1333/8520 = 15%, 1114 KB/s], Decompressed: 1281
Downloaded: 1367 file(s) [attempted 1367/8520 = 16%, 152 KB/s], Decompressed: 1281
Downloaded: 1401 file(s) [attempted 1401/8520 = 16%, 398 KB/s], Decompressed: 1326
Downloaded: 1442 file(s) [attempted 1442/8520 = 16%, 87 KB/s], Decompressed: 1405
Downloaded: 1487 file(s) [attempted 1487/8520 = 17%, 24 KB/s], Decompressed: 1456
Downloaded: 1531 file(s) [attempted 1531/8520 = 17%, 164 KB/s], Decompressed: 1500
Downloaded: 1566 file(s) [attempted 1566/8520 = 18%, 255 KB/s], Decompressed: 1528
Downloaded: 1603 file(s) [attempted 1603/8520 = 18%, 155 KB/s], Decompressed: 1583
Downloaded: 1644 file(s) [attempted 1644/8520 = 19%, 1074 KB/s], Decompressed: 1627
Downloaded: 1692 file(s) [attempted 1692/8520 = 19%, 162 KB/s], Decompressed: 1644
Downloaded: 1733 file(s) [attempted 1733/8520 = 20%, 118 KB/s], Decompressed: 1696
Downloaded: 1774 file(s) [attempted 1774/8520 = 20%, 304 KB/s], Decompressed: 1726
Downloaded: 1822 file(s) [attempted 1822/8520 = 21%, 62 KB/s], Decompressed: 1788
Downloaded: 1867 file(s) [attempted 1867/8520 = 21%, 186 KB/s], Decompressed: 1843
Downloaded: 1908 file(s) [attempted 1908/8520 = 22%, 138 KB/s], Decompressed: 1877
Downloaded: 1945 file(s) [attempted 1945/8520 = 22%, 259 KB/s], Decompressed: 1901
Downloaded: 1986 file(s) [attempted 1986/8520 = 23%, 247 KB/s], Decompressed: 1939
Downloaded: 2024 file(s) [attempted 2024/8520 = 23%, 68 KB/s], Decompressed: 1976
Downloaded: 2065 file(s) [attempted 2065/8520 = 24%, 23 KB/s], Decompressed: 1976
Downloaded: 2103 file(s) [attempted 2103/8520 = 24%, 689 KB/s], Decompressed: 2017
Downloaded: 2144 file(s) [attempted 2144/8520 = 25%, 599 KB/s], Decompressed: 2075
Downloaded: 2184 file(s) [attempted 2184/8520 = 25%, 764 KB/s], Decompressed: 2127
Downloaded: 2226 file(s) [attempted 2226/8520 = 26%, 866 KB/s], Decompressed: 2127
Downloaded: 2260 file(s) [attempted 2260/8520 = 26%, 1066 KB/s], Decompressed: 2182
Downloaded: 2301 file(s) [attempted 2301/8520 = 27%, 753 KB/s], Decompressed: 2236
Downloaded: 2342 file(s) [attempted 2342/8520 = 27%, 40 KB/s], Decompressed: 2236
Downloaded: 2387 file(s) [attempted 2387/8520 = 28%, 302 KB/s], Decompressed: 2291
Downloaded: 2425 file(s) [attempted 2425/8520 = 28%, 170 KB/s], Decompressed: 2346
Downloaded: 2462 file(s) [attempted 2462/8520 = 28%, 256 KB/s], Decompressed: 2401
Downloaded: 2500 file(s) [attempted 2500/8520 = 29%, 41 KB/s], Decompressed: 2401
Downloaded: 2534 file(s) [attempted 2534/8520 = 29%, 934 KB/s], Decompressed: 2462
Downloaded: 2579 file(s) [attempted 2579/8520 = 30%, 47 KB/s], Decompressed: 2524
Downloaded: 2623 file(s) [attempted 2623/8520 = 30%, 228 KB/s], Decompressed: 2575
Downloaded: 2664 file(s) [attempted 2664/8520 = 31%, 191 KB/s], Decompressed: 2575
Downloaded: 2705 file(s) [attempted 2705/8520 = 31%, 320 KB/s], Decompressed: 2620
Downloaded: 2746 file(s) [attempted 2746/8520 = 32%, 76 KB/s], Decompressed: 2671
Downloaded: 2784 file(s) [attempted 2784/8520 = 32%, 238 KB/s], Decompressed: 2722
Downloaded: 2822 file(s) [attempted 2822/8520 = 33%, 67 KB/s], Decompressed: 2770
Downloaded: 2863 file(s) [attempted 2863/8520 = 33%, 70 KB/s], Decompressed: 2770
Downloaded: 2904 file(s) [attempted 2904/8520 = 34%, 181 KB/s], Decompressed: 2818
Downloaded: 2945 file(s) [attempted 2945/8520 = 34%, 659 KB/s], Decompressed: 2869
Downloaded: 2982 file(s) [attempted 2982/8520 = 35%, 181 KB/s], Decompressed: 2869
Downloaded: 3020 file(s) [attempted 3020/8520 = 35%, 397 KB/s], Decompressed: 2931
Downloaded: 3058 file(s) [attempted 3058/8520 = 35%, 124 KB/s], Decompressed: 2986
Downloaded: 3102 file(s) [attempted 3102/8520 = 36%, 501 KB/s], Decompressed: 3041
Downloaded: 3143 file(s) [attempted 3143/8520 = 36%, 337 KB/s], Decompressed: 3041
Downloaded: 3184 file(s) [attempted 3184/8520 = 37%, 486 KB/s], Decompressed: 3102
Downloaded: 3218 file(s) [attempted 3218/8520 = 37%, 189 KB/s], Decompressed: 3153
Downloaded: 3256 file(s) [attempted 3256/8520 = 38%, 183 KB/s], Decompressed: 3153
Downloaded: 3301 file(s) [attempted 3301/8520 = 38%, 238 KB/s], Decompressed: 3205
Downloaded: 3345 file(s) [attempted 3345/8520 = 39%, 176 KB/s], Decompressed: 3270
Downloaded: 3383 file(s) [attempted 3383/8520 = 39%, 285 KB/s], Decompressed: 3331
Downloaded: 3424 file(s) [attempted 3424/8520 = 40%, 197 KB/s], Decompressed: 3331
Downloaded: 3461 file(s) [attempted 3461/8520 = 40%, 68 KB/s], Decompressed: 3383
Downloaded: 3499 file(s) [attempted 3499/8520 = 41%, 142 KB/s], Decompressed: 3468
Downloaded: 3537 file(s) [attempted 3537/8520 = 41%, 235 KB/s], Decompressed: 3499
Downloaded: 3581 file(s) [attempted 3581/8520 = 42%, 284 KB/s], Decompressed: 3561
Downloaded: 3629 file(s) [attempted 3629/8520 = 42%, 1068 KB/s], Decompressed: 3581
Downloaded: 3674 file(s) [attempted 3674/8520 = 43%, 445 KB/s], Decompressed: 3609
Downloaded: 3711 file(s) [attempted 3711/8520 = 43%, 51 KB/s], Decompressed: 3646
Downloaded: 3756 file(s) [attempted 3756/8520 = 44%, 24 KB/s], Decompressed: 3718
Downloaded: 3793 file(s) [attempted 3793/8520 = 44%, 61 KB/s], Decompressed: 3756
Downloaded: 3831 file(s) [attempted 3831/8520 = 44%, 259 KB/s], Decompressed: 3793
Downloaded: 3872 file(s) [attempted 3872/8520 = 45%, 737 KB/s], Decompressed: 3828
Downloaded: 3910 file(s) [attempted 3910/8520 = 45%, 149 KB/s], Decompressed: 3858
Downloaded: 3954 file(s) [attempted 3954/8520 = 46%, 243 KB/s], Decompressed: 3917
Downloaded: 3995 file(s) [attempted 3995/8520 = 46%, 321 KB/s], Decompressed: 3947
Downloaded: 4040 file(s) [attempted 4040/8520 = 47%, 442 KB/s], Decompressed: 4009
Downloaded: 4081 file(s) [attempted 4081/8520 = 47%, 65 KB/s], Decompressed: 4040
Downloaded: 4115 file(s) [attempted 4115/8520 = 48%, 495 KB/s], Decompressed: 4040
Downloaded: 4156 file(s) [attempted 4156/8520 = 48%, 315 KB/s], Decompressed: 4081
Downloaded: 4197 file(s) [attempted 4197/8520 = 49%, 1168 KB/s], Decompressed: 4119
Downloaded: 4238 file(s) [attempted 4238/8520 = 49%, 706 KB/s], Decompressed: 4201
Downloaded: 4273 file(s) [attempted 4273/8520 = 50%, 162 KB/s], Decompressed: 4238
Downloaded: 4314 file(s) [attempted 4314/8520 = 50%, 318 KB/s], Decompressed: 4273
Downloaded: 4351 file(s) [attempted 4351/8520 = 51%, 506 KB/s], Decompressed: 4310
Downloaded: 4396 file(s) [attempted 4396/8520 = 51%, 351 KB/s], Decompressed: 4344
Downloaded: 4433 file(s) [attempted 4433/8520 = 52%, 480 KB/s], Decompressed: 4382
Downloaded: 4481 file(s) [attempted 4481/8520 = 52%, 24 KB/s], Decompressed: 4427
Downloaded: 4526 file(s) [attempted 4526/8520 = 53%, 596 KB/s], Decompressed: 4457
Downloaded: 4563 file(s) [attempted 4563/8520 = 53%, 61 KB/s], Decompressed: 4492
Downloaded: 4598 file(s) [attempted 4598/8520 = 53%, 233 KB/s], Decompressed: 4529
Downloaded: 4639 file(s) [attempted 4639/8520 = 54%, 358 KB/s], Decompressed: 4570
Downloaded: 4680 file(s) [attempted 4680/8520 = 54%, 533 KB/s], Decompressed: 4608
Downloaded: 4718 file(s) [attempted 4718/8520 = 55%, 48 KB/s], Decompressed: 4649
Downloaded: 4759 file(s) [attempted 4759/8520 = 55%, 101 KB/s], Decompressed: 4697
Downloaded: 4793 file(s) [attempted 4793/8520 = 56%, 22 KB/s], Decompressed: 4745
Downloaded: 4837 file(s) [attempted 4837/8520 = 56%, 369 KB/s], Decompressed: 4786
Downloaded: 4878 file(s) [attempted 4878/8520 = 57%, 112 KB/s], Decompressed: 4827
Downloaded: 4919 file(s) [attempted 4919/8520 = 57%, 75 KB/s], Decompressed: 4861
Downloaded: 4957 file(s) [attempted 4957/8520 = 58%, 144 KB/s], Decompressed: 4892
Downloaded: 5002 file(s) [attempted 5002/8520 = 58%, 185 KB/s], Decompressed: 4961
Downloaded: 5046 file(s) [attempted 5046/8520 = 59%, 239 KB/s], Decompressed: 4991
Downloaded: 5084 file(s) [attempted 5084/8520 = 59%, 206 KB/s], Decompressed: 5049
Downloaded: 5125 file(s) [attempted 5125/8520 = 60%, 612 KB/s], Decompressed: 5077
Downloaded: 5162 file(s) [attempted 5162/8520 = 60%, 42 KB/s], Decompressed: 5128
Downloaded: 5200 file(s) [attempted 5200/8520 = 61%, 413 KB/s], Decompressed: 5162
Downloaded: 5248 file(s) [attempted 5248/8520 = 61%, 134 KB/s], Decompressed: 5197
Downloaded: 5292 file(s) [attempted 5292/8520 = 62%, 85 KB/s], Decompressed: 5258
Downloaded: 5337 file(s) [attempted 5337/8520 = 62%, 718 KB/s], Decompressed: 5296
Downloaded: 5381 file(s) [attempted 5381/8520 = 63%, 750 KB/s], Decompressed: 5340
Downloaded: 5419 file(s) [attempted 5419/8520 = 63%, 250 KB/s], Decompressed: 5378
Downloaded: 5457 file(s) [attempted 5457/8520 = 64%, 222 KB/s], Decompressed: 5406
Downloaded: 5494 file(s) [attempted 5494/8520 = 64%, 261 KB/s], Decompressed: 5440
Downloaded: 5542 file(s) [attempted 5542/8520 = 65%, 184 KB/s], Decompressed: 5488
Downloaded: 5587 file(s) [attempted 5587/8520 = 65%, 216 KB/s], Decompressed: 5532
Downloaded: 5621 file(s) [attempted 5621/8520 = 65%, 342 KB/s], Decompressed: 5566
Downloaded: 5662 file(s) [attempted 5662/8520 = 66%, 60 KB/s], Decompressed: 5597
Downloaded: 5700 file(s) [attempted 5700/8520 = 66%, 997 KB/s], Decompressed: 5642
Downloaded: 5744 file(s) [attempted 5744/8520 = 67%, 549 KB/s], Decompressed: 5683
Downloaded: 5785 file(s) [attempted 5785/8520 = 67%, 347 KB/s], Decompressed: 5717
Downloaded: 5830 file(s) [attempted 5830/8520 = 68%, 41 KB/s], Decompressed: 5761
Downloaded: 5867 file(s) [attempted 5867/8520 = 68%, 754 KB/s], Decompressed: 5806
Downloaded: 5905 file(s) [attempted 5905/8520 = 69%, 164 KB/s], Decompressed: 5847
Downloaded: 5939 file(s) [attempted 5939/8520 = 69%, 673 KB/s], Decompressed: 5888
Downloaded: 5984 file(s) [attempted 5984/8520 = 70%, 93 KB/s], Decompressed: 5932
Downloaded: 6025 file(s) [attempted 6025/8520 = 70%, 150 KB/s], Decompressed: 5974
Downloaded: 6066 file(s) [attempted 6066/8520 = 71%, 145 KB/s], Decompressed: 6004
Downloaded: 6097 file(s) [attempted 6097/8520 = 71%, 222 KB/s], Decompressed: 6035
Downloaded: 6138 file(s) [attempted 6138/8520 = 72%, 73 KB/s], Decompressed: 6076
Downloaded: 6182 file(s) [attempted 6182/8520 = 72%, 724 KB/s], Decompressed: 6124
Downloaded: 6227 file(s) [attempted 6227/8520 = 73%, 189 KB/s], Decompressed: 6165
Downloaded: 6268 file(s) [attempted 6268/8520 = 73%, 151 KB/s], Decompressed: 6165
Downloaded: 6302 file(s) [attempted 6302/8520 = 73%, 53 KB/s], Decompressed: 6227
Downloaded: 6343 file(s) [attempted 6343/8520 = 74%, 334 KB/s], Decompressed: 6278
Downloaded: 6384 file(s) [attempted 6384/8520 = 74%, 262 KB/s], Decompressed: 6329
Downloaded: 6425 file(s) [attempted 6425/8520 = 75%, 119 KB/s], Decompressed: 6329
Downloaded: 6466 file(s) [attempted 6466/8520 = 75%, 146 KB/s], Decompressed: 6381
Downloaded: 6507 file(s) [attempted 6507/8520 = 76%, 137 KB/s], Decompressed: 6436
Downloaded: 6548 file(s) [attempted 6548/8520 = 76%, 101 KB/s], Decompressed: 6487
Downloaded: 6590 file(s) [attempted 6590/8520 = 77%, 1451 KB/s], Decompressed: 6531
Downloaded: 6631 file(s) [attempted 6631/8520 = 77%, 416 KB/s], Decompressed: 6576
Downloaded: 6668 file(s) [attempted 6668/8520 = 78%, 398 KB/s], Decompressed: 6620
Downloaded: 6709 file(s) [attempted 6709/8520 = 78%, 333 KB/s], Decompressed: 6658
Downloaded: 6750 file(s) [attempted 6750/8520 = 79%, 484 KB/s], Decompressed: 6713
Downloaded: 6788 file(s) [attempted 6788/8520 = 79%, 98 KB/s], Decompressed: 6733
Downloaded: 6833 file(s) [attempted 6833/8520 = 80%, 523 KB/s], Decompressed: 6768
Downloaded: 6873 file(s) [attempted 6873/8520 = 80%, 972 KB/s], Decompressed: 6798
Downloaded: 6911 file(s) [attempted 6911/8520 = 81%, 446 KB/s], Decompressed: 6874
Downloaded: 6949 file(s) [attempted 6949/8520 = 81%, 108 KB/s], Decompressed: 6911
Downloaded: 6987 file(s) [attempted 6987/8520 = 82%, 435 KB/s], Decompressed: 6939
Downloaded: 7031 file(s) [attempted 7031/8520 = 82%, 327 KB/s], Decompressed: 7000
Downloaded: 7072 file(s) [attempted 7072/8520 = 83%, 1163 KB/s], Decompressed: 7031
Downloaded: 7103 file(s) [attempted 7103/8520 = 83%, 234 KB/s], Decompressed: 7052
Downloaded: 7144 file(s) [attempted 7144/8520 = 83%, 134 KB/s], Decompressed: 7106
Downloaded: 7185 file(s) [attempted 7185/8520 = 84%, 496 KB/s], Decompressed: 7137
Downloaded: 7233 file(s) [attempted 7233/8520 = 84%, 1451 KB/s], Decompressed: 7178
Downloaded: 7267 file(s) [attempted 7267/8520 = 85%, 779 KB/s], Decompressed: 7202
Downloaded: 7305 file(s) [attempted 7305/8520 = 85%, 113 KB/s], Decompressed: 7274
Downloaded: 7346 file(s) [attempted 7346/8520 = 86%, 396 KB/s], Decompressed: 7301
Downloaded: 7390 file(s) [attempted 7390/8520 = 86%, 418 KB/s], Decompressed: 7339
Downloaded: 7435 file(s) [attempted 7435/8520 = 87%, 554 KB/s], Decompressed: 7380
Downloaded: 7469 file(s) [attempted 7469/8520 = 87%, 346 KB/s], Decompressed: 7414
Downloaded: 7510 file(s) [attempted 7510/8520 = 88%, 827 KB/s], Decompressed: 7445
Downloaded: 7548 file(s) [attempted 7548/8520 = 88%, 27 KB/s], Decompressed: 7486
Downloaded: 7589 file(s) [attempted 7589/8520 = 89%, 137 KB/s], Decompressed: 7520
Downloaded: 7630 file(s) [attempted 7630/8520 = 89%, 120 KB/s], Decompressed: 7551
Downloaded: 7668 file(s) [attempted 7668/8520 = 90%, 34 KB/s], Decompressed: 7596
Downloaded: 7705 file(s) [attempted 7705/8520 = 90%, 42 KB/s], Decompressed: 7640
Downloaded: 7746 file(s) [attempted 7746/8520 = 90%, 22 KB/s], Decompressed: 7681
Downloaded: 7787 file(s) [attempted 7787/8520 = 91%, 180 KB/s], Decompressed: 7729
Downloaded: 7832 file(s) [attempted 7832/8520 = 91%, 192 KB/s], Decompressed: 7777
Downloaded: 7873 file(s) [attempted 7873/8520 = 92%, 141 KB/s], Decompressed: 7777
Downloaded: 7914 file(s) [attempted 7914/8520 = 92%, 113 KB/s], Decompressed: 7832
Downloaded: 7958 file(s) [attempted 7958/8520 = 93%, 187 KB/s], Decompressed: 7832
Downloaded: 7993 file(s) [attempted 7993/8520 = 93%, 111 KB/s], Decompressed: 7887
Downloaded: 8034 file(s) [attempted 8034/8520 = 94%, 822 KB/s], Decompressed: 7962
Downloaded: 8078 file(s) [attempted 8078/8520 = 94%, 681 KB/s], Decompressed: 7962
Downloaded: 8116 file(s) [attempted 8116/8520 = 95%, 342 KB/s], Decompressed: 8034
Downloaded: 8157 file(s) [attempted 8157/8520 = 95%, 153 KB/s], Decompressed: 8034
Downloaded: 8198 file(s) [attempted 8198/8520 = 96%, 72 KB/s], Decompressed: 8116
Downloaded: 8236 file(s) [attempted 8236/8520 = 96%, 53 KB/s], Decompressed: 8116
Downloaded: 8280 file(s) [attempted 8280/8520 = 97%, 706 KB/s], Decompressed: 8198
Downloaded: 8314 file(s) [attempted 8314/8520 = 97%, 49 KB/s], Decompressed: 8198
Downloaded: 8359 file(s) [attempted 8359/8520 = 98%, 592 KB/s], Decompressed: 8280
Downloaded: 8403 file(s) [attempted 8403/8520 = 98%, 411 KB/s], Decompressed: 8280
Downloaded: 8448 file(s) [attempted 8448/8520 = 99%, 169 KB/s], Decompressed: 8355
Downloaded: 8496 file(s) [attempted 8496/8520 = 99%, 36 KB/s], Decompressed: 8355
Downloaded: 8520 file(s) [attempted 8520/8520 = 100%, 258 KB/s], Decompressed: 8444
Downloaded: 8520 file(s) [attempted 8520/8520 = 100%, 258 KB/s], Decompressed: 8444

lean_checker exit 0 duration 5m 5s · created 6/10/2026, 2:36:12 PM

lake build

✔ [2952/2969] Built FLT.Assumptions.Mazur (4.7s)
✔ [3085/3181] Built FLT.Mathlib.Algebra.Algebra.Tower (4.4s)
✔ [3176/3278] Built FLT.Assumptions.Odlyzko (4.5s)
✔ [3177/3278] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (4.5s)
✔ [3300/3319] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (1.9s)
✔ [3301/3319] Built FLT.Mathlib.Algebra.FixedPoints.Basic (3.1s)
✔ [3306/3319] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (2.3s)
✔ [3307/3319] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (4.5s)
✔ [3308/3319] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (6.3s)
✔ [3310/3320] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (2.1s)
✔ [3311/3320] Built FLT.Mathlib.MeasureTheory.Group.Action (2.0s)
✔ [3312/3320] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (5.2s)
✔ [3314/3333] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (2.3s)
✔ [3319/3340] Built FLT.Mathlib.MeasureTheory.Group.Measure (1.9s)
✔ [3323/3340] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.8s)
✔ [3324/3340] Built FLT.Hacks.RightActionInstances (4.8s)
✔ [3327/3341] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.8s)
✔ [3328/3341] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (2.5s)
✔ [3329/3345] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (7.2s)
✔ [3333/3345] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (2.1s)
✔ [3336/3351] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (2.8s)
✔ [3340/3362] Built FLT.Mathlib.LinearAlgebra.Countable (2.1s)
✔ [3343/3362] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (1.6s)
✔ [3352/3378] Built FLT.AutomorphicForm.QuaternionAlgebra.Defs (5.4s)
✔ [3359/3378] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (3.0s)
✔ [3363/3380] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (7.3s)
✔ [3366/3380] Built FLT.Mathlib.RingTheory.Localization.BaseChange (3.5s)
✔ [3369/3380] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (3.4s)
✔ [3371/3382] Built FLT.DedekindDomain.AdicValuation (13s)
✔ [3373/3396] Built FLT.HaarMeasure.HaarChar.AddEquiv (9.6s)
✔ [3375/3396] Built FLT.DedekindDomain.IntegralClosure (7.4s)
✔ [3378/3396] Built FLT.NumberField.Completion.Finite (3.3s)
✔ [3379/3396] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (2.2s)
✔ [3380/3396] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (1.8s)
✔ [3381/3396] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (14s)
✔ [3382/3406] Built FLT.HaarMeasure.HaarChar.Ring (4.6s)
✔ [3386/3406] Built FLT.Mathlib.Algebra.Algebra.Hom (2.9s)
✔ [3387/3406] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (2.3s)
✔ [3388/3410] Built FLT.NumberField.HeightOneSpectrum (2.2s)
✔ [3391/3410] Built FLT.Mathlib.Topology.Algebra.MulAction (1.6s)
✔ [3392/3410] Built FLT.Mathlib.Algebra.IsDirectLimit (2.8s)
✔ [3393/3410] Built FLT.Mathlib.LinearAlgebra.Pi (1.9s)
✔ [3394/3410] Built FLT.Mathlib.Topology.Algebra.UniformRing (1.0s)
✔ [3396/3410] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (2.2s)
✔ [3399/3410] Built FLT.Mathlib.Algebra.Algebra.Pi (1.9s)
✔ [3400/3410] Built FLT.Mathlib.Algebra.Algebra.Bilinear (2.8s)
✔ [3401/3425] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (3.9s)
✔ [3403/3426] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (3.9s)
✔ [3406/3426] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (2.1s)
✔ [3407/3426] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (2.3s)
✔ [3408/3426] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (2.4s)
✔ [3409/3426] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (2.1s)
✔ [3410/3426] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (2.1s)
✔ [3411/3426] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (9.7s)
✔ [3412/3429] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (2.2s)
✔ [3414/3429] Built FLT.NumberField.InfinitePlace.Extension (3.8s)
✔ [3415/3429] Built FLT.Mathlib.Topology.Constructions (1.9s)
✔ [3417/3436] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (3.1s)
✔ [3420/3438] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (3.1s)
✔ [3422/3438] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (2.4s)
✔ [3423/3438] Built FLT.Mathlib.Data.Real.Archimedean (2.7s)
✔ [3424/3438] Built FLT.NumberField.Padics.RestrictedProduct (5.1s)
✔ [3426/3438] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (3.3s)
✔ [3428/3441] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (3.7s)
✔ [3429/3441] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (12s)
✔ [3430/3441] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (2.5s)
✔ [3432/3444] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (2.4s)
✔ [3439/3457] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (8.5s)
✔ [3442/3466] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (3.7s)
✔ [3444/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (2.1s)
✔ [3445/3469] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (3.2s)
✔ [3446/3469] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (6.8s)
✔ [3448/3469] Built FLT.HaarMeasure.MeasurableSpacePadics (2.7s)
✔ [3450/3469] Built FLT.HaarMeasure.HaarChar.RealComplex (3.5s)
✔ [3452/3469] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.5s)
✔ [3454/3469] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (2.9s)
✔ [3455/3469] Built FLT.DedekindDomain.Completion.BaseChange (44s)
✔ [3456/3469] Built FLT.HaarMeasure.HaarChar.Padic (3.7s)
✔ [3458/3469] Built FLT.Mathlib.Algebra.Central.TensorProduct (3.1s)
✔ [3459/3471] Built FLT.Mathlib.GroupTheory.DoubleCoset (1.7s)
✔ [3460/3474] Built FLT.NumberField.Completion.Infinite (27s)
✔ [3463/3475] Built FLT.Mathlib.LinearAlgebra.Determinant (5.6s)
✔ [3465/3488] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (9.7s)
✔ [3474/3488] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (4.8s)
✔ [3476/3500] Built FLT.Mathlib.Topology.Polish (2.6s)
✔ [3478/3505] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (3.1s)
✔ [3480/3505] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (1.0s)
✔ [3481/3505] Built FLT.Mathlib.Topology.Instances.Matrix (1.8s)
✔ [3482/3505] Built FLT.NumberField.InfiniteAdeleRing (17s)
✔ [3484/3505] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (1.0s)
✔ [3487/3505] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (4.7s)
✔ [3488/3505] Built FLT.Deformations.Algebra.InverseLimit.Basic (7.8s)
✔ [3489/3505] Built FLT.Mathlib.MeasureTheory.Haar.Extension (3.7s)
✔ [3491/3511] Built FLT.Deformations.Algebra.InverseLimit.Topology (6.4s)
✔ [3492/3512] Built FLT.Data.QHat (10s)
✔ [3493/3514] Built FLT.Data.Hurwitz (7.7s)
✔ [3496/3514] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (4.0s)
✔ [3499/3517] Built FLT.Data.HurwitzRatHat (3.5s)
✔ [3502/3517] Built FLT.Patching.Utils.Lemmas (7.7s)
✔ [3516/3535] Built FLT.QuaternionAlgebra.NumberField (14s)
✔ [3517/3535] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.6s)
✔ [3519/3535] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (47s)
✔ [3521/3536] Built FLT.Deformations.Lemmas (5.8s)
✔ [3523/3536] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (1.8s)
✔ [3524/3559] Built FLT.Deformations.IsResidueAlgebra (2.8s)
✔ [3571/3589] Built FLT.Patching.Utils.AdicTopology (4.7s)
✔ [3575/3594] Built FLT.Deformations.IsProartinian (3.2s)
✔ [3579/3594] Built FLT.Deformations.RepresentationTheory.IntegralClosure (3.6s)
✔ [3580/3597] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (9.1s)
✔ [3582/3606] Built FLT.Deformations.RepresentationTheory.Frobenius (3.1s)
✔ [3596/3619] Built FLT.Deformations.Categories (3.0s)
✔ [3608/3622] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (12s)
✔ [3625/3654] Built FLT.Deformations.RepresentationTheory.Etale (11s)
✔ [3801/3828] Built FLT.Mathlib.RepresentationTheory.Basic (2.5s)
✔ [3803/3828] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (2.1s)
✔ [3806/3834] Built FLT.GaloisRepresentation.Cyclotomic (2.3s)
✔ [3808/3837] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (15s)
✔ [3811/3838] Built FLT.Deformations.RepresentationTheory.Irreducible (1.8s)
✔ [3933/3970] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (2.1s)
✔ [3934/3970] Built FLT.FreyCurve.FreyPackage (4.1s)
✔ [3937/3970] Built FLT.Mathlib.GroupTheory.Index (1.3s)
✔ [3938/3970] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.0s)
✔ [3939/3970] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.6s)
✔ [3940/3970] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.7s)
✔ [3942/3970] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.9s)
✔ [3944/3971] Built FLT.Mathlib.Topology.Algebra.Monoid (1.6s)
✔ [3955/3984] Built FLT.Mathlib.Topology.Algebra.Order.Field (3.3s)
✔ [3958/3987] Built FLT.Patching.Utils.TopologicallyFG (2.2s)
✔ [3960/3989] Built FLT.Deformations.RepresentationTheory.GaloisRep (15s)
✔ [3962/3989] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (101s)
✔ [3963/3989] Built FLT.NumberField.DiscriminantBounds (4.4s)
✔ [3964/3989] Built FLT.GlobalLanglandsConjectures.GLnDefs (10s)
✔ [3965/3989] Built FLT.GaloisRepresentation.Automorphic (3.0s)
✔ [3966/3989] Built FLT.Patching.Utils.StructureFiniteness (5.2s)
✔ [3967/3989] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.8s)
✔ [3969/3989] Built FLT.EllipticCurve.Torsion (3.1s)
✔ [3970/3989] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (2.6s)
✔ [3971/3989] Built FLT.GlobalLanglandsConjectures.GLzero (2.9s)
✔ [3972/3989] Built FLT.Deformations.LiftFunctor (5.2s)
✔ [3973/3989] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (2.8s)
✔ [3974/3989] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (2.5s)
✔ [3976/3992] Built FLT.GaloisRepresentation.HardlyRamified.Lift (2.4s)
✔ [3977/3992] Built FLT.GaloisRepresentation.HardlyRamified.Frey (2.7s)
✔ [3978/3992] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.9s)
✔ [3980/3996] Built FLT.Patching.Ultraproduct (11s)
✔ [3982/3996] Built FLT.Deformations.Representable (3.2s)
✔ [3983/4006] Built FLT.FreyCurve.Contradiction (2.6s)
✔ [3998/4013] Built FLT.Patching.VanishingFilter (4.2s)
✔ [4000/4013] Built FLT.Patching.Utils.CompactHausdorffRings (3.1s)
✔ [4001/4013] Built FLT.Patching.Utils.Depth (5.4s)
✔ [4002/4013] Built FLT.Patching.Algebra (14s)
✔ [4003/4013] Built FLT.Patching.Module (17s)
✔ [4004/4013] Built FLT.NumberField.AdeleRing (31s)
✔ [4005/4013] Built FLT.HaarMeasure.HaarChar.AdeleRing (7.2s)
✔ [4006/4013] Built FLT.Patching.Over (13s)
✔ [4007/4013] Built FLT.Patching.System (10s)
✔ [4008/4013] Built FLT.Patching.REqualsT (4.2s)
✔ [4009/4013] Built FLT.DivisionAlgebra.Finiteness (41s)
✔ [4010/4013] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (2.4s)
✔ [4011/4013] Built FLT (2.1s)
✔ [4012/4013] Built FermatsLastTheorem (15s)
Build completed successfully (4013 jobs).

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

blueprint_build exit 1 duration 1s · created 6/10/2026, 2:36:12 PM

lake build :blueprint

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

semantic_extract exit 0 duration 7m 5s · created 6/10/2026, 2:36:12 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)

warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache be210bb031eeda2d3730e9c87b962db00dbf21ab8ade771edbb8c30e86bc8762
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 35s · created 6/10/2026, 2:36:12 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)

warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 2ee8f3dd04d3feda4e75d1d86be5f8ec2fc3f57f9e7d911638edc2211c1c3068
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 3m 54s · created 6/10/2026, 2:36:12 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)

warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 064de9be88f32610a045e9c1f486b756883735df8adfeee88ed8571acd552581
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 143 duration 5m 40s · created 6/10/2026, 2:36:12 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)

warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: stored compiled static runner cache 358e05531b681902ebd502946a9deb0c496d4ef4133c7f0b7a3520023503c093
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes