diff --git a/reference-manual/Manual/BuildTools/Lake.lean b/reference-manual/Manual/BuildTools/Lake.lean
index 7fe5ca6d3..8bdafd3c1 100644
--- a/reference-manual/Manual/BuildTools/Lake.lean
+++ b/reference-manual/Manual/BuildTools/Lake.lean
@@ -728,6 +728,7 @@ root = "Tests"
           weakLinkArgs := #[],
           backend := Lake.Backend.default,
           platformIndependent := none,
+          precompileImports := false,
           dynlibs := #[],
           plugins := #[],
           requiresModuleSystem := false,
@@ -793,6 +794,7 @@ root = "Tests"
                     weakLinkArgs := #[],
                     backend := Lake.Backend.default,
                     platformIndependent := none,
+                    precompileImports := false,
                     dynlibs := #[],
                     plugins := #[],
                     requiresModuleSystem := false,
@@ -828,6 +830,7 @@ root = "Tests"
                           weakLinkArgs := #[],
                           backend := Lake.Backend.default,
                           platformIndependent := none,
+                          precompileImports := false,
                           dynlibs := #[],
                           plugins := #[],
                           requiresModuleSystem := false,
@@ -893,6 +896,7 @@ lean_exe «my-package-tests» where
           weakLinkArgs := #[],
           backend := Lake.Backend.default,
           platformIndependent := none,
+          precompileImports := false,
           dynlibs := #[],
           plugins := #[],
           requiresModuleSystem := false,
@@ -958,6 +962,7 @@ lean_exe «my-package-tests» where
                     weakLinkArgs := #[],
                     backend := Lake.Backend.default,
                     platformIndependent := none,
+                    precompileImports := false,
                     dynlibs := #[],
                     plugins := #[],
                     requiresModuleSystem := false,
@@ -993,6 +998,7 @@ lean_exe «my-package-tests» where
                           weakLinkArgs := #[],
                           backend := Lake.Backend.default,
                           platformIndependent := none,
+                          precompileImports := false,
                           dynlibs := #[],
                           plugins := #[],
                           requiresModuleSystem := false,
@@ -1098,6 +1104,7 @@ root = "Lint"
           weakLinkArgs := #[],
           backend := Lake.Backend.default,
           platformIndependent := none,
+          precompileImports := false,
           dynlibs := #[],
           plugins := #[],
           requiresModuleSystem := false,
@@ -1163,6 +1170,7 @@ root = "Lint"
                     weakLinkArgs := #[],
                     backend := Lake.Backend.default,
                     platformIndependent := none,
+                    precompileImports := false,
                     dynlibs := #[],
                     plugins := #[],
                     requiresModuleSystem := false,
@@ -1198,6 +1206,7 @@ root = "Lint"
                           weakLinkArgs := #[],
                           backend := Lake.Backend.default,
                           platformIndependent := none,
+                          precompileImports := false,
                           dynlibs := #[],
                           plugins := #[],
                           requiresModuleSystem := false,
@@ -1264,6 +1273,7 @@ lean_exe «my-package-lint» where
           weakLinkArgs := #[],
           backend := Lake.Backend.default,
           platformIndependent := none,
+          precompileImports := false,
           dynlibs := #[],
           plugins := #[],
           requiresModuleSystem := false,
@@ -1329,6 +1339,7 @@ lean_exe «my-package-lint» where
                     weakLinkArgs := #[],
                     backend := Lake.Backend.default,
                     platformIndependent := none,
+                    precompileImports := false,
                     dynlibs := #[],
                     plugins := #[],
                     requiresModuleSystem := false,
@@ -1364,6 +1375,7 @@ lean_exe «my-package-lint» where
                           weakLinkArgs := #[],
                           backend := Lake.Backend.default,
                           platformIndependent := none,
+                          precompileImports := false,
                           dynlibs := #[],
                           plugins := #[],
                           requiresModuleSystem := false,
diff --git a/reference-manual/Manual/BuildTools/Lake/Config.lean b/reference-manual/Manual/BuildTools/Lake/Config.lean
index 62b3289c9..376c8a592 100644
--- a/reference-manual/Manual/BuildTools/Lake/Config.lean
+++ b/reference-manual/Manual/BuildTools/Lake/Config.lean
@@ -158,6 +158,7 @@ name = "example-package"
           weakLinkArgs := #[],
           backend := Lake.Backend.default,
           platformIndependent := none,
+          precompileImports := false,
           dynlibs := #[],
           plugins := #[],
           requiresModuleSystem := false,
@@ -250,6 +251,7 @@ name = "Sorting"
           weakLinkArgs := #[],
           backend := Lake.Backend.default,
           platformIndependent := none,
+          precompileImports := false,
           dynlibs := #[],
           plugins := #[],
           requiresModuleSystem := false,
@@ -315,6 +317,7 @@ name = "Sorting"
                     weakLinkArgs := #[],
                     backend := Lake.Backend.default,
                     platformIndependent := none,
+                    precompileImports := false,
                     dynlibs := #[],
                     plugins := #[],
                     requiresModuleSystem := false,
@@ -326,6 +329,7 @@ name = "Sorting"
                 libPrefixOnWindows := false,
                 needs := #[],
                 extraDepTargets := #[],
+                precompileLibrary := false,
                 precompileModules := false,
                 defaultFacets := #[`lean_lib.leanArts],
                 nativeFacets := #<fun>,
@@ -354,6 +358,7 @@ name = "Sorting"
                           weakLinkArgs := #[],
                           backend := Lake.Backend.default,
                           platformIndependent := none,
+                          precompileImports := false,
                           dynlibs := #[],
                           plugins := #[],
                           requiresModuleSystem := false,
@@ -365,6 +370,7 @@ name = "Sorting"
                       libPrefixOnWindows := false,
                       needs := #[],
                       extraDepTargets := #[],
+                      precompileLibrary := false,
                       precompileModules := false,
                       defaultFacets := #[`lean_lib.leanArts],
                       nativeFacets := #<fun>,
@@ -589,6 +595,7 @@ name = "TacticTools"
           weakLinkArgs := #[],
           backend := Lake.Backend.default,
           platformIndependent := none,
+          precompileImports := false,
           dynlibs := #[],
           plugins := #[],
           requiresModuleSystem := false,
@@ -600,6 +607,7 @@ name = "TacticTools"
       libPrefixOnWindows := false,
       needs := #[],
       extraDepTargets := #[],
+      precompileLibrary := false,
       precompileModules := false,
       defaultFacets := #[`lean_lib.leanArts],
       nativeFacets := #<fun>,
@@ -634,6 +642,7 @@ precompileModules = true
           weakLinkArgs := #[],
           backend := Lake.Backend.default,
           platformIndependent := none,
+          precompileImports := false,
           dynlibs := #[],
           plugins := #[],
           requiresModuleSystem := false,
@@ -645,6 +654,7 @@ precompileModules = true
       libPrefixOnWindows := false,
       needs := #[],
       extraDepTargets := #[],
+      precompileLibrary := false,
       precompileModules := true,
       defaultFacets := #[`lean_lib.leanArts],
       nativeFacets := #<fun>,
@@ -687,6 +697,7 @@ name = "trustworthytool"
           weakLinkArgs := #[],
           backend := Lake.Backend.default,
           platformIndependent := none,
+          precompileImports := false,
           dynlibs := #[],
           plugins := #[],
           requiresModuleSystem := false,
@@ -737,6 +748,7 @@ exeName = "tt"
           weakLinkArgs := #[],
           backend := Lake.Backend.default,
           platformIndependent := none,
+          precompileImports := false,
           dynlibs := #[],
           plugins := #[],
           requiresModuleSystem := false,