Verification run

Run 37

ImperialCollegeLondon/FLT branch main triggered via poller

failed commit 8bfa71aed90f toolchain lean-v4-32-0-rc1 prover lean took 2h 36m · finished 2w ago

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset) failed with exit code 1 (toolchain lean-v4-32-0-rc1, command: <command argv unavailable>)

Open project

Package inputs

This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.

Trust verification

Recomputes trust checks from the recorded attestations, manifest, and command history.

(verification not run)

Manifest

Loads the published files manifest and location metadata for this job.

(manifest not loaded)

Verifier log excerpt

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


$ git checkout 8bfa71aed90f8eeb8edda2fc0729e29eb65318c9
exit_code=Some(0) duration_ms=46
stderr:
Note: switching to '8bfa71aed90f8eeb8edda2fc0729e29eb65318c9'.

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 8bfa71a chore: bump mathlib to 059f3b6, fix breaking changes (#1046)

Resolved source revision: 8bfa71aed90f8eeb8edda2fc0729e29eb65318c9

Detected prover: lean
Detected requested toolchain: lean-v4-32-0-rc1
Materialized Lean semantic helper assets
Prepared source: revision=8bfa71aed90f8eeb8edda2fc0729e29eb65318c9 provenance={"branch":"main","checked_out_revision":"8bfa71aed90f8eeb8edda2fc0729e29eb65318c9","clone_url_hash":"26972c4fa07707e04a8d064eb61ea9ced3487bda0b6c5e8ecd8face933c5481e","credential_mode":"none","local_clone":false,"requested_commit_sha":"8bfa71aed90f8eeb8edda2fc0729e29eb65318c9","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: computed 184 module hash fact(s) from source and olean files; skipping Lean module-facts probe
Lean semantic module cache: 173/184 module hit(s), 11 miss(es)
Lean semantic module cache: stable superset runner maps 11 missing module(s) to 6 weighted target group(s) capped at target weight 32, but will attempt them in one Lean invocation
Lean semantic module cache: trying stable superset runner for 11 missing module(s) with 184 imported module candidate(s)
Lean semantic module cache: stable superset runner target set maps to 6 weighted batch(es), but will run in one Lean invocation so the superset import is paid once
Lean semantic module cache: stable superset runner failed with import_failure after checkpointing 1 completed module(s); falling back for 10 remaining module(s)
Lean semantic module cache: stable superset runner fell back to exact-module batches
Lean semantic module cache: capping exact extraction batch extract-batch-00000 at 3600s; total exact budget remaining is 43200s
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00000
Lean semantic module cache: capping exact extraction batch extract-batch-00001 at 3600s; total exact budget remaining is 42797s
Lean semantic module cache: extraction batch extract-batch-00001 failed for module FLT/QuaternionAlgebra/NumberField.lean; continuing with remaining modules
Lean semantic module cache: extraction batch extract-batch-00001 did not fully complete; continuing with remaining batches
Lean semantic module cache: capping exact extraction batch extract-batch-00002 at 3600s; total exact budget remaining is 42281s
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00002
Lean semantic module cache: capping exact extraction batch extract-batch-00003 at 3600s; total exact budget remaining is 41880s
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00003
Lean semantic module cache: capping exact extraction batch extract-batch-00004 at 3600s; total exact budget remaining is 41550s
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00004
Lean semantic module cache: capping exact extraction batch extract-batch-00005 at 3600s; total exact budget remaining is 41227s
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00005
Lean semantic module cache: capping exact extraction batch extract-batch-00006 at 3600s; total exact budget remaining is 40903s
Lean semantic module cache: extraction batch extract-batch-00006 failed for module FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean; continuing with remaining modules
Lean semantic module cache: extraction batch extract-batch-00006 did not fully complete; continuing with remaining batches
Lean semantic module cache: capping exact extraction batch extract-batch-00007 at 3600s; total exact budget remaining is 40337s
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00007
Lean semantic module cache: capping exact extraction batch extract-batch-00008 at 3600s; total exact budget remaining is 39894s
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00008
Lean semantic module cache: capping exact extraction batch extract-batch-00009 at 3600s; total exact budget remaining is 39539s
Lean semantic module cache: checkpointed 1 module fragment row(s) from batch extract-batch-00009
Lean semantic module cache: extracted 8 module fragment(s) before one or more module failures; leaving full semantic response unwritten

$ lake exe cache get
exit_code=Some(0) duration_ms=123251
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
Decompressed 8580 file(s)
Already decompressed 8580 file(s)

stderr:
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '059f3b6cd2acee40e6db108d5c9946ae2d0efa29'
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 (351ms)
✔ [3/11] Built Cache.Lean (378ms)
✔ [6/11] Built Cache.Infra (411ms)
✔ [7/12] Built Cache.IO (1.5s)
✔ [9/26] Built Cache.Hashing (829ms)
✔ [10/26] Built Cache.Requests (1.0s)
✔ [11/26] Built Cache.Cli:c.o (1.4s)
✔ [12/26] Built Cache.Lean:c.o (130ms)
✔ [14/26] Built Cache.IO:c.o (1.2s)
✔ [15/26] Built Cache.Hashing:c.o (342ms)
✔ [16/26] Built Cache.Infra:c.o (170ms)
✔ [17/26] Built Cache.Requests:c.o (2.1s)
✔ [18/26] Built Cache.Marker (648ms)
✔ [19/26] Built Cache.Marker:c.o (98ms)
✔ [20/26] Built Cache.Query (701ms)
✔ [21/26] Built Cache.Query:c.o (222ms)
✔ [22/26] Built Cache.Warning (707ms)
✔ [23/26] Built Cache.Warning:c.o (236ms)
✔ [24/26] Built Cache.Main (1.4s)
✔ [25/26] Built Cache.Main:c.o (726ms)
✔ [26/26] Built cache:exe (5.4s)

Downloaded: 1 file(s) [attempted 1/8580 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 18 file(s) [attempted 18/8580 = 0%, 1 KB/s], Decompressed: 15
Downloaded: 40 file(s) [attempted 40/8580 = 0%, 22 KB/s], Decompressed: 27
Downloaded: 64 file(s) [attempted 64/8580 = 0%, 147 KB/s], Decompressed: 53
Downloaded: 84 file(s) [attempted 84/8580 = 0%, 304 KB/s], Decompressed: 74
Downloaded: 119 file(s) [attempted 119/8580 = 1%, 335 KB/s], Decompressed: 98
Downloaded: 149 file(s) [attempted 149/8580 = 1%, 341 KB/s], Decompressed: 112
Downloaded: 183 file(s) [attempted 183/8580 = 2%, 47 KB/s], Decompressed: 167
Downloaded: 221 file(s) [attempted 221/8580 = 2%, 93 KB/s], Decompressed: 190
Downloaded: 258 file(s) [attempted 258/8580 = 3%, 242 KB/s], Decompressed: 231
Downloaded: 295 file(s) [attempted 295/8580 = 3%, 699 KB/s], Decompressed: 255
Downloaded: 338 file(s) [attempted 338/8580 = 3%, 139 KB/s], Decompressed: 316
Downloaded: 373 file(s) [attempted 373/8580 = 4%, 187 KB/s], Decompressed: 336
Downloaded: 407 file(s) [attempted 407/8580 = 4%, 237 KB/s], Decompressed: 383
Downloaded: 444 file(s) [attempted 444/8580 = 5%, 1622 KB/s], Decompressed: 420
Downloaded: 488 file(s) [attempted 488/8580 = 5%, 1114 KB/s], Decompressed: 458
Downloaded: 529 file(s) [attempted 529/8580 = 6%, 622 KB/s], Decompressed: 488
Downloaded: 569 file(s) [attempted 569/8580 = 6%, 555 KB/s], Decompressed: 488
Downloaded: 603 file(s) [attempted 603/8580 = 7%, 261 KB/s], Decompressed: 525
Downloaded: 647 file(s) [attempted 647/8580 = 7%, 279 KB/s], Decompressed: 573
Downloaded: 688 file(s) [attempted 688/8580 = 8%, 65 KB/s], Decompressed: 617
Downloaded: 729 file(s) [attempted 729/8580 = 8%, 45 KB/s], Decompressed: 657
Downloaded: 769 file(s) [attempted 769/8580 = 8%, 162 KB/s], Decompressed: 735
Downloaded: 806 file(s) [attempted 806/8580 = 9%, 549 KB/s], Decompressed: 766
Downloaded: 847 file(s) [attempted 847/8580 = 9%, 1144 KB/s], Decompressed: 796
Downloaded: 894 file(s) [attempted 894/8580 = 10%, 971 KB/s], Decompressed: 830
Downloaded: 932 file(s) [attempted 932/8580 = 10%, 144 KB/s], Decompressed: 874
Downloaded: 969 file(s) [attempted 969/8580 = 11%, 33 KB/s], Decompressed: 918
Downloaded: 1013 file(s) [attempted 1013/8580 = 11%, 102 KB/s], Decompressed: 962
Downloaded: 1047 file(s) [attempted 1047/8580 = 12%, 360 KB/s], Decompressed: 999
Downloaded: 1091 file(s) [attempted 1091/8580 = 12%, 121 KB/s], Decompressed: 1037
Downloaded: 1125 file(s) [attempted 1125/8580 = 13%, 350 KB/s], Decompressed: 1070
Downloaded: 1165 file(s) [attempted 1165/8580 = 13%, 161 KB/s], Decompressed: 1114
Downloaded: 1206 file(s) [attempted 1206/8580 = 14%, 59 KB/s], Decompressed: 1162
Downloaded: 1243 file(s) [attempted 1243/8580 = 14%, 404 KB/s], Decompressed: 1162
Downloaded: 1280 file(s) [attempted 1280/8580 = 14%, 611 KB/s], Decompressed: 1206
Downloaded: 1317 file(s) [attempted 1317/8580 = 15%, 187 KB/s], Decompressed: 1250
Downloaded: 1366 file(s) [attempted 1366/8580 = 15%, 135 KB/s], Decompressed: 1294
Downloaded: 1402 file(s) [attempted 1402/8580 = 16%, 179 KB/s], Decompressed: 1338
Downloaded: 1439 file(s) [attempted 1439/8580 = 16%, 659 KB/s], Decompressed: 1385
Downloaded: 1476 file(s) [attempted 1476/8580 = 17%, 697 KB/s], Decompressed: 1422
Downloaded: 1517 file(s) [attempted 1517/8580 = 17%, 40 KB/s], Decompressed: 1487
Downloaded: 1561 file(s) [attempted 1561/8580 = 18%, 1054 KB/s], Decompressed: 1517
Downloaded: 1598 file(s) [attempted 1598/8580 = 18%, 166 KB/s], Decompressed: 1547
Downloaded: 1642 file(s) [attempted 1642/8580 = 19%, 80 KB/s], Decompressed: 1608
Downloaded: 1679 file(s) [attempted 1679/8580 = 19%, 347 KB/s], Decompressed: 1642
Downloaded: 1723 file(s) [attempted 1723/8580 = 20%, 1491 KB/s], Decompressed: 1676
Downloaded: 1767 file(s) [attempted 1767/8580 = 20%, 234 KB/s], Decompressed: 1713
Downloaded: 1805 file(s) [attempted 1805/8580 = 21%, 66 KB/s], Decompressed: 1747
Downloaded: 1842 file(s) [attempted 1842/8580 = 21%, 446 KB/s], Decompressed: 1784
Downloaded: 1882 file(s) [attempted 1882/8580 = 21%, 1919 KB/s], Decompressed: 1825
Downloaded: 1926 file(s) [attempted 1926/8580 = 22%, 77 KB/s], Decompressed: 1825
Downloaded: 1967 file(s) [attempted 1967/8580 = 22%, 452 KB/s], Decompressed: 1872
Downloaded: 2007 file(s) [attempted 2007/8580 = 23%, 1320 KB/s], Decompressed: 1872
Downloaded: 2045 file(s) [attempted 2045/8580 = 23%, 769 KB/s], Decompressed: 1872
Downloaded: 2082 file(s) [attempted 2082/8580 = 24%, 105 KB/s], Decompressed: 1960
Downloaded: 2126 file(s) [attempted 2126/8580 = 24%, 1669 KB/s], Decompressed: 1960
Downloaded: 2170 file(s) [attempted 2170/8580 = 25%, 488 KB/s], Decompressed: 1960
Downloaded: 2204 file(s) [attempted 2204/8580 = 25%, 524 KB/s], Decompressed: 2068
Downloaded: 2238 file(s) [attempted 2238/8580 = 26%, 68 KB/s], Decompressed: 2068
Downloaded: 2278 file(s) [attempted 2278/8580 = 26%, 470 KB/s], Decompressed: 2068
Downloaded: 2325 file(s) [attempted 2325/8580 = 27%, 207 KB/s], Decompressed: 2200
Downloaded: 2369 file(s) [attempted 2369/8580 = 27%, 181 KB/s], Decompressed: 2200
Downloaded: 2407 file(s) [attempted 2407/8580 = 28%, 435 KB/s], Decompressed: 2200
Downloaded: 2440 file(s) [attempted 2440/8580 = 28%, 124 KB/s], Decompressed: 2200
Downloaded: 2481 file(s) [attempted 2481/8580 = 28%, 371 KB/s], Decompressed: 2325
Downloaded: 2522 file(s) [attempted 2522/8580 = 29%, 367 KB/s], Decompressed: 2325
Downloaded: 2562 file(s) [attempted 2562/8580 = 29%, 1105 KB/s], Decompressed: 2325
Downloaded: 2603 file(s) [attempted 2603/8580 = 30%, 434 KB/s], Decompressed: 2457
Downloaded: 2637 file(s) [attempted 2637/8580 = 30%, 142 KB/s], Decompressed: 2457
Downloaded: 2681 file(s) [attempted 2681/8580 = 31%, 248 KB/s], Decompressed: 2457
Downloaded: 2721 file(s) [attempted 2721/8580 = 31%, 132 KB/s], Decompressed: 2457
Downloaded: 2755 file(s) [attempted 2755/8580 = 32%, 509 KB/s], Decompressed: 2589
Downloaded: 2792 file(s) [attempted 2792/8580 = 32%, 645 KB/s], Decompressed: 2589
Downloaded: 2836 file(s) [attempted 2836/8580 = 33%, 129 KB/s], Decompressed: 2589
Downloaded: 2880 file(s) [attempted 2880/8580 = 33%, 107 KB/s], Decompressed: 2725
Downloaded: 2921 file(s) [attempted 2921/8580 = 34%, 305 KB/s], Decompressed: 2725
Downloaded: 2958 file(s) [attempted 2958/8580 = 34%, 32 KB/s], Decompressed: 2725
Downloaded: 3002 file(s) [attempted 3002/8580 = 34%, 208 KB/s], Decompressed: 2860
Downloaded: 3039 file(s) [attempted 3039/8580 = 35%, 389 KB/s], Decompressed: 2860
Downloaded: 3083 file(s) [attempted 3083/8580 = 35%, 158 KB/s], Decompressed: 2860
Downloaded: 3127 file(s) [attempted 3127/8580 = 36%, 381 KB/s], Decompressed: 2860
Downloaded: 3164 file(s) [attempted 3164/8580 = 36%, 178 KB/s], Decompressed: 2995
Downloaded: 3205 file(s) [attempted 3205/8580 = 37%, 69 KB/s], Decompressed: 2995
Downloaded: 3246 file(s) [attempted 3246/8580 = 37%, 595 KB/s], Decompressed: 2995
Downloaded: 3290 file(s) [attempted 3290/8580 = 38%, 587 KB/s], Decompressed: 3134
Downloaded: 3327 file(s) [attempted 3327/8580 = 38%, 371 KB/s], Decompressed: 3134
Downloaded: 3367 file(s) [attempted 3367/8580 = 39%, 89 KB/s], Decompressed: 3134
Downloaded: 3408 file(s) [attempted 3408/8580 = 39%, 849 KB/s], Decompressed: 3134
Downloaded: 3445 file(s) [attempted 3445/8580 = 40%, 206 KB/s], Decompressed: 3286
Downloaded: 3492 file(s) [attempted 3492/8580 = 40%, 176 KB/s], Decompressed: 3286
Downloaded: 3535 file(s) [attempted 3535/8580 = 41%, 101 KB/s], Decompressed: 3286
Downloaded: 3567 file(s) [attempted 3567/8580 = 41%, 152 KB/s], Decompressed: 3286
Downloaded: 3604 file(s) [attempted 3604/8580 = 42%, 216 KB/s], Decompressed: 3442
Downloaded: 3645 file(s) [attempted 3645/8580 = 42%, 592 KB/s], Decompressed: 3442
Downloaded: 3685 file(s) [attempted 3685/8580 = 42%, 105 KB/s], Decompressed: 3442
Downloaded: 3723 file(s) [attempted 3723/8580 = 43%, 386 KB/s], Decompressed: 3442
Downloaded: 3763 file(s) [attempted 3763/8580 = 43%, 159 KB/s], Decompressed: 3601
Downloaded: 3800 file(s) [attempted 3800/8580 = 44%, 62 KB/s], Decompressed: 3601
Downloaded: 3841 file(s) [attempted 3841/8580 = 44%, 347 KB/s], Decompressed: 3601
Downloaded: 3882 file(s) [attempted 3882/8580 = 45%, 23 KB/s], Decompressed: 3601
Downloaded: 3922 file(s) [attempted 3922/8580 = 45%, 89 KB/s], Decompressed: 3601
Downloaded: 3963 file(s) [attempted 3963/8580 = 46%, 131 KB/s], Decompressed: 3601
Downloaded: 4000 file(s) [attempted 4000/8580 = 46%, 218 KB/s], Decompressed: 3763
Downloaded: 4037 file(s) [attempted 4037/8580 = 47%, 53 KB/s], Decompressed: 3763
Downloaded: 4074 file(s) [attempted 4074/8580 = 47%, 236 KB/s], Decompressed: 3763
Downloaded: 4115 file(s) [attempted 4115/8580 = 47%, 1059 KB/s], Decompressed: 3763
Downloaded: 4159 file(s) [attempted 4159/8580 = 48%, 159 KB/s], Decompressed: 3763
Downloaded: 4200 file(s) [attempted 4200/8580 = 48%, 68 KB/s], Decompressed: 3983
Downloaded: 4233 file(s) [attempted 4233/8580 = 49%, 24 KB/s], Decompressed: 3983
Downloaded: 4274 file(s) [attempted 4274/8580 = 49%, 299 KB/s], Decompressed: 3983
Downloaded: 4315 file(s) [attempted 4315/8580 = 50%, 54 KB/s], Decompressed: 3983
Downloaded: 4359 file(s) [attempted 4359/8580 = 50%, 1201 KB/s], Decompressed: 3983
Downloaded: 4402 file(s) [attempted 4402/8580 = 51%, 366 KB/s], Decompressed: 3983
Downloaded: 4440 file(s) [attempted 4440/8580 = 51%, 846 KB/s], Decompressed: 4196
Downloaded: 4470 file(s) [attempted 4470/8580 = 52%, 1143 KB/s], Decompressed: 4196
Downloaded: 4514 file(s) [attempted 4514/8580 = 52%, 506 KB/s], Decompressed: 4196
Downloaded: 4561 file(s) [attempted 4561/8580 = 53%, 127 KB/s], Decompressed: 4196
Downloaded: 4602 file(s) [attempted 4602/8580 = 53%, 56 KB/s], Decompressed: 4196
Downloaded: 4643 file(s) [attempted 4643/8580 = 54%, 465 KB/s], Decompressed: 4196
Downloaded: 4676 file(s) [attempted 4676/8580 = 54%, 835 KB/s], Decompressed: 4423
Downloaded: 4714 file(s) [attempted 4714/8580 = 54%, 353 KB/s], Decompressed: 4423
Downloaded: 4758 file(s) [attempted 4758/8580 = 55%, 211 KB/s], Decompressed: 4423
Downloaded: 4798 file(s) [attempted 4798/8580 = 55%, 611 KB/s], Decompressed: 4423
Downloaded: 4846 file(s) [attempted 4846/8580 = 56%, 76 KB/s], Decompressed: 4423
Downloaded: 4886 file(s) [attempted 4886/8580 = 56%, 277 KB/s], Decompressed: 4423
Downloaded: 4920 file(s) [attempted 4920/8580 = 57%, 174 KB/s], Decompressed: 4656
Downloaded: 4954 file(s) [attempted 4954/8580 = 57%, 41 KB/s], Decompressed: 4656
Downloaded: 4998 file(s) [attempted 4998/8580 = 58%, 76 KB/s], Decompressed: 4656
Downloaded: 5042 file(s) [attempted 5042/8580 = 58%, 298 KB/s], Decompressed: 4656
Downloaded: 5079 file(s) [attempted 5079/8580 = 59%, 191 KB/s], Decompressed: 4656
Downloaded: 5116 file(s) [attempted 5116/8580 = 59%, 114 KB/s], Decompressed: 4656
Downloaded: 5150 file(s) [attempted 5150/8580 = 60%, 58 KB/s], Decompressed: 4896
Downloaded: 5194 file(s) [attempted 5194/8580 = 60%, 94 KB/s], Decompressed: 4896
Downloaded: 5235 file(s) [attempted 5235/8580 = 61%, 432 KB/s], Decompressed: 4896
Downloaded: 5275 file(s) [attempted 5275/8580 = 61%, 492 KB/s], Decompressed: 4896
Downloaded: 5312 file(s) [attempted 5312/8580 = 61%, 200 KB/s], Decompressed: 4896
Downloaded: 5350 file(s) [attempted 5350/8580 = 62%, 292 KB/s], Decompressed: 4896
Downloaded: 5390 file(s) [attempted 5390/8580 = 62%, 158 KB/s], Decompressed: 5140
Downloaded: 5434 file(s) [attempted 5434/8580 = 63%, 560 KB/s], Decompressed: 5140
Downloaded: 5475 file(s) [attempted 5475/8580 = 63%, 219 KB/s], Decompressed: 5140
Downloaded: 5512 file(s) [attempted 5512/8580 = 64%, 288 KB/s], Decompressed: 5140
Downloaded: 5546 file(s) [attempted 5546/8580 = 64%, 883 KB/s], Decompressed: 5140
Downloaded: 5587 file(s) [attempted 5587/8580 = 65%, 62 KB/s], Decompressed: 5140
Downloaded: 5634 file(s) [attempted 5634/8580 = 65%, 415 KB/s], Decompressed: 5370
Downloaded: 5681 file(s) [attempted 5681/8580 = 66%, 1779 KB/s], Decompressed: 5370
Downloaded: 5725 file(s) [attempted 5725/8580 = 66%, 122 KB/s], Decompressed: 5370
Downloaded: 5766 file(s) [attempted 5766/8580 = 67%, 66 KB/s], Decompressed: 5370
Downloaded: 5800 file(s) [attempted 5800/8580 = 67%, 218 KB/s], Decompressed: 5370
Downloaded: 5837 file(s) [attempted 5837/8580 = 68%, 36 KB/s], Decompressed: 5370
Downloaded: 5881 file(s) [attempted 5881/8580 = 68%, 133 KB/s], Decompressed: 5607
Downloaded: 5928 file(s) [attempted 5928/8580 = 69%, 677 KB/s], Decompressed: 5607
Downloaded: 5969 file(s) [attempted 5969/8580 = 69%, 87 KB/s], Decompressed: 5607
Downloaded: 6013 file(s) [attempted 6013/8580 = 70%, 673 KB/s], Decompressed: 5607
Downloaded: 6053 file(s) [attempted 6053/8580 = 70%, 74 KB/s], Decompressed: 5607
Downloaded: 6091 file(s) [attempted 6091/8580 = 70%, 52 KB/s], Decompressed: 5607
Downloaded: 6131 file(s) [attempted 6131/8580 = 71%, 364 KB/s], Decompressed: 5607
Downloaded: 6173 file(s) [attempted 6173/8580 = 71%, 1491 KB/s], Decompressed: 5881
Downloaded: 6206 file(s) [attempted 6206/8580 = 72%, 277 KB/s], Decompressed: 5881
Downloaded: 6246 file(s) [attempted 6246/8580 = 72%, 44 KB/s], Decompressed: 5881
Downloaded: 6287 file(s) [attempted 6287/8580 = 73%, 160 KB/s], Decompressed: 5881
Downloaded: 6327 file(s) [attempted 6327/8580 = 73%, 207 KB/s], Decompressed: 5881
Downloaded: 6371 file(s) [attempted 6371/8580 = 74%, 106 KB/s], Decompressed: 5881
Downloaded: 6415 file(s) [attempted 6415/8580 = 74%, 630 KB/s], Decompressed: 5881
Downloaded: 6446 file(s) [attempted 6446/8580 = 75%, 44 KB/s], Decompressed: 6162
Downloaded: 6490 file(s) [attempted 6490/8580 = 75%, 56 KB/s], Decompressed: 6162
Downloaded: 6530 file(s) [attempted 6530/8580 = 76%, 151 KB/s], Decompressed: 6162
Downloaded: 6571 file(s) [attempted 6571/8580 = 76%, 244 KB/s], Decompressed: 6162
Downloaded: 6611 file(s) [attempted 6611/8580 = 77%, 419 KB/s], Decompressed: 6162
Downloaded: 6652 file(s) [attempted 6652/8580 = 77%, 230 KB/s], Decompressed: 6162
Downloaded: 6689 file(s) [attempted 6689/8580 = 77%, 1352 KB/s], Decompressed: 6162
Downloaded: 6733 file(s) [attempted 6733/8580 = 78%, 62 KB/s], Decompressed: 6162
Downloaded: 6774 file(s) [attempted 6774/8580 = 78%, 359 KB/s], Decompressed: 6442
Downloaded: 6818 file(s) [attempted 6818/8580 = 79%, 130 KB/s], Decompressed: 6442
Downloaded: 6858 file(s) [attempted 6858/8580 = 79%, 798 KB/s], Decompressed: 6442
Downloaded: 6892 file(s) [attempted 6892/8580 = 80%, 71 KB/s], Decompressed: 6442
Downloaded: 6933 file(s) [attempted 6933/8580 = 80%, 236 KB/s], Decompressed: 6442
Downloaded: 6973 file(s) [attempted 6973/8580 = 81%, 196 KB/s], Decompressed: 6442
Downloaded: 7014 file(s) [attempted 7014/8580 = 81%, 216 KB/s], Decompressed: 6442
Downloaded: 7061 file(s) [attempted 7061/8580 = 82%, 156 KB/s], Decompressed: 6442
Downloaded: 7102 file(s) [attempted 7102/8580 = 82%, 166 KB/s], Decompressed: 6770
Downloaded: 7132 file(s) [attempted 7132/8580 = 83%, 80 KB/s], Decompressed: 6770
Downloaded: 7176 file(s) [attempted 7176/8580 = 83%, 1193 KB/s], Decompressed: 6770
Downloaded: 7217 file(s) [attempted 7217/8580 = 84%, 45 KB/s], Decompressed: 6770
Downloaded: 7264 file(s) [attempted 7264/8580 = 84%, 303 KB/s], Decompressed: 6770
Downloaded: 7308 file(s) [attempted 7308/8580 = 85%, 24 KB/s], Decompressed: 6770
Downloaded: 7349 file(s) [attempted 7349/8580 = 85%, 1113 KB/s], Decompressed: 6770
Downloaded: 7386 file(s) [attempted 7386/8580 = 86%, 58 KB/s], Decompressed: 7078
Downloaded: 7420 file(s) [attempted 7420/8580 = 86%, 170 KB/s], Decompressed: 7078
Downloaded: 7467 file(s) [attempted 7467/8580 = 87%, 146 KB/s], Decompressed: 7078
Downloaded: 7508 file(s) [attempted 7508/8580 = 87%, 1846 KB/s], Decompressed: 7078
Downloaded: 7548 file(s) [attempted 7548/8580 = 87%, 105 KB/s], Decompressed: 7078
Downloaded: 7589 file(s) [attempted 7589/8580 = 88%, 141 KB/s], Decompressed: 7078
Downloaded: 7623 file(s) [attempted 7623/8580 = 88%, 481 KB/s], Decompressed: 7078
Downloaded: 7663 file(s) [attempted 7663/8580 = 89%, 594 KB/s], Decompressed: 7078
Downloaded: 7701 file(s) [attempted 7701/8580 = 89%, 160 KB/s], Decompressed: 7078
Downloaded: 7738 file(s) [attempted 7738/8580 = 90%, 128 KB/s], Decompressed: 7373
Downloaded: 7779 file(s) [attempted 7779/8580 = 90%, 94 KB/s], Decompressed: 7373
Downloaded: 7812 file(s) [attempted 7812/8580 = 91%, 45 KB/s], Decompressed: 7373
Downloaded: 7850 file(s) [attempted 7850/8580 = 91%, 236 KB/s], Decompressed: 7373
Downloaded: 7894 file(s) [attempted 7894/8580 = 92%, 115 KB/s], Decompressed: 7373
Downloaded: 7934 file(s) [attempted 7934/8580 = 92%, 133 KB/s], Decompressed: 7373
Downloaded: 7975 file(s) [attempted 7975/8580 = 92%, 692 KB/s], Decompressed: 7373
Downloaded: 8009 file(s) [attempted 8009/8580 = 93%, 1231 KB/s], Decompressed: 7373
Downloaded: 8049 file(s) [attempted 8049/8580 = 93%, 106 KB/s], Decompressed: 7711
Downloaded: 8093 file(s) [attempted 8093/8580 = 94%, 360 KB/s], Decompressed: 7711
Downloaded: 8134 file(s) [attempted 8134/8580 = 94%, 227 KB/s], Decompressed: 7711
Downloaded: 8178 file(s) [attempted 8178/8580 = 95%, 172 KB/s], Decompressed: 7711
Downloaded: 8218 file(s) [attempted 8218/8580 = 95%, 54 KB/s], Decompressed: 7711
Downloaded: 8255 file(s) [attempted 8255/8580 = 96%, 73 KB/s], Decompressed: 7711
Downloaded: 8293 file(s) [attempted 8293/8580 = 96%, 52 KB/s], Decompressed: 7711
Downloaded: 8333 file(s) [attempted 8333/8580 = 97%, 102 KB/s], Decompressed: 7711
Downloaded: 8374 file(s) [attempted 8374/8580 = 97%, 78 KB/s], Decompressed: 7711
Downloaded: 8414 file(s) [attempted 8414/8580 = 98%, 257 KB/s], Decompressed: 8046
Downloaded: 8452 file(s) [attempted 8452/8580 = 98%, 85 KB/s], Decompressed: 8046
Downloaded: 8492 file(s) [attempted 8492/8580 = 98%, 743 KB/s], Decompressed: 8046
Downloaded: 8529 file(s) [attempted 8529/8580 = 99%, 132 KB/s], Decompressed: 8046
Downloaded: 8570 file(s) [attempted 8570/8580 = 99%, 168 KB/s], Decompressed: 8046
Downloaded: 8580 file(s) [attempted 8580/8580 = 100%, 168 KB/s], Decompressed: 8046


$ lake build
exit_code=Some(0) duration_ms=1087940
stdout:
✔ [1/21] Built FLT.Assumptions.KnownIn1980s (357ms)
✔ [1957/1960] Built FLT.Assumptions.Mazur (11s)
✔ [2954/2967] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (2.0s)
✔ [2956/2967] Built FLT.Mathlib.Topology.Algebra.Group.Units (945ms)
✔ [2958/2968] Built FLT.AutomorphicForm.GroupTheoryStuff (3.7s)
✔ [2960/2968] Built FLT.Mathlib.Order.Filter.Cofinite (826ms)
✔ [2961/2968] Built FLT.Mathlib.Topology.Bases (918ms)
✔ [2963/2974] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (1.6s)
✔ [2965/2974] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (2.7s)
✔ [2966/2974] Built FLT.Assumptions.Odlyzko (4.8s)
✔ [2968/2974] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (911ms)
✔ [2969/2974] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (1.5s)
✔ [2970/2974] Built FLT.Mathlib.Algebra.Algebra.Tower (1.3s)
✔ [2971/2975] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (4.0s)
✔ [2974/2991] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (5.8s)
✔ [3246/3255] Built FLT.Mathlib.Topology.Algebra.MulAction (1.1s)
✔ [3252/3257] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (4.9s)
✔ [3253/3257] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (7.1s)
✔ [3255/3273] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Algebra (1.3s)
✔ [3334/3342] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (1.8s)
✔ [3335/3342] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.0s)
✔ [3336/3342] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (2.0s)
✔ [3337/3347] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (6.5s)
✔ [3341/3348] Built FLT.Mathlib.LinearAlgebra.Countable (1.2s)
✔ [3345/3349] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (890ms)
✔ [3347/3355] Built FLT.DedekindDomain.AdicValuation (6.0s)
✔ [3354/3373] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (1.0s)
✔ [3364/3373] Built FLT.Mathlib.RingTheory.Localization.BaseChange (1.8s)
✔ [3369/3376] Built FLT.DedekindDomain.IntegralClosure (4.9s)
✔ [3372/3378] Built FLT.NumberField.HeightOneSpectrum (1.5s)
✔ [3373/3379] Built FLT.NumberField.Completion.Finite (2.3s)
✔ [3376/3387] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (2.3s)
✔ [3381/3387] Built FLT.Hacks.RightActionInstances (3.5s)
✔ [3382/3387] Built FLT.Mathlib.Topology.Algebra.Group.Basic (1.3s)
✔ [3386/3398] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (3.8s)
✔ [3388/3398] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (1.9s)
✔ [3389/3398] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (1.5s)
✔ [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.1s)
✔ [3401/3407] Built FLT.Mathlib.GroupTheory.DoubleCoset (3.8s)
✔ [3402/3407] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (3.4s)
✔ [3403/3408] Built FLT.Mathlib.MeasureTheory.Group.Measure (1.3s)
✔ [3404/3408] Built FLT.AutomorphicForm.Stuff (2.4s)
✔ [3406/3408] Built FLT.QuaternionAlgebra.NumberField (12s)
✔ [3407/3422] Built FLT.AutomorphicForm.QuaternionAlgebra.Basic (36s)
✔ [3414/3422] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.1s)
✔ [3417/3422] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (1.3s)
✔ [3419/3424] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (1.5s)
✔ [3420/3424] Built FLT.HaarMeasure.HaarChar.AddEquiv (5.7s)
✔ [3422/3431] Built FLT.HaarMeasure.HaarChar.Ring (2.5s)
✔ [3427/3439] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (1.4s)
✔ [3428/3439] Built FLT.Mathlib.Algebra.Algebra.Hom (1.9s)
✔ [3430/3447] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (1.5s)
✔ [3431/3447] Built FLT.Mathlib.Topology.Algebra.UniformRing (1.2s)
✔ [3432/3447] Built FLT.Mathlib.Algebra.Algebra.Pi (1.3s)
✔ [3434/3447] Built FLT.Mathlib.Algebra.Algebra.Bilinear (1.0s)
✔ [3436/3447] Built FLT.Mathlib.Algebra.IsDirectLimit (1.8s)
✔ [3437/3447] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (1.7s)
✔ [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.0s)
✔ [3446/3451] Built FLT.DedekindDomain.Completion.BaseChange (22s)
✔ [3447/3451] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (7.1s)
✔ [3448/3465] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (1.8s)
✔ [3451/3466] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (67s)
✔ [3453/3466] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (1.4s)
✔ [3454/3466] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (1.5s)
✔ [3455/3466] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (1.1s)
✔ [3456/3466] Built FLT.NumberField.InfinitePlace.Extension (2.5s)
✔ [3457/3466] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (1.4s)
✔ [3459/3469] Built FLT.Mathlib.Topology.Constructions (996ms)
✔ [3462/3469] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (1.4s)
✔ [3464/3469] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (1.8s)
✔ [3465/3478] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (1.6s)
✔ [3466/3478] Built FLT.NumberField.Completion.Infinite (15s)
✔ [3468/3478] Built FLT.NumberField.Padics.RestrictedProduct (2.5s)
✔ [3469/3478] Built FLT.Mathlib.Data.Real.Archimedean (937ms)
✔ [3470/3478] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (1.3s)
✔ [3471/3478] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (1.6s)
✔ [3474/3481] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (1.7s)
✔ [3475/3481] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (5.7s)
✔ [3476/3487] Built FLT.NumberField.InfiniteAdeleRing (13s)
✔ [3478/3490] Built FLT.NumberField.AdeleRing (22s)
✔ [3481/3496] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (1.9s)
✔ [3483/3496] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (2.8s)
✔ [3485/3500] Built FLT.HaarMeasure.MeasurableSpacePadics (1.9s)
✔ [3487/3500] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (1.1s)
✔ [3488/3500] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (1.3s)
✔ [3489/3500] Built FLT.HaarMeasure.HaarChar.RealComplex (2.2s)
✔ [3490/3500] Built FLT.HaarMeasure.HaarChar.Padic (2.4s)
✔ [3491/3500] Built FLT.Mathlib.LinearAlgebra.Determinant (3.7s)
✔ [3493/3500] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.1s)
✔ [3494/3500] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (2.2s)
✔ [3495/3500] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (2.6s)
✔ [3496/3500] Built FLT.Mathlib.Algebra.Central.TensorProduct (1.9s)
✔ [3497/3500] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (5.8s)
✔ [3498/3501] Built FLT.HaarMeasure.HaarChar.AdeleRing (4.4s)
✔ [3499/3505] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (18s)
✔ [3510/3518] Built FLT.Mathlib.Topology.HomToDiscrete (1.5s)
✔ [3514/3518] Built FLT.Mathlib.Topology.Polish (1.3s)
✔ [3515/3518] Built FLT.Mathlib.MeasureTheory.Haar.Extension (2.1s)
✔ [3516/3520] Built FLT.DivisionAlgebra.Finiteness (39s)
✔ [3517/3523] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (2.3s)
✔ [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 (4.3s)
✔ [3547/3558] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (4.1s)
✔ [3557/3560] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (37s)
✔ [3568/3570] Built FLT.Mathlib.MeasureTheory.Group.ModularCharacter (7.6s)
✔ [3569/3576] Built FLT.HaarMeasure.Quotient (3.8s)
✔ [3648/3655] Built FLT.HaarMeasure.FiniteAdeleRing (5.4s)
✔ [8709/8780] Built FLT.Data.Hurwitz (3.5s)
✔ [8710/8780] Built FLT.Data.QHat (5.4s)
✔ [8711/8780] Built FLT.Deformations.Algebra.InverseLimit.Basic (5.3s)
✔ [8712/8780] Built FLT.Patching.Utils.InverseLimit (1.1s)
✔ [8713/8780] Built FLT.Patching.Utils.Lemmas (3.6s)
✔ [8714/8780] Built FLT.Deformations.Lemmas (3.4s)
✔ [8715/8780] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.1s)
✔ [8716/8780] Built FLT.Deformations.Subfunctor (834ms)
✔ [8717/8780] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (1.2s)
✔ [8718/8780] Built FLT.Mathlib.RepresentationTheory.Basic (2.1s)
✔ [8719/8780] Built FLT.FreyCurve.FreyPackage (2.8s)
✔ [8720/8780] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (1.5s)
✔ [8721/8780] Built FLT.GlobalLanglandsConjectures.GLnDefs (8.1s)
✔ [8722/8780] Built FLT.GroupScheme.FiniteFlat (266ms)
✔ [8723/8780] Built FLT.HenselianLocalRing.EtaleDecomposition (12s)
✔ [8724/8780] Built FLT.HenselianLocalRing.Stuff (1.9s)
✔ [8725/8780] Built FLT.Mathlib.Algebra.FixedPoints.Basic (1.9s)
✔ [8726/8780] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (1.1s)
✔ [8727/8780] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.3s)
✔ [8728/8780] Built FLT.Mathlib.Data.Fin.Basic (815ms)
✔ [8729/8780] Built FLT.Mathlib.Data.Set.Prod (594ms)
✔ [8730/8780] Built FLT.Mathlib.GroupTheory.Index (978ms)
✔ [8731/8780] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.2s)
✔ [8732/8780] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.2s)
✔ [8733/8780] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.2s)
✔ [8734/8780] Built FLT.Mathlib.Topology.Algebra.Monoid (1.1s)
✔ [8735/8780] Built FLT.NumberField.DiscriminantBounds (2.4s)
✔ [8736/8780] Built FLT.Patching.Utils.TopologicallyFG (1.4s)
✔ [8737/8780] Built FLT.Patching.Utils.Depth (2.7s)
✔ [8738/8780] Built FLT.Patching.Utils.CompactHausdorffRings (2.1s)
✔ [8740/8780] Built FLT.TateCurve.TateCurve (298ms)
✔ [8741/8780] Built FLT.Data.HurwitzRatHat (2.1s)
✔ [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.1s)
✔ [8745/8780] Built FLT.Deformations.IsResidueAlgebra (1.8s)
✔ [8746/8780] Built FLT.Deformations.RepresentationTheory.IntegralClosure (1.9s)
✔ [8747/8780] Built FLT.Deformations.RepresentationTheory.Etale (8.5s)
✔ [8748/8780] Built FLT.Deformations.RepresentationTheory.Frobenius (2.1s)
✔ [8749/8780] Built FLT.Deformations.RepresentationTheory.Irreducible (1.3s)
✔ [8750/8780] Built FLT.GlobalLanglandsConjectures.GLzero (1.8s)
✔ [8751/8780] Built FLT.HenselianLocalRing.Finite (4.9s)
✔ [8752/8780] Built FLT.Mathlib.Topology.Algebra.Order.Field (2.1s)
✔ [8753/8780] Built FLT.Patching.Utils.StructureFiniteness (3.4s)
✔ [8754/8780] Built FLT.AutomorphicForm.QuaternionAlgebra.InnerProduct (57s)
✔ [8755/8780] Built FLT.Deformations.IsProartinian (1.7s)
✔ [8756/8780] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (13s)
✔ [8757/8780] Built FLT.Patching.Ultraproduct (7.9s)
✔ [8758/8780] Built FLT.Deformations.Categories (2.9s)
✔ [8759/8780] Built FLT.Deformations.RepresentationTheory.GaloisRep (11s)
✔ [8760/8780] Built FLT.Patching.Algebra (9.5s)
✔ [8761/8780] Built FLT.Patching.VanishingFilter (2.5s)
✔ [8762/8780] Built FLT.Patching.Module (11s)
✔ [8763/8780] Built FLT.Deformations.LiftFunctor (3.5s)
✔ [8764/8780] Built FLT.GaloisRepresentation.Automorphic (3.9s)
✔ [8765/8780] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.5s)
✔ [8766/8780] Built FLT.EllipticCurve.Torsion (2.1s)
✔ [8767/8780] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (1.8s)
✔ [8768/8780] Built FLT.Patching.Over (11s)
✔ [8769/8780] Built FLT.Deformations.Representable (2.5s)
✔ [8770/8780] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (1.8s)
✔ [8771/8780] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (1.8s)
✔ [8772/8780] Built FLT.GaloisRepresentation.HardlyRamified.Lift (1.8s)
✔ [8773/8780] Built FLT.GaloisRepresentation.HardlyRamified.Frey (1.7s)
✔ [8774/8780] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.0s)
✔ [8775/8780] Built FLT.Patching.System (9.5s)
✔ [8776/8780] Built FLT.FreyCurve.Contradiction (1.7s)
✔ [8777/8780] Built FLT.Patching.REqualsT (3.8s)
✔ [8778/8780] Built FLT (2.0s)
✔ [8779/8780] Built FermatsLastTheorem (186s)
Build completed successfully (8780 jobs).


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


blueprint_build failed; continuing (non-fatal phase).

$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)
exit_code=Some(1) duration_ms=1949104
stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":43376}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":4407,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 8c482a2f24e4ea14c2be87c192355c4352bb046ff534e5fe86f395fb8ae9c4cc
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":62,"runner_cache_hit":true}
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1900376,"ok":false}
lean semantic helper failed: generated static runner exited non-zero
remediation: inspect the generated repository runner and imported root modules


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
exit_code=Some(0) duration_ms=402949
stdout:
apx-semantic-phase	{"duration_ms":23,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":26,"diagnostic_count":8,"duration_ms":1917,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":26,"dependency_count":28,"diagnostic_count":46,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":306775,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":26,"dependency_count":28,"diagnostic_count":46,"duration_ms":113,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":999111,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":6,"ok":true,"payload_bytes":999111,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1344,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":28,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":88262,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache e229f92da80b09ecb21d2e16f814ce547b8c210bca3fd2f1b913d0262f0244da
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":312399,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
exit_code=Some(137) duration_ms=516554
stdout:
apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":163,"diagnostic_count":86,"duration_ms":19159,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":163,"dependency_count":745,"diagnostic_count":1367,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":468908,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":163,"dependency_count":745,"diagnostic_count":1367,"duration_ms":6719,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":769738786,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1612,"ok":true,"payload_bytes":769738786,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":249,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache cfae54b19702e39775998d4a4530367ffaf0454dac7c4891721321f7a3fd6de4
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":39,"runner_cache_hit":true}
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":504721,"ok":true}
/apx/source/.apodeixis/tools/lean-semantic-extract.sh: line 383: 10110 Killed                  python3 <<'PY'
import hashlib
import json
import os
import pathlib
import sys

request_path = pathlib.Path(os.environ["APX_LEAN_HELPER_REQUEST_PATH"])
response_path = pathlib.Path(os.environ["APX_LEAN_HELPER_RESPONSE_PATH"])

with request_path.open("r", encoding="utf-8") as handle:
    request = json.load(handle)

if request.get("operation") != "extract_repository_semantics":
    raise SystemExit(0)

with response_path.open("r", encoding="utf-8") as handle:
    response = json.load(handle)

if "helper" not in response:
    raise SystemExit(0)

helper = response.get("helper")
helper_version = response.get("helper_version")

if not helper or helper_version in (None, ""):
    print(
        "lean semantic extractor failed: repository semantics response is missing helper metadata required for normalization",
        file=sys.stderr,
    )
    raise SystemExit(1)

without_checksum = {k: v for k, v in response.items() if k != "checksum"}
canonical = json.dumps(without_checksum, sort_keys=True, separators=(",", ":"), ensure_ascii=False)
response["checksum"] = hashlib.sha256(canonical.encode("utf-8")).hexdigest()

tmp_path = pathlib.Path(f"{response_path}.tmp")
with tmp_path.open("w", encoding="utf-8") as handle:
    json.dump(response, handle, sort_keys=True, separators=(",", ":"), ensure_ascii=False)
os.replace(tmp_path, response_path)
PY



$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
exit_code=Some(0) duration_ms=400657
stdout:
apx-semantic-phase	{"duration_ms":17,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":99,"diagnostic_count":52,"duration_ms":7902,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":99,"dependency_count":464,"diagnostic_count":1414,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":304902,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":99,"dependency_count":464,"diagnostic_count":1414,"duration_ms":1235,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":110549709,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":83,"ok":true,"payload_bytes":110549709,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":570,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":77769,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 2ab56cb015eb785ed07034add1350d210ab18c01645232489190b7368d00e000
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":318758,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)
exit_code=Some(0) duration_ms=329990
stdout:
apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":178,"diagnostic_count":116,"duration_ms":12614,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":178,"dependency_count":551,"diagnostic_count":2186,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":302877,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":178,"dependency_count":551,"diagnostic_count":2186,"duration_ms":716,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":37846658,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":27,"ok":true,"payload_bytes":37846658,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":233,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":7779,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 024b47d071e6a1d68ac450abbf05a2abc990fed42f4f262fc8a833a2fb7f43d7
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":320315,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)
exit_code=Some(0) duration_ms=322429
stdout:
apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":58,"diagnostic_count":46,"duration_ms":4726,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":58,"dependency_count":112,"diagnostic_count":46,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":304628,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":58,"dependency_count":112,"diagnostic_count":46,"duration_ms":649,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":68346489,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":62,"ok":true,"payload_bytes":68346489,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":286,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":5663,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 4b5969385b39e67ee424aee21eeba0fcdf220e9b224773ff62705fb5d20514b8
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":314391,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)
exit_code=Some(0) duration_ms=324281
stdout:
apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":26,"diagnostic_count":16,"duration_ms":1826,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":26,"dependency_count":62,"diagnostic_count":465,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":308193,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":26,"dependency_count":62,"diagnostic_count":465,"duration_ms":244,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":15596493,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":10,"ok":true,"payload_bytes":15596493,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":310,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":8927,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 324704e13ca54a61679cf24b8134b1cc5d55fa33575e8ba619ec8a0ed91d62e9
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":314017,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006)
exit_code=Some(1) duration_ms=566089
stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":20}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":99,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":21,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":4597,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache add9abc3203c65105be67be28e03225b6b2805a513c9fb8163923127d21648bd
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":560750,"ok":false}
lean semantic helper failed: generated static runner exited non-zero
remediation: inspect the generated repository runner and imported root modules


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007)
exit_code=Some(0) duration_ms=442223
stdout:
apx-semantic-phase	{"duration_ms":18,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":26,"diagnostic_count":12,"duration_ms":2240,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":26,"dependency_count":26,"diagnostic_count":25,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":326215,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":26,"dependency_count":26,"diagnostic_count":25,"duration_ms":498,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":72279073,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":58,"ok":true,"payload_bytes":72279073,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1327,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":105212,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 0cd980907453956ffc5e14bdf1a057935c20a4c0e6abec4ebdc0aefa62ed638a
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":332932,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00008)
exit_code=Some(0) duration_ms=354976
stdout:
apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":246,"diagnostic_count":135,"duration_ms":19770,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":246,"dependency_count":983,"diagnostic_count":1922,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":317889,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":246,"dependency_count":983,"diagnostic_count":1922,"duration_ms":2000,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":174946227,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":181,"ok":true,"payload_bytes":174946227,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":12}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":243,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":12,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3540,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 8d12888e4eb4af384bb800a855b9692f9111a509092a6b21652243a9cdb2c1db
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":345501,"ok":true}


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00009)
exit_code=Some(0) duration_ms=2239292
stdout:
apx-semantic-phase	{"duration_ms":246,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":218,"diagnostic_count":105,"duration_ms":32078,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":218,"dependency_count":617,"diagnostic_count":2242,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":1402867,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":218,"dependency_count":617,"diagnostic_count":2242,"duration_ms":2554,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":194195460,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":159,"ok":true,"payload_bytes":194195460,"phase":"lean_json_write"}

stderr:
apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":426,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":380091,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 6bbce7152ff7d200fcdcdd653b0a23662dbf321c826ed5e1e145ffefc1af1e63
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1852437,"ok":true}

Stored Lean workspace build cache
Mirrored 8 Lean dependency package snapshot(s)
Created 8 shared Lean git mirror(s)

Command runs

git_clone exit 0 duration 1s · created 6/30/2026, 3:15:46 PM

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

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

git_checkout exit 0 duration 46 ms · created 6/30/2026, 3:15:46 PM

git checkout 8bfa71aed90f8eeb8edda2fc0729e29eb65318c9

Note: switching to '8bfa71aed90f8eeb8edda2fc0729e29eb65318c9'.

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 8bfa71a chore: bump mathlib to 059f3b6, fix breaking changes (#1046)

lake_cache exit 0 duration 2m 3s · created 6/30/2026, 3:15:46 PM

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
Decompressed 8580 file(s)
Already decompressed 8580 file(s)

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '059f3b6cd2acee40e6db108d5c9946ae2d0efa29'
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 (351ms)
✔ [3/11] Built Cache.Lean (378ms)
✔ [6/11] Built Cache.Infra (411ms)
✔ [7/12] Built Cache.IO (1.5s)
✔ [9/26] Built Cache.Hashing (829ms)
✔ [10/26] Built Cache.Requests (1.0s)
✔ [11/26] Built Cache.Cli:c.o (1.4s)
✔ [12/26] Built Cache.Lean:c.o (130ms)
✔ [14/26] Built Cache.IO:c.o (1.2s)
✔ [15/26] Built Cache.Hashing:c.o (342ms)
✔ [16/26] Built Cache.Infra:c.o (170ms)
✔ [17/26] Built Cache.Requests:c.o (2.1s)
✔ [18/26] Built Cache.Marker (648ms)
✔ [19/26] Built Cache.Marker:c.o (98ms)
✔ [20/26] Built Cache.Query (701ms)
✔ [21/26] Built Cache.Query:c.o (222ms)
✔ [22/26] Built Cache.Warning (707ms)
✔ [23/26] Built Cache.Warning:c.o (236ms)
✔ [24/26] Built Cache.Main (1.4s)
✔ [25/26] Built Cache.Main:c.o (726ms)
✔ [26/26] Built cache:exe (5.4s)

Downloaded: 1 file(s) [attempted 1/8580 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 18 file(s) [attempted 18/8580 = 0%, 1 KB/s], Decompressed: 15
Downloaded: 40 file(s) [attempted 40/8580 = 0%, 22 KB/s], Decompressed: 27
Downloaded: 64 file(s) [attempted 64/8580 = 0%, 147 KB/s], Decompressed: 53
Downloaded: 84 file(s) [attempted 84/8580 = 0%, 304 KB/s], Decompressed: 74
Downloaded: 119 file(s) [attempted 119/8580 = 1%, 335 KB/s], Decompressed: 98
Downloaded: 149 file(s) [attempted 149/8580 = 1%, 341 KB/s], Decompressed: 112
Downloaded: 183 file(s) [attempted 183/8580 = 2%, 47 KB/s], Decompressed: 167
Downloaded: 221 file(s) [attempted 221/8580 = 2%, 93 KB/s], Decompressed: 190
Downloaded: 258 file(s) [attempted 258/8580 = 3%, 242 KB/s], Decompressed: 231
Downloaded: 295 file(s) [attempted 295/8580 = 3%, 699 KB/s], Decompressed: 255
Downloaded: 338 file(s) [attempted 338/8580 = 3%, 139 KB/s], Decompressed: 316
Downloaded: 373 file(s) [attempted 373/8580 = 4%, 187 KB/s], Decompressed: 336
Downloaded: 407 file(s) [attempted 407/8580 = 4%, 237 KB/s], Decompressed: 383
Downloaded: 444 file(s) [attempted 444/8580 = 5%, 1622 KB/s], Decompressed: 420
Downloaded: 488 file(s) [attempted 488/8580 = 5%, 1114 KB/s], Decompressed: 458
Downloaded: 529 file(s) [attempted 529/8580 = 6%, 622 KB/s], Decompressed: 488
Downloaded: 569 file(s) [attempted 569/8580 = 6%, 555 KB/s], Decompressed: 488
Downloaded: 603 file(s) [attempted 603/8580 = 7%, 261 KB/s], Decompressed: 525
Downloaded: 647 file(s) [attempted 647/8580 = 7%, 279 KB/s], Decompressed: 573
Downloaded: 688 file(s) [attempted 688/8580 = 8%, 65 KB/s], Decompressed: 617
Downloaded: 729 file(s) [attempted 729/8580 = 8%, 45 KB/s], Decompressed: 657
Downloaded: 769 file(s) [attempted 769/8580 = 8%, 162 KB/s], Decompressed: 735
Downloaded: 806 file(s) [attempted 806/8580 = 9%, 549 KB/s], Decompressed: 766
Downloaded: 847 file(s) [attempted 847/8580 = 9%, 1144 KB/s], Decompressed: 796
Downloaded: 894 file(s) [attempted 894/8580 = 10%, 971 KB/s], Decompressed: 830
Downloaded: 932 file(s) [attempted 932/8580 = 10%, 144 KB/s], Decompressed: 874
Downloaded: 969 file(s) [attempted 969/8580 = 11%, 33 KB/s], Decompressed: 918
Downloaded: 1013 file(s) [attempted 1013/8580 = 11%, 102 KB/s], Decompressed: 962
Downloaded: 1047 file(s) [attempted 1047/8580 = 12%, 360 KB/s], Decompressed: 999
Downloaded: 1091 file(s) [attempted 1091/8580 = 12%, 121 KB/s], Decompressed: 1037
Downloaded: 1125 file(s) [attempted 1125/8580 = 13%, 350 KB/s], Decompressed: 1070
Downloaded: 1165 file(s) [attempted 1165/8580 = 13%, 161 KB/s], Decompressed: 1114
Downloaded: 1206 file(s) [attempted 1206/8580 = 14%, 59 KB/s], Decompressed: 1162
Downloaded: 1243 file(s) [attempted 1243/8580 = 14%, 404 KB/s], Decompressed: 1162
Downloaded: 1280 file(s) [attempted 1280/8580 = 14%, 611 KB/s], Decompressed: 1206
Downloaded: 1317 file(s) [attempted 1317/8580 = 15%, 187 KB/s], Decompressed: 1250
Downloaded: 1366 file(s) [attempted 1366/8580 = 15%, 135 KB/s], Decompressed: 1294
Downloaded: 1402 file(s) [attempted 1402/8580 = 16%, 179 KB/s], Decompressed: 1338
Downloaded: 1439 file(s) [attempted 1439/8580 = 16%, 659 KB/s], Decompressed: 1385
Downloaded: 1476 file(s) [attempted 1476/8580 = 17%, 697 KB/s], Decompressed: 1422
Downloaded: 1517 file(s) [attempted 1517/8580 = 17%, 40 KB/s], Decompressed: 1487
Downloaded: 1561 file(s) [attempted 1561/8580 = 18%, 1054 KB/s], Decompressed: 1517
Downloaded: 1598 file(s) [attempted 1598/8580 = 18%, 166 KB/s], Decompressed: 1547
Downloaded: 1642 file(s) [attempted 1642/8580 = 19%, 80 KB/s], Decompressed: 1608
Downloaded: 1679 file(s) [attempted 1679/8580 = 19%, 347 KB/s], Decompressed: 1642
Downloaded: 1723 file(s) [attempted 1723/8580 = 20%, 1491 KB/s], Decompressed: 1676
Downloaded: 1767 file(s) [attempted 1767/8580 = 20%, 234 KB/s], Decompressed: 1713
Downloaded: 1805 file(s) [attempted 1805/8580 = 21%, 66 KB/s], Decompressed: 1747
Downloaded: 1842 file(s) [attempted 1842/8580 = 21%, 446 KB/s], Decompressed: 1784
Downloaded: 1882 file(s) [attempted 1882/8580 = 21%, 1919 KB/s], Decompressed: 1825
Downloaded: 1926 file(s) [attempted 1926/8580 = 22%, 77 KB/s], Decompressed: 1825
Downloaded: 1967 file(s) [attempted 1967/8580 = 22%, 452 KB/s], Decompressed: 1872
Downloaded: 2007 file(s) [attempted 2007/8580 = 23%, 1320 KB/s], Decompressed: 1872
Downloaded: 2045 file(s) [attempted 2045/8580 = 23%, 769 KB/s], Decompressed: 1872
Downloaded: 2082 file(s) [attempted 2082/8580 = 24%, 105 KB/s], Decompressed: 1960
Downloaded: 2126 file(s) [attempted 2126/8580 = 24%, 1669 KB/s], Decompressed: 1960
Downloaded: 2170 file(s) [attempted 2170/8580 = 25%, 488 KB/s], Decompressed: 1960
Downloaded: 2204 file(s) [attempted 2204/8580 = 25%, 524 KB/s], Decompressed: 2068
Downloaded: 2238 file(s) [attempted 2238/8580 = 26%, 68 KB/s], Decompressed: 2068
Downloaded: 2278 file(s) [attempted 2278/8580 = 26%, 470 KB/s], Decompressed: 2068
Downloaded: 2325 file(s) [attempted 2325/8580 = 27%, 207 KB/s], Decompressed: 2200
Downloaded: 2369 file(s) [attempted 2369/8580 = 27%, 181 KB/s], Decompressed: 2200
Downloaded: 2407 file(s) [attempted 2407/8580 = 28%, 435 KB/s], Decompressed: 2200
Downloaded: 2440 file(s) [attempted 2440/8580 = 28%, 124 KB/s], Decompressed: 2200
Downloaded: 2481 file(s) [attempted 2481/8580 = 28%, 371 KB/s], Decompressed: 2325
Downloaded: 2522 file(s) [attempted 2522/8580 = 29%, 367 KB/s], Decompressed: 2325
Downloaded: 2562 file(s) [attempted 2562/8580 = 29%, 1105 KB/s], Decompressed: 2325
Downloaded: 2603 file(s) [attempted 2603/8580 = 30%, 434 KB/s], Decompressed: 2457
Downloaded: 2637 file(s) [attempted 2637/8580 = 30%, 142 KB/s], Decompressed: 2457
Downloaded: 2681 file(s) [attempted 2681/8580 = 31%, 248 KB/s], Decompressed: 2457
Downloaded: 2721 file(s) [attempted 2721/8580 = 31%, 132 KB/s], Decompressed: 2457
Downloaded: 2755 file(s) [attempted 2755/8580 = 32%, 509 KB/s], Decompressed: 2589
Downloaded: 2792 file(s) [attempted 2792/8580 = 32%, 645 KB/s], Decompressed: 2589
Downloaded: 2836 file(s) [attempted 2836/8580 = 33%, 129 KB/s], Decompressed: 2589
Downloaded: 2880 file(s) [attempted 2880/8580 = 33%, 107 KB/s], Decompressed: 2725
Downloaded: 2921 file(s) [attempted 2921/8580 = 34%, 305 KB/s], Decompressed: 2725
Downloaded: 2958 file(s) [attempted 2958/8580 = 34%, 32 KB/s], Decompressed: 2725
Downloaded: 3002 file(s) [attempted 3002/8580 = 34%, 208 KB/s], Decompressed: 2860
Downloaded: 3039 file(s) [attempted 3039/8580 = 35%, 389 KB/s], Decompressed: 2860
Downloaded: 3083 file(s) [attempted 3083/8580 = 35%, 158 KB/s], Decompressed: 2860
Downloaded: 3127 file(s) [attempted 3127/8580 = 36%, 381 KB/s], Decompressed: 2860
Downloaded: 3164 file(s) [attempted 3164/8580 = 36%, 178 KB/s], Decompressed: 2995
Downloaded: 3205 file(s) [attempted 3205/8580 = 37%, 69 KB/s], Decompressed: 2995
Downloaded: 3246 file(s) [attempted 3246/8580 = 37%, 595 KB/s], Decompressed: 2995
Downloaded: 3290 file(s) [attempted 3290/8580 = 38%, 587 KB/s], Decompressed: 3134
Downloaded: 3327 file(s) [attempted 3327/8580 = 38%, 371 KB/s], Decompressed: 3134
Downloaded: 3367 file(s) [attempted 3367/8580 = 39%, 89 KB/s], Decompressed: 3134
Downloaded: 3408 file(s) [attempted 3408/8580 = 39%, 849 KB/s], Decompressed: 3134
Downloaded: 3445 file(s) [attempted 3445/8580 = 40%, 206 KB/s], Decompressed: 3286
Downloaded: 3492 file(s) [attempted 3492/8580 = 40%, 176 KB/s], Decompressed: 3286
Downloaded: 3535 file(s) [attempted 3535/8580 = 41%, 101 KB/s], Decompressed: 3286
Downloaded: 3567 file(s) [attempted 3567/8580 = 41%, 152 KB/s], Decompressed: 3286
Downloaded: 3604 file(s) [attempted 3604/8580 = 42%, 216 KB/s], Decompressed: 3442
Downloaded: 3645 file(s) [attempted 3645/8580 = 42%, 592 KB/s], Decompressed: 3442
Downloaded: 3685 file(s) [attempted 3685/8580 = 42%, 105 KB/s], Decompressed: 3442
Downloaded: 3723 file(s) [attempted 3723/8580 = 43%, 386 KB/s], Decompressed: 3442
Downloaded: 3763 file(s) [attempted 3763/8580 = 43%, 159 KB/s], Decompressed: 3601
Downloaded: 3800 file(s) [attempted 3800/8580 = 44%, 62 KB/s], Decompressed: 3601
Downloaded: 3841 file(s) [attempted 3841/8580 = 44%, 347 KB/s], Decompressed: 3601
Downloaded: 3882 file(s) [attempted 3882/8580 = 45%, 23 KB/s], Decompressed: 3601
Downloaded: 3922 file(s) [attempted 3922/8580 = 45%, 89 KB/s], Decompressed: 3601
Downloaded: 3963 file(s) [attempted 3963/8580 = 46%, 131 KB/s], Decompressed: 3601
Downloaded: 4000 file(s) [attempted 4000/8580 = 46%, 218 KB/s], Decompressed: 3763
Downloaded: 4037 file(s) [attempted 4037/8580 = 47%, 53 KB/s], Decompressed: 3763
Downloaded: 4074 file(s) [attempted 4074/8580 = 47%, 236 KB/s], Decompressed: 3763
Downloaded: 4115 file(s) [attempted 4115/8580 = 47%, 1059 KB/s], Decompressed: 3763
Downloaded: 4159 file(s) [attempted 4159/8580 = 48%, 159 KB/s], Decompressed: 3763
Downloaded: 4200 file(s) [attempted 4200/8580 = 48%, 68 KB/s], Decompressed: 3983
Downloaded: 4233 file(s) [attempted 4233/8580 = 49%, 24 KB/s], Decompressed: 3983
Downloaded: 4274 file(s) [attempted 4274/8580 = 49%, 299 KB/s], Decompressed: 3983
Downloaded: 4315 file(s) [attempted 4315/8580 = 50%, 54 KB/s], Decompressed: 3983
Downloaded: 4359 file(s) [attempted 4359/8580 = 50%, 1201 KB/s], Decompressed: 3983
Downloaded: 4402 file(s) [attempted 4402/8580 = 51%, 366 KB/s], Decompressed: 3983
Downloaded: 4440 file(s) [attempted 4440/8580 = 51%, 846 KB/s], Decompressed: 4196
Downloaded: 4470 file(s) [attempted 4470/8580 = 52%, 1143 KB/s], Decompressed: 4196
Downloaded: 4514 file(s) [attempted 4514/8580 = 52%, 506 KB/s], Decompressed: 4196
Downloaded: 4561 file(s) [attempted 4561/8580 = 53%, 127 KB/s], Decompressed: 4196
Downloaded: 4602 file(s) [attempted 4602/8580 = 53%, 56 KB/s], Decompressed: 4196
Downloaded: 4643 file(s) [attempted 4643/8580 = 54%, 465 KB/s], Decompressed: 4196
Downloaded: 4676 file(s) [attempted 4676/8580 = 54%, 835 KB/s], Decompressed: 4423
Downloaded: 4714 file(s) [attempted 4714/8580 = 54%, 353 KB/s], Decompressed: 4423
Downloaded: 4758 file(s) [attempted 4758/8580 = 55%, 211 KB/s], Decompressed: 4423
Downloaded: 4798 file(s) [attempted 4798/8580 = 55%, 611 KB/s], Decompressed: 4423
Downloaded: 4846 file(s) [attempted 4846/8580 = 56%, 76 KB/s], Decompressed: 4423
Downloaded: 4886 file(s) [attempted 4886/8580 = 56%, 277 KB/s], Decompressed: 4423
Downloaded: 4920 file(s) [attempted 4920/8580 = 57%, 174 KB/s], Decompressed: 4656
Downloaded: 4954 file(s) [attempted 4954/8580 = 57%, 41 KB/s], Decompressed: 4656
Downloaded: 4998 file(s) [attempted 4998/8580 = 58%, 76 KB/s], Decompressed: 4656
Downloaded: 5042 file(s) [attempted 5042/8580 = 58%, 298 KB/s], Decompressed: 4656
Downloaded: 5079 file(s) [attempted 5079/8580 = 59%, 191 KB/s], Decompressed: 4656
Downloaded: 5116 file(s) [attempted 5116/8580 = 59%, 114 KB/s], Decompressed: 4656
Downloaded: 5150 file(s) [attempted 5150/8580 = 60%, 58 KB/s], Decompressed: 4896
Downloaded: 5194 file(s) [attempted 5194/8580 = 60%, 94 KB/s], Decompressed: 4896
Downloaded: 5235 file(s) [attempted 5235/8580 = 61%, 432 KB/s], Decompressed: 4896
Downloaded: 5275 file(s) [attempted 5275/8580 = 61%, 492 KB/s], Decompressed: 4896
Downloaded: 5312 file(s) [attempted 5312/8580 = 61%, 200 KB/s], Decompressed: 4896
Downloaded: 5350 file(s) [attempted 5350/8580 = 62%, 292 KB/s], Decompressed: 4896
Downloaded: 5390 file(s) [attempted 5390/8580 = 62%, 158 KB/s], Decompressed: 5140
Downloaded: 5434 file(s) [attempted 5434/8580 = 63%, 560 KB/s], Decompressed: 5140
Downloaded: 5475 file(s) [attempted 5475/8580 = 63%, 219 KB/s], Decompressed: 5140
Downloaded: 5512 file(s) [attempted 5512/8580 = 64%, 288 KB/s], Decompressed: 5140
Downloaded: 5546 file(s) [attempted 5546/8580 = 64%, 883 KB/s], Decompressed: 5140
Downloaded: 5587 file(s) [attempted 5587/8580 = 65%, 62 KB/s], Decompressed: 5140
Downloaded: 5634 file(s) [attempted 5634/8580 = 65%, 415 KB/s], Decompressed: 5370
Downloaded: 5681 file(s) [attempted 5681/8580 = 66%, 1779 KB/s], Decompressed: 5370
Downloaded: 5725 file(s) [attempted 5725/8580 = 66%, 122 KB/s], Decompressed: 5370
Downloaded: 5766 file(s) [attempted 5766/8580 = 67%, 66 KB/s], Decompressed: 5370
Downloaded: 5800 file(s) [attempted 5800/8580 = 67%, 218 KB/s], Decompressed: 5370
Downloaded: 5837 file(s) [attempted 5837/8580 = 68%, 36 KB/s], Decompressed: 5370
Downloaded: 5881 file(s) [attempted 5881/8580 = 68%, 133 KB/s], Decompressed: 5607
Downloaded: 5928 file(s) [attempted 5928/8580 = 69%, 677 KB/s], Decompressed: 5607
Downloaded: 5969 file(s) [attempted 5969/8580 = 69%, 87 KB/s], Decompressed: 5607
Downloaded: 6013 file(s) [attempted 6013/8580 = 70%, 673 KB/s], Decompressed: 5607
Downloaded: 6053 file(s) [attempted 6053/8580 = 70%, 74 KB/s], Decompressed: 5607
Downloaded: 6091 file(s) [attempted 6091/8580 = 70%, 52 KB/s], Decompressed: 5607
Downloaded: 6131 file(s) [attempted 6131/8580 = 71%, 364 KB/s], Decompressed: 5607
Downloaded: 6173 file(s) [attempted 6173/8580 = 71%, 1491 KB/s], Decompressed: 5881
Downloaded: 6206 file(s) [attempted 6206/8580 = 72%, 277 KB/s], Decompressed: 5881
Downloaded: 6246 file(s) [attempted 6246/8580 = 72%, 44 KB/s], Decompressed: 5881
Downloaded: 6287 file(s) [attempted 6287/8580 = 73%, 160 KB/s], Decompressed: 5881
Downloaded: 6327 file(s) [attempted 6327/8580 = 73%, 207 KB/s], Decompressed: 5881
Downloaded: 6371 file(s) [attempted 6371/8580 = 74%, 106 KB/s], Decompressed: 5881
Downloaded: 6415 file(s) [attempted 6415/8580 = 74%, 630 KB/s], Decompressed: 5881
Downloaded: 6446 file(s) [attempted 6446/8580 = 75%, 44 KB/s], Decompressed: 6162
Downloaded: 6490 file(s) [attempted 6490/8580 = 75%, 56 KB/s], Decompressed: 6162
Downloaded: 6530 file(s) [attempted 6530/8580 = 76%, 151 KB/s], Decompressed: 6162
Downloaded: 6571 file(s) [attempted 6571/8580 = 76%, 244 KB/s], Decompressed: 6162
Downloaded: 6611 file(s) [attempted 6611/8580 = 77%, 419 KB/s], Decompressed: 6162
Downloaded: 6652 file(s) [attempted 6652/8580 = 77%, 230 KB/s], Decompressed: 6162
Downloaded: 6689 file(s) [attempted 6689/8580 = 77%, 1352 KB/s], Decompressed: 6162
Downloaded: 6733 file(s) [attempted 6733/8580 = 78%, 62 KB/s], Decompressed: 6162
Downloaded: 6774 file(s) [attempted 6774/8580 = 78%, 359 KB/s], Decompressed: 6442
Downloaded: 6818 file(s) [attempted 6818/8580 = 79%, 130 KB/s], Decompressed: 6442
Downloaded: 6858 file(s) [attempted 6858/8580 = 79%, 798 KB/s], Decompressed: 6442
Downloaded: 6892 file(s) [attempted 6892/8580 = 80%, 71 KB/s], Decompressed: 6442
Downloaded: 6933 file(s) [attempted 6933/8580 = 80%, 236 KB/s], Decompressed: 6442
Downloaded: 6973 file(s) [attempted 6973/8580 = 81%, 196 KB/s], Decompressed: 6442
Downloaded: 7014 file(s) [attempted 7014/8580 = 81%, 216 KB/s], Decompressed: 6442
Downloaded: 7061 file(s) [attempted 7061/8580 = 82%, 156 KB/s], Decompressed: 6442
Downloaded: 7102 file(s) [attempted 7102/8580 = 82%, 166 KB/s], Decompressed: 6770
Downloaded: 7132 file(s) [attempted 7132/8580 = 83%, 80 KB/s], Decompressed: 6770
Downloaded: 7176 file(s) [attempted 7176/8580 = 83%, 1193 KB/s], Decompressed: 6770
Downloaded: 7217 file(s) [attempted 7217/8580 = 84%, 45 KB/s], Decompressed: 6770
Downloaded: 7264 file(s) [attempted 7264/8580 = 84%, 303 KB/s], Decompressed: 6770
Downloaded: 7308 file(s) [attempted 7308/8580 = 85%, 24 KB/s], Decompressed: 6770
Downloaded: 7349 file(s) [attempted 7349/8580 = 85%, 1113 KB/s], Decompressed: 6770
Downloaded: 7386 file(s) [attempted 7386/8580 = 86%, 58 KB/s], Decompressed: 7078
Downloaded: 7420 file(s) [attempted 7420/8580 = 86%, 170 KB/s], Decompressed: 7078
Downloaded: 7467 file(s) [attempted 7467/8580 = 87%, 146 KB/s], Decompressed: 7078
Downloaded: 7508 file(s) [attempted 7508/8580 = 87%, 1846 KB/s], Decompressed: 7078
Downloaded: 7548 file(s) [attempted 7548/8580 = 87%, 105 KB/s], Decompressed: 7078
Downloaded: 7589 file(s) [attempted 7589/8580 = 88%, 141 KB/s], Decompressed: 7078
Downloaded: 7623 file(s) [attempted 7623/8580 = 88%, 481 KB/s], Decompressed: 7078
Downloaded: 7663 file(s) [attempted 7663/8580 = 89%, 594 KB/s], Decompressed: 7078
Downloaded: 7701 file(s) [attempted 7701/8580 = 89%, 160 KB/s], Decompressed: 7078
Downloaded: 7738 file(s) [attempted 7738/8580 = 90%, 128 KB/s], Decompressed: 7373
Downloaded: 7779 file(s) [attempted 7779/8580 = 90%, 94 KB/s], Decompressed: 7373
Downloaded: 7812 file(s) [attempted 7812/8580 = 91%, 45 KB/s], Decompressed: 7373
Downloaded: 7850 file(s) [attempted 7850/8580 = 91%, 236 KB/s], Decompressed: 7373
Downloaded: 7894 file(s) [attempted 7894/8580 = 92%, 115 KB/s], Decompressed: 7373
Downloaded: 7934 file(s) [attempted 7934/8580 = 92%, 133 KB/s], Decompressed: 7373
Downloaded: 7975 file(s) [attempted 7975/8580 = 92%, 692 KB/s], Decompressed: 7373
Downloaded: 8009 file(s) [attempted 8009/8580 = 93%, 1231 KB/s], Decompressed: 7373
Downloaded: 8049 file(s) [attempted 8049/8580 = 93%, 106 KB/s], Decompressed: 7711
Downloaded: 8093 file(s) [attempted 8093/8580 = 94%, 360 KB/s], Decompressed: 7711
Downloaded: 8134 file(s) [attempted 8134/8580 = 94%, 227 KB/s], Decompressed: 7711
Downloaded: 8178 file(s) [attempted 8178/8580 = 95%, 172 KB/s], Decompressed: 7711
Downloaded: 8218 file(s) [attempted 8218/8580 = 95%, 54 KB/s], Decompressed: 7711
Downloaded: 8255 file(s) [attempted 8255/8580 = 96%, 73 KB/s], Decompressed: 7711
Downloaded: 8293 file(s) [attempted 8293/8580 = 96%, 52 KB/s], Decompressed: 7711
Downloaded: 8333 file(s) [attempted 8333/8580 = 97%, 102 KB/s], Decompressed: 7711
Downloaded: 8374 file(s) [attempted 8374/8580 = 97%, 78 KB/s], Decompressed: 7711
Downloaded: 8414 file(s) [attempted 8414/8580 = 98%, 257 KB/s], Decompressed: 8046
Downloaded: 8452 file(s) [attempted 8452/8580 = 98%, 85 KB/s], Decompressed: 8046
Downloaded: 8492 file(s) [attempted 8492/8580 = 98%, 743 KB/s], Decompressed: 8046
Downloaded: 8529 file(s) [attempted 8529/8580 = 99%, 132 KB/s], Decompressed: 8046
Downloaded: 8570 file(s) [attempted 8570/8580 = 99%, 168 KB/s], Decompressed: 8046
Downloaded: 8580 file(s) [attempted 8580/8580 = 100%, 168 KB/s], Decompressed: 8046

lean_checker exit 0 duration 18m 8s · created 6/30/2026, 3:15:46 PM

lake build

✔ [1/21] Built FLT.Assumptions.KnownIn1980s (357ms)
✔ [1957/1960] Built FLT.Assumptions.Mazur (11s)
✔ [2954/2967] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (2.0s)
✔ [2956/2967] Built FLT.Mathlib.Topology.Algebra.Group.Units (945ms)
✔ [2958/2968] Built FLT.AutomorphicForm.GroupTheoryStuff (3.7s)
✔ [2960/2968] Built FLT.Mathlib.Order.Filter.Cofinite (826ms)
✔ [2961/2968] Built FLT.Mathlib.Topology.Bases (918ms)
✔ [2963/2974] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (1.6s)
✔ [2965/2974] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (2.7s)
✔ [2966/2974] Built FLT.Assumptions.Odlyzko (4.8s)
✔ [2968/2974] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (911ms)
✔ [2969/2974] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (1.5s)
✔ [2970/2974] Built FLT.Mathlib.Algebra.Algebra.Tower (1.3s)
✔ [2971/2975] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (4.0s)
✔ [2974/2991] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (5.8s)
✔ [3246/3255] Built FLT.Mathlib.Topology.Algebra.MulAction (1.1s)
✔ [3252/3257] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (4.9s)
✔ [3253/3257] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (7.1s)
✔ [3255/3273] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Algebra (1.3s)
✔ [3334/3342] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (1.8s)
✔ [3335/3342] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.0s)
✔ [3336/3342] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (2.0s)
✔ [3337/3347] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (6.5s)
✔ [3341/3348] Built FLT.Mathlib.LinearAlgebra.Countable (1.2s)
✔ [3345/3349] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (890ms)
✔ [3347/3355] Built FLT.DedekindDomain.AdicValuation (6.0s)
✔ [3354/3373] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (1.0s)
✔ [3364/3373] Built FLT.Mathlib.RingTheory.Localization.BaseChange (1.8s)
✔ [3369/3376] Built FLT.DedekindDomain.IntegralClosure (4.9s)
✔ [3372/3378] Built FLT.NumberField.HeightOneSpectrum (1.5s)
✔ [3373/3379] Built FLT.NumberField.Completion.Finite (2.3s)
✔ [3376/3387] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (2.3s)
✔ [3381/3387] Built FLT.Hacks.RightActionInstances (3.5s)
✔ [3382/3387] Built FLT.Mathlib.Topology.Algebra.Group.Basic (1.3s)
✔ [3386/3398] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (3.8s)
✔ [3388/3398] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (1.9s)
✔ [3389/3398] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (1.5s)
✔ [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.1s)
✔ [3401/3407] Built FLT.Mathlib.GroupTheory.DoubleCoset (3.8s)
✔ [3402/3407] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (3.4s)
✔ [3403/3408] Built FLT.Mathlib.MeasureTheory.Group.Measure (1.3s)
✔ [3404/3408] Built FLT.AutomorphicForm.Stuff (2.4s)
✔ [3406/3408] Built FLT.QuaternionAlgebra.NumberField (12s)
✔ [3407/3422] Built FLT.AutomorphicForm.QuaternionAlgebra.Basic (36s)
✔ [3414/3422] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.1s)
✔ [3417/3422] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (1.3s)
✔ [3419/3424] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (1.5s)
✔ [3420/3424] Built FLT.HaarMeasure.HaarChar.AddEquiv (5.7s)
✔ [3422/3431] Built FLT.HaarMeasure.HaarChar.Ring (2.5s)
✔ [3427/3439] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (1.4s)
✔ [3428/3439] Built FLT.Mathlib.Algebra.Algebra.Hom (1.9s)
✔ [3430/3447] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (1.5s)
✔ [3431/3447] Built FLT.Mathlib.Topology.Algebra.UniformRing (1.2s)
✔ [3432/3447] Built FLT.Mathlib.Algebra.Algebra.Pi (1.3s)
✔ [3434/3447] Built FLT.Mathlib.Algebra.Algebra.Bilinear (1.0s)
✔ [3436/3447] Built FLT.Mathlib.Algebra.IsDirectLimit (1.8s)
✔ [3437/3447] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (1.7s)
✔ [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.0s)
✔ [3446/3451] Built FLT.DedekindDomain.Completion.BaseChange (22s)
✔ [3447/3451] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (7.1s)
✔ [3448/3465] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (1.8s)
✔ [3451/3466] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (67s)
✔ [3453/3466] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (1.4s)
✔ [3454/3466] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (1.5s)
✔ [3455/3466] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (1.1s)
✔ [3456/3466] Built FLT.NumberField.InfinitePlace.Extension (2.5s)
✔ [3457/3466] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (1.4s)
✔ [3459/3469] Built FLT.Mathlib.Topology.Constructions (996ms)
✔ [3462/3469] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (1.4s)
✔ [3464/3469] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (1.8s)
✔ [3465/3478] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (1.6s)
✔ [3466/3478] Built FLT.NumberField.Completion.Infinite (15s)
✔ [3468/3478] Built FLT.NumberField.Padics.RestrictedProduct (2.5s)
✔ [3469/3478] Built FLT.Mathlib.Data.Real.Archimedean (937ms)
✔ [3470/3478] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (1.3s)
✔ [3471/3478] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (1.6s)
✔ [3474/3481] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (1.7s)
✔ [3475/3481] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (5.7s)
✔ [3476/3487] Built FLT.NumberField.InfiniteAdeleRing (13s)
✔ [3478/3490] Built FLT.NumberField.AdeleRing (22s)
✔ [3481/3496] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (1.9s)
✔ [3483/3496] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (2.8s)
✔ [3485/3500] Built FLT.HaarMeasure.MeasurableSpacePadics (1.9s)
✔ [3487/3500] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (1.1s)
✔ [3488/3500] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (1.3s)
✔ [3489/3500] Built FLT.HaarMeasure.HaarChar.RealComplex (2.2s)
✔ [3490/3500] Built FLT.HaarMeasure.HaarChar.Padic (2.4s)
✔ [3491/3500] Built FLT.Mathlib.LinearAlgebra.Determinant (3.7s)
✔ [3493/3500] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.1s)
✔ [3494/3500] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (2.2s)
✔ [3495/3500] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (2.6s)
✔ [3496/3500] Built FLT.Mathlib.Algebra.Central.TensorProduct (1.9s)
✔ [3497/3500] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (5.8s)
✔ [3498/3501] Built FLT.HaarMeasure.HaarChar.AdeleRing (4.4s)
✔ [3499/3505] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (18s)
✔ [3510/3518] Built FLT.Mathlib.Topology.HomToDiscrete (1.5s)
✔ [3514/3518] Built FLT.Mathlib.Topology.Polish (1.3s)
✔ [3515/3518] Built FLT.Mathlib.MeasureTheory.Haar.Extension (2.1s)
✔ [3516/3520] Built FLT.DivisionAlgebra.Finiteness (39s)
✔ [3517/3523] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (2.3s)
✔ [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 (4.3s)
✔ [3547/3558] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (4.1s)
✔ [3557/3560] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (37s)
✔ [3568/3570] Built FLT.Mathlib.MeasureTheory.Group.ModularCharacter (7.6s)
✔ [3569/3576] Built FLT.HaarMeasure.Quotient (3.8s)
✔ [3648/3655] Built FLT.HaarMeasure.FiniteAdeleRing (5.4s)
✔ [8709/8780] Built FLT.Data.Hurwitz (3.5s)
✔ [8710/8780] Built FLT.Data.QHat (5.4s)
✔ [8711/8780] Built FLT.Deformations.Algebra.InverseLimit.Basic (5.3s)
✔ [8712/8780] Built FLT.Patching.Utils.InverseLimit (1.1s)
✔ [8713/8780] Built FLT.Patching.Utils.Lemmas (3.6s)
✔ [8714/8780] Built FLT.Deformations.Lemmas (3.4s)
✔ [8715/8780] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.1s)
✔ [8716/8780] Built FLT.Deformations.Subfunctor (834ms)
✔ [8717/8780] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (1.2s)
✔ [8718/8780] Built FLT.Mathlib.RepresentationTheory.Basic (2.1s)
✔ [8719/8780] Built FLT.FreyCurve.FreyPackage (2.8s)
✔ [8720/8780] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (1.5s)
✔ [8721/8780] Built FLT.GlobalLanglandsConjectures.GLnDefs (8.1s)
✔ [8722/8780] Built FLT.GroupScheme.FiniteFlat (266ms)
✔ [8723/8780] Built FLT.HenselianLocalRing.EtaleDecomposition (12s)
✔ [8724/8780] Built FLT.HenselianLocalRing.Stuff (1.9s)
✔ [8725/8780] Built FLT.Mathlib.Algebra.FixedPoints.Basic (1.9s)
✔ [8726/8780] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (1.1s)
✔ [8727/8780] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.3s)
✔ [8728/8780] Built FLT.Mathlib.Data.Fin.Basic (815ms)
✔ [8729/8780] Built FLT.Mathlib.Data.Set.Prod (594ms)
✔ [8730/8780] Built FLT.Mathlib.GroupTheory.Index (978ms)
✔ [8731/8780] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.2s)
✔ [8732/8780] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.2s)
✔ [8733/8780] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.2s)
✔ [8734/8780] Built FLT.Mathlib.Topology.Algebra.Monoid (1.1s)
✔ [8735/8780] Built FLT.NumberField.DiscriminantBounds (2.4s)
✔ [8736/8780] Built FLT.Patching.Utils.TopologicallyFG (1.4s)
✔ [8737/8780] Built FLT.Patching.Utils.Depth (2.7s)
✔ [8738/8780] Built FLT.Patching.Utils.CompactHausdorffRings (2.1s)
✔ [8740/8780] Built FLT.TateCurve.TateCurve (298ms)
✔ [8741/8780] Built FLT.Data.HurwitzRatHat (2.1s)
✔ [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.1s)
✔ [8745/8780] Built FLT.Deformations.IsResidueAlgebra (1.8s)
✔ [8746/8780] Built FLT.Deformations.RepresentationTheory.IntegralClosure (1.9s)
✔ [8747/8780] Built FLT.Deformations.RepresentationTheory.Etale (8.5s)
✔ [8748/8780] Built FLT.Deformations.RepresentationTheory.Frobenius (2.1s)
✔ [8749/8780] Built FLT.Deformations.RepresentationTheory.Irreducible (1.3s)
✔ [8750/8780] Built FLT.GlobalLanglandsConjectures.GLzero (1.8s)
✔ [8751/8780] Built FLT.HenselianLocalRing.Finite (4.9s)
✔ [8752/8780] Built FLT.Mathlib.Topology.Algebra.Order.Field (2.1s)
✔ [8753/8780] Built FLT.Patching.Utils.StructureFiniteness (3.4s)
✔ [8754/8780] Built FLT.AutomorphicForm.QuaternionAlgebra.InnerProduct (57s)
✔ [8755/8780] Built FLT.Deformations.IsProartinian (1.7s)
✔ [8756/8780] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (13s)
✔ [8757/8780] Built FLT.Patching.Ultraproduct (7.9s)
✔ [8758/8780] Built FLT.Deformations.Categories (2.9s)
✔ [8759/8780] Built FLT.Deformations.RepresentationTheory.GaloisRep (11s)
✔ [8760/8780] Built FLT.Patching.Algebra (9.5s)
✔ [8761/8780] Built FLT.Patching.VanishingFilter (2.5s)
✔ [8762/8780] Built FLT.Patching.Module (11s)
✔ [8763/8780] Built FLT.Deformations.LiftFunctor (3.5s)
✔ [8764/8780] Built FLT.GaloisRepresentation.Automorphic (3.9s)
✔ [8765/8780] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.5s)
✔ [8766/8780] Built FLT.EllipticCurve.Torsion (2.1s)
✔ [8767/8780] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (1.8s)
✔ [8768/8780] Built FLT.Patching.Over (11s)
✔ [8769/8780] Built FLT.Deformations.Representable (2.5s)
✔ [8770/8780] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (1.8s)
✔ [8771/8780] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (1.8s)
✔ [8772/8780] Built FLT.GaloisRepresentation.HardlyRamified.Lift (1.8s)
✔ [8773/8780] Built FLT.GaloisRepresentation.HardlyRamified.Frey (1.7s)
✔ [8774/8780] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.0s)
✔ [8775/8780] Built FLT.Patching.System (9.5s)
✔ [8776/8780] Built FLT.FreyCurve.Contradiction (1.7s)
✔ [8777/8780] Built FLT.Patching.REqualsT (3.8s)
✔ [8778/8780] Built FLT (2.0s)
✔ [8779/8780] Built FermatsLastTheorem (186s)
Build completed successfully (8780 jobs).

blueprint_build exit 1 duration 8s · created 6/30/2026, 3:15:46 PM

lake build :blueprint

error: unknown package facet `blueprint`

semantic_extract exit 1 duration 32m 29s · created 6/30/2026, 3:15:46 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)

apx-semantic-phase	{"phase":"core_compile","duration_ms":43376}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":4407,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 8c482a2f24e4ea14c2be87c192355c4352bb046ff534e5fe86f395fb8ae9c4cc
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":62,"runner_cache_hit":true}
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1900376,"ok":false}
lean semantic helper failed: generated static runner exited non-zero
remediation: inspect the generated repository runner and imported root modules

semantic_extract exit 0 duration 6m 43s · created 6/30/2026, 3:15:46 PM

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

apx-semantic-phase	{"duration_ms":23,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":26,"diagnostic_count":8,"duration_ms":1917,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":26,"dependency_count":28,"diagnostic_count":46,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":306775,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":26,"dependency_count":28,"diagnostic_count":46,"duration_ms":113,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":999111,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":6,"ok":true,"payload_bytes":999111,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1344,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":28,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":88262,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache e229f92da80b09ecb21d2e16f814ce547b8c210bca3fd2f1b913d0262f0244da
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":312399,"ok":true}

semantic_extract exit 137 duration 8m 37s · created 6/30/2026, 3:15:46 PM

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

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":163,"diagnostic_count":86,"duration_ms":19159,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":163,"dependency_count":745,"diagnostic_count":1367,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":468908,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":163,"dependency_count":745,"diagnostic_count":1367,"duration_ms":6719,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":769738786,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":1612,"ok":true,"payload_bytes":769738786,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":249,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache cfae54b19702e39775998d4a4530367ffaf0454dac7c4891721321f7a3fd6de4
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":39,"runner_cache_hit":true}
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":504721,"ok":true}
/apx/source/.apodeixis/tools/lean-semantic-extract.sh: line 383: 10110 Killed                  python3 <<'PY'
import hashlib
import json
import os
import pathlib
import sys

request_path = pathlib.Path(os.environ["APX_LEAN_HELPER_REQUEST_PATH"])
response_path = pathlib.Path(os.environ["APX_LEAN_HELPER_RESPONSE_PATH"])

with request_path.open("r", encoding="utf-8") as handle:
    request = json.load(handle)

if request.get("operation") != "extract_repository_semantics":
    raise SystemExit(0)

with response_path.open("r", encoding="utf-8") as handle:
    response = json.load(handle)

if "helper" not in response:
    raise SystemExit(0)

helper = response.get("helper")
helper_version = response.get("helper_version")

if not helper or helper_version in (None, ""):
    print(
        "lean semantic extractor failed: repository semantics response is missing helper metadata required for normalization",
        file=sys.stderr,
    )
    raise SystemExit(1)

without_checksum = {k: v for k, v in response.items() if k != "checksum"}
canonical = json.dumps(without_checksum, sort_keys=True, separators=(",", ":"), ensure_ascii=False)
response["checksum"] = hashlib.sha256(canonical.encode("utf-8")).hexdigest()

tmp_path = pathlib.Path(f"{response_path}.tmp")
with tmp_path.open("w", encoding="utf-8") as handle:
    json.dump(response, handle, sort_keys=True, separators=(",", ":"), ensure_ascii=False)
os.replace(tmp_path, response_path)
PY

semantic_extract exit 0 duration 6m 41s · created 6/30/2026, 3:15:46 PM

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

apx-semantic-phase	{"duration_ms":17,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":99,"diagnostic_count":52,"duration_ms":7902,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":99,"dependency_count":464,"diagnostic_count":1414,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":304902,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":99,"dependency_count":464,"diagnostic_count":1414,"duration_ms":1235,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":110549709,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":83,"ok":true,"payload_bytes":110549709,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":570,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":77769,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 2ab56cb015eb785ed07034add1350d210ab18c01645232489190b7368d00e000
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":318758,"ok":true}

semantic_extract exit 0 duration 5m 30s · created 6/30/2026, 3:15:46 PM

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

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":178,"diagnostic_count":116,"duration_ms":12614,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":178,"dependency_count":551,"diagnostic_count":2186,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":302877,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":178,"dependency_count":551,"diagnostic_count":2186,"duration_ms":716,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":37846658,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":27,"ok":true,"payload_bytes":37846658,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":233,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":7779,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 024b47d071e6a1d68ac450abbf05a2abc990fed42f4f262fc8a833a2fb7f43d7
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":320315,"ok":true}

semantic_extract exit 0 duration 5m 22s · created 6/30/2026, 3:15:46 PM

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

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":58,"diagnostic_count":46,"duration_ms":4726,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":58,"dependency_count":112,"diagnostic_count":46,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":304628,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":58,"dependency_count":112,"diagnostic_count":46,"duration_ms":649,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":68346489,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":62,"ok":true,"payload_bytes":68346489,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":286,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":5663,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 4b5969385b39e67ee424aee21eeba0fcdf220e9b224773ff62705fb5d20514b8
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":314391,"ok":true}

semantic_extract exit 0 duration 5m 24s · created 6/30/2026, 3:15:46 PM

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

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":26,"diagnostic_count":16,"duration_ms":1826,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":26,"dependency_count":62,"diagnostic_count":465,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":308193,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":26,"dependency_count":62,"diagnostic_count":465,"duration_ms":244,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":15596493,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":10,"ok":true,"payload_bytes":15596493,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":310,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":8927,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 324704e13ca54a61679cf24b8134b1cc5d55fa33575e8ba619ec8a0ed91d62e9
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":314017,"ok":true}

semantic_extract exit 1 duration 9m 26s · created 6/30/2026, 3:15:46 PM

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

apx-semantic-phase	{"phase":"core_compile","duration_ms":20}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":99,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":21,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":4597,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache add9abc3203c65105be67be28e03225b6b2805a513c9fb8163923127d21648bd
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":560750,"ok":false}
lean semantic helper failed: generated static runner exited non-zero
remediation: inspect the generated repository runner and imported root modules

semantic_extract exit 0 duration 7m 22s · created 6/30/2026, 3:15:46 PM

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

apx-semantic-phase	{"duration_ms":18,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":26,"diagnostic_count":12,"duration_ms":2240,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":26,"dependency_count":26,"diagnostic_count":25,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":326215,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":26,"dependency_count":26,"diagnostic_count":25,"duration_ms":498,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":72279073,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":58,"ok":true,"payload_bytes":72279073,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":1327,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":105212,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 0cd980907453956ffc5e14bdf1a057935c20a4c0e6abec4ebdc0aefa62ed638a
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":332932,"ok":true}

semantic_extract exit 0 duration 5m 55s · created 6/30/2026, 3:15:46 PM

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

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":246,"diagnostic_count":135,"duration_ms":19770,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":246,"dependency_count":983,"diagnostic_count":1922,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":317889,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":246,"dependency_count":983,"diagnostic_count":1922,"duration_ms":2000,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":174946227,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":181,"ok":true,"payload_bytes":174946227,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":12}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":243,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":12,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":3540,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 8d12888e4eb4af384bb800a855b9692f9111a509092a6b21652243a9cdb2c1db
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":345501,"ok":true}

semantic_extract exit 0 duration 37m 19s · created 6/30/2026, 3:15:46 PM

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

apx-semantic-phase	{"duration_ms":246,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":218,"diagnostic_count":105,"duration_ms":32078,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"declaration_count":218,"dependency_count":617,"diagnostic_count":2242,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":1402867,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":218,"dependency_count":617,"diagnostic_count":2242,"duration_ms":2554,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":194195460,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":159,"ok":true,"payload_bytes":194195460,"phase":"lean_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":25}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":426,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
apx-semantic-phase	{"phase":"runner_compile","duration_ms":380091,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 6bbce7152ff7d200fcdcdd653b0a23662dbf321c826ed5e1e145ffefc1af1e63
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1852437,"ok":true}