Verification run

Run 5

ImperialCollegeLondon/FLT branch main triggered via manual

succeeded commit manual toolchain lean-v4-31-0-rc1 prover lean took 32m 7s · finished 6w ago

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/2/2026, 7:00:14 PM

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

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

lake_cache exit 0 duration 1m 26s · created 6/2/2026, 7:00:14 PM

lake exe cache get

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

info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git
info: checkdecls: checking out revision '3d425859e73fcfbef85b9638c2a91708ef4a22d4'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'd568c8c09630de097a046763c17b9ea99f95f950'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'd575be693add4fe9cb996968968ce42ce75c5ccd'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'c5d5b8fe6e5158def25cd28eb94e4141ad97c843'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '6db47de43aa7f516708053ae2fdadd29dd9baaaa'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '85bb7e7637e84a7d9803be7d954579fdae42c64b'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'fafca80479ff95e041d84373dda7122adf1295f2'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '8d33324ee877e9735d2829bc6f1f439e60cf98b1'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '708b057842c4cd0845fba132bd94b08493f6fc42'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '48bdcff4c5fa27e09028f9f330e59baa0d4640cf'
✔ [4/24] Built Batteries.Data.String.Basic (338ms)
✔ [5/24] Built Cache.Lean (399ms)
✔ [6/24] Built Batteries.Data.Array.Match (633ms)
✔ [7/24] Built Cache.Init (263ms)
✔ [8/24] Built Batteries.Data.String.Basic:c.o (450ms)
✔ [9/24] Built Cache.Lean:c.o (154ms)
✔ [10/24] Built Batteries.Tactic.OpenPrivate (895ms)
✔ [11/24] Built Batteries.Data.Array.Match:c.o (194ms)
✔ [12/24] Built Cache.Init:c.o (68ms)
✔ [13/24] Built Batteries.Data.String.Matcher (300ms)
✔ [14/24] Built Batteries.Data.String.Matcher:c.o (164ms)
✔ [15/24] Built Batteries.Tactic.OpenPrivate:c.o (947ms)
✔ [16/24] Built Cache.IO (1.5s)
✔ [17/24] Built Cache.Hashing (838ms)
✔ [18/24] Built Cache.IO:c.o (1.2s)
✔ [19/24] Built Cache.Hashing:c.o (359ms)
✔ [20/24] Built Cache.Requests (1.8s)
✔ [21/24] Built Cache.Main (915ms)
✔ [22/24] Built Cache.Main:c.o (519ms)
✔ [23/24] Built Cache.Requests:c.o (1.8s)
✔ [24/24] Built cache:exe (2.2s)

Downloaded: 1 file(s) [attempted 1/8477 = 0%, 11 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8477 = 0%, 10 KB/s], Decompressed: 11
Downloaded: 37 file(s) [attempted 37/8477 = 0%, 22 KB/s], Decompressed: 21
Downloaded: 60 file(s) [attempted 60/8477 = 0%, 231 KB/s], Decompressed: 58
Downloaded: 88 file(s) [attempted 88/8477 = 1%, 486 KB/s], Decompressed: 76
Downloaded: 121 file(s) [attempted 121/8477 = 1%, 148 KB/s], Decompressed: 103
Downloaded: 162 file(s) [attempted 162/8477 = 1%, 87 KB/s], Decompressed: 141
Downloaded: 206 file(s) [attempted 206/8477 = 2%, 324 KB/s], Decompressed: 172
Downloaded: 247 file(s) [attempted 247/8477 = 2%, 530 KB/s], Decompressed: 192
Downloaded: 288 file(s) [attempted 288/8477 = 3%, 102 KB/s], Decompressed: 227
Downloaded: 329 file(s) [attempted 329/8477 = 3%, 43 KB/s], Decompressed: 254
Downloaded: 367 file(s) [attempted 367/8477 = 4%, 1266 KB/s], Decompressed: 333
Downloaded: 405 file(s) [attempted 405/8477 = 4%, 604 KB/s], Decompressed: 364
Downloaded: 446 file(s) [attempted 446/8477 = 5%, 249 KB/s], Decompressed: 395
Downloaded: 490 file(s) [attempted 490/8477 = 5%, 282 KB/s], Decompressed: 432
Downloaded: 535 file(s) [attempted 535/8477 = 6%, 564 KB/s], Decompressed: 494
Downloaded: 580 file(s) [attempted 580/8477 = 6%, 293 KB/s], Decompressed: 532
Downloaded: 617 file(s) [attempted 617/8477 = 7%, 566 KB/s], Decompressed: 532
Downloaded: 655 file(s) [attempted 655/8477 = 7%, 395 KB/s], Decompressed: 576
Downloaded: 696 file(s) [attempted 696/8477 = 8%, 915 KB/s], Decompressed: 624
Downloaded: 737 file(s) [attempted 737/8477 = 8%, 777 KB/s], Decompressed: 665
Downloaded: 782 file(s) [attempted 782/8477 = 9%, 173 KB/s], Decompressed: 713
Downloaded: 826 file(s) [attempted 826/8477 = 9%, 124 KB/s], Decompressed: 764
Downloaded: 867 file(s) [attempted 867/8477 = 10%, 276 KB/s], Decompressed: 764
Downloaded: 912 file(s) [attempted 912/8477 = 10%, 651 KB/s], Decompressed: 819
Downloaded: 953 file(s) [attempted 953/8477 = 11%, 435 KB/s], Decompressed: 874
Downloaded: 994 file(s) [attempted 994/8477 = 11%, 879 KB/s], Decompressed: 928
Downloaded: 1032 file(s) [attempted 1032/8477 = 12%, 296 KB/s], Decompressed: 970
Downloaded: 1076 file(s) [attempted 1076/8477 = 12%, 82 KB/s], Decompressed: 1045
Downloaded: 1117 file(s) [attempted 1117/8477 = 13%, 405 KB/s], Decompressed: 1073
Downloaded: 1162 file(s) [attempted 1162/8477 = 13%, 529 KB/s], Decompressed: 1127
Downloaded: 1203 file(s) [attempted 1203/8477 = 14%, 35 KB/s], Decompressed: 1165
Downloaded: 1240 file(s) [attempted 1240/8477 = 14%, 126 KB/s], Decompressed: 1223
Downloaded: 1278 file(s) [attempted 1278/8477 = 15%, 322 KB/s], Decompressed: 1254
Downloaded: 1316 file(s) [attempted 1316/8477 = 15%, 46 KB/s], Decompressed: 1299
Downloaded: 1364 file(s) [attempted 1364/8477 = 16%, 66 KB/s], Decompressed: 1336
Downloaded: 1411 file(s) [attempted 1411/8477 = 16%, 732 KB/s], Decompressed: 1381
Downloaded: 1459 file(s) [attempted 1459/8477 = 17%, 326 KB/s], Decompressed: 1432
Downloaded: 1507 file(s) [attempted 1507/8477 = 17%, 40 KB/s], Decompressed: 1480
Downloaded: 1545 file(s) [attempted 1545/8477 = 18%, 431 KB/s], Decompressed: 1507
Downloaded: 1586 file(s) [attempted 1586/8477 = 18%, 417 KB/s], Decompressed: 1562
Downloaded: 1620 file(s) [attempted 1620/8477 = 19%, 187 KB/s], Decompressed: 1603
Downloaded: 1661 file(s) [attempted 1661/8477 = 19%, 128 KB/s], Decompressed: 1637
Downloaded: 1706 file(s) [attempted 1706/8477 = 20%, 205 KB/s], Decompressed: 1672
Downloaded: 1750 file(s) [attempted 1750/8477 = 20%, 218 KB/s], Decompressed: 1716
Downloaded: 1791 file(s) [attempted 1791/8477 = 21%, 265 KB/s], Decompressed: 1743
Downloaded: 1829 file(s) [attempted 1829/8477 = 21%, 457 KB/s], Decompressed: 1795
Downloaded: 1870 file(s) [attempted 1870/8477 = 22%, 136 KB/s], Decompressed: 1850
Downloaded: 1915 file(s) [attempted 1915/8477 = 22%, 120 KB/s], Decompressed: 1870
Downloaded: 1952 file(s) [attempted 1952/8477 = 23%, 56 KB/s], Decompressed: 1904
Downloaded: 1997 file(s) [attempted 1997/8477 = 23%, 35 KB/s], Decompressed: 1935
Downloaded: 2031 file(s) [attempted 2031/8477 = 23%, 960 KB/s], Decompressed: 1969
Downloaded: 2072 file(s) [attempted 2072/8477 = 24%, 349 KB/s], Decompressed: 1969
Downloaded: 2106 file(s) [attempted 2106/8477 = 24%, 56 KB/s], Decompressed: 2028
Downloaded: 2151 file(s) [attempted 2151/8477 = 25%, 115 KB/s], Decompressed: 2089
Downloaded: 2188 file(s) [attempted 2188/8477 = 25%, 35 KB/s], Decompressed: 2089
Downloaded: 2233 file(s) [attempted 2233/8477 = 26%, 302 KB/s], Decompressed: 2147
Downloaded: 2271 file(s) [attempted 2271/8477 = 26%, 510 KB/s], Decompressed: 2205
Downloaded: 2312 file(s) [attempted 2312/8477 = 27%, 140 KB/s], Decompressed: 2253
Downloaded: 2349 file(s) [attempted 2349/8477 = 27%, 244 KB/s], Decompressed: 2253
Downloaded: 2387 file(s) [attempted 2387/8477 = 28%, 272 KB/s], Decompressed: 2301
Downloaded: 2424 file(s) [attempted 2424/8477 = 28%, 1285 KB/s], Decompressed: 2356
Downloaded: 2468 file(s) [attempted 2468/8477 = 29%, 24 KB/s], Decompressed: 2404
Downloaded: 2507 file(s) [attempted 2507/8477 = 29%, 718 KB/s], Decompressed: 2404
Downloaded: 2548 file(s) [attempted 2548/8477 = 30%, 346 KB/s], Decompressed: 2462
Downloaded: 2585 file(s) [attempted 2585/8477 = 30%, 110 KB/s], Decompressed: 2520
Downloaded: 2630 file(s) [attempted 2630/8477 = 31%, 244 KB/s], Decompressed: 2520
Downloaded: 2671 file(s) [attempted 2671/8477 = 31%, 256 KB/s], Decompressed: 2582
Downloaded: 2715 file(s) [attempted 2715/8477 = 32%, 351 KB/s], Decompressed: 2640
Downloaded: 2756 file(s) [attempted 2756/8477 = 32%, 224 KB/s], Decompressed: 2640
Downloaded: 2798 file(s) [attempted 2798/8477 = 33%, 1883 KB/s], Decompressed: 2702
Downloaded: 2835 file(s) [attempted 2835/8477 = 33%, 988 KB/s], Decompressed: 2702
Downloaded: 2880 file(s) [attempted 2880/8477 = 33%, 60 KB/s], Decompressed: 2777
Downloaded: 2921 file(s) [attempted 2921/8477 = 34%, 51 KB/s], Decompressed: 2777
Downloaded: 2965 file(s) [attempted 2965/8477 = 34%, 237 KB/s], Decompressed: 2777
Downloaded: 3006 file(s) [attempted 3006/8477 = 35%, 2305 KB/s], Decompressed: 2876
Downloaded: 3047 file(s) [attempted 3047/8477 = 35%, 287 KB/s], Decompressed: 2876
Downloaded: 3082 file(s) [attempted 3082/8477 = 36%, 248 KB/s], Decompressed: 2972
Downloaded: 3129 file(s) [attempted 3129/8477 = 36%, 346 KB/s], Decompressed: 2972
Downloaded: 3174 file(s) [attempted 3174/8477 = 37%, 68 KB/s], Decompressed: 3071
Downloaded: 3218 file(s) [attempted 3218/8477 = 37%, 126 KB/s], Decompressed: 3071
Downloaded: 3256 file(s) [attempted 3256/8477 = 38%, 237 KB/s], Decompressed: 3071
Downloaded: 3301 file(s) [attempted 3301/8477 = 38%, 1075 KB/s], Decompressed: 3174
Downloaded: 3338 file(s) [attempted 3338/8477 = 39%, 112 KB/s], Decompressed: 3174
Downloaded: 3376 file(s) [attempted 3376/8477 = 39%, 316 KB/s], Decompressed: 3270
Downloaded: 3417 file(s) [attempted 3417/8477 = 40%, 757 KB/s], Decompressed: 3270
Downloaded: 3461 file(s) [attempted 3461/8477 = 40%, 50 KB/s], Decompressed: 3366
Downloaded: 3509 file(s) [attempted 3509/8477 = 41%, 288 KB/s], Decompressed: 3366
Downloaded: 3554 file(s) [attempted 3554/8477 = 41%, 24 KB/s], Decompressed: 3366
Downloaded: 3592 file(s) [attempted 3592/8477 = 42%, 620 KB/s], Decompressed: 3461
Downloaded: 3633 file(s) [attempted 3633/8477 = 42%, 426 KB/s], Decompressed: 3461
Downloaded: 3670 file(s) [attempted 3670/8477 = 43%, 669 KB/s], Decompressed: 3561
Downloaded: 3704 file(s) [attempted 3704/8477 = 43%, 654 KB/s], Decompressed: 3561
Downloaded: 3752 file(s) [attempted 3752/8477 = 44%, 75 KB/s], Decompressed: 3561
Downloaded: 3797 file(s) [attempted 3797/8477 = 44%, 88 KB/s], Decompressed: 3657
Downloaded: 3838 file(s) [attempted 3838/8477 = 45%, 677 KB/s], Decompressed: 3657
Downloaded: 3876 file(s) [attempted 3876/8477 = 45%, 137 KB/s], Decompressed: 3756
Downloaded: 3913 file(s) [attempted 3913/8477 = 46%, 238 KB/s], Decompressed: 3756
Downloaded: 3961 file(s) [attempted 3961/8477 = 46%, 376 KB/s], Decompressed: 3852
Downloaded: 4002 file(s) [attempted 4002/8477 = 47%, 195 KB/s], Decompressed: 3852
Downloaded: 4040 file(s) [attempted 4040/8477 = 47%, 105 KB/s], Decompressed: 3930
Downloaded: 4084 file(s) [attempted 4084/8477 = 48%, 1613 KB/s], Decompressed: 4009
Downloaded: 4125 file(s) [attempted 4125/8477 = 48%, 325 KB/s], Decompressed: 4009
Downloaded: 4160 file(s) [attempted 4160/8477 = 49%, 387 KB/s], Decompressed: 4081
Downloaded: 4201 file(s) [attempted 4201/8477 = 49%, 342 KB/s], Decompressed: 4081
Downloaded: 4242 file(s) [attempted 4242/8477 = 50%, 45 KB/s], Decompressed: 4149
Downloaded: 4286 file(s) [attempted 4286/8477 = 50%, 232 KB/s], Decompressed: 4149
Downloaded: 4324 file(s) [attempted 4324/8477 = 51%, 470 KB/s], Decompressed: 4231
Downloaded: 4365 file(s) [attempted 4365/8477 = 51%, 362 KB/s], Decompressed: 4231
Downloaded: 4409 file(s) [attempted 4409/8477 = 52%, 220 KB/s], Decompressed: 4307
Downloaded: 4454 file(s) [attempted 4454/8477 = 52%, 807 KB/s], Decompressed: 4382
Downloaded: 4488 file(s) [attempted 4488/8477 = 52%, 81 KB/s], Decompressed: 4382
Downloaded: 4533 file(s) [attempted 4533/8477 = 53%, 180 KB/s], Decompressed: 4451
Downloaded: 4577 file(s) [attempted 4577/8477 = 53%, 34 KB/s], Decompressed: 4512
Downloaded: 4618 file(s) [attempted 4618/8477 = 54%, 49 KB/s], Decompressed: 4512
Downloaded: 4659 file(s) [attempted 4659/8477 = 54%, 608 KB/s], Decompressed: 4567
Downloaded: 4700 file(s) [attempted 4700/8477 = 55%, 339 KB/s], Decompressed: 4625
Downloaded: 4735 file(s) [attempted 4735/8477 = 55%, 426 KB/s], Decompressed: 4676
Downloaded: 4779 file(s) [attempted 4779/8477 = 56%, 449 KB/s], Decompressed: 4676
Downloaded: 4820 file(s) [attempted 4820/8477 = 56%, 220 KB/s], Decompressed: 4728
Downloaded: 4865 file(s) [attempted 4865/8477 = 57%, 327 KB/s], Decompressed: 4786
Downloaded: 4906 file(s) [attempted 4906/8477 = 57%, 556 KB/s], Decompressed: 4841
Downloaded: 4940 file(s) [attempted 4940/8477 = 58%, 590 KB/s], Decompressed: 4885
Downloaded: 4984 file(s) [attempted 4984/8477 = 58%, 427 KB/s], Decompressed: 4933
Downloaded: 5029 file(s) [attempted 5029/8477 = 59%, 202 KB/s], Decompressed: 4981
Downloaded: 5070 file(s) [attempted 5070/8477 = 59%, 87 KB/s], Decompressed: 5025
Downloaded: 5111 file(s) [attempted 5111/8477 = 60%, 365 KB/s], Decompressed: 5025
Downloaded: 5156 file(s) [attempted 5156/8477 = 60%, 178 KB/s], Decompressed: 5070
Downloaded: 5193 file(s) [attempted 5193/8477 = 61%, 305 KB/s], Decompressed: 5125
Downloaded: 5234 file(s) [attempted 5234/8477 = 61%, 77 KB/s], Decompressed: 5125
Downloaded: 5275 file(s) [attempted 5275/8477 = 62%, 770 KB/s], Decompressed: 5190
Downloaded: 5316 file(s) [attempted 5316/8477 = 62%, 394 KB/s], Decompressed: 5255
Downloaded: 5357 file(s) [attempted 5357/8477 = 63%, 322 KB/s], Decompressed: 5255
Downloaded: 5395 file(s) [attempted 5395/8477 = 63%, 792 KB/s], Decompressed: 5310
Downloaded: 5436 file(s) [attempted 5436/8477 = 64%, 641 KB/s], Decompressed: 5364
Downloaded: 5477 file(s) [attempted 5477/8477 = 64%, 968 KB/s], Decompressed: 5422
Downloaded: 5515 file(s) [attempted 5515/8477 = 65%, 1039 KB/s], Decompressed: 5422
Downloaded: 5559 file(s) [attempted 5559/8477 = 65%, 2278 KB/s], Decompressed: 5477
Downloaded: 5604 file(s) [attempted 5604/8477 = 66%, 258 KB/s], Decompressed: 5529
Downloaded: 5645 file(s) [attempted 5645/8477 = 66%, 143 KB/s], Decompressed: 5573
Downloaded: 5686 file(s) [attempted 5686/8477 = 67%, 191 KB/s], Decompressed: 5614
Downloaded: 5730 file(s) [attempted 5730/8477 = 67%, 401 KB/s], Decompressed: 5655
Downloaded: 5768 file(s) [attempted 5768/8477 = 68%, 200 KB/s], Decompressed: 5696
Downloaded: 5806 file(s) [attempted 5806/8477 = 68%, 181 KB/s], Decompressed: 5751
Downloaded: 5850 file(s) [attempted 5850/8477 = 69%, 689 KB/s], Decompressed: 5751
Downloaded: 5891 file(s) [attempted 5891/8477 = 69%, 167 KB/s], Decompressed: 5806
Downloaded: 5937 file(s) [attempted 5937/8477 = 70%, 607 KB/s], Decompressed: 5867
Downloaded: 5973 file(s) [attempted 5973/8477 = 70%, 141 KB/s], Decompressed: 5867
Downloaded: 6011 file(s) [attempted 6011/8477 = 70%, 608 KB/s], Decompressed: 5932
Downloaded: 6052 file(s) [attempted 6052/8477 = 71%, 374 KB/s], Decompressed: 5932
Downloaded: 6093 file(s) [attempted 6093/8477 = 71%, 291 KB/s], Decompressed: 5994
Downloaded: 6141 file(s) [attempted 6141/8477 = 72%, 129 KB/s], Decompressed: 6056
Downloaded: 6182 file(s) [attempted 6182/8477 = 72%, 55 KB/s], Decompressed: 6056
Downloaded: 6216 file(s) [attempted 6216/8477 = 73%, 74 KB/s], Decompressed: 6114
Downloaded: 6259 file(s) [attempted 6259/8477 = 73%, 70 KB/s], Decompressed: 6114
Downloaded: 6295 file(s) [attempted 6295/8477 = 74%, 355 KB/s], Decompressed: 6192
Downloaded: 6340 file(s) [attempted 6340/8477 = 74%, 397 KB/s], Decompressed: 6192
Downloaded: 6381 file(s) [attempted 6381/8477 = 75%, 274 KB/s], Decompressed: 6278
Downloaded: 6418 file(s) [attempted 6418/8477 = 75%, 108 KB/s], Decompressed: 6278
Downloaded: 6459 file(s) [attempted 6459/8477 = 76%, 96 KB/s], Decompressed: 6278
Downloaded: 6504 file(s) [attempted 6504/8477 = 76%, 296 KB/s], Decompressed: 6357
Downloaded: 6542 file(s) [attempted 6542/8477 = 77%, 109 KB/s], Decompressed: 6357
Downloaded: 6586 file(s) [attempted 6586/8477 = 77%, 90 KB/s], Decompressed: 6463
Downloaded: 6624 file(s) [attempted 6624/8477 = 78%, 171 KB/s], Decompressed: 6463
Downloaded: 6665 file(s) [attempted 6665/8477 = 78%, 51 KB/s], Decompressed: 6463
Downloaded: 6702 file(s) [attempted 6702/8477 = 79%, 330 KB/s], Decompressed: 6583
Downloaded: 6747 file(s) [attempted 6747/8477 = 79%, 1003 KB/s], Decompressed: 6583
Downloaded: 6788 file(s) [attempted 6788/8477 = 80%, 113 KB/s], Decompressed: 6583
Downloaded: 6829 file(s) [attempted 6829/8477 = 80%, 836 KB/s], Decompressed: 6696
Downloaded: 6863 file(s) [attempted 6863/8477 = 80%, 89 KB/s], Decompressed: 6696
Downloaded: 6908 file(s) [attempted 6908/8477 = 81%, 176 KB/s], Decompressed: 6696
Downloaded: 6952 file(s) [attempted 6952/8477 = 82%, 307 KB/s], Decompressed: 6809
Downloaded: 6993 file(s) [attempted 6993/8477 = 82%, 55 KB/s], Decompressed: 6809
Downloaded: 7034 file(s) [attempted 7034/8477 = 82%, 210 KB/s], Decompressed: 6809
Downloaded: 7069 file(s) [attempted 7069/8477 = 83%, 182 KB/s], Decompressed: 6935
Downloaded: 7113 file(s) [attempted 7113/8477 = 83%, 77 KB/s], Decompressed: 6935
Downloaded: 7154 file(s) [attempted 7154/8477 = 84%, 135 KB/s], Decompressed: 7048
Downloaded: 7199 file(s) [attempted 7199/8477 = 84%, 284 KB/s], Decompressed: 7048
Downloaded: 7243 file(s) [attempted 7243/8477 = 85%, 326 KB/s], Decompressed: 7048
Downloaded: 7277 file(s) [attempted 7277/8477 = 85%, 616 KB/s], Decompressed: 7154
Downloaded: 7318 file(s) [attempted 7318/8477 = 86%, 46 KB/s], Decompressed: 7154
Downloaded: 7363 file(s) [attempted 7363/8477 = 86%, 316 KB/s], Decompressed: 7154
Downloaded: 7401 file(s) [attempted 7401/8477 = 87%, 289 KB/s], Decompressed: 7274
Downloaded: 7442 file(s) [attempted 7442/8477 = 87%, 109 KB/s], Decompressed: 7274
Downloaded: 7483 file(s) [attempted 7483/8477 = 88%, 966 KB/s], Decompressed: 7274
Downloaded: 7520 file(s) [attempted 7520/8477 = 88%, 1419 KB/s], Decompressed: 7397
Downloaded: 7561 file(s) [attempted 7561/8477 = 89%, 2145 KB/s], Decompressed: 7397
Downloaded: 7602 file(s) [attempted 7602/8477 = 89%, 44 KB/s], Decompressed: 7397
Downloaded: 7644 file(s) [attempted 7644/8477 = 90%, 163 KB/s], Decompressed: 7510
Downloaded: 7681 file(s) [attempted 7681/8477 = 90%, 208 KB/s], Decompressed: 7510
Downloaded: 7719 file(s) [attempted 7719/8477 = 91%, 427 KB/s], Decompressed: 7510
Downloaded: 7760 file(s) [attempted 7760/8477 = 91%, 1593 KB/s], Decompressed: 7626
Downloaded: 7798 file(s) [attempted 7798/8477 = 91%, 149 KB/s], Decompressed: 7626
Downloaded: 7842 file(s) [attempted 7842/8477 = 92%, 685 KB/s], Decompressed: 7626
Downloaded: 7883 file(s) [attempted 7883/8477 = 92%, 692 KB/s], Decompressed: 7729
Downloaded: 7921 file(s) [attempted 7921/8477 = 93%, 80 KB/s], Decompressed: 7729
Downloaded: 7965 file(s) [attempted 7965/8477 = 93%, 183 KB/s], Decompressed: 7729
Downloaded: 8006 file(s) [attempted 8006/8477 = 94%, 195 KB/s], Decompressed: 7852
Downloaded: 8047 file(s) [attempted 8047/8477 = 94%, 449 KB/s], Decompressed: 7852
Downloaded: 8092 file(s) [attempted 8092/8477 = 95%, 103 KB/s], Decompressed: 7852
Downloaded: 8133 file(s) [attempted 8133/8477 = 95%, 449 KB/s], Decompressed: 7852
Downloaded: 8174 file(s) [attempted 8174/8477 = 96%, 119 KB/s], Decompressed: 7993
Downloaded: 8212 file(s) [attempted 8212/8477 = 96%, 52 KB/s], Decompressed: 7993
Downloaded: 8256 file(s) [attempted 8256/8477 = 97%, 56 KB/s], Decompressed: 7993
Downloaded: 8297 file(s) [attempted 8297/8477 = 97%, 86 KB/s], Decompressed: 7993
Downloaded: 8342 file(s) [attempted 8342/8477 = 98%, 293 KB/s], Decompressed: 8150
Downloaded: 8379 file(s) [attempted 8379/8477 = 98%, 935 KB/s], Decompressed: 8150
Downloaded: 8420 file(s) [attempted 8420/8477 = 99%, 243 KB/s], Decompressed: 8150
Downloaded: 8461 file(s) [attempted 8461/8477 = 99%, 473 KB/s], Decompressed: 8150
Downloaded: 8477 file(s) [attempted 8477/8477 = 100%, 473 KB/s], Decompressed: 8311

lean_checker exit 0 duration 4m 57s · created 6/2/2026, 7:00:14 PM

lake build

✔ [461/702] Built FLT.Assumptions.KnownIn1980s (298ms)
✔ [2946/2958] Built FLT.Assumptions.Mazur (4.0s)
✔ [3045/3107] Built FLT.Assumptions.Odlyzko (3.9s)
✔ [3105/3246] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (3.9s)
✔ [3106/3246] Built FLT.Mathlib.Algebra.Algebra.Tower (3.9s)
✔ [3295/3316] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (1.0s)
✔ [3296/3316] Built FLT.Mathlib.Algebra.FixedPoints.Basic (2.9s)
✔ [3297/3316] Built FLT.Mathlib.Topology.Algebra.Group.Units (1.5s)
✔ [3299/3316] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (4.1s)
✔ [3301/3316] Built FLT.Mathlib.Order.Filter.Cofinite (1.4s)
✔ [3302/3316] Built FLT.Mathlib.Topology.Bases (1.1s)
✔ [3303/3316] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (1.6s)
✔ [3304/3316] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (6.0s)
✔ [3306/3316] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (1.6s)
✔ [3307/3317] Built FLT.Mathlib.MeasureTheory.Group.Action (2.7s)
✔ [3309/3317] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (1.8s)
✔ [3310/3330] Built FLT.Mathlib.MeasureTheory.Group.Measure (1.8s)
✔ [3316/3337] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (4.9s)
✔ [3322/3337] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.5s)
✔ [3323/3337] Built FLT.Hacks.RightActionInstances (5.1s)
✔ [3325/3338] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.4s)
✔ [3326/3338] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (2.3s)
✔ [3327/3341] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (6.0s)
✔ [3330/3342] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (1.7s)
✔ [3332/3348] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (2.5s)
✔ [3339/3354] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (1.4s)
✔ [3343/3355] Built FLT.Mathlib.LinearAlgebra.Countable (1.8s)
✔ [3348/3375] Built FLT.AutomorphicForm.QuaternionAlgebra.Defs (5.7s)
✔ [3357/3375] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (6.6s)
✔ [3360/3375] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (3.8s)
✔ [3363/3375] Built FLT.Mathlib.RingTheory.Localization.BaseChange (2.0s)
✔ [3364/3377] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (3.2s)
✔ [3365/3379] Built FLT.HaarMeasure.HaarChar.AddEquiv (9.3s)
✔ [3369/3384] Built FLT.DedekindDomain.AdicValuation (14s)
✔ [3372/3393] Built FLT.NumberField.Completion.Finite (3.2s)
✔ [3375/3393] Built FLT.HaarMeasure.HaarChar.Ring (4.1s)
✔ [3376/3393] Built FLT.DedekindDomain.IntegralClosure (8.6s)
✔ [3377/3393] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (14s)
✔ [3379/3403] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (1.1s)
✔ [3381/3403] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (1.6s)
✔ [3383/3403] Built FLT.Mathlib.Algebra.Algebra.Hom (2.3s)
✔ [3384/3403] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (1.9s)
✔ [3385/3407] Built FLT.NumberField.HeightOneSpectrum (1.6s)
✔ [3388/3407] Built FLT.Mathlib.Topology.Algebra.MulAction (1.4s)
✔ [3389/3407] Built FLT.Mathlib.Algebra.IsDirectLimit (2.4s)
✔ [3390/3407] Built FLT.Mathlib.LinearAlgebra.Pi (1.6s)
✔ [3391/3407] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (2.0s)
✔ [3393/3407] Built FLT.Mathlib.Topology.Algebra.UniformRing (1.6s)
✔ [3395/3407] Built FLT.Mathlib.Algebra.Algebra.Pi (1.6s)
✔ [3397/3407] Built FLT.Mathlib.Algebra.Algebra.Bilinear (2.5s)
✔ [3398/3409] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (1.7s)
✔ [3400/3422] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (3.6s)
✔ [3401/3423] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (3.5s)
✔ [3404/3423] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (1.8s)
✔ [3405/3423] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (2.7s)
✔ [3406/3423] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (9.3s)
✔ [3407/3423] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (1.6s)
✔ [3408/3423] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (1.7s)
✔ [3409/3423] Built FLT.NumberField.InfinitePlace.Extension (3.5s)
✔ [3410/3426] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (2.0s)
✔ [3411/3426] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (10s)
✔ [3415/3435] Built FLT.Mathlib.Topology.Constructions (1.2s)
✔ [3417/3435] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (2.0s)
✔ [3419/3435] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (1.0s)
✔ [3420/3435] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (2.4s)
✔ [3421/3435] Built FLT.Mathlib.Data.Real.Archimedean (1.6s)
✔ [3423/3435] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (2.2s)
✔ [3425/3438] Built FLT.NumberField.Padics.RestrictedProduct (4.2s)
✔ [3426/3438] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (2.0s)
✔ [3428/3438] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (3.3s)
✔ [3430/3441] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (2.4s)
✔ [3436/3460] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (9.1s)
✔ [3439/3463] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (2.8s)
✔ [3441/3463] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (1.9s)
✔ [3442/3466] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (4.7s)
✔ [3443/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (2.2s)
✔ [3445/3466] Built FLT.HaarMeasure.MeasurableSpacePadics (2.5s)
✔ [3447/3466] Built FLT.HaarMeasure.HaarChar.RealComplex (3.0s)
✔ [3449/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.5s)
✔ [3451/3466] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (3.7s)
✔ [3452/3466] Built FLT.HaarMeasure.HaarChar.Padic (4.2s)
✔ [3453/3466] Built FLT.Mathlib.Algebra.Central.TensorProduct (4.0s)
✔ [3455/3468] Built FLT.Mathlib.GroupTheory.DoubleCoset (1.0s)
✔ [3456/3471] Built FLT.NumberField.Completion.Infinite (29s)
✔ [3459/3471] Built FLT.Mathlib.LinearAlgebra.Determinant (6.0s)
✔ [3461/3485] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (9.4s)
✔ [3469/3485] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (3.0s)
✔ [3470/3485] Built FLT.Mathlib.Topology.HomToDiscrete (1.0s)
✔ [3473/3497] Built FLT.Mathlib.Topology.Polish (1.6s)
✔ [3475/3497] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (1.6s)
✔ [3476/3497] Built FLT.DedekindDomain.Completion.BaseChange (54s)
✔ [3477/3497] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (2.7s)
✔ [3480/3497] Built FLT.Mathlib.Topology.Instances.Matrix (1.4s)
✔ [3482/3497] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (1.7s)
✔ [3483/3497] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (4.1s)
✔ [3484/3500] Built FLT.Mathlib.MeasureTheory.Haar.Extension (2.2s)
✔ [3487/3520] Built FLT.NumberField.InfiniteAdeleRing (16s)
✔ [3694/3710] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (1.7s)
✔ [3699/3714] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (1.4s)
✔ [3702/3734] Built FLT.Basic.FreyPackage (3.7s)
✔ [3719/3734] Built FLT.Deformations.Lemmas (6.3s)
✔ [3720/3737] Built FLT.QuaternionAlgebra.NumberField (11s)
✔ [3724/3739] Built FLT.Deformations.RepresentationTheory.IntegralClosure (3.6s)
✔ [3729/3754] Built FLT.Deformations.RepresentationTheory.Frobenius (3.5s)
✔ [3744/3758] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (11s)
✔ [3746/3763] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (17s)
✔ [3755/3770] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (24s)
✔ [3770/3803] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (50s)
✔ [3778/3803] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (1.7s)
✔ [3779/3803] Built FLT.Data.Hurwitz (7.2s)
✔ [3780/3803] Built FLT.Data.QHat (8.9s)
✔ [3781/3805] Built FLT.Deformations.RepresentationTheory.Etale (12s)
✔ [3784/3805] Built FLT.Patching.Utils.InverseLimit (1.4s)
✔ [3786/3806] Built FLT.Data.HurwitzRatHat (2.5s)
✔ [3788/3825] Built FLT.Deformations.Algebra.InverseLimit.Basic (6.8s)
✔ [3791/3825] Built FLT.Deformations.Algebra.InverseLimit.Topology (3.7s)
✔ [3795/3825] Built FLT.Patching.Utils.Lemmas (5.4s)
✔ [3797/3825] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.4s)
✔ [3798/3825] Built FLT.Mathlib.RepresentationTheory.Basic (2.3s)
✔ [3800/3825] Built FLT.GaloisRepresentation.Cyclotomic (1.9s)
✔ [3801/3825] Built FLT.Deformations.Subfunctor (1.0s)
✔ [3802/3825] Built FLT.Deformations.IsResidueAlgebra (2.0s)
✔ [3803/3830] Built FLT.Patching.Utils.AdicTopology (4.1s)
✔ [3804/3835] Built FLT.Deformations.RepresentationTheory.Irreducible (1.6s)
✔ [3927/3966] Built FLT.GroupScheme.FiniteFlat (261ms)
✔ [3928/3966] Built FLT.Deformations.RepresentationTheory.GaloisRep (15s)
✔ [3929/3966] Built FLT.Deformations.IsProartinian (2.2s)
✔ [3930/3966] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (1.6s)
✔ [3931/3966] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.5s)
✔ [3932/3966] Built FLT.Mathlib.Data.Fin.Basic (963ms)
✔ [3933/3966] Built FLT.Mathlib.Data.Set.Prod (509ms)
✔ [3934/3966] Built FLT.Mathlib.GroupTheory.Index (1.1s)
✔ [3935/3966] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.3s)
✔ [3937/3966] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.4s)
✔ [3939/3966] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.4s)
✔ [3940/3966] Built FLT.Mathlib.Topology.Algebra.Monoid (1.2s)
✔ [3941/3966] Built FLT.GaloisRepresentation.Automorphic (2.7s)
✔ [3942/3966] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (2.1s)
✔ [3943/3966] Built FLT.EllipticCurve.Torsion (2.4s)
✔ [3944/3969] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.3s)
✔ [3946/3969] Built FLT.Mathlib.Topology.Algebra.Order.Field (2.9s)
✔ [3947/3969] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (86s)
✔ [3948/3969] Built FLT.Deformations.Categories (3.7s)
✔ [3949/3969] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (2.1s)
✔ [3950/3971] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (1.0s)
✔ [3954/3971] Built FLT.GaloisRepresentation.HardlyRamified.Lift (1.9s)
✔ [3955/3980] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.1s)
✔ [3963/3983] Built FLT.GaloisRepresentation.HardlyRamified.Frey (1.8s)
✔ [3966/3983] Built FLT.Patching.Utils.TopologicallyFG (1.5s)
✔ [3967/3985] Built FLT.Basic.Reductions (2.2s)
✔ [3969/3985] Built FLT.Deformations.LiftFunctor (4.1s)
✔ [3970/3985] Built FLT.NumberField.DiscriminantBounds (4.2s)
✔ [3972/3985] Built FLT.Patching.Utils.StructureFiniteness (4.4s)
✔ [3974/3985] Built FLT.GlobalLanglandsConjectures.GLnDefs (9.9s)
✔ [3976/4009] Built FLT.Deformations.Representable (2.8s)
✔ [3991/4009] Built FLT.TateCurve.TateCurve (279ms)
✔ [3992/4009] Built FLT.GlobalLanglandsConjectures.GLzero (2.2s)
✔ [3994/4009] Built FLT.Patching.Utils.CompactHausdorffRings (2.6s)
✔ [3995/4009] Built FLT.Patching.Utils.Depth (3.6s)
✔ [3996/4009] Built FLT.Patching.Ultraproduct (9.6s)
✔ [3997/4009] Built FLT.Patching.VanishingFilter (3.3s)
✔ [3998/4009] Built FLT.Patching.Algebra (13s)
✔ [3999/4009] Built FLT.NumberField.AdeleRing (33s)
✔ [4000/4009] Built FLT.Patching.Module (15s)
✔ [4001/4009] Built FLT.HaarMeasure.HaarChar.AdeleRing (11s)
✔ [4002/4009] Built FLT.Patching.Over (13s)
✔ [4003/4009] Built FLT.Patching.System (9.9s)
✔ [4004/4009] Built FLT.Patching.REqualsT (4.1s)
✔ [4005/4009] Built FLT.DivisionAlgebra.Finiteness (40s)
✔ [4006/4009] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (2.2s)
✔ [4007/4009] Built FLT (1.8s)
✔ [4008/4009] Built FermatsLastTheorem (15s)
Build completed successfully (4009 jobs).

blueprint_build exit 1 duration 1s · created 6/2/2026, 7:00:14 PM

lake build :blueprint

error: unknown package facet `blueprint`

semantic_extract exit 0 duration 25m 11s · created 6/2/2026, 7:00:14 PM

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