fix: Precompile modules - #48
Merged
Merged
Conversation
Downstream packages that run Blake3 hashing inside `#eval` at
elaboration time (e.g. Verso blog posts) need the FFI symbols loaded
into the elaborating process — in batch `lake build` and in
language-server file workers alike. Lake's mechanism for this is
`precompileModules`: the lib's shared library (which bundles the
moreLinkObjs native objects) is then built and auto-loaded for
importers, the same pattern MD4Lean uses.
Rather than forcing every consumer to pay the native-compile cost,
gate it behind a require option, off by default:
[[require]]
name = "Blake3"
git = "..."
rev = "..."
options = {precompile = "on"}
or in a lakefile.lean:
require Blake3 from git "..." @ "..."
with NameMap.empty.insert `precompile "on"
With no option passed, behavior is identical to before.
Gating this behind a require option leaves the broken configuration as the default. A consumer that reaches the FFI at elaboration time -- `#eval`, or `native_decide` over a hash -- fails outright without it, and the option is undiscoverable and silent in every failure mode: it applies at dependency materialization so a rebuild is not enough, Lake ignores unknown require keys in TOML without a diagnostic, and the presence check treated `precompile = "off"` as a request to turn precompilation on. Measured against a consumer that links an executable, so the native objects are built either way: ~1334ms -> ~1638ms cold for the C backend and ~6579ms -> ~6966ms cold for the Rust backend, with no measurable difference on rebuilds. Roughly 0.3s once, against builds that otherwise cannot succeed. This also covers what `blake3_rs_shared` was added for: a downstream `native_decide` over a Blake3 hash now elaborates with no dynlib wiring on the consumer side. That target stays -- consumers combining these externs with their own into a single dynlib fetch it directly.
`precompileModules` links `moreLinkObjs` into each lib's shared object and Lake loads it for importers, so the raw `rs_blake3_*` symbols already reach the elaborating process. The separate `cdylib` and its `blake3_rs_shared` target were a second path to the same place, and only existed because the libs were not precompiled. Verified against a consumer that defines externs of its own alongside these: `native_decide` over both its extern and a Blake3 hash elaborates with no dynlib wiring on the consumer side and no cdylib built anywhere. Breaking for consumers that fetch `blake3_rs_shared` to assemble their own combined dynlib. They no longer need to: precompilation covers the Blake3 half, leaving only their own externs to handle.
johnchandlerburnham
approved these changes
Sep 2, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Enable
precompileModules := true, which adds minimal overhead and allows removing thecdylibmachinery. Allows downstream users like argumentcomputer/ix#607 to easily use Blake3 fornative_decideproofs without hacky build scripts.Supersedes #47