feat: re-enable precompileModules

[Vtec234]

This PR re-enables precompileModules and documents how this can be leveraged to speed up rebuilds as a tip.

No-Changelog: internal optimization detail.

We do not change Verso's benchmarking configuration at this time - it will continue to measure build times for the default setup (with native-compiled Main executables), as experienced by most users (though leanprover/verso-blueprint's vbp build CLI should immediately benefit from this).

Benchmark results with interpreted Main and precompileModules:

• Cold build (from scratch to HTML via CLI) times increase or reduce depending on specifics of the project and hardware. They are more likely to increase on highly parallel hardware since the build graph is now more serial (and the critical path longer). They are more likely to reduce when many modules (e.g. Mathlib) are imported by Main since we don't compile these when interpreting Main.
• Rebuild (from editing the doc to HTML via CLI) and LSP re-elaboration (from editing the doc interactively to LSP server quiescence) reduce by 10–30%.

Raw radar data:

• runner-leanN with nproc (48?) cores
  • Cold build

Metric	Submetric	Value	Ref	Delta	Delta%
blueprint-natson-o0/build/.total	wall clock time	2m 6s	2m 9s	-2s	-1.8%
blueprint-natson/build/.total	wall clock time	2m 6s	2m 18s	-11s	-8.4%
lean4cs1-o0/build/.total	wall clock time	1m 21s	53s	+28s	+53.3%
lean4cs1/build/.total	wall clock time	1m 21s	53s	+28s	+52.8%
refman/build/.total	wall clock time	2m 42s	2m 1s	+41s	+34.5%
sherlock-o0/build/.total	wall clock time	1m 25s	49s	+35s	+71.4%
sherlock/build/.total	wall clock time	1m 25s	50s	+34s	+68.0%

• Rebuild

Metric	Submetric	Value	Ref	Delta	Delta%
blueprint-natson-o0/rebuild/.total	wall clock time	28s	33s	-4s	-14.1%
blueprint-natson/rebuild/.total	wall clock time	29s	42s	-13s	-30.8%
lean4cs1-o0/rebuild/.total	wall clock time	3s	4s	-1s	-22.2%
lean4cs1/rebuild/.total	wall clock time	3s	4s	-1s	-23.3%
refman/rebuild/.total	wall clock time	9s	11s	-1s	-12.6%
sherlock-o0/rebuild/.total	wall clock time	3s	3s	-268ms	-7.2%
sherlock/rebuild/.total	wall clock time	3s	3s	-199ms	-5.4%

• LSP re-elaboration (from interactive doc edit to LSP server quiescence)

Metric	Submetric	Value	Ref	Delta	Delta%
blueprint-natson-o0/lsp-elab/CarlesonBlueprint.Chapters.Main	wall clock time	15s	19s	-3s	-17.1%
blueprint-natson/lsp-elab/CarlesonBlueprint.Chapters.Main	wall clock time	15s	19s	-3s	-17.8%
lean4cs1-o0/lsp-elab/FPCourse.Unit1.Week00_AlgebraicTypes	wall clock time	829ms	1s	-348ms	-29.6%
lean4cs1/lsp-elab/FPCourse.Unit1.Week00_AlgebraicTypes	wall clock time	824ms	1s	-358ms	-30.3%
refman/lsp-elab/Manual.Tactics	wall clock time	3s	3s	-388ms	-10.7%
sherlock-o0/lsp-elab/Sherlock.Study001	wall clock time	698ms	1s	-334ms	-32.4%
sherlock/lsp-elab/Sherlock.Study001	wall clock time	701ms	1s	-342ms	-32.8%

• runner-leanN limited to 4 cores (emulating GitHub's CI runners or a small laptop)
  • Cold build

Metric	Submetric	Value	Ref	Delta	Delta%
blueprint-natson-o0/build/.total	wall clock time	2m 28s	4m 20s	-1m 51s	-43.0%
blueprint-natson/build/.total	wall clock time	2m 27s	4m 31s	-2m 4s	-45.9%
lean4cs1-o0/build/.total	wall clock time	1m 38s	2m 7s	-28s	-22.5%
lean4cs1/build/.total	wall clock time	1m 38s	2m 7s	-29s	-22.9%
refman/build/.total	wall clock time	5m 3s	4m 59s	+3s	+1.2%
sherlock-o0/build/.total	wall clock time	1m 49s	1m 33s	+16s	+17.2%
sherlock/build/.total	wall clock time	1m 49s	1m 37s	+12s	+12.4%

• Rebuild

Metric	Submetric	Value	Ref	Delta	Delta%
blueprint-natson-o0/rebuild/.total	wall clock time	29s	33s	-4s	-13.7%
blueprint-natson/rebuild/.total	wall clock time	29s	42s	-13s	-31.4%
lean4cs1-o0/rebuild/.total	wall clock time	3s	4s	-1s	-22.7%
lean4cs1/rebuild/.total	wall clock time	3s	4s	-1s	-24.8%
refman/rebuild/.total	wall clock time	9s	11s	-1s	-11.2%
sherlock-o0/rebuild/.total	wall clock time	3s	3s	-274ms	-7.5%
sherlock/rebuild/.total	wall clock time	3s	3s	-279ms	-7.6%

• LSP re-elaboration

Metric	Submetric	Value	Ref	Delta	Delta%
blueprint-natson-o0/lsp-elab/CarlesonBlueprint.Chapters.Main	wall clock time	15s	19s	-3s	-18.6%
blueprint-natson/lsp-elab/CarlesonBlueprint.Chapters.Main	wall clock time	16s	19s	-3s	-17.7%
lean4cs1-o0/lsp-elab/FPCourse.Unit1.Week00_AlgebraicTypes	wall clock time	831ms	1s	-347ms	-29.5%
lean4cs1/lsp-elab/FPCourse.Unit1.Week00_AlgebraicTypes	wall clock time	829ms	1s	-359ms	-30.2%
refman/lsp-elab/Manual.Tactics	wall clock time	3s	3s	-431ms	-11.9%
sherlock-o0/lsp-elab/Sherlock.Study001	wall clock time	716ms	1s	-335ms	-31.9%
sherlock/lsp-elab/Sherlock.Study001	wall clock time	725ms	1s	-338ms	-31.8%

[david-christiansen]

Looks basically good modulo docs nitpicks.

Also, because the PR description becomes the commit message, it would be nice to summarize the benchmark runs in the text, because they will presumably not be accessible at that URL in the time period where understanding this commit message might be useful.

[Vtec234]

One remaining concern from the sf-in-lean thread: merging this will break Verso on Linux with Lean below v4.34.

[david-christiansen]

I don't think that this will. From what I can see, the issue on that thread came from them importing Lake, and its .so not being present (fixable by setting LD_LIBRARY_PATH or adding it in a Lean-format Lakefile). In that PR, I enabled precompilation of one of their sublibraries to force precompilation of Verso, and that sublibrary is what depended on Lake. Once we have precompilation on Verso main, it should just work, because we don't take a runtime dependency on Lake.

I'll run a Linux build of SF against this PR to be sure, though.

[david-christiansen]

Do you mind if I OCR the tables so that we have actual numbers in the commit message, rather than links to GitHub images? I don't know how long those links last.

[Vtec234]

OCR the tables

Updated.

Once we have precompilation on Verso main, it should just work, because we don't take a runtime dependency on Lake.

Well, VersoLiterate.Config imports it, so at the end of the day

$ ldd .lake/build/lib/libverso_VersoLiterate.so
	linux-vdso.so.1 (0x000075def12fa000)
	libc.so.6 => /nix/store/qqiqd3ah10x8hzsif4j1y4xc1miw23nx-glibc-2.42-67/lib/libc.so.6 (0x000075def1000000)
	libLake_shared.so => /home/wjn/.elan/toolchains/leanprover--lean4---v4.34.0-rc2/lib/lean/libLake_shared.so (0x000075def0600000)
	(...)

and with precompileModules this library becomes a --plugin when elaborating (for instance) DemoSite.lean.

But maybe older versions are a moot point? I just tried changing lean-toolchain, and main doesn't build on v4.33.0 anyway. We can simply not backport this change to the v4.33.0 tag.

[david-christiansen]

Yep, I checked it out and it does indeed - I'd forgotten that part. We'll just have to say this is a 4.34 and up feature.

[david-christiansen]

I think this is good go now. Hooray!

[ejgallego]

I tested the exact PR head (6c2483eefb453d783ae858142a927bb4bd0bb8c9) downstream on the FLT Blueprint under Linux x86-64 with Lean v4.34.0-rc2. This is a substantial improvement for us.

Representative warmed medians for the controlled interpreted-generator comparison:

Verso precompiled	VBP precompiled	Median
no	no	46.003 s
yes	no	27.709 s (-39.77%)
yes	yes	16.936 s (-63.19% overall; -38.88% from the preceding row)

Precompilation increases clean build cost: Verso went from 51.90 to 111.22 seconds (+114.30%), while enabling it in VBP went from 64.57 to 73.97 seconds (+14.56%). Fully compiling the FLT generator is considerably more expensive because it pulls in the native FLT/Mathlib closure and produces a 426 MB executable.

My takeaway is that this PR is an unambiguous win. We will enable precompileModules in VBP on its 4.34 line. The interpreted generator remains the default because it avoids compiling the formal dependency closure.

[ejgallego]

Follow-up on performance

A. Matched end-to-end measurements

Dependencies and the Lake artifact cache were warm. The edit case starts after a unique prose edit in one Blueprint module.

Path	No-edit median	Edit-to-site median
Interpreted lake exe vbp build	9.505 s	16.625 s
Fully native lake exe blueprint-gen	5.590 s	16.160 s
Export + lake exe generic host	8.365 s	15.130 s

Native is 3.915 seconds faster than interpreted when nothing changed. After a prose edit the difference is only 0.465 seconds.

The interpreted no-edit path includes the outer VBP target check and its internal lake lean ... --run. A direct invocation of the post-target VBP runner took 8.179 seconds and decomposed approximately as follows:

Phase	Time
VBP discovery and process orchestration	0.3 s
Lake workspace setup and dependency validation	2.0 s
Loading and finalizing the OLean environment, then elaborating the generator entry point	2.25 s
Interpreting main and writing the site	3.23 s

The actual traversal and emission are therefore a minority of the elapsed time.

B. Measuring generation without the full Mathlib closure

To measure the generator without importing the full FLT and Mathlib environment into a compiled host, I constructed a project-specific runtime artifact:

1. Starting from FLTBlueprint.«the canonical document object name», follow the erased IR dependencies returned by Lean.IR.findEnvDecl.
2. Store the resulting declarations in a synthetic, non-module ModuleData with no imports, together with the root constant's ConstantInfo.
3. Have a generic compiled VBP host register the file through Lean.ImportArtifacts, load it with Lean.importModules, evaluate the document with env.evalConst, and pass it to the existing renderer.

For FLT, the runtime closure contains 8,733 IR declarations from 79 modules. It contains no formal FLT.* or Mathlib modules, and the resulting project-specific artifact is 12.13 MiB.

At the direct-execution boundary:

Generator path	Median
Fully native FLT generator	2.543 s
Generic compiled VBP host plus runtime artifact	2.243 s

The generic host is 286 MB, compared with 426 MB for the fully native FLT executable. The host can be shared between projects, leaving only the 12.13 MiB runtime artifact as project-specific cached data. The export-plus-host row in section A includes the complete producer and host workflow through their public Lake commands.

C. Could the module system provide this?

The module system can express the relevant phase distinction: formal dependencies can be meta imports, and Lean excludes those imports from the generated runtime initializer.

Lake's native build graph does not currently preserve that distinction. Module.recParseImports reduces the parsed Import values to an Array Module, after which transImports, precompileImports, dynlib construction, and executable construction recurse over the phase-erased graph.

In a minimal FLT test, a single meta import still caused Lake to schedule the native Batteries, Aesop, and Mathlib closure, expanding the build from 902 to 2,770 and then 9,775 jobs.

A phase-aware Lake native graph could eventually make a small Blueprint runtime module viable. However, that would require Lake to preserve Import.isMeta when constructing native targets and to expose an appropriate runtime-only artifact or entry point. It would also operate at module granularity, whereas the experiment above retains only the closure of the document constant.

So the module system could become part of the solution, but it does not currently provide an alternative to a cached runtime artifact.