From 7cbf163330cfd9a31bb06b9b5a6a173036c58b54 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Sat, 26 Sep 2026 15:41:01 +0200
Subject: [PATCH] fix: rebuild elaboration-time tools before building the
 manual

The manual runs subverso-extract-mod and extract-lakefile while
elaborating, but they weren't getting rebuilt on toolchain changes,
which led to weird errors.
---
 ExtractLakefile.lean                                      | 2 +-
 Manual/Meta/LakeToml.lean                                 | 4 ++--
 ManualLakeTest.lean                                       | 8 ++++++++
 {Manual/Meta/LakeToml => ManualLakeTest}/PackageTest.lean | 2 +-
 {Manual/Meta/LakeToml => ManualLakeTest}/Test.lean        | 0
 lakefile.lean                                             | 5 +++++
 6 files changed, 17 insertions(+), 4 deletions(-)
 create mode 100644 ManualLakeTest.lean
 rename {Manual/Meta/LakeToml => ManualLakeTest}/PackageTest.lean (99%)
 rename {Manual/Meta/LakeToml => ManualLakeTest}/Test.lean (100%)

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