From 88c1ceb742a73e24a5e687c141f82d748a44fa9e Mon Sep 17 00:00:00 2001
From: "J. C. Burnham" <jcb@agathic.com>
Date: Thu, 27 Aug 2026 15:16:06 -0400
Subject: [PATCH] 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]