From ef9ba8d7aca7a1e405b4bba2621fefa7f0dbdf01 Mon Sep 17 00:00:00 2001 From: "J. C. Burnham" Date: Thu, 27 Aug 2026 15:16:06 -0400 Subject: [PATCH 1/3] lakefile: make precompileModules opt-in via `precompile` option MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- lakefile.lean | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index c8a5fe4..553359d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,8 +4,15 @@ open Lake DSL package Blake3 +/- Passing the `precompile` option (e.g. `options = {precompile = "on"}` on the +downstream `[[require]]`, or `with NameMap.empty.insert `precompile "on"` in a +`lakefile.lean` require) precompiles these libs so the C/Rust FFI symbols are +auto-loaded into elaborating processes (batch builds and language-server +workers) — needed by consumers that call Blake3 in `#eval` at elaboration +time. Off by default: without the option, behavior is unchanged. -/ @[default_target] -lean_lib Blake3 +lean_lib Blake3 where + precompileModules := (get_config? precompile).isSome @[test_driver] lean_exe Blake3Test @@ -78,6 +85,7 @@ target blake3_c pkg : System.FilePath := do buildStaticLib (pkg.staticLibDir / name) oFileJobs lean_lib Blake3C where + precompileModules := (get_config? precompile).isSome roots := #[`Blake3.C] moreLinkObjs := #[blake3_c] @@ -88,6 +96,7 @@ target blake3_rs pkg : System.FilePath := do inputBinFile $ pkg.dir / "rust" / "target" / "release" / libName lean_lib Blake3Rust where + precompileModules := (get_config? precompile).isSome roots := #[`Blake3.Rust] moreLinkObjs := #[blake3_rs] From 720c0dee76f2eae9fae29dc04e3888d198563e79 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 27 Aug 2026 20:06:39 -0400 Subject: [PATCH 2/3] lakefile: precompile the libs unconditionally 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. --- lakefile.lean | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 553359d..dc26fc8 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,15 +4,16 @@ open Lake DSL package Blake3 -/- Passing the `precompile` option (e.g. `options = {precompile = "on"}` on the -downstream `[[require]]`, or `with NameMap.empty.insert `precompile "on"` in a -`lakefile.lean` require) precompiles these libs so the C/Rust FFI symbols are -auto-loaded into elaborating processes (batch builds and language-server -workers) — needed by consumers that call Blake3 in `#eval` at elaboration -time. Off by default: without the option, behavior is unchanged. -/ +/- Precompiled so the C/Rust FFI symbols are auto-loaded into elaborating +processes -- batch builds and language-server workers alike. Without this, +any consumer that reaches the FFI at elaboration time (`#eval`, or +`native_decide` over a hash) fails outright with "Could not find native +implementation of external declaration", and cannot fix it from their side. +The cost is one shared-library link per lib, measured at ~0.3s on a cold +build of a consumer that links an executable, and nothing on rebuilds. -/ @[default_target] lean_lib Blake3 where - precompileModules := (get_config? precompile).isSome + precompileModules := true @[test_driver] lean_exe Blake3Test @@ -85,7 +86,7 @@ target blake3_c pkg : System.FilePath := do buildStaticLib (pkg.staticLibDir / name) oFileJobs lean_lib Blake3C where - precompileModules := (get_config? precompile).isSome + precompileModules := true roots := #[`Blake3.C] moreLinkObjs := #[blake3_c] @@ -96,7 +97,7 @@ target blake3_rs pkg : System.FilePath := do inputBinFile $ pkg.dir / "rust" / "target" / "release" / libName lean_lib Blake3Rust where - precompileModules := (get_config? precompile).isSome + precompileModules := true roots := #[`Blake3.Rust] moreLinkObjs := #[blake3_rs] From 5ff5e70b6c7fc371cc6b454b83844f1f5b44ac96 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 27 Aug 2026 20:13:47 -0400 Subject: [PATCH 3/3] lakefile: drop the cdylib now that the libs are precompiled `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. --- lakefile.lean | 9 --------- rust/Cargo.toml | 9 ++++----- 2 files changed, 4 insertions(+), 14 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index dc26fc8..735ae95 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -101,12 +101,3 @@ lean_lib Blake3Rust where roots := #[`Blake3.Rust] moreLinkObjs := #[blake3_rs] -/-- The `blake3-rs` shared library. Produced by the same `cargo build` as -`blake3_rs`; this target selects the `cdylib` output for downstream tooling -that loads the raw `rs_blake3_*` symbols at runtime rather than linking them -statically — e.g. supplying the BLAKE3 backend to Lean's native evaluator for -`native_decide` proofs. -/ -target blake3_rs_shared pkg : System.FilePath := do - proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir / "rust" } (quiet := true) - inputBinFile $ pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs" - diff --git a/rust/Cargo.toml b/rust/Cargo.toml index 3606212..319c06b 100644 --- a/rust/Cargo.toml +++ b/rust/Cargo.toml @@ -8,11 +8,10 @@ version = "0.1.0" edition = "2024" [lib] -# `staticlib` is linked into final Lean executables. `cdylib` additionally -# builds a position-independent shared object exporting the raw `rs_blake3_*` -# symbols, so they can be loaded at runtime — e.g. by Lean's native evaluator -# for `native_decide` proofs elaborated before any executable is linked. -crate-type = ["staticlib", "cdylib"] +# Linked into the precompiled Lean shared libraries and into final +# executables. A `cdylib` is not needed: `precompileModules` bundles these +# symbols into each lib's shared object, which Lake loads for importers. +crate-type = ["staticlib"] [dependencies] blake3 = "1.8.7"