Verification run

Run 35

ImperialCollegeLondon/FLT branch main triggered via poller

failed commit 91d59f2eb39c toolchain lean-v4-32-0-rc1 prover lean took 16m 50s · finished 2w ago

lake build failed with exit code 1 (toolchain lean-v4-32-0-rc1, command: elan run leanprover/lean4:v4.32.0-rc1 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase lake build)

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

$ git clone --depth 1 --branch main --single-branch https://github.com/ImperialCollegeLondon/FLT.git /var/lib/apodeixis/repos/job-742-source
exit_code=Some(0) duration_ms=1018
stderr:
Cloning into '/var/lib/apodeixis/repos/job-742-source'...


$ git checkout 91d59f2eb39cbea51b5808145386dd762ce62378
exit_code=Some(0) duration_ms=20
stderr:
Note: switching to '91d59f2eb39cbea51b5808145386dd762ce62378'.

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 91d59f2 chore: bump mathlib to 41520da, fix breaking changes (#1039)

Resolved source revision: 91d59f2eb39cbea51b5808145386dd762ce62378

Detected prover: lean
Detected requested toolchain: lean-v4-32-0-rc1
Materialized Lean semantic helper assets
Prepared source: revision=91d59f2eb39cbea51b5808145386dd762ce62378 provenance={"branch":"main","checked_out_revision":"91d59f2eb39cbea51b5808145386dd762ce62378","clone_url_hash":"26972c4fa07707e04a8d064eb61ea9ced3487bda0b6c5e8ecd8face933c5481e","credential_mode":"none","local_clone":false,"requested_commit_sha":"91d59f2eb39cbea51b5808145386dd762ce62378","used_missing_commit_fetch":false}
Resolved toolchain: lean-v4-32-0-rc1 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
Restored 2 Lean dependency package snapshot(s)
Prepared 2 shared Lean git mirror alias(es)
Lean semantic module cache: pre-semantic phase failed; not running semantic extraction

$ lake exe cache get
exit_code=Some(0) duration_ms=122926
stdout:
Current branch: HEAD
Using cache from origin: (some leanprover-community/mathlib4)
Attempting to download 8580 file(s) from leanprover-community/mathlib4 cache at https://lakecache.blob.core.windows.net/mathlib4-master
Attempting to download 4 file(s) from leanprover-community/mathlib4 cache at https://lakecache.blob.core.windows.net/mathlib4
Decompressed 4 file(s)
Decompressing 1739 file(s) (6841 already decompressed)
Decompressed in 5923 ms
Completed successfully!

stderr:
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '41520dac113c0aad66a755d8229c4900f99fd58a'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'f3f26cc72646205ca167117487c008ee1dafe816'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '41f407a8e85b0fdc00910633a8f14754139b63f4'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'e6518a674e62de322b8f79eebeda7bcae2a36bc3'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '7a62bd13860cd39ac98da16ffc8c24d601353f69'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '7d1b02eb63b526dff04cb990cf05b06b38ccbd3f'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '406ebb8c8e2f7e852a1b47764b42494022ce652c'
✔ [1/5] Built Cache.Cli (348ms)
✔ [2/5] Built Cache.Lean (405ms)
✔ [6/11] Built Cache.Infra (397ms)
✔ [7/12] Built Cache.IO (1.4s)
✔ [9/26] Built Cache.Hashing (812ms)
✔ [10/26] Built Cache.Requests (1.9s)
✔ [11/26] Built Cache.Cli:c.o (1.2s)
✔ [12/26] Built Cache.Lean:c.o (122ms)
✔ [14/26] Built Cache.IO:c.o (1.3s)
✔ [15/26] Built Cache.Hashing:c.o (356ms)
✔ [16/26] Built Cache.Infra:c.o (172ms)
✔ [17/26] Built Cache.Requests:c.o (2.1s)
✔ [18/26] Built Cache.Marker (617ms)
✔ [19/26] Built Cache.Marker:c.o (100ms)
✔ [20/26] Built Cache.Query (727ms)
✔ [21/26] Built Cache.Query:c.o (224ms)
✔ [22/26] Built Cache.Warning (692ms)
✔ [23/26] Built Cache.Warning:c.o (207ms)
✔ [24/26] Built Cache.Main (1.4s)
✔ [25/26] Built Cache.Main:c.o (732ms)
✔ [26/26] Built cache:exe (5.3s)

Downloaded: 1 file(s) [attempted 1/8580 = 0%, 13 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8580 = 0%, 12 KB/s], Decompressed: 12
Downloaded: 41 file(s) [attempted 41/8580 = 0%, 129 KB/s], Decompressed: 25
Downloaded: 63 file(s) [attempted 63/8580 = 0%, 46 KB/s], Decompressed: 49
Downloaded: 88 file(s) [attempted 88/8580 = 1%, 200 KB/s], Decompressed: 79
Downloaded: 122 file(s) [attempted 122/8580 = 1%, 36 KB/s], Decompressed: 105
Downloaded: 156 file(s) [attempted 156/8580 = 1%, 583 KB/s], Decompressed: 132
Downloaded: 194 file(s) [attempted 194/8580 = 2%, 45 KB/s], Decompressed: 150
Downloaded: 234 file(s) [attempted 234/8580 = 2%, 57 KB/s], Decompressed: 177
Downloaded: 275 file(s) [attempted 275/8580 = 3%, 538 KB/s], Decompressed: 200
Downloaded: 312 file(s) [attempted 312/8580 = 3%, 81 KB/s], Decompressed: 238
Downloaded: 346 file(s) [attempted 346/8580 = 4%, 577 KB/s], Decompressed: 282
Downloaded: 383 file(s) [attempted 383/8580 = 4%, 114 KB/s], Decompressed: 282
Downloaded: 427 file(s) [attempted 427/8580 = 4%, 90 KB/s], Decompressed: 332
Downloaded: 471 file(s) [attempted 471/8580 = 5%, 353 KB/s], Decompressed: 332
Downloaded: 515 file(s) [attempted 515/8580 = 6%, 109 KB/s], Decompressed: 390
Downloaded: 556 file(s) [attempted 556/8580 = 6%, 580 KB/s], Decompressed: 390
Downloaded: 597 file(s) [attempted 597/8580 = 6%, 799 KB/s], Decompressed: 390
Downloaded: 637 file(s) [attempted 637/8580 = 7%, 282 KB/s], Decompressed: 390
Downloaded: 678 file(s) [attempted 678/8580 = 7%, 62 KB/s], Decompressed: 495
Downloaded: 718 file(s) [attempted 718/8580 = 8%, 296 KB/s], Decompressed: 495
Downloaded: 762 file(s) [attempted 762/8580 = 8%, 54 KB/s], Decompressed: 495
Downloaded: 806 file(s) [attempted 806/8580 = 9%, 2026 KB/s], Decompressed: 495
Downloaded: 850 file(s) [attempted 850/8580 = 9%, 684 KB/s], Decompressed: 495
Downloaded: 898 file(s) [attempted 898/8580 = 10%, 291 KB/s], Decompressed: 654
Downloaded: 938 file(s) [attempted 938/8580 = 10%, 340 KB/s], Decompressed: 654
Downloaded: 979 file(s) [attempted 979/8580 = 11%, 165 KB/s], Decompressed: 654
Downloaded: 1023 file(s) [attempted 1023/8580 = 11%, 358 KB/s], Decompressed: 654
Downloaded: 1060 file(s) [attempted 1060/8580 = 12%, 665 KB/s], Decompressed: 654
Downloaded: 1094 file(s) [attempted 1094/8580 = 12%, 75 KB/s], Decompressed: 654
Downloaded: 1135 file(s) [attempted 1135/8580 = 13%, 163 KB/s], Decompressed: 867
Downloaded: 1179 file(s) [attempted 1179/8580 = 13%, 335 KB/s], Decompressed: 867
Downloaded: 1219 file(s) [attempted 1219/8580 = 14%, 111 KB/s], Decompressed: 867
Downloaded: 1256 file(s) [attempted 1256/8580 = 14%, 660 KB/s], Decompressed: 867
Downloaded: 1290 file(s) [attempted 1290/8580 = 15%, 1196 KB/s], Decompressed: 867
Downloaded: 1340 file(s) [attempted 1340/8580 = 15%, 1196 KB/s], Decompressed: 867
Downloaded: 1385 file(s) [attempted 1385/8580 = 16%, 824 KB/s], Decompressed: 867
Downloaded: 1422 file(s) [attempted 1422/8580 = 16%, 712 KB/s], Decompressed: 867
Downloaded: 1463 file(s) [attempted 1463/8580 = 17%, 282 KB/s], Decompressed: 1131
Downloaded: 1503 file(s) [attempted 1503/8580 = 17%, 69 KB/s], Decompressed: 1131
Downloaded: 1543 file(s) [attempted 1544/8580 = 17%, 1208 KB/s], Decompressed: 1131
Downloaded: 1590 file(s) [attempted 1591/8580 = 18%, 282 KB/s], Decompressed: 1131
Downloaded: 1634 file(s) [attempted 1635/8580 = 19%, 431 KB/s], Decompressed: 1131
Downloaded: 1675 file(s) [attempted 1676/8580 = 19%, 82 KB/s], Decompressed: 1131
Downloaded: 1709 file(s) [attempted 1710/8580 = 19%, 472 KB/s], Decompressed: 1131
Downloaded: 1749 file(s) [attempted 1750/8580 = 20%, 198 KB/s], Decompressed: 1131
Downloaded: 1793 file(s) [attempted 1794/8580 = 20%, 241 KB/s], Decompressed: 1131
Downloaded: 1837 file(s) [attempted 1838/8580 = 21%, 308 KB/s], Decompressed: 1131
Downloaded: 1871 file(s) [attempted 1872/8580 = 21%, 35 KB/s], Decompressed: 1449
Downloaded: 1908 file(s) [attempted 1909/8580 = 22%, 764 KB/s], Decompressed: 1449
Downloaded: 1949 file(s) [attempted 1950/8580 = 22%, 299 KB/s], Decompressed: 1449
Downloaded: 1983 file(s) [attempted 1984/8580 = 23%, 2468 KB/s], Decompressed: 1449
Downloaded: 2020 file(s) [attempted 2021/8580 = 23%, 81 KB/s], Decompressed: 1449
Downloaded: 2067 file(s) [attempted 2068/8580 = 24%, 246 KB/s], Decompressed: 1449
Downloaded: 2108 file(s) [attempted 2109/8580 = 24%, 27 KB/s], Decompressed: 1449
Downloaded: 2149 file(s) [attempted 2150/8580 = 25%, 127 KB/s], Decompressed: 1449
Downloaded: 2182 file(s) [attempted 2183/8580 = 25%, 728 KB/s], Decompressed: 1449
Downloaded: 2226 file(s) [attempted 2227/8580 = 25%, 551 KB/s], Decompressed: 1449
Downloaded: 2270 file(s) [attempted 2271/8580 = 26%, 209 KB/s], Decompressed: 1449
Downloaded: 2314 file(s) [attempted 2315/8580 = 26%, 21 KB/s], Decompressed: 1449
Downloaded: 2352 file(s) [attempted 2353/8580 = 27%, 251 KB/s], Decompressed: 1847
Downloaded: 2392 file(s) [attempted 2393/8580 = 27%, 408 KB/s], Decompressed: 1847
Downloaded: 2433 file(s) [attempted 2434/8580 = 28%, 267 KB/s], Decompressed: 1847
Downloaded: 2473 file(s) [attempted 2474/8580 = 28%, 713 KB/s], Decompressed: 1847
Downloaded: 2521 file(s) [attempted 2522/8580 = 29%, 399 KB/s], Decompressed: 1847
Downloaded: 2565 file(s) [attempted 2566/8580 = 29%, 319 KB/s], Decompressed: 1847
Downloaded: 2609 file(s) [attempted 2610/8580 = 30%, 65 KB/s], Decompressed: 1847
Downloaded: 2639 file(s) [attempted 2640/8580 = 30%, 257 KB/s], Decompressed: 1847
Downloaded: 2680 file(s) [attempted 2681/8580 = 31%, 258 KB/s], Decompressed: 1847
Downloaded: 2724 file(s) [attempted 2725/8580 = 31%, 351 KB/s], Decompressed: 1847
Downloaded: 2768 file(s) [attempted 2769/8580 = 32%, 562 KB/s], Decompressed: 1847
Downloaded: 2812 file(s) [attempted 2813/8580 = 32%, 333 KB/s], Decompressed: 1847
Downloaded: 2852 file(s) [attempted 2853/8580 = 33%, 740 KB/s], Decompressed: 1847
Downloaded: 2893 file(s) [attempted 2894/8580 = 33%, 335 KB/s], Decompressed: 1847
Downloaded: 2937 file(s) [attempted 2938/8580 = 34%, 128 KB/s], Decompressed: 1847
Downloaded: 2977 file(s) [attempted 2978/8580 = 34%, 35 KB/s], Decompressed: 1847
Downloaded: 3021 file(s) [attempted 3022/8580 = 35%, 757 KB/s], Decompressed: 1847
Downloaded: 3065 file(s) [attempted 3066/8580 = 35%, 24 KB/s], Decompressed: 2324
Downloaded: 3109 file(s) [attempted 3110/8580 = 36%, 922 KB/s], Decompressed: 2324
Downloaded: 3146 file(s) [attempted 3147/8580 = 36%, 702 KB/s], Decompressed: 2324
Downloaded: 3190 file(s) [attempted 3191/8580 = 37%, 198 KB/s], Decompressed: 2324
Downloaded: 3234 file(s) [attempted 3235/8580 = 37%, 186 KB/s], Decompressed: 2324
Downloaded: 3278 file(s) [attempted 3279/8580 = 38%, 273 KB/s], Decompressed: 2324
Downloaded: 3319 file(s) [attempted 3320/8580 = 38%, 323 KB/s], Decompressed: 2324
Downloaded: 3360 file(s) [attempted 3361/8580 = 39%, 1460 KB/s], Decompressed: 2324
Downloaded: 3400 file(s) [attempted 3401/8580 = 39%, 924 KB/s], Decompressed: 2324
Downloaded: 3444 file(s) [attempted 3445/8580 = 40%, 216 KB/s], Decompressed: 2324
Downloaded: 3491 file(s) [attempted 3492/8580 = 40%, 378 KB/s], Decompressed: 2324
Downloaded: 3529 file(s) [attempted 3530/8580 = 41%, 486 KB/s], Decompressed: 2324
Downloaded: 3569 file(s) [attempted 3570/8580 = 41%, 106 KB/s], Decompressed: 2324
Downloaded: 3617 file(s) [attempted 3618/8580 = 42%, 82 KB/s], Decompressed: 2324
Downloaded: 3654 file(s) [attempted 3655/8580 = 42%, 306 KB/s], Decompressed: 2324
Downloaded: 3688 file(s) [attempted 3689/8580 = 42%, 504 KB/s], Decompressed: 2324
Downloaded: 3732 file(s) [attempted 3733/8580 = 43%, 55 KB/s], Decompressed: 2324
Downloaded: 3776 file(s) [attempted 3777/8580 = 44%, 1019 KB/s], Decompressed: 2324
Downloaded: 3823 file(s) [attempted 3824/8580 = 44%, 468 KB/s], Decompressed: 2324
Downloaded: 3870 file(s) [attempted 3871/8580 = 45%, 511 KB/s], Decompressed: 2324
Downloaded: 3914 file(s) [attempted 3915/8580 = 45%, 1108 KB/s], Decompressed: 2324
Downloaded: 3955 file(s) [attempted 3956/8580 = 46%, 400 KB/s], Decompressed: 3031
Downloaded: 3992 file(s) [attempted 3993/8580 = 46%, 296 KB/s], Decompressed: 3031
Downloaded: 4029 file(s) [attempted 4030/8580 = 46%, 337 KB/s], Decompressed: 3031
Downloaded: 4073 file(s) [attempted 4074/8580 = 47%, 46 KB/s], Decompressed: 3031
Downloaded: 4117 file(s) [attempted 4118/8580 = 47%, 265 KB/s], Decompressed: 3031
Downloaded: 4161 file(s) [attempted 4162/8580 = 48%, 454 KB/s], Decompressed: 3031
Downloaded: 4205 file(s) [attempted 4206/8580 = 49%, 373 KB/s], Decompressed: 3031
Downloaded: 4242 file(s) [attempted 4243/8580 = 49%, 330 KB/s], Decompressed: 3031
Downloaded: 4280 file(s) [attempted 4281/8580 = 49%, 560 KB/s], Decompressed: 3031
Downloaded: 4320 file(s) [attempted 4321/8580 = 50%, 51 KB/s], Decompressed: 3031
Downloaded: 4364 file(s) [attempted 4365/8580 = 50%, 50 KB/s], Decompressed: 3031
Downloaded: 4405 file(s) [attempted 4406/8580 = 51%, 179 KB/s], Decompressed: 3031
Downloaded: 4449 file(s) [attempted 4450/8580 = 51%, 230 KB/s], Decompressed: 3031
Downloaded: 4489 file(s) [attempted 4490/8580 = 52%, 118 KB/s], Decompressed: 3031
Downloaded: 4527 file(s) [attempted 4528/8580 = 52%, 335 KB/s], Decompressed: 3031
Downloaded: 4570 file(s) [attempted 4571/8580 = 53%, 36 KB/s], Decompressed: 3031
Downloaded: 4611 file(s) [attempted 4612/8580 = 53%, 519 KB/s], Decompressed: 3031
Downloaded: 4648 file(s) [attempted 4649/8580 = 54%, 229 KB/s], Decompressed: 3031
Downloaded: 4692 file(s) [attempted 4693/8580 = 54%, 1090 KB/s], Decompressed: 3031
Downloaded: 4736 file(s) [attempted 4737/8580 = 55%, 707 KB/s], Decompressed: 3031
Downloaded: 4774 file(s) [attempted 4775/8580 = 55%, 180 KB/s], Decompressed: 3031
Downloaded: 4814 file(s) [attempted 4815/8580 = 56%, 148 KB/s], Decompressed: 3031
Downloaded: 4858 file(s) [attempted 4859/8580 = 56%, 52 KB/s], Decompressed: 3031
Downloaded: 4902 file(s) [attempted 4903/8580 = 57%, 182 KB/s], Decompressed: 3031
Downloaded: 4946 file(s) [attempted 4947/8580 = 57%, 93 KB/s], Decompressed: 3031
Downloaded: 4987 file(s) [attempted 4988/8580 = 58%, 49 KB/s], Decompressed: 3031
Downloaded: 5021 file(s) [attempted 5022/8580 = 58%, 124 KB/s], Decompressed: 3031
Downloaded: 5058 file(s) [attempted 5059/8580 = 58%, 56 KB/s], Decompressed: 3031
Downloaded: 5099 file(s) [attempted 5100/8580 = 59%, 128 KB/s], Decompressed: 3031
Downloaded: 5142 file(s) [attempted 5143/8580 = 59%, 340 KB/s], Decompressed: 3031
Downloaded: 5186 file(s) [attempted 5187/8580 = 60%, 125 KB/s], Decompressed: 3945
Downloaded: 5230 file(s) [attempted 5231/8580 = 60%, 133 KB/s], Decompressed: 3945
Downloaded: 5274 file(s) [attempted 5275/8580 = 61%, 92 KB/s], Decompressed: 3945
Downloaded: 5315 file(s) [attempted 5316/8580 = 61%, 101 KB/s], Decompressed: 3945
Downloaded: 5352 file(s) [attempted 5353/8580 = 62%, 128 KB/s], Decompressed: 3945
Downloaded: 5393 file(s) [attempted 5394/8580 = 62%, 737 KB/s], Decompressed: 3945
Downloaded: 5437 file(s) [attempted 5438/8580 = 63%, 712 KB/s], Decompressed: 3945
Downloaded: 5481 file(s) [attempted 5482/8580 = 63%, 190 KB/s], Decompressed: 3945
Downloaded: 5525 file(s) [attempted 5526/8580 = 64%, 989 KB/s], Decompressed: 3945
Downloaded: 5565 file(s) [attempted 5566/8580 = 64%, 235 KB/s], Decompressed: 3945
Downloaded: 5609 file(s) [attempted 5610/8580 = 65%, 191 KB/s], Decompressed: 3945
Downloaded: 5653 file(s) [attempted 5654/8580 = 65%, 461 KB/s], Decompressed: 3945
Downloaded: 5685 file(s) [attempted 5686/8580 = 66%, 340 KB/s], Decompressed: 3945
Downloaded: 5728 file(s) [attempted 5729/8580 = 66%, 167 KB/s], Decompressed: 3945
Downloaded: 5778 file(s) [attempted 5779/8580 = 67%, 541 KB/s], Decompressed: 3945
Downloaded: 5819 file(s) [attempted 5820/8580 = 67%, 651 KB/s], Decompressed: 3945
Downloaded: 5866 file(s) [attempted 5867/8580 = 68%, 101 KB/s], Decompressed: 3945
Downloaded: 5914 file(s) [attempted 5915/8580 = 68%, 271 KB/s], Decompressed: 3945
Downloaded: 5964 file(s) [attempted 5965/8580 = 69%, 389 KB/s], Decompressed: 3945
Downloaded: 6012 file(s) [attempted 6013/8580 = 70%, 340 KB/s], Decompressed: 3945
Downloaded: 6052 file(s) [attempted 6053/8580 = 70%, 77 KB/s], Decompressed: 3945
Downloaded: 6093 file(s) [attempted 6094/8580 = 71%, 185 KB/s], Decompressed: 3945
Downloaded: 6130 file(s) [attempted 6131/8580 = 71%, 723 KB/s], Decompressed: 3945
Downloaded: 6174 file(s) [attempted 6175/8580 = 71%, 245 KB/s], Decompressed: 3945
Downloaded: 6215 file(s) [attempted 6216/8580 = 72%, 434 KB/s], Decompressed: 3945
Downloaded: 6259 file(s) [attempted 6260/8580 = 72%, 78 KB/s], Decompressed: 3945
Downloaded: 6299 file(s) [attempted 6300/8580 = 73%, 107 KB/s], Decompressed: 3945
Downloaded: 6336 file(s) [attempted 6337/8580 = 73%, 662 KB/s], Decompressed: 3945
Downloaded: 6377 file(s) [attempted 6378/8580 = 74%, 171 KB/s], Decompressed: 3945
Downloaded: 6421 file(s) [attempted 6422/8580 = 74%, 1451 KB/s], Decompressed: 3945
Downloaded: 6448 file(s) [attempted 6449/8580 = 75%, 113 KB/s], Decompressed: 3945
Downloaded: 6495 file(s) [attempted 6496/8580 = 75%, 35 KB/s], Decompressed: 3945
Downloaded: 6539 file(s) [attempted 6540/8580 = 76%, 1286 KB/s], Decompressed: 3945
Downloaded: 6580 file(s) [attempted 6581/8580 = 76%, 189 KB/s], Decompressed: 3945
Downloaded: 6624 file(s) [attempted 6625/8580 = 77%, 445 KB/s], Decompressed: 3945
Downloaded: 6668 file(s) [attempted 6669/8580 = 77%, 357 KB/s], Decompressed: 3945
Downloaded: 6704 file(s) [attempted 6706/8580 = 78%, 89 KB/s], Decompressed: 3945
Downloaded: 6748 file(s) [attempted 6750/8580 = 78%, 301 KB/s], Decompressed: 3945
Downloaded: 6785 file(s) [attempted 6787/8580 = 79%, 357 KB/s], Decompressed: 3945
Downloaded: 6829 file(s) [attempted 6831/8580 = 79%, 133 KB/s], Decompressed: 5149
Downloaded: 6873 file(s) [attempted 6875/8580 = 80%, 319 KB/s], Decompressed: 5149
Downloaded: 6921 file(s) [attempted 6923/8580 = 80%, 129 KB/s], Decompressed: 5149
Downloaded: 6958 file(s) [attempted 6960/8580 = 81%, 450 KB/s], Decompressed: 5149
Downloaded: 7001 file(s) [attempted 7004/8580 = 81%, 116 KB/s], Decompressed: 5149
Downloaded: 7041 file(s) [attempted 7044/8580 = 82%, 258 KB/s], Decompressed: 5149
Downloaded: 7089 file(s) [attempted 7092/8580 = 82%, 37 KB/s], Decompressed: 5149
Downloaded: 7136 file(s) [attempted 7139/8580 = 83%, 1864 KB/s], Decompressed: 5149
Downloaded: 7180 file(s) [attempted 7183/8580 = 83%, 47 KB/s], Decompressed: 5149
Downloaded: 7224 file(s) [attempted 7227/8580 = 84%, 53 KB/s], Decompressed: 5149
Downloaded: 7261 file(s) [attempted 7264/8580 = 84%, 308 KB/s], Decompressed: 5149
Downloaded: 7302 file(s) [attempted 7305/8580 = 85%, 203 KB/s], Decompressed: 5149
Downloaded: 7342 file(s) [attempted 7345/8580 = 85%, 97 KB/s], Decompressed: 5149
Downloaded: 7386 file(s) [attempted 7389/8580 = 86%, 278 KB/s], Decompressed: 5149
Downloaded: 7430 file(s) [attempted 7433/8580 = 86%, 240 KB/s], Decompressed: 5149
Downloaded: 7468 file(s) [attempted 7471/8580 = 87%, 61 KB/s], Decompressed: 5149
Downloaded: 7512 file(s) [attempted 7515/8580 = 87%, 43 KB/s], Decompressed: 5149
Downloaded: 7552 file(s) [attempted 7555/8580 = 88%, 176 KB/s], Decompressed: 5149
Downloaded: 7593 file(s) [attempted 7596/8580 = 88%, 1372 KB/s], Decompressed: 5149
Downloaded: 7633 file(s) [attempted 7636/8580 = 88%, 340 KB/s], Decompressed: 5149
Downloaded: 7676 file(s) [attempted 7680/8580 = 89%, 1 KB/s], Decompressed: 5149
Downloaded: 7717 file(s) [attempted 7721/8580 = 89%, 141 KB/s], Decompressed: 5149
Downloaded: 7754 file(s) [attempted 7758/8580 = 90%, 396 KB/s], Decompressed: 5149
Downloaded: 7795 file(s) [attempted 7799/8580 = 90%, 243 KB/s], Decompressed: 5149
Downloaded: 7842 file(s) [attempted 7846/8580 = 91%, 126 KB/s], Decompressed: 5149
Downloaded: 7883 file(s) [attempted 7887/8580 = 91%, 323 KB/s], Decompressed: 5149
Downloaded: 7927 file(s) [attempted 7931/8580 = 92%, 1101 KB/s], Decompressed: 5149
Downloaded: 7967 file(s) [attempted 7971/8580 = 92%, 34 KB/s], Decompressed: 5149
Downloaded: 8004 file(s) [attempted 8008/8580 = 93%, 547 KB/s], Decompressed: 5149
Downloaded: 8048 file(s) [attempted 8052/8580 = 93%, 384 KB/s], Decompressed: 5149
Downloaded: 8092 file(s) [attempted 8096/8580 = 94%, 371 KB/s], Decompressed: 5149
Downloaded: 8133 file(s) [attempted 8137/8580 = 94%, 233 KB/s], Decompressed: 5149
Downloaded: 8170 file(s) [attempted 8174/8580 = 95%, 431 KB/s], Decompressed: 5149
Downloaded: 8211 file(s) [attempted 8215/8580 = 95%, 380 KB/s], Decompressed: 5149
Downloaded: 8251 file(s) [attempted 8255/8580 = 96%, 184 KB/s], Decompressed: 5149
Downloaded: 8299 file(s) [attempted 8303/8580 = 96%, 115 KB/s], Decompressed: 5149
Downloaded: 8339 file(s) [attempted 8343/8580 = 97%, 191 KB/s], Decompressed: 5149
Downloaded: 8380 file(s) [attempted 8384/8580 = 97%, 608 KB/s], Decompressed: 5149
Downloaded: 8421 file(s) [attempted 8425/8580 = 98%, 629 KB/s], Decompressed: 5149
Downloaded: 8461 file(s) [attempted 8465/8580 = 98%, 80 KB/s], Decompressed: 5149
Downloaded: 8502 file(s) [attempted 8506/8580 = 99%, 93 KB/s], Decompressed: 5149
Downloaded: 8546 file(s) [attempted 8550/8580 = 99%, 1252 KB/s], Decompressed: 5149
Downloaded: 8576 file(s) [attempted 8580/8580 = 100%, 1252 KB/s], Decompressed: 5149

Downloaded: 1 file(s) [attempted 1/4 = 25%, 18 KB/s], Decompressed: 0
Downloaded: 3 file(s) [attempted 3/4 = 75%, 22 KB/s], Decompressed: 2
Downloaded: 4 file(s) [attempted 4/4 = 100%, 22 KB/s], Decompressed: 2


$ lake build
exit_code=Some(1) duration_ms=877285
stdout:
✔ [1/3] Built FLT.Assumptions.KnownIn1980s (482ms)
✔ [1957/1968] Built FLT.Assumptions.Mazur (14s)
✔ [2954/2967] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (2.4s)
✔ [2956/2967] Built FLT.Mathlib.Topology.Algebra.Group.Units (1.3s)
✔ [2958/2968] Built FLT.AutomorphicForm.GroupTheoryStuff (4.1s)
✔ [2960/2968] Built FLT.Mathlib.Order.Filter.Cofinite (1.0s)
✔ [2961/2968] Built FLT.Mathlib.Topology.Bases (1.0s)
✔ [2963/2974] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (1.8s)
✔ [2965/2974] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (2.8s)
✔ [2966/2974] Built FLT.Assumptions.Odlyzko (6.5s)
✔ [2968/2974] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (885ms)
✔ [2969/2974] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (1.4s)
✔ [2970/2974] Built FLT.Mathlib.Algebra.Algebra.Tower (1.2s)
✔ [2971/2975] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (4.8s)
✔ [2974/2981] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (6.0s)
✔ [3248/3255] Built FLT.Mathlib.Topology.Algebra.MulAction (1.0s)
✔ [3252/3257] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (5.8s)
✔ [3253/3257] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (7.2s)
✔ [3255/3267] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Algebra (1.4s)
✔ [3334/3342] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (2.0s)
✔ [3335/3342] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.1s)
✔ [3336/3342] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (2.0s)
✔ [3337/3347] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (6.6s)
✔ [3341/3347] Built FLT.Mathlib.LinearAlgebra.Countable (1.3s)
✔ [3343/3348] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (884ms)
✔ [3347/3355] Built FLT.DedekindDomain.AdicValuation (6.4s)
✔ [3354/3359] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (1.0s)
✔ [3364/3373] Built FLT.Mathlib.RingTheory.Localization.BaseChange (1.9s)
✔ [3365/3376] Built FLT.DedekindDomain.IntegralClosure (4.6s)
✔ [3372/3376] Built FLT.NumberField.HeightOneSpectrum (1.5s)
✔ [3373/3379] Built FLT.NumberField.Completion.Finite (2.3s)
✔ [3375/3387] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (2.2s)
✔ [3381/3387] Built FLT.Hacks.RightActionInstances (3.3s)
✔ [3385/3397] Built FLT.Mathlib.Topology.Algebra.Group.Basic (1.3s)
✔ [3386/3398] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (3.9s)
✔ [3388/3398] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (1.9s)
✔ [3389/3398] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (1.4s)
✔ [3390/3398] Built FLT.Mathlib.Topology.Instances.Matrix (1.3s)
✔ [3393/3407] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (1.2s)
✔ [3397/3407] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (1.2s)
✔ [3398/3407] Built FLT.Mathlib.MeasureTheory.Group.Action (2.1s)
✔ [3399/3407] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (1.2s)
✔ [3401/3407] Built FLT.Mathlib.GroupTheory.DoubleCoset (3.9s)
✔ [3402/3408] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (3.3s)
✔ [3403/3408] Built FLT.Mathlib.MeasureTheory.Group.Measure (1.4s)
✔ [3404/3408] Built FLT.AutomorphicForm.Stuff (2.6s)
✔ [3406/3408] Built FLT.QuaternionAlgebra.NumberField (12s)
✔ [3407/3422] Built FLT.AutomorphicForm.QuaternionAlgebra.Basic (36s)
✔ [3414/3422] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.0s)
✔ [3417/3422] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (1.4s)
✔ [3418/3422] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (1.6s)
✔ [3420/3424] Built FLT.HaarMeasure.HaarChar.AddEquiv (5.9s)
✔ [3422/3439] Built FLT.HaarMeasure.HaarChar.Ring (2.9s)
✔ [3427/3439] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (1.5s)
✔ [3428/3439] Built FLT.Mathlib.Algebra.Algebra.Hom (1.9s)
✔ [3430/3447] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (1.6s)
✔ [3431/3447] Built FLT.Mathlib.Topology.Algebra.UniformRing (1.2s)
✔ [3432/3447] Built FLT.Mathlib.Algebra.Algebra.Pi (1.2s)
✔ [3434/3447] Built FLT.Mathlib.Algebra.Algebra.Bilinear (1.8s)
✔ [3436/3447] Built FLT.Mathlib.Algebra.IsDirectLimit (1.9s)
✔ [3437/3447] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (1.5s)
✔ [3440/3451] Built FLT.Mathlib.LinearAlgebra.Pi (1.3s)
✔ [3442/3451] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (1.4s)
✔ [3444/3451] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (2.9s)
✔ [3446/3451] Built FLT.DedekindDomain.Completion.BaseChange (22s)
✔ [3447/3451] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (7.0s)
✔ [3448/3465] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (1.9s)
✔ [3451/3466] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (67s)
✔ [3453/3466] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (1.5s)
✔ [3454/3466] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (1.6s)
✔ [3455/3466] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (1.1s)
✔ [3456/3466] Built FLT.NumberField.InfinitePlace.Extension (2.6s)
✔ [3457/3466] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (1.4s)
✔ [3459/3469] Built FLT.Mathlib.Topology.Constructions (1.1s)
✔ [3461/3469] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (1.5s)
✔ [3464/3476] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (1.8s)
✔ [3465/3478] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (1.7s)
✔ [3467/3478] Built FLT.NumberField.Padics.RestrictedProduct (2.6s)
✔ [3468/3478] Built FLT.Mathlib.Data.Real.Archimedean (999ms)
✔ [3469/3478] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (1.3s)
✔ [3470/3478] Built FLT.NumberField.Completion.Infinite (16s)
✔ [3471/3478] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (1.7s)
✔ [3474/3481] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (1.7s)
✔ [3475/3481] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (5.8s)
✔ [3476/3487] Built FLT.NumberField.InfiniteAdeleRing (13s)
✔ [3478/3490] Built FLT.NumberField.AdeleRing (23s)
✔ [3481/3496] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (1.0s)
✔ [3483/3496] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (2.8s)
✔ [3485/3500] Built FLT.HaarMeasure.MeasurableSpacePadics (1.8s)
✔ [3487/3500] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (1.0s)
✔ [3488/3500] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (1.3s)
✔ [3489/3500] Built FLT.HaarMeasure.HaarChar.RealComplex (2.3s)
✔ [3490/3500] Built FLT.HaarMeasure.HaarChar.Padic (2.4s)
✔ [3491/3500] Built FLT.Mathlib.LinearAlgebra.Determinant (3.6s)
✔ [3493/3500] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.0s)
✔ [3494/3500] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (2.1s)
✔ [3495/3500] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (2.8s)
✔ [3496/3500] Built FLT.Mathlib.Algebra.Central.TensorProduct (1.9s)
✔ [3497/3500] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (5.7s)
✔ [3498/3501] Built FLT.HaarMeasure.HaarChar.AdeleRing (4.9s)
✔ [3499/3505] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (19s)
✔ [3510/3518] Built FLT.Mathlib.Topology.HomToDiscrete (1.5s)
✔ [3514/3518] Built FLT.Mathlib.Topology.Polish (1.4s)
✔ [3515/3518] Built FLT.Mathlib.MeasureTheory.Haar.Extension (2.0s)
✔ [3516/3520] Built FLT.DivisionAlgebra.Finiteness (41s)
✔ [3517/3522] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (2.4s)
✔ [3539/3547] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (2.5s)
✔ [3541/3547] Built FLT.Mathlib.FieldTheory.SplittingField.IsSplittingField (2.6s)
✔ [3545/3551] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (5.0s)
✔ [3547/3558] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (4.2s)
✔ [3557/3569] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (38s)
✖ [3568/3573] Building FLT.Mathlib.MeasureTheory.Group.ModularCharacter (7.4s)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/packages/checkdecls/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /apx/source/FLT/Mathlib/MeasureTheory/Group/ModularCharacter.lean -o /apx/source/.lake/build/lib/lean/FLT/Mathlib/MeasureTheory/Group/ModularCharacter.olean -i /apx/source/.lake/build/lib/lean/FLT/Mathlib/MeasureTheory/Group/ModularCharacter.ilean -c /apx/source/.lake/build/ir/FLT/Mathlib/MeasureTheory/Group/ModularCharacter.c --setup /apx/source/.lake/build/ir/FLT/Mathlib/MeasureTheory/Group/ModularCharacter.setup.json --json
error: FLT/Mathlib/MeasureTheory/Group/ModularCharacter.lean:407:20: typeclass instance problem is stuck
  TopologicalSpace (Matrix ?m.54 ?m.54 ?m.55)

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `TopologicalSpace` contains metavariables. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
error: Lean exited with code 1
✔ [8709/8780] Built FLT.Data.Hurwitz (4.3s)
✔ [8710/8780] Built FLT.Data.QHat (5.0s)
✔ [8711/8780] Built FLT.Deformations.Algebra.InverseLimit.Basic (5.0s)
✔ [8712/8780] Built FLT.Patching.Utils.InverseLimit (1.1s)
✔ [8713/8780] Built FLT.Patching.Utils.Lemmas (4.1s)
✔ [8714/8780] Built FLT.Deformations.Lemmas (3.7s)
✔ [8715/8780] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.2s)
✔ [8716/8780] Built FLT.Deformations.Subfunctor (831ms)
✔ [8717/8780] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (1.2s)
✔ [8718/8780] Built FLT.Mathlib.RepresentationTheory.Basic (2.0s)
✔ [8719/8780] Built FLT.FreyCurve.FreyPackage (3.6s)
✔ [8720/8780] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (1.6s)
✔ [8721/8780] Built FLT.GlobalLanglandsConjectures.GLnDefs (8.4s)
✔ [8722/8780] Built FLT.GroupScheme.FiniteFlat (312ms)
✔ [8723/8780] Built FLT.HenselianLocalRing.EtaleDecomposition (13s)
✔ [8724/8780] Built FLT.HenselianLocalRing.Stuff (2.1s)
✔ [8725/8780] Built FLT.Mathlib.Algebra.FixedPoints.Basic (2.0s)
✔ [8726/8780] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (1.2s)
✔ [8727/8780] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.3s)
✔ [8728/8780] Built FLT.Mathlib.Data.Fin.Basic (830ms)
✔ [8729/8780] Built FLT.Mathlib.Data.Set.Prod (590ms)
✔ [8730/8780] Built FLT.Mathlib.GroupTheory.Index (920ms)
✔ [8731/8780] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.3s)
✔ [8732/8780] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.2s)
✔ [8733/8780] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.4s)
✔ [8734/8780] Built FLT.Mathlib.Topology.Algebra.Monoid (1.1s)
✔ [8735/8780] Built FLT.NumberField.DiscriminantBounds (2.8s)
✔ [8736/8780] Built FLT.Patching.Utils.TopologicallyFG (1.5s)
✔ [8737/8780] Built FLT.Patching.Utils.Depth (2.7s)
✔ [8738/8780] Built FLT.Patching.Utils.CompactHausdorffRings (2.1s)
✔ [8740/8780] Built FLT.TateCurve.TateCurve (274ms)
✔ [8741/8780] Built FLT.Data.HurwitzRatHat (2.0s)
✔ [8742/8780] Built FLT.GaloisRepresentation.Cyclotomic (1.7s)
✔ [8743/8780] Built FLT.Deformations.Algebra.InverseLimit.Topology (3.2s)
✔ [8744/8780] Built FLT.Patching.Utils.AdicTopology (3.2s)
✔ [8745/8780] Built FLT.Deformations.IsResidueAlgebra (1.7s)
✔ [8746/8780] Built FLT.Deformations.RepresentationTheory.IntegralClosure (2.0s)
✔ [8747/8780] Built FLT.Deformations.RepresentationTheory.Etale (8.4s)
✔ [8748/8780] Built FLT.Deformations.RepresentationTheory.Frobenius (2.1s)
✔ [8749/8780] Built FLT.Deformations.RepresentationTheory.Irreducible (1.4s)
✔ [8750/8780] Built FLT.GlobalLanglandsConjectures.GLzero (2.2s)
✔ [8751/8780] Built FLT.HenselianLocalRing.Finite (5.8s)
✔ [8752/8780] Built FLT.Mathlib.Topology.Algebra.Order.Field (2.2s)
✔ [8754/8780] Built FLT.Patching.Utils.StructureFiniteness (3.5s)
✔ [8755/8780] Built FLT.Deformations.IsProartinian (1.8s)
✔ [8756/8780] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (13s)
✔ [8757/8780] Built FLT.Patching.Ultraproduct (7.8s)
✔ [8758/8780] Built FLT.Deformations.Categories (2.9s)
✔ [8759/8780] Built FLT.Deformations.RepresentationTheory.GaloisRep (11s)
✔ [8760/8780] Built FLT.Patching.Algebra (9.8s)
✔ [8761/8780] Built FLT.Patching.VanishingFilter (2.6s)
✔ [8762/8780] Built FLT.Patching.Module (11s)
✔ [8763/8780] Built FLT.Deformations.LiftFunctor (3.7s)
✔ [8764/8780] Built FLT.GaloisRepresentation.Automorphic (4.2s)
✔ [8765/8780] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.4s)
✔ [8766/8780] Built FLT.EllipticCurve.Torsion (2.2s)
✔ [8767/8780] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (1.9s)
✔ [8768/8780] Built FLT.Patching.Over (12s)
✔ [8769/8780] Built FLT.Deformations.Representable (2.7s)
✔ [8770/8780] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (2.0s)
✔ [8771/8780] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (1.0s)
✔ [8772/8780] Built FLT.GaloisRepresentation.HardlyRamified.Lift (1.0s)
✔ [8773/8780] Built FLT.GaloisRepresentation.HardlyRamified.Frey (1.9s)
✔ [8774/8780] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.2s)
✔ [8775/8780] Built FLT.Patching.System (9.6s)
✔ [8776/8780] Built FLT.FreyCurve.Contradiction (1.8s)
✔ [8777/8780] Built FLT.Patching.REqualsT (3.9s)
Some required targets logged failures:
- FLT.Mathlib.MeasureTheory.Group.ModularCharacter

stderr:
error: build failed


$ lake build :blueprint
exit_code=Some(1) duration_ms=8097
stderr:
error: unknown package facet `blueprint`


blueprint_build failed; continuing (non-fatal phase).

Command runs

git_clone exit 0 duration 1s · created 6/29/2026, 1:19:48 AM

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

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

git_checkout exit 0 duration 20 ms · created 6/29/2026, 1:19:48 AM

git checkout 91d59f2eb39cbea51b5808145386dd762ce62378

Note: switching to '91d59f2eb39cbea51b5808145386dd762ce62378'.

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 91d59f2 chore: bump mathlib to 41520da, fix breaking changes (#1039)

lake_cache exit 0 duration 2m 3s · created 6/29/2026, 1:19:48 AM

lake exe cache get

Current branch: HEAD
Using cache from origin: (some leanprover-community/mathlib4)
Attempting to download 8580 file(s) from leanprover-community/mathlib4 cache at https://lakecache.blob.core.windows.net/mathlib4-master
Attempting to download 4 file(s) from leanprover-community/mathlib4 cache at https://lakecache.blob.core.windows.net/mathlib4
Decompressed 4 file(s)
Decompressing 1739 file(s) (6841 already decompressed)
Decompressed in 5923 ms
Completed successfully!

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '41520dac113c0aad66a755d8229c4900f99fd58a'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'f3f26cc72646205ca167117487c008ee1dafe816'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '41f407a8e85b0fdc00910633a8f14754139b63f4'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'e6518a674e62de322b8f79eebeda7bcae2a36bc3'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '7a62bd13860cd39ac98da16ffc8c24d601353f69'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '7d1b02eb63b526dff04cb990cf05b06b38ccbd3f'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '406ebb8c8e2f7e852a1b47764b42494022ce652c'
✔ [1/5] Built Cache.Cli (348ms)
✔ [2/5] Built Cache.Lean (405ms)
✔ [6/11] Built Cache.Infra (397ms)
✔ [7/12] Built Cache.IO (1.4s)
✔ [9/26] Built Cache.Hashing (812ms)
✔ [10/26] Built Cache.Requests (1.9s)
✔ [11/26] Built Cache.Cli:c.o (1.2s)
✔ [12/26] Built Cache.Lean:c.o (122ms)
✔ [14/26] Built Cache.IO:c.o (1.3s)
✔ [15/26] Built Cache.Hashing:c.o (356ms)
✔ [16/26] Built Cache.Infra:c.o (172ms)
✔ [17/26] Built Cache.Requests:c.o (2.1s)
✔ [18/26] Built Cache.Marker (617ms)
✔ [19/26] Built Cache.Marker:c.o (100ms)
✔ [20/26] Built Cache.Query (727ms)
✔ [21/26] Built Cache.Query:c.o (224ms)
✔ [22/26] Built Cache.Warning (692ms)
✔ [23/26] Built Cache.Warning:c.o (207ms)
✔ [24/26] Built Cache.Main (1.4s)
✔ [25/26] Built Cache.Main:c.o (732ms)
✔ [26/26] Built cache:exe (5.3s)

Downloaded: 1 file(s) [attempted 1/8580 = 0%, 13 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8580 = 0%, 12 KB/s], Decompressed: 12
Downloaded: 41 file(s) [attempted 41/8580 = 0%, 129 KB/s], Decompressed: 25
Downloaded: 63 file(s) [attempted 63/8580 = 0%, 46 KB/s], Decompressed: 49
Downloaded: 88 file(s) [attempted 88/8580 = 1%, 200 KB/s], Decompressed: 79
Downloaded: 122 file(s) [attempted 122/8580 = 1%, 36 KB/s], Decompressed: 105
Downloaded: 156 file(s) [attempted 156/8580 = 1%, 583 KB/s], Decompressed: 132
Downloaded: 194 file(s) [attempted 194/8580 = 2%, 45 KB/s], Decompressed: 150
Downloaded: 234 file(s) [attempted 234/8580 = 2%, 57 KB/s], Decompressed: 177
Downloaded: 275 file(s) [attempted 275/8580 = 3%, 538 KB/s], Decompressed: 200
Downloaded: 312 file(s) [attempted 312/8580 = 3%, 81 KB/s], Decompressed: 238
Downloaded: 346 file(s) [attempted 346/8580 = 4%, 577 KB/s], Decompressed: 282
Downloaded: 383 file(s) [attempted 383/8580 = 4%, 114 KB/s], Decompressed: 282
Downloaded: 427 file(s) [attempted 427/8580 = 4%, 90 KB/s], Decompressed: 332
Downloaded: 471 file(s) [attempted 471/8580 = 5%, 353 KB/s], Decompressed: 332
Downloaded: 515 file(s) [attempted 515/8580 = 6%, 109 KB/s], Decompressed: 390
Downloaded: 556 file(s) [attempted 556/8580 = 6%, 580 KB/s], Decompressed: 390
Downloaded: 597 file(s) [attempted 597/8580 = 6%, 799 KB/s], Decompressed: 390
Downloaded: 637 file(s) [attempted 637/8580 = 7%, 282 KB/s], Decompressed: 390
Downloaded: 678 file(s) [attempted 678/8580 = 7%, 62 KB/s], Decompressed: 495
Downloaded: 718 file(s) [attempted 718/8580 = 8%, 296 KB/s], Decompressed: 495
Downloaded: 762 file(s) [attempted 762/8580 = 8%, 54 KB/s], Decompressed: 495
Downloaded: 806 file(s) [attempted 806/8580 = 9%, 2026 KB/s], Decompressed: 495
Downloaded: 850 file(s) [attempted 850/8580 = 9%, 684 KB/s], Decompressed: 495
Downloaded: 898 file(s) [attempted 898/8580 = 10%, 291 KB/s], Decompressed: 654
Downloaded: 938 file(s) [attempted 938/8580 = 10%, 340 KB/s], Decompressed: 654
Downloaded: 979 file(s) [attempted 979/8580 = 11%, 165 KB/s], Decompressed: 654
Downloaded: 1023 file(s) [attempted 1023/8580 = 11%, 358 KB/s], Decompressed: 654
Downloaded: 1060 file(s) [attempted 1060/8580 = 12%, 665 KB/s], Decompressed: 654
Downloaded: 1094 file(s) [attempted 1094/8580 = 12%, 75 KB/s], Decompressed: 654
Downloaded: 1135 file(s) [attempted 1135/8580 = 13%, 163 KB/s], Decompressed: 867
Downloaded: 1179 file(s) [attempted 1179/8580 = 13%, 335 KB/s], Decompressed: 867
Downloaded: 1219 file(s) [attempted 1219/8580 = 14%, 111 KB/s], Decompressed: 867
Downloaded: 1256 file(s) [attempted 1256/8580 = 14%, 660 KB/s], Decompressed: 867
Downloaded: 1290 file(s) [attempted 1290/8580 = 15%, 1196 KB/s], Decompressed: 867
Downloaded: 1340 file(s) [attempted 1340/8580 = 15%, 1196 KB/s], Decompressed: 867
Downloaded: 1385 file(s) [attempted 1385/8580 = 16%, 824 KB/s], Decompressed: 867
Downloaded: 1422 file(s) [attempted 1422/8580 = 16%, 712 KB/s], Decompressed: 867
Downloaded: 1463 file(s) [attempted 1463/8580 = 17%, 282 KB/s], Decompressed: 1131
Downloaded: 1503 file(s) [attempted 1503/8580 = 17%, 69 KB/s], Decompressed: 1131
Downloaded: 1543 file(s) [attempted 1544/8580 = 17%, 1208 KB/s], Decompressed: 1131
Downloaded: 1590 file(s) [attempted 1591/8580 = 18%, 282 KB/s], Decompressed: 1131
Downloaded: 1634 file(s) [attempted 1635/8580 = 19%, 431 KB/s], Decompressed: 1131
Downloaded: 1675 file(s) [attempted 1676/8580 = 19%, 82 KB/s], Decompressed: 1131
Downloaded: 1709 file(s) [attempted 1710/8580 = 19%, 472 KB/s], Decompressed: 1131
Downloaded: 1749 file(s) [attempted 1750/8580 = 20%, 198 KB/s], Decompressed: 1131
Downloaded: 1793 file(s) [attempted 1794/8580 = 20%, 241 KB/s], Decompressed: 1131
Downloaded: 1837 file(s) [attempted 1838/8580 = 21%, 308 KB/s], Decompressed: 1131
Downloaded: 1871 file(s) [attempted 1872/8580 = 21%, 35 KB/s], Decompressed: 1449
Downloaded: 1908 file(s) [attempted 1909/8580 = 22%, 764 KB/s], Decompressed: 1449
Downloaded: 1949 file(s) [attempted 1950/8580 = 22%, 299 KB/s], Decompressed: 1449
Downloaded: 1983 file(s) [attempted 1984/8580 = 23%, 2468 KB/s], Decompressed: 1449
Downloaded: 2020 file(s) [attempted 2021/8580 = 23%, 81 KB/s], Decompressed: 1449
Downloaded: 2067 file(s) [attempted 2068/8580 = 24%, 246 KB/s], Decompressed: 1449
Downloaded: 2108 file(s) [attempted 2109/8580 = 24%, 27 KB/s], Decompressed: 1449
Downloaded: 2149 file(s) [attempted 2150/8580 = 25%, 127 KB/s], Decompressed: 1449
Downloaded: 2182 file(s) [attempted 2183/8580 = 25%, 728 KB/s], Decompressed: 1449
Downloaded: 2226 file(s) [attempted 2227/8580 = 25%, 551 KB/s], Decompressed: 1449
Downloaded: 2270 file(s) [attempted 2271/8580 = 26%, 209 KB/s], Decompressed: 1449
Downloaded: 2314 file(s) [attempted 2315/8580 = 26%, 21 KB/s], Decompressed: 1449
Downloaded: 2352 file(s) [attempted 2353/8580 = 27%, 251 KB/s], Decompressed: 1847
Downloaded: 2392 file(s) [attempted 2393/8580 = 27%, 408 KB/s], Decompressed: 1847
Downloaded: 2433 file(s) [attempted 2434/8580 = 28%, 267 KB/s], Decompressed: 1847
Downloaded: 2473 file(s) [attempted 2474/8580 = 28%, 713 KB/s], Decompressed: 1847
Downloaded: 2521 file(s) [attempted 2522/8580 = 29%, 399 KB/s], Decompressed: 1847
Downloaded: 2565 file(s) [attempted 2566/8580 = 29%, 319 KB/s], Decompressed: 1847
Downloaded: 2609 file(s) [attempted 2610/8580 = 30%, 65 KB/s], Decompressed: 1847
Downloaded: 2639 file(s) [attempted 2640/8580 = 30%, 257 KB/s], Decompressed: 1847
Downloaded: 2680 file(s) [attempted 2681/8580 = 31%, 258 KB/s], Decompressed: 1847
Downloaded: 2724 file(s) [attempted 2725/8580 = 31%, 351 KB/s], Decompressed: 1847
Downloaded: 2768 file(s) [attempted 2769/8580 = 32%, 562 KB/s], Decompressed: 1847
Downloaded: 2812 file(s) [attempted 2813/8580 = 32%, 333 KB/s], Decompressed: 1847
Downloaded: 2852 file(s) [attempted 2853/8580 = 33%, 740 KB/s], Decompressed: 1847
Downloaded: 2893 file(s) [attempted 2894/8580 = 33%, 335 KB/s], Decompressed: 1847
Downloaded: 2937 file(s) [attempted 2938/8580 = 34%, 128 KB/s], Decompressed: 1847
Downloaded: 2977 file(s) [attempted 2978/8580 = 34%, 35 KB/s], Decompressed: 1847
Downloaded: 3021 file(s) [attempted 3022/8580 = 35%, 757 KB/s], Decompressed: 1847
Downloaded: 3065 file(s) [attempted 3066/8580 = 35%, 24 KB/s], Decompressed: 2324
Downloaded: 3109 file(s) [attempted 3110/8580 = 36%, 922 KB/s], Decompressed: 2324
Downloaded: 3146 file(s) [attempted 3147/8580 = 36%, 702 KB/s], Decompressed: 2324
Downloaded: 3190 file(s) [attempted 3191/8580 = 37%, 198 KB/s], Decompressed: 2324
Downloaded: 3234 file(s) [attempted 3235/8580 = 37%, 186 KB/s], Decompressed: 2324
Downloaded: 3278 file(s) [attempted 3279/8580 = 38%, 273 KB/s], Decompressed: 2324
Downloaded: 3319 file(s) [attempted 3320/8580 = 38%, 323 KB/s], Decompressed: 2324
Downloaded: 3360 file(s) [attempted 3361/8580 = 39%, 1460 KB/s], Decompressed: 2324
Downloaded: 3400 file(s) [attempted 3401/8580 = 39%, 924 KB/s], Decompressed: 2324
Downloaded: 3444 file(s) [attempted 3445/8580 = 40%, 216 KB/s], Decompressed: 2324
Downloaded: 3491 file(s) [attempted 3492/8580 = 40%, 378 KB/s], Decompressed: 2324
Downloaded: 3529 file(s) [attempted 3530/8580 = 41%, 486 KB/s], Decompressed: 2324
Downloaded: 3569 file(s) [attempted 3570/8580 = 41%, 106 KB/s], Decompressed: 2324
Downloaded: 3617 file(s) [attempted 3618/8580 = 42%, 82 KB/s], Decompressed: 2324
Downloaded: 3654 file(s) [attempted 3655/8580 = 42%, 306 KB/s], Decompressed: 2324
Downloaded: 3688 file(s) [attempted 3689/8580 = 42%, 504 KB/s], Decompressed: 2324
Downloaded: 3732 file(s) [attempted 3733/8580 = 43%, 55 KB/s], Decompressed: 2324
Downloaded: 3776 file(s) [attempted 3777/8580 = 44%, 1019 KB/s], Decompressed: 2324
Downloaded: 3823 file(s) [attempted 3824/8580 = 44%, 468 KB/s], Decompressed: 2324
Downloaded: 3870 file(s) [attempted 3871/8580 = 45%, 511 KB/s], Decompressed: 2324
Downloaded: 3914 file(s) [attempted 3915/8580 = 45%, 1108 KB/s], Decompressed: 2324
Downloaded: 3955 file(s) [attempted 3956/8580 = 46%, 400 KB/s], Decompressed: 3031
Downloaded: 3992 file(s) [attempted 3993/8580 = 46%, 296 KB/s], Decompressed: 3031
Downloaded: 4029 file(s) [attempted 4030/8580 = 46%, 337 KB/s], Decompressed: 3031
Downloaded: 4073 file(s) [attempted 4074/8580 = 47%, 46 KB/s], Decompressed: 3031
Downloaded: 4117 file(s) [attempted 4118/8580 = 47%, 265 KB/s], Decompressed: 3031
Downloaded: 4161 file(s) [attempted 4162/8580 = 48%, 454 KB/s], Decompressed: 3031
Downloaded: 4205 file(s) [attempted 4206/8580 = 49%, 373 KB/s], Decompressed: 3031
Downloaded: 4242 file(s) [attempted 4243/8580 = 49%, 330 KB/s], Decompressed: 3031
Downloaded: 4280 file(s) [attempted 4281/8580 = 49%, 560 KB/s], Decompressed: 3031
Downloaded: 4320 file(s) [attempted 4321/8580 = 50%, 51 KB/s], Decompressed: 3031
Downloaded: 4364 file(s) [attempted 4365/8580 = 50%, 50 KB/s], Decompressed: 3031
Downloaded: 4405 file(s) [attempted 4406/8580 = 51%, 179 KB/s], Decompressed: 3031
Downloaded: 4449 file(s) [attempted 4450/8580 = 51%, 230 KB/s], Decompressed: 3031
Downloaded: 4489 file(s) [attempted 4490/8580 = 52%, 118 KB/s], Decompressed: 3031
Downloaded: 4527 file(s) [attempted 4528/8580 = 52%, 335 KB/s], Decompressed: 3031
Downloaded: 4570 file(s) [attempted 4571/8580 = 53%, 36 KB/s], Decompressed: 3031
Downloaded: 4611 file(s) [attempted 4612/8580 = 53%, 519 KB/s], Decompressed: 3031
Downloaded: 4648 file(s) [attempted 4649/8580 = 54%, 229 KB/s], Decompressed: 3031
Downloaded: 4692 file(s) [attempted 4693/8580 = 54%, 1090 KB/s], Decompressed: 3031
Downloaded: 4736 file(s) [attempted 4737/8580 = 55%, 707 KB/s], Decompressed: 3031
Downloaded: 4774 file(s) [attempted 4775/8580 = 55%, 180 KB/s], Decompressed: 3031
Downloaded: 4814 file(s) [attempted 4815/8580 = 56%, 148 KB/s], Decompressed: 3031
Downloaded: 4858 file(s) [attempted 4859/8580 = 56%, 52 KB/s], Decompressed: 3031
Downloaded: 4902 file(s) [attempted 4903/8580 = 57%, 182 KB/s], Decompressed: 3031
Downloaded: 4946 file(s) [attempted 4947/8580 = 57%, 93 KB/s], Decompressed: 3031
Downloaded: 4987 file(s) [attempted 4988/8580 = 58%, 49 KB/s], Decompressed: 3031
Downloaded: 5021 file(s) [attempted 5022/8580 = 58%, 124 KB/s], Decompressed: 3031
Downloaded: 5058 file(s) [attempted 5059/8580 = 58%, 56 KB/s], Decompressed: 3031
Downloaded: 5099 file(s) [attempted 5100/8580 = 59%, 128 KB/s], Decompressed: 3031
Downloaded: 5142 file(s) [attempted 5143/8580 = 59%, 340 KB/s], Decompressed: 3031
Downloaded: 5186 file(s) [attempted 5187/8580 = 60%, 125 KB/s], Decompressed: 3945
Downloaded: 5230 file(s) [attempted 5231/8580 = 60%, 133 KB/s], Decompressed: 3945
Downloaded: 5274 file(s) [attempted 5275/8580 = 61%, 92 KB/s], Decompressed: 3945
Downloaded: 5315 file(s) [attempted 5316/8580 = 61%, 101 KB/s], Decompressed: 3945
Downloaded: 5352 file(s) [attempted 5353/8580 = 62%, 128 KB/s], Decompressed: 3945
Downloaded: 5393 file(s) [attempted 5394/8580 = 62%, 737 KB/s], Decompressed: 3945
Downloaded: 5437 file(s) [attempted 5438/8580 = 63%, 712 KB/s], Decompressed: 3945
Downloaded: 5481 file(s) [attempted 5482/8580 = 63%, 190 KB/s], Decompressed: 3945
Downloaded: 5525 file(s) [attempted 5526/8580 = 64%, 989 KB/s], Decompressed: 3945
Downloaded: 5565 file(s) [attempted 5566/8580 = 64%, 235 KB/s], Decompressed: 3945
Downloaded: 5609 file(s) [attempted 5610/8580 = 65%, 191 KB/s], Decompressed: 3945
Downloaded: 5653 file(s) [attempted 5654/8580 = 65%, 461 KB/s], Decompressed: 3945
Downloaded: 5685 file(s) [attempted 5686/8580 = 66%, 340 KB/s], Decompressed: 3945
Downloaded: 5728 file(s) [attempted 5729/8580 = 66%, 167 KB/s], Decompressed: 3945
Downloaded: 5778 file(s) [attempted 5779/8580 = 67%, 541 KB/s], Decompressed: 3945
Downloaded: 5819 file(s) [attempted 5820/8580 = 67%, 651 KB/s], Decompressed: 3945
Downloaded: 5866 file(s) [attempted 5867/8580 = 68%, 101 KB/s], Decompressed: 3945
Downloaded: 5914 file(s) [attempted 5915/8580 = 68%, 271 KB/s], Decompressed: 3945
Downloaded: 5964 file(s) [attempted 5965/8580 = 69%, 389 KB/s], Decompressed: 3945
Downloaded: 6012 file(s) [attempted 6013/8580 = 70%, 340 KB/s], Decompressed: 3945
Downloaded: 6052 file(s) [attempted 6053/8580 = 70%, 77 KB/s], Decompressed: 3945
Downloaded: 6093 file(s) [attempted 6094/8580 = 71%, 185 KB/s], Decompressed: 3945
Downloaded: 6130 file(s) [attempted 6131/8580 = 71%, 723 KB/s], Decompressed: 3945
Downloaded: 6174 file(s) [attempted 6175/8580 = 71%, 245 KB/s], Decompressed: 3945
Downloaded: 6215 file(s) [attempted 6216/8580 = 72%, 434 KB/s], Decompressed: 3945
Downloaded: 6259 file(s) [attempted 6260/8580 = 72%, 78 KB/s], Decompressed: 3945
Downloaded: 6299 file(s) [attempted 6300/8580 = 73%, 107 KB/s], Decompressed: 3945
Downloaded: 6336 file(s) [attempted 6337/8580 = 73%, 662 KB/s], Decompressed: 3945
Downloaded: 6377 file(s) [attempted 6378/8580 = 74%, 171 KB/s], Decompressed: 3945
Downloaded: 6421 file(s) [attempted 6422/8580 = 74%, 1451 KB/s], Decompressed: 3945
Downloaded: 6448 file(s) [attempted 6449/8580 = 75%, 113 KB/s], Decompressed: 3945
Downloaded: 6495 file(s) [attempted 6496/8580 = 75%, 35 KB/s], Decompressed: 3945
Downloaded: 6539 file(s) [attempted 6540/8580 = 76%, 1286 KB/s], Decompressed: 3945
Downloaded: 6580 file(s) [attempted 6581/8580 = 76%, 189 KB/s], Decompressed: 3945
Downloaded: 6624 file(s) [attempted 6625/8580 = 77%, 445 KB/s], Decompressed: 3945
Downloaded: 6668 file(s) [attempted 6669/8580 = 77%, 357 KB/s], Decompressed: 3945
Downloaded: 6704 file(s) [attempted 6706/8580 = 78%, 89 KB/s], Decompressed: 3945
Downloaded: 6748 file(s) [attempted 6750/8580 = 78%, 301 KB/s], Decompressed: 3945
Downloaded: 6785 file(s) [attempted 6787/8580 = 79%, 357 KB/s], Decompressed: 3945
Downloaded: 6829 file(s) [attempted 6831/8580 = 79%, 133 KB/s], Decompressed: 5149
Downloaded: 6873 file(s) [attempted 6875/8580 = 80%, 319 KB/s], Decompressed: 5149
Downloaded: 6921 file(s) [attempted 6923/8580 = 80%, 129 KB/s], Decompressed: 5149
Downloaded: 6958 file(s) [attempted 6960/8580 = 81%, 450 KB/s], Decompressed: 5149
Downloaded: 7001 file(s) [attempted 7004/8580 = 81%, 116 KB/s], Decompressed: 5149
Downloaded: 7041 file(s) [attempted 7044/8580 = 82%, 258 KB/s], Decompressed: 5149
Downloaded: 7089 file(s) [attempted 7092/8580 = 82%, 37 KB/s], Decompressed: 5149
Downloaded: 7136 file(s) [attempted 7139/8580 = 83%, 1864 KB/s], Decompressed: 5149
Downloaded: 7180 file(s) [attempted 7183/8580 = 83%, 47 KB/s], Decompressed: 5149
Downloaded: 7224 file(s) [attempted 7227/8580 = 84%, 53 KB/s], Decompressed: 5149
Downloaded: 7261 file(s) [attempted 7264/8580 = 84%, 308 KB/s], Decompressed: 5149
Downloaded: 7302 file(s) [attempted 7305/8580 = 85%, 203 KB/s], Decompressed: 5149
Downloaded: 7342 file(s) [attempted 7345/8580 = 85%, 97 KB/s], Decompressed: 5149
Downloaded: 7386 file(s) [attempted 7389/8580 = 86%, 278 KB/s], Decompressed: 5149
Downloaded: 7430 file(s) [attempted 7433/8580 = 86%, 240 KB/s], Decompressed: 5149
Downloaded: 7468 file(s) [attempted 7471/8580 = 87%, 61 KB/s], Decompressed: 5149
Downloaded: 7512 file(s) [attempted 7515/8580 = 87%, 43 KB/s], Decompressed: 5149
Downloaded: 7552 file(s) [attempted 7555/8580 = 88%, 176 KB/s], Decompressed: 5149
Downloaded: 7593 file(s) [attempted 7596/8580 = 88%, 1372 KB/s], Decompressed: 5149
Downloaded: 7633 file(s) [attempted 7636/8580 = 88%, 340 KB/s], Decompressed: 5149
Downloaded: 7676 file(s) [attempted 7680/8580 = 89%, 1 KB/s], Decompressed: 5149
Downloaded: 7717 file(s) [attempted 7721/8580 = 89%, 141 KB/s], Decompressed: 5149
Downloaded: 7754 file(s) [attempted 7758/8580 = 90%, 396 KB/s], Decompressed: 5149
Downloaded: 7795 file(s) [attempted 7799/8580 = 90%, 243 KB/s], Decompressed: 5149
Downloaded: 7842 file(s) [attempted 7846/8580 = 91%, 126 KB/s], Decompressed: 5149
Downloaded: 7883 file(s) [attempted 7887/8580 = 91%, 323 KB/s], Decompressed: 5149
Downloaded: 7927 file(s) [attempted 7931/8580 = 92%, 1101 KB/s], Decompressed: 5149
Downloaded: 7967 file(s) [attempted 7971/8580 = 92%, 34 KB/s], Decompressed: 5149
Downloaded: 8004 file(s) [attempted 8008/8580 = 93%, 547 KB/s], Decompressed: 5149
Downloaded: 8048 file(s) [attempted 8052/8580 = 93%, 384 KB/s], Decompressed: 5149
Downloaded: 8092 file(s) [attempted 8096/8580 = 94%, 371 KB/s], Decompressed: 5149
Downloaded: 8133 file(s) [attempted 8137/8580 = 94%, 233 KB/s], Decompressed: 5149
Downloaded: 8170 file(s) [attempted 8174/8580 = 95%, 431 KB/s], Decompressed: 5149
Downloaded: 8211 file(s) [attempted 8215/8580 = 95%, 380 KB/s], Decompressed: 5149
Downloaded: 8251 file(s) [attempted 8255/8580 = 96%, 184 KB/s], Decompressed: 5149
Downloaded: 8299 file(s) [attempted 8303/8580 = 96%, 115 KB/s], Decompressed: 5149
Downloaded: 8339 file(s) [attempted 8343/8580 = 97%, 191 KB/s], Decompressed: 5149
Downloaded: 8380 file(s) [attempted 8384/8580 = 97%, 608 KB/s], Decompressed: 5149
Downloaded: 8421 file(s) [attempted 8425/8580 = 98%, 629 KB/s], Decompressed: 5149
Downloaded: 8461 file(s) [attempted 8465/8580 = 98%, 80 KB/s], Decompressed: 5149
Downloaded: 8502 file(s) [attempted 8506/8580 = 99%, 93 KB/s], Decompressed: 5149
Downloaded: 8546 file(s) [attempted 8550/8580 = 99%, 1252 KB/s], Decompressed: 5149
Downloaded: 8576 file(s) [attempted 8580/8580 = 100%, 1252 KB/s], Decompressed: 5149

Downloaded: 1 file(s) [attempted 1/4 = 25%, 18 KB/s], Decompressed: 0
Downloaded: 3 file(s) [attempted 3/4 = 75%, 22 KB/s], Decompressed: 2
Downloaded: 4 file(s) [attempted 4/4 = 100%, 22 KB/s], Decompressed: 2

lean_checker exit 1 duration 14m 37s · created 6/29/2026, 1:19:48 AM

lake build

✔ [1/3] Built FLT.Assumptions.KnownIn1980s (482ms)
✔ [1957/1968] Built FLT.Assumptions.Mazur (14s)
✔ [2954/2967] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (2.4s)
✔ [2956/2967] Built FLT.Mathlib.Topology.Algebra.Group.Units (1.3s)
✔ [2958/2968] Built FLT.AutomorphicForm.GroupTheoryStuff (4.1s)
✔ [2960/2968] Built FLT.Mathlib.Order.Filter.Cofinite (1.0s)
✔ [2961/2968] Built FLT.Mathlib.Topology.Bases (1.0s)
✔ [2963/2974] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (1.8s)
✔ [2965/2974] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (2.8s)
✔ [2966/2974] Built FLT.Assumptions.Odlyzko (6.5s)
✔ [2968/2974] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (885ms)
✔ [2969/2974] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (1.4s)
✔ [2970/2974] Built FLT.Mathlib.Algebra.Algebra.Tower (1.2s)
✔ [2971/2975] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (4.8s)
✔ [2974/2981] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (6.0s)
✔ [3248/3255] Built FLT.Mathlib.Topology.Algebra.MulAction (1.0s)
✔ [3252/3257] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (5.8s)
✔ [3253/3257] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (7.2s)
✔ [3255/3267] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Algebra (1.4s)
✔ [3334/3342] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (2.0s)
✔ [3335/3342] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.1s)
✔ [3336/3342] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (2.0s)
✔ [3337/3347] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (6.6s)
✔ [3341/3347] Built FLT.Mathlib.LinearAlgebra.Countable (1.3s)
✔ [3343/3348] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (884ms)
✔ [3347/3355] Built FLT.DedekindDomain.AdicValuation (6.4s)
✔ [3354/3359] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (1.0s)
✔ [3364/3373] Built FLT.Mathlib.RingTheory.Localization.BaseChange (1.9s)
✔ [3365/3376] Built FLT.DedekindDomain.IntegralClosure (4.6s)
✔ [3372/3376] Built FLT.NumberField.HeightOneSpectrum (1.5s)
✔ [3373/3379] Built FLT.NumberField.Completion.Finite (2.3s)
✔ [3375/3387] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (2.2s)
✔ [3381/3387] Built FLT.Hacks.RightActionInstances (3.3s)
✔ [3385/3397] Built FLT.Mathlib.Topology.Algebra.Group.Basic (1.3s)
✔ [3386/3398] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (3.9s)
✔ [3388/3398] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (1.9s)
✔ [3389/3398] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (1.4s)
✔ [3390/3398] Built FLT.Mathlib.Topology.Instances.Matrix (1.3s)
✔ [3393/3407] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (1.2s)
✔ [3397/3407] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (1.2s)
✔ [3398/3407] Built FLT.Mathlib.MeasureTheory.Group.Action (2.1s)
✔ [3399/3407] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (1.2s)
✔ [3401/3407] Built FLT.Mathlib.GroupTheory.DoubleCoset (3.9s)
✔ [3402/3408] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (3.3s)
✔ [3403/3408] Built FLT.Mathlib.MeasureTheory.Group.Measure (1.4s)
✔ [3404/3408] Built FLT.AutomorphicForm.Stuff (2.6s)
✔ [3406/3408] Built FLT.QuaternionAlgebra.NumberField (12s)
✔ [3407/3422] Built FLT.AutomorphicForm.QuaternionAlgebra.Basic (36s)
✔ [3414/3422] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.0s)
✔ [3417/3422] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (1.4s)
✔ [3418/3422] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (1.6s)
✔ [3420/3424] Built FLT.HaarMeasure.HaarChar.AddEquiv (5.9s)
✔ [3422/3439] Built FLT.HaarMeasure.HaarChar.Ring (2.9s)
✔ [3427/3439] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (1.5s)
✔ [3428/3439] Built FLT.Mathlib.Algebra.Algebra.Hom (1.9s)
✔ [3430/3447] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (1.6s)
✔ [3431/3447] Built FLT.Mathlib.Topology.Algebra.UniformRing (1.2s)
✔ [3432/3447] Built FLT.Mathlib.Algebra.Algebra.Pi (1.2s)
✔ [3434/3447] Built FLT.Mathlib.Algebra.Algebra.Bilinear (1.8s)
✔ [3436/3447] Built FLT.Mathlib.Algebra.IsDirectLimit (1.9s)
✔ [3437/3447] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (1.5s)
✔ [3440/3451] Built FLT.Mathlib.LinearAlgebra.Pi (1.3s)
✔ [3442/3451] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (1.4s)
✔ [3444/3451] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (2.9s)
✔ [3446/3451] Built FLT.DedekindDomain.Completion.BaseChange (22s)
✔ [3447/3451] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (7.0s)
✔ [3448/3465] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (1.9s)
✔ [3451/3466] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (67s)
✔ [3453/3466] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (1.5s)
✔ [3454/3466] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (1.6s)
✔ [3455/3466] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (1.1s)
✔ [3456/3466] Built FLT.NumberField.InfinitePlace.Extension (2.6s)
✔ [3457/3466] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (1.4s)
✔ [3459/3469] Built FLT.Mathlib.Topology.Constructions (1.1s)
✔ [3461/3469] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (1.5s)
✔ [3464/3476] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (1.8s)
✔ [3465/3478] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (1.7s)
✔ [3467/3478] Built FLT.NumberField.Padics.RestrictedProduct (2.6s)
✔ [3468/3478] Built FLT.Mathlib.Data.Real.Archimedean (999ms)
✔ [3469/3478] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (1.3s)
✔ [3470/3478] Built FLT.NumberField.Completion.Infinite (16s)
✔ [3471/3478] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (1.7s)
✔ [3474/3481] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (1.7s)
✔ [3475/3481] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (5.8s)
✔ [3476/3487] Built FLT.NumberField.InfiniteAdeleRing (13s)
✔ [3478/3490] Built FLT.NumberField.AdeleRing (23s)
✔ [3481/3496] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (1.0s)
✔ [3483/3496] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (2.8s)
✔ [3485/3500] Built FLT.HaarMeasure.MeasurableSpacePadics (1.8s)
✔ [3487/3500] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (1.0s)
✔ [3488/3500] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (1.3s)
✔ [3489/3500] Built FLT.HaarMeasure.HaarChar.RealComplex (2.3s)
✔ [3490/3500] Built FLT.HaarMeasure.HaarChar.Padic (2.4s)
✔ [3491/3500] Built FLT.Mathlib.LinearAlgebra.Determinant (3.6s)
✔ [3493/3500] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.0s)
✔ [3494/3500] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (2.1s)
✔ [3495/3500] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (2.8s)
✔ [3496/3500] Built FLT.Mathlib.Algebra.Central.TensorProduct (1.9s)
✔ [3497/3500] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (5.7s)
✔ [3498/3501] Built FLT.HaarMeasure.HaarChar.AdeleRing (4.9s)
✔ [3499/3505] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (19s)
✔ [3510/3518] Built FLT.Mathlib.Topology.HomToDiscrete (1.5s)
✔ [3514/3518] Built FLT.Mathlib.Topology.Polish (1.4s)
✔ [3515/3518] Built FLT.Mathlib.MeasureTheory.Haar.Extension (2.0s)
✔ [3516/3520] Built FLT.DivisionAlgebra.Finiteness (41s)
✔ [3517/3522] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (2.4s)
✔ [3539/3547] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (2.5s)
✔ [3541/3547] Built FLT.Mathlib.FieldTheory.SplittingField.IsSplittingField (2.6s)
✔ [3545/3551] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (5.0s)
✔ [3547/3558] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (4.2s)
✔ [3557/3569] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (38s)
✖ [3568/3573] Building FLT.Mathlib.MeasureTheory.Group.ModularCharacter (7.4s)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/packages/checkdecls/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/lean /apx/source/FLT/Mathlib/MeasureTheory/Group/ModularCharacter.lean -o /apx/source/.lake/build/lib/lean/FLT/Mathlib/MeasureTheory/Group/ModularCharacter.olean -i /apx/source/.lake/build/lib/lean/FLT/Mathlib/MeasureTheory/Group/ModularCharacter.ilean -c /apx/source/.lake/build/ir/FLT/Mathlib/MeasureTheory/Group/ModularCharacter.c --setup /apx/source/.lake/build/ir/FLT/Mathlib/MeasureTheory/Group/ModularCharacter.setup.json --json
error: FLT/Mathlib/MeasureTheory/Group/ModularCharacter.lean:407:20: typeclass instance problem is stuck
  TopologicalSpace (Matrix ?m.54 ?m.54 ?m.55)

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `TopologicalSpace` contains metavariables. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
error: Lean exited with code 1
✔ [8709/8780] Built FLT.Data.Hurwitz (4.3s)
✔ [8710/8780] Built FLT.Data.QHat (5.0s)
✔ [8711/8780] Built FLT.Deformations.Algebra.InverseLimit.Basic (5.0s)
✔ [8712/8780] Built FLT.Patching.Utils.InverseLimit (1.1s)
✔ [8713/8780] Built FLT.Patching.Utils.Lemmas (4.1s)
✔ [8714/8780] Built FLT.Deformations.Lemmas (3.7s)
✔ [8715/8780] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.2s)
✔ [8716/8780] Built FLT.Deformations.Subfunctor (831ms)
✔ [8717/8780] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (1.2s)
✔ [8718/8780] Built FLT.Mathlib.RepresentationTheory.Basic (2.0s)
✔ [8719/8780] Built FLT.FreyCurve.FreyPackage (3.6s)
✔ [8720/8780] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (1.6s)
✔ [8721/8780] Built FLT.GlobalLanglandsConjectures.GLnDefs (8.4s)
✔ [8722/8780] Built FLT.GroupScheme.FiniteFlat (312ms)
✔ [8723/8780] Built FLT.HenselianLocalRing.EtaleDecomposition (13s)
✔ [8724/8780] Built FLT.HenselianLocalRing.Stuff (2.1s)
✔ [8725/8780] Built FLT.Mathlib.Algebra.FixedPoints.Basic (2.0s)
✔ [8726/8780] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (1.2s)
✔ [8727/8780] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.3s)
✔ [8728/8780] Built FLT.Mathlib.Data.Fin.Basic (830ms)
✔ [8729/8780] Built FLT.Mathlib.Data.Set.Prod (590ms)
✔ [8730/8780] Built FLT.Mathlib.GroupTheory.Index (920ms)
✔ [8731/8780] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.3s)
✔ [8732/8780] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.2s)
✔ [8733/8780] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.4s)
✔ [8734/8780] Built FLT.Mathlib.Topology.Algebra.Monoid (1.1s)
✔ [8735/8780] Built FLT.NumberField.DiscriminantBounds (2.8s)
✔ [8736/8780] Built FLT.Patching.Utils.TopologicallyFG (1.5s)
✔ [8737/8780] Built FLT.Patching.Utils.Depth (2.7s)
✔ [8738/8780] Built FLT.Patching.Utils.CompactHausdorffRings (2.1s)
✔ [8740/8780] Built FLT.TateCurve.TateCurve (274ms)
✔ [8741/8780] Built FLT.Data.HurwitzRatHat (2.0s)
✔ [8742/8780] Built FLT.GaloisRepresentation.Cyclotomic (1.7s)
✔ [8743/8780] Built FLT.Deformations.Algebra.InverseLimit.Topology (3.2s)
✔ [8744/8780] Built FLT.Patching.Utils.AdicTopology (3.2s)
✔ [8745/8780] Built FLT.Deformations.IsResidueAlgebra (1.7s)
✔ [8746/8780] Built FLT.Deformations.RepresentationTheory.IntegralClosure (2.0s)
✔ [8747/8780] Built FLT.Deformations.RepresentationTheory.Etale (8.4s)
✔ [8748/8780] Built FLT.Deformations.RepresentationTheory.Frobenius (2.1s)
✔ [8749/8780] Built FLT.Deformations.RepresentationTheory.Irreducible (1.4s)
✔ [8750/8780] Built FLT.GlobalLanglandsConjectures.GLzero (2.2s)
✔ [8751/8780] Built FLT.HenselianLocalRing.Finite (5.8s)
✔ [8752/8780] Built FLT.Mathlib.Topology.Algebra.Order.Field (2.2s)
✔ [8754/8780] Built FLT.Patching.Utils.StructureFiniteness (3.5s)
✔ [8755/8780] Built FLT.Deformations.IsProartinian (1.8s)
✔ [8756/8780] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (13s)
✔ [8757/8780] Built FLT.Patching.Ultraproduct (7.8s)
✔ [8758/8780] Built FLT.Deformations.Categories (2.9s)
✔ [8759/8780] Built FLT.Deformations.RepresentationTheory.GaloisRep (11s)
✔ [8760/8780] Built FLT.Patching.Algebra (9.8s)
✔ [8761/8780] Built FLT.Patching.VanishingFilter (2.6s)
✔ [8762/8780] Built FLT.Patching.Module (11s)
✔ [8763/8780] Built FLT.Deformations.LiftFunctor (3.7s)
✔ [8764/8780] Built FLT.GaloisRepresentation.Automorphic (4.2s)
✔ [8765/8780] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.4s)
✔ [8766/8780] Built FLT.EllipticCurve.Torsion (2.2s)
✔ [8767/8780] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (1.9s)
✔ [8768/8780] Built FLT.Patching.Over (12s)
✔ [8769/8780] Built FLT.Deformations.Representable (2.7s)
✔ [8770/8780] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (2.0s)
✔ [8771/8780] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (1.0s)
✔ [8772/8780] Built FLT.GaloisRepresentation.HardlyRamified.Lift (1.0s)
✔ [8773/8780] Built FLT.GaloisRepresentation.HardlyRamified.Frey (1.9s)
✔ [8774/8780] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.2s)
✔ [8775/8780] Built FLT.Patching.System (9.6s)
✔ [8776/8780] Built FLT.FreyCurve.Contradiction (1.8s)
✔ [8777/8780] Built FLT.Patching.REqualsT (3.9s)
Some required targets logged failures:
- FLT.Mathlib.MeasureTheory.Group.ModularCharacter

error: build failed

blueprint_build exit 1 duration 8s · created 6/29/2026, 1:19:48 AM

lake build :blueprint

error: unknown package facet `blueprint`