diff --git a/ExtractLakefile.lean b/ExtractLakefile.lean
index 9f43722389..fa1d324b53 100644
--- a/ExtractLakefile.lean
+++ b/ExtractLakefile.lean
@@ -11,7 +11,7 @@ import SubVerso.Compat
 import SubVerso.Highlighting.Code
 import SubVerso.Module
 
-import Manual.Meta.LakeToml.PackageTest
+import ManualLakeTest.PackageTest
 
 /-!
 # Lean-format Lakefile Extractor
diff --git a/Manual/Meta/LakeToml.lean b/Manual/Meta/LakeToml.lean
index de5b188dcb..af17b1a158 100644
--- a/Manual/Meta/LakeToml.lean
+++ b/Manual/Meta/LakeToml.lean
@@ -19,8 +19,8 @@ import SubVerso.Examples
 import Manual.Meta.Basic
 import Manual.Meta.ExpectString
 import Manual.Meta.LakeToml.Toml
-import Manual.Meta.LakeToml.Test
-import Manual.Meta.LakeToml.PackageTest
+import ManualLakeTest.Test
+import ManualLakeTest.PackageTest
 
 import Lake.Toml.Decode
 import Lake.Load.Toml
diff --git a/ManualLakeTest.lean b/ManualLakeTest.lean
new file mode 100644
index 0000000000..59e6a24079
--- /dev/null
+++ b/ManualLakeTest.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import ManualLakeTest.Test
+import ManualLakeTest.PackageTest
diff --git a/Manual/Meta/LakeToml/PackageTest.lean b/ManualLakeTest/PackageTest.lean
similarity index 99%
rename from Manual/Meta/LakeToml/PackageTest.lean
rename to ManualLakeTest/PackageTest.lean
index f772a37f4e..edd405c377 100644
--- a/Manual/Meta/LakeToml/PackageTest.lean
+++ b/ManualLakeTest/PackageTest.lean
@@ -7,7 +7,7 @@ Author: David Thrane Christiansen
 import Lake.Toml.Decode
 import Lake.Load.Toml
 
-import Manual.Meta.LakeToml.Test
+import ManualLakeTest.Test
 
 /-!
 Shared `Manual.Toml.Test` instances for rendering an elaborated `Lake.Package` (and its constituent
diff --git a/Manual/Meta/LakeToml/Test.lean b/ManualLakeTest/Test.lean
similarity index 100%
rename from Manual/Meta/LakeToml/Test.lean
rename to ManualLakeTest/Test.lean
diff --git a/lakefile.lean b/lakefile.lean
index 5cc6d86cfc..48b65a50bb 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -58,6 +58,11 @@ lean_lib IndexMapGrind where
 @[default_target]
 lean_lib Manual where
   weakLeanArgs := lakePluginArgs%
+  -- These executables run during elaboration
+  needs := #[`@/subversoExtractMod, `@/«extract-lakefile»]
+
+/-- Rendering of elaborated Lake configurations, shared by `Manual` and `extract-lakefile`. -/
+lean_lib ManualLakeTest where
 
 /--
 Elaborates Lean-format `lakefile.lean` examples for the manual, emitting both the elaborated