feat: lake: precompileLibrary & precompileImports

[tydeu]

This PR adds two new configuration options that are subsets of precompileModules: precompileLibrary for lean_lib targets and precompileImports for all Lean configurations (e.g., settable on package, lean_lib, or lean_exe). precompileImports compiles a module's imports but not the module itself. precompileLibrary compiles the whole library for importers, but the library's modules do not compile their own imports during elaboration.

Closes #2757 with the finer-grain precompileLibrary instead of the more general precompilePackage.

[leanprover-bot]

Reference manual CI status:

• 🟡 Reference manual branch lean-pr-testing-15015 build against this PR didn't complete normally. (2026-09-04 08:05:37) View Log
• 💥 Reference manual branch lean-pr-testing-15015 build failed against this PR. (2026-09-04 08:06:23) View Log
• 💥 Reference manual branch lean-pr-testing-15015 build failed against this PR. (2026-09-04 11:01:56) View Log
• 🟡 Reference manual branch lean-pr-testing-15015 build against this PR didn't complete normally. (2026-09-04 11:01:59) View Log
• 💥 Reference manual branch lean-pr-testing-15015 build failed against this PR. (2026-09-04 13:21:18) View Log
• 🟡 Reference manual branch lean-pr-testing-15015 build against this PR didn't complete normally. (2026-09-04 13:22:19) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-15015 build failed against this PR. (2026-09-04 08:16:26) View Log
• 💥 Mathlib branch lean-pr-testing-15015 build failed against this PR. (2026-09-04 11:07:16) View Log
• ✅ Mathlib branch lean-pr-testing-15015 has successfully built against this PR. (2026-09-04 14:17:17) View Log

[tydeu]

!bench

[leanprover-radar]

Benchmark results for aec9733 against e991a05 are in. No significant results found. @tydeu

• 🟥 build//instructions: +1.9G (+0.02%)

Small changes (6🟥)

• 🟥 build/module/Lake.CLI.Translate.Lean//instructions: +138.7M (+0.95%)
• 🟥 build/module/Lake.CLI.Translate.Toml//instructions: +100.1M (+1.45%)
• 🟥 build/module/Lake.Config.LeanConfig//instructions: +137.5M (+3.94%) (reduced significance based on *//lines)
• 🟥 build/module/Lake.Config.LeanLib//instructions: +50.2M (+2.64%)
• 🟥 build/module/Lake.Config.LeanLibConfig//instructions: +101.9M (+4.81%) (reduced significance based on *//lines)
• 🟥 build/module/Lake.Load.Toml//instructions: +120.3M (+0.92%)

[tydeu]

!bench

[leanprover-radar]

Benchmark results for 31a6a7f against e991a05 are in. No significant results found. @tydeu

• 🟥 build//instructions: +1.7G (+0.01%)

Medium changes (2🟥)

• 🟥 compiled/liasolver//task-clock: +20ms (+11.47%)
• 🟥 compiled/liasolver//wall-clock: +20ms (+11.49%)

Small changes (7🟥)

• 🟥 build/module/Lake.CLI.Translate.Lean//instructions: +126.3M (+0.87%)
• 🟥 build/module/Lake.CLI.Translate.Toml//instructions: +105.1M (+1.52%)
• 🟥 build/module/Lake.Config.LeanConfig//instructions: +140.4M (+4.02%) (reduced significance based on *//lines)
• 🟥 build/module/Lake.Config.LeanLib//instructions: +51.5M (+2.71%)
• 🟥 build/module/Lake.Config.LeanLibConfig//instructions: +102.8M (+4.85%) (reduced significance based on *//lines)
• 🟥 build/module/Lake.Load.Toml//instructions: +100.1M (+0.77%)
• 🟥 vcgen/AdcChain/250/vcgen//wall-clock: +5ms (+9.34%)