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
    
  • Rebuild
    
  • LSP re-elaboration (from interactive doc edit to LSP server quiescence)
    
• runner-leanN limited to 4 cores (emulating GitHub's CI runners or a small laptop)
  • Cold build
    
  • Rebuild
    
  • LSP re-elaboration
    

[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.