fix: Precompile modules by samuelburnham · Pull Request #48 · argumentcomputer/Blake3.lean

samuelburnham · 2026-09-02T12:44:58Z

Enable precompileModules := true, which adds minimal overhead and allows removing the cdylib machinery. Allows downstream users like argumentcomputer/ix#607 to easily use Blake3 for native_decide proofs without hacky build scripts.

Supersedes #47

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.

samuelburnham · 2026-09-02T12:44:58Z

Enable precompileModules := true, which adds minimal overhead and allows removing the cdylib machinery. Allows downstream users like argumentcomputer/ix#607 to easily use Blake3 for native_decide proofs without hacky build scripts.

Supersedes #47

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.

samuelburnham · 2026-09-02T12:44:58Z

Enable precompileModules := true, which adds minimal overhead and allows removing the cdylib machinery. Allows downstream users like argumentcomputer/ix#607 to easily use Blake3 for native_decide proofs without hacky build scripts.

Supersedes #47

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.

samuelburnham · 2026-09-02T12:44:58Z

Enable precompileModules := true, which adds minimal overhead and allows removing the cdylib machinery. Allows downstream users like argumentcomputer/ix#607 to easily use Blake3 for native_decide proofs without hacky build scripts.

Supersedes #47

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.

samuelburnham · 2026-09-02T12:44:58Z

Enable precompileModules := true, which adds minimal overhead and allows removing the cdylib machinery. Allows downstream users like argumentcomputer/ix#607 to easily use Blake3 for native_decide proofs without hacky build scripts.

Supersedes #47

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.

samuelburnham · 2026-09-02T12:44:58Z

Enable precompileModules := true, which adds minimal overhead and allows removing the cdylib machinery. Allows downstream users like argumentcomputer/ix#607 to easily use Blake3 for native_decide proofs without hacky build scripts.

Supersedes #47

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.

samuelburnham · 2026-09-02T12:44:58Z

Enable precompileModules := true, which adds minimal overhead and allows removing the cdylib machinery. Allows downstream users like argumentcomputer/ix#607 to easily use Blake3 for native_decide proofs without hacky build scripts.

Supersedes #47

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.

samuelburnham · 2026-09-02T12:44:58Z

Enable precompileModules := true, which adds minimal overhead and allows removing the cdylib machinery. Allows downstream users like argumentcomputer/ix#607 to easily use Blake3 for native_decide proofs without hacky build scripts.

Supersedes #47

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.

johnchandlerburnhamand others added 3 commits August 27, 2026 20:04

johnchandlerburnham approved these changes Sep 2, 2026
View reviewed changes

johnchandlerburnham merged commit 2db8f69 into mainSep 2, 2026
3 checks passed