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]