diff --git a/doc/UsersGuide/Manuals.lean b/doc/UsersGuide/Manuals.lean
index 21576de2..18811910 100644
--- a/doc/UsersGuide/Manuals.lean
+++ b/doc/UsersGuide/Manuals.lean
@@ -6,8 +6,9 @@ Author: David Thrane Christiansen
 import Lean.DocString.Syntax
 import VersoManual
 import VersoBlog
+import VersoManual.DB
 
-open Verso Genre Manual
+open Verso Genre Manual DB
 
 open InlineLean
 open Verso.Doc
@@ -21,25 +22,47 @@ htmlSplit := .never
 Verso's {name}`Manual` genre can be used to write reference manuals, textbooks, or other book-like documents.
 It supports generating both HTML and PDFs via LaTeX, but the PDF support is relatively immature and untested compared to the HTML support.
 
+{dbDocstring Manual}
 {docstring Manual}
 
+
+
+
+{dbDocstring Manual.PartMetadata}
 {docstring Manual.PartMetadata}
 
+
+
+{dbDocstring Manual.HtmlSplitMode}
 {docstring Manual.HtmlSplitMode}
 
+
+
 The {name}`Manual` genre's block and inline element types are extensible.
 In the document, they consist of instances of {name}`Manual.Block` and {name}`Manual.Inline`, respectively:
 
+{dbDocstring Manual.Block}
 {docstring Manual.Block}
 
+
+
+{dbDocstring Manual.Inline}
 {docstring Manual.Inline}
 
+
+
 The fields {name}`Block.name` and {name Manual.Inline.name}`Inline.name` are used to look up concrete implementations of traversal and output generation in run-time tables that contain descriptions:
 
+{dbDocstring Manual.BlockDescr}
 {docstring Manual.BlockDescr}
 
+
+
+{dbDocstring Manual.InlineDescr}
 {docstring Manual.InlineDescr}
 
+
+
 Typically, the `inline_extension` and `block_extension` commands are used to simultaneously define an element and its descriptor, registering them for use by {name}`manualMain`.
 
 :::paragraph
@@ -47,12 +70,18 @@ The type {name}`HtmlAssets` contains CSS and JavaScript code.
 {name}`Manual.TraverseState`, {name}`Manual.BlockDescr`, and {name}`Manual.InlineDescr` all inherit from this structure.
 During traversal, HTML assets are collected; they are all included in the final rendered document.
 
+{dbDocstring Manual.HtmlAssets}
 {docstring Manual.HtmlAssets}
 
+
+
 Use {name}`HtmlAssets.combine` to combine multiple assets.
 
+{dbDocstring Manual.HtmlAssets.combine}
 {docstring Manual.HtmlAssets.combine}
 
+
+
 :::
 
 # Tags and References
@@ -92,13 +121,19 @@ tag := "docstrings"
 Docstrings can be included using the `docstring` directive. For instance,
 
 ```
+{dbDocstring List.forM}
 {docstring List.forM}
+
+
 ```
 
 results in
 
+{dbDocstring List.forM}
 {docstring List.forM}
 
+
+
 The {name}`docstring` command takes a positional parameter which is the documented name.
 It also accepts the following optional named parameters:
 
@@ -154,11 +189,17 @@ Elsewhere in the document, `tech` can be used to annotate a use site of a techni
 A {deftech}_technical term_ is a term with a specific meaning that's used precisely, like this one.
 References to technical terms are valid both before and after their definition sites.
 
+{dbDocstring deftech}
 {docstring deftech}
 
+
+
+{dbDocstring tech}
 {docstring tech}
 
 
+
+
 # Open-Source Licenses
 %%%
 tag := "oss-licenses"
@@ -168,8 +209,12 @@ To facilitate providing appropriate credit to the authors of open-source JavaScr
 This is done using the {name HtmlAssets.licenseInfo}`licenseInfo` field that {name}`BlockDescr` and {name}`InlineDescr` inherit from {name}`HtmlAssets`.
 These contain a {name}`LicenseInfo`:
 
+{dbDocstring LicenseInfo}
 {docstring LicenseInfo}
 
+
+
 The {name}`licenseInfo` command displays the licenses for all components that were included in the generated document:
 
+{dbDocstring licenseInfo}
 {docstring licenseInfo}
diff --git a/lake-manifest.json b/lake-manifest.json
index 03cf5b53..165aff77 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,7 +1,17 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/plausible",
+ [{"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "f178e492e7f345d7be5a57d2178e95f7a3cc070b",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "",
@@ -30,6 +40,46 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/david-christiansen/leansqlite",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "739abe6c8ae0602d6ce56461d33f3e49837c9b70",
+   "name": "leansqlite",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "474983579ecce1ca7d8a63e65c7ae0b1a22db6a3",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "9484dd63d30bce157c7f98007a9f26ca4dfb7fb6",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "29e7df238aa51dba17463e360e68657a8d433f43",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "verso",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index dbedffd7..dd7c9a2b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,6 +4,7 @@ open Lake DSL
 require subverso from git "https://github.com/leanprover/subverso"@"main"
 require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main"
 require plausible from git "https://github.com/leanprover-community/plausible"@"main"
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4"@"main"
 
 package verso where
   precompileModules := false -- temporarily disabled to work around an issue with nightly-2025-03-30
@@ -105,6 +106,7 @@ lean_exe «verso-demo» where
 lean_lib UsersGuide where
   srcDir := "doc"
   leanOptions := #[⟨`weak.linter.verso.manual.headerTags, true⟩]
+  needs := #[`@:docSource]
 
 @[default_target]
 lean_exe usersguide where
@@ -197,3 +199,38 @@ package_facet literate pkg : Array System.FilePath := do
   let libs := Job.collectArray (← pkg.leanLibs.mapM (·.facet `literate |>.fetch))
   let exes := Job.collectArray (← pkg.leanExes.mapM (·.toLeanLib.facet `literate |>.fetch))
   return libs.zipWith (·.flatten ++ ·.flatten) exes
+
+lean_exe «verso-docgen-setup» where
+  root := `VersoManual.DB.Setup
+  srcDir := "src/verso-manual"
+  supportInterpreter := true
+
+package_facet docSource pkg : System.FilePath := do
+  let ws ← getWorkspace
+  let exeJob ← «verso-docgen-setup».fetch
+
+  let pkgDir := ws.root.dir
+  let buildDir := ws.root.buildDir
+  let tomlPath := pkgDir / "doc-sources.toml"
+  let wsDir := buildDir / "verso-doc-db"
+  let dbPath := wsDir / ".lake" / "build" / "api-docs.db"
+
+  let docgen4Dir := match ws.findPackageByName? `«doc-gen4» with
+    | some pkg => pkg.dir
+    | none => buildDir / ".." / "packages" / "doc-gen4"
+
+  exeJob.mapM fun exeFile => do
+    -- Always run the setup exe and let the inner `lake build` handle incrementality.
+    -- This avoids stale DB issues from incomplete traces — the inner workspace's own
+    -- build system correctly tracks all dependencies (doc-gen4, documented libraries, etc.).
+    let args :=
+      if ← tomlPath.pathExists then
+        #[wsDir.toString, docgen4Dir.toString, pkgDir.toString, tomlPath.toString]
+      else
+        #[wsDir.toString, docgen4Dir.toString, pkgDir.toString]
+    proc {
+      cmd := exeFile.toString
+      args
+    }
+
+    pure dbPath
diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean
index 22534291..a5434416 100644
--- a/src/tests/TestMain.lean
+++ b/src/tests/TestMain.lean
@@ -153,6 +153,11 @@ def testBlog (_ : Config) : IO Unit := do
   if fails > 0 then
     throw <| .userError s!"{fails} blog tests failed"
 
+def testDocSourceConfig (_ : Config) : IO Unit := do
+  let fails ← runDocSourceConfigTests
+  if fails > 0 then
+    throw <| .userError s!"{fails} doc source config tests failed"
+
 -- Interactive tests via the LSP server
 def testInteractive (_ : Config) : IO Unit := do
   IO.println "Running interactive (LSP) tests..."
@@ -167,6 +172,7 @@ open Verso.Integration in
 def tests := [
   testSerialization,
   testBlog,
+  testDocSourceConfig,
   testStemmer,
   testTexOutput "sample-doc" SampleDoc.doc,
   testTexOutput "inheritance-doc" InheritanceDoc.doc,
diff --git a/src/tests/Tests.lean b/src/tests/Tests.lean
index 704aeeea..77d2d92f 100644
--- a/src/tests/Tests.lean
+++ b/src/tests/Tests.lean
@@ -31,3 +31,4 @@ import Tests.VersoBlog
 import Tests.VersoManual
 import Tests.Z85
 import Tests.Zip
+import Tests.DocSourceConfig
diff --git a/src/tests/Tests/DocSourceConfig.lean b/src/tests/Tests/DocSourceConfig.lean
new file mode 100644
index 00000000..151470ed
--- /dev/null
+++ b/src/tests/Tests/DocSourceConfig.lean
@@ -0,0 +1,361 @@
+/-
+Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import Lake.Toml
+import VersoManual.DB.Config
+
+/-! # Tests for Doc Source Configuration Parsing
+
+Tests for `Verso.Genre.Manual.DocSource.Config` — TOML parsing and lakefile generation.
+-/
+
+open Verso.Genre.Manual.DocSource
+open Lake.Toml
+
+/-- Parses a TOML string into a `Table`. Throws on parse error. -/
+private def parseToml (input : String) : IO Table := do
+  let ictx := Lean.Parser.mkInputContext input "<test>"
+  match (← Lake.Toml.loadToml ictx |>.toBaseIO) with
+  | .ok table => pure table
+  | .error msgs =>
+    let msgStrs ← msgs.toList.mapM fun msg => msg.data.toString
+    throw <| .userError s!"TOML parse error:\n{"\n".intercalate msgStrs}"
+
+/-- Asserts that two values are equal, throwing a descriptive error if not. -/
+private def assertEqual [BEq α] [Repr α] (label : String) (expected actual : α) : IO Unit := do
+  unless expected == actual do
+    throw <| IO.userError s!"{label}: expected\n  {repr expected}\nbut got\n  {repr actual}"
+
+/-- Asserts that a result is an error. -/
+private def assertError [Repr α] (label : String) (result : Except String α) : IO Unit := do
+  match result with
+  | .error _ => pure ()
+  | .ok v => throw <| IO.userError s!"{label}: expected an error but got\n  {repr v}"
+
+/-- Asserts that a string contains a substring. -/
+private def assertContains (label : String) (haystack needle : String) : IO Unit := do
+  unless (haystack.splitOn needle).length > 1 do
+    throw <| IO.userError s!"{label}: expected string to contain '{needle}' but got:\n  {haystack}"
+
+-- ============================================================================
+-- Config.ofToml tests
+-- ============================================================================
+
+private def testEmptyConfig : IO Unit := do
+  let table ← parseToml ""
+  let config ← IO.ofExcept <| Config.ofToml table
+  assertEqual "empty config require" #[] config.require
+  assertEqual "empty config libraries" #[] config.libraries
+  assertEqual "empty config setup" #[] config.setup
+
+private def testPathDependency : IO Unit := do
+  let table ← parseToml "
+[[require]]
+name = \"Batteries\"
+path = \"../batteries\"
+"
+  let config ← IO.ofExcept <| Config.ofToml table
+  assertEqual "path dep count" 1 config.require.size
+  let req := config.require[0]!
+  assertEqual "path dep name" "Batteries" req.name
+  assertEqual "path dep path" (some ⟨"../batteries"⟩) req.path
+  assertEqual "path dep git" none req.git
+  assertEqual "path dep rev" none req.rev
+
+private def testGitDependency : IO Unit := do
+  let table ← parseToml "
+[[require]]
+name = \"Mathlib\"
+git = \"https://github.com/leanprover-community/mathlib4\"
+rev = \"main\"
+"
+  let config ← IO.ofExcept <| Config.ofToml table
+  assertEqual "git dep count" 1 config.require.size
+  let req := config.require[0]!
+  assertEqual "git dep name" "Mathlib" req.name
+  assertEqual "git dep git" (some "https://github.com/leanprover-community/mathlib4") req.git
+  assertEqual "git dep rev" (some "main") req.rev
+  assertEqual "git dep path" none req.path
+
+private def testGitDepWithSubDir : IO Unit := do
+  let table ← parseToml "
+[[require]]
+name = \"MyLib\"
+git = \"https://github.com/example/monorepo\"
+rev = \"v1.0\"
+subDir = \"packages/mylib\"
+"
+  let config ← IO.ofExcept <| Config.ofToml table
+  let req := config.require[0]!
+  assertEqual "subDir dep name" "MyLib" req.name
+  assertEqual "subDir dep subDir" (some "packages/mylib") req.subDir
+
+private def testMultipleRequires : IO Unit := do
+  let table ← parseToml "
+[[require]]
+name = \"Batteries\"
+git = \"https://github.com/leanprover/batteries\"
+rev = \"main\"
+
+[[require]]
+name = \"Mathlib\"
+git = \"https://github.com/leanprover-community/mathlib4\"
+rev = \"main\"
+"
+  let config ← IO.ofExcept <| Config.ofToml table
+  assertEqual "multi req count" 2 config.require.size
+  assertEqual "multi req first name" "Batteries" config.require[0]!.name
+  assertEqual "multi req second name" "Mathlib" config.require[1]!.name
+
+private def testLibrariesField : IO Unit := do
+  let table ← parseToml "
+libraries = [\"Mathlib\", \"Batteries\"]
+
+[[require]]
+name = \"Mathlib\"
+git = \"https://github.com/leanprover-community/mathlib4\"
+rev = \"main\"
+"
+  let config ← IO.ofExcept <| Config.ofToml table
+  assertEqual "libraries" #["Mathlib", "Batteries"] config.libraries
+
+private def testSetupField : IO Unit := do
+  let table ← parseToml "
+setup = [\"lake exe cache get\", \"lake build Foo\"]
+"
+  let config ← IO.ofExcept <| Config.ofToml table
+  assertEqual "setup" #["lake exe cache get", "lake build Foo"] config.setup
+
+private def testFullConfig : IO Unit := do
+  let table ← parseToml "
+setup = [\"lake exe cache get\"]
+libraries = [\"Mathlib\"]
+
+[[require]]
+name = \"Mathlib\"
+git = \"https://github.com/leanprover-community/mathlib4\"
+rev = \"main\"
+"
+  let config ← IO.ofExcept <| Config.ofToml table
+  assertEqual "full config setup" #["lake exe cache get"] config.setup
+  assertEqual "full config libraries" #["Mathlib"] config.libraries
+  assertEqual "full config require count" 1 config.require.size
+  assertEqual "full config require name" "Mathlib" config.require[0]!.name
+
+private def testMissingName : IO Unit := do
+  let table ← parseToml "
+[[require]]
+git = \"https://github.com/example/lib\"
+"
+  let result := Config.ofToml table
+  assertError "missing name" result
+
+private def testNoRequireEntries : IO Unit := do
+  let table ← parseToml "
+libraries = [\"Init\"]
+"
+  let config ← IO.ofExcept <| Config.ofToml table
+  assertEqual "no requires" #[] config.require
+  assertEqual "libraries only" #["Init"] config.libraries
+
+-- ============================================================================
+-- Lakefile generation tests
+-- ============================================================================
+
+private def testLakefileGenCoreOnly : IO Unit := do
+  let lakefile := generateLakefile none "/abs/path/to/doc-gen4" "/project"
+  assertContains "core-only header" lakefile "import Lake"
+  assertContains "core-only package" lakefile "package «docgen-workspace»"
+  assertContains "core-only docgen4" lakefile "require «doc-gen4» from \"/abs/path/to/doc-gen4\""
+  -- Should not contain any user requires
+  let lines := lakefile.splitOn "\n"
+  let requireCount := lines.filter (·.startsWith "require") |>.length
+  -- Only the doc-gen4 require
+  assertEqual "core-only require count" 1 requireCount
+
+private def testLakefileGenGitDep : IO Unit := do
+  let config : Config := {
+    require := #[{
+      name := "Mathlib"
+      git := some "https://github.com/leanprover-community/mathlib4"
+      rev := some "main"
+    }]
+  }
+  let lakefile := generateLakefile (some config) "/path/to/doc-gen4" "/project"
+  assertContains "git dep lakefile docgen4" lakefile "require «doc-gen4» from \"/path/to/doc-gen4\""
+  assertContains "git dep lakefile Mathlib" lakefile "require «Mathlib» from git"
+  assertContains "git dep lakefile url" lakefile "\"https://github.com/leanprover-community/mathlib4\""
+  assertContains "git dep lakefile rev" lakefile "@ \"main\""
+
+private def testLakefileGenPathDep : IO Unit := do
+  let config : Config := {
+    require := #[{
+      name := "Batteries"
+      path := some "../batteries"
+    }]
+  }
+  let lakefile := generateLakefile (some config) "/path/to/doc-gen4" "/project"
+  -- Path should be resolved to absolute
+  assertContains "path dep lakefile abs" lakefile "require «Batteries» from \"/project/../batteries\""
+
+private def testLakefileGenAbsPathDep : IO Unit := do
+  let config : Config := {
+    require := #[{
+      name := "Batteries"
+      path := some "/absolute/path/to/batteries"
+    }]
+  }
+  let lakefile := generateLakefile (some config) "/path/to/doc-gen4" "/project"
+  assertContains "abs path dep lakefile" lakefile "require «Batteries» from \"/absolute/path/to/batteries\""
+
+private def testLakefileGenMultipleDeps : IO Unit := do
+  let config : Config := {
+    require := #[
+      { name := "Batteries", git := some "https://github.com/leanprover/batteries", rev := some "main" },
+      { name := "Mathlib", git := some "https://github.com/leanprover-community/mathlib4", rev := some "main" }
+    ]
+  }
+  let lakefile := generateLakefile (some config) "/path/to/doc-gen4" "/project"
+  assertContains "multi dep Batteries" lakefile "require «Batteries»"
+  assertContains "multi dep Mathlib" lakefile "require «Mathlib»"
+
+-- ============================================================================
+-- splitCommand tests
+-- ============================================================================
+
+private def testSplitSimple : IO Unit := do
+  assertEqual "simple" (some ("lake", #["exe", "cache", "get"])) (splitCommand "lake exe cache get")
+
+private def testSplitSingleArg : IO Unit := do
+  assertEqual "single arg" (some ("lake", #[])) (splitCommand "lake")
+
+private def testSplitEmpty : IO Unit := do
+  assertEqual "empty" none (splitCommand "")
+
+private def testSplitOnlySpaces : IO Unit := do
+  assertEqual "only spaces" none (splitCommand "   ")
+
+private def testSplitLeadingTrailingSpaces : IO Unit := do
+  assertEqual "leading/trailing" (some ("lake", #["build"])) (splitCommand "  lake  build  ")
+
+private def testSplitTabs : IO Unit := do
+  assertEqual "tabs" (some ("lake", #["build", "Foo"])) (splitCommand "lake\tbuild\tFoo")
+
+private def testSplitMixedWhitespace : IO Unit := do
+  assertEqual "mixed ws" (some ("lake", #["build"])) (splitCommand " \t lake \t build \t ")
+
+private def testSplitDoubleQuoted : IO Unit := do
+  assertEqual "double quoted" (some ("echo", #["hello world"])) (splitCommand "echo \"hello world\"")
+
+private def testSplitSingleQuoted : IO Unit := do
+  assertEqual "single quoted" (some ("echo", #["hello world"])) (splitCommand "echo 'hello world'")
+
+private def testSplitDoubleQuotedBackslash : IO Unit := do
+  assertEqual "dq backslash" (some ("echo", #["hello\"world"])) (splitCommand "echo \"hello\\\"world\"")
+
+private def testSplitDoubleQuotedBackslashN : IO Unit := do
+  assertEqual "dq backslash-n" (some ("echo", #["hellonworld"])) (splitCommand "echo \"hello\\nworld\"")
+
+private def testSplitSingleQuotedNoEscape : IO Unit := do
+  assertEqual "sq no escape" (some ("echo", #["hello\\nworld"])) (splitCommand "echo 'hello\\nworld'")
+
+private def testSplitEmptyDoubleQuotes : IO Unit := do
+  assertEqual "empty dq" (some ("echo", #[""])) (splitCommand "echo \"\"")
+
+private def testSplitEmptySingleQuotes : IO Unit := do
+  assertEqual "empty sq" (some ("echo", #[""])) (splitCommand "echo ''")
+
+private def testSplitQuotedConcat : IO Unit := do
+  -- "hello"' '"world" → hello world (quotes are just delimiters, adjacent runs concatenate)
+  assertEqual "quoted concat" (some ("echo", #["hello world"])) (splitCommand "echo \"hello\"' 'world")
+
+private def testSplitMixedQuotesInArg : IO Unit := do
+  assertEqual "mixed quotes" (some ("cmd", #["it's", "a \"test\""])) (splitCommand "cmd \"it's\" 'a \"test\"'")
+
+private def testSplitUnclosedDoubleQuote : IO Unit := do
+  -- Unmatched quote is treated as if closed at end of string
+  assertEqual "unclosed dq" (some ("echo", #["hello world"])) (splitCommand "echo \"hello world")
+
+private def testSplitUnclosedSingleQuote : IO Unit := do
+  assertEqual "unclosed sq" (some ("echo", #["hello world"])) (splitCommand "echo 'hello world")
+
+private def testSplitQuotedEmpty : IO Unit := do
+  -- Just a pair of quotes produces a single empty-string argument (the executable name)
+  assertEqual "just quotes" (some ("", #[])) (splitCommand "\"\"")
+
+private def testSplitBackslashInDoubleQuotes : IO Unit := do
+  -- Backslash at end of double-quoted string
+  assertEqual "trailing backslash in dq" (some ("echo", #["hello\\"])) (splitCommand "echo \"hello\\\\\"")
+
+private def testSplitMultipleQuotedArgs : IO Unit := do
+  assertEqual "multi quoted" (some ("cmd", #["arg one", "arg two", "three"])) (splitCommand "cmd 'arg one' \"arg two\" three")
+
+private def testSplitPathWithSpaces : IO Unit := do
+  assertEqual "path with spaces" (some ("cd", #["/path/to/my project"])) (splitCommand "cd '/path/to/my project'")
+
+private def testSplitConsecutiveSpaces : IO Unit := do
+  assertEqual "consecutive spaces" (some ("a", #["b", "c"])) (splitCommand "a    b    c")
+
+private def testSplitTabsAndSpaces : IO Unit := do
+  assertEqual "tabs and spaces" (some ("a", #["b"])) (splitCommand "\t a \t b \t")
+
+-- ============================================================================
+-- Test runner
+-- ============================================================================
+
+private def docSourceConfigTests : List (String × IO Unit) := [
+  ("Config.ofToml: empty config", testEmptyConfig),
+  ("Config.ofToml: path dependency", testPathDependency),
+  ("Config.ofToml: git dependency", testGitDependency),
+  ("Config.ofToml: git dep with subDir", testGitDepWithSubDir),
+  ("Config.ofToml: multiple requires", testMultipleRequires),
+  ("Config.ofToml: libraries field", testLibrariesField),
+  ("Config.ofToml: setup field", testSetupField),
+  ("Config.ofToml: full config", testFullConfig),
+  ("Config.ofToml: missing name error", testMissingName),
+  ("Config.ofToml: no require entries", testNoRequireEntries),
+  ("generateLakefile: core-only", testLakefileGenCoreOnly),
+  ("generateLakefile: git dependency", testLakefileGenGitDep),
+  ("generateLakefile: path dependency (relative)", testLakefileGenPathDep),
+  ("generateLakefile: path dependency (absolute)", testLakefileGenAbsPathDep),
+  ("generateLakefile: multiple dependencies", testLakefileGenMultipleDeps),
+  ("splitCommand: simple", testSplitSimple),
+  ("splitCommand: single arg", testSplitSingleArg),
+  ("splitCommand: empty", testSplitEmpty),
+  ("splitCommand: only spaces", testSplitOnlySpaces),
+  ("splitCommand: leading/trailing spaces", testSplitLeadingTrailingSpaces),
+  ("splitCommand: tabs", testSplitTabs),
+  ("splitCommand: mixed whitespace", testSplitMixedWhitespace),
+  ("splitCommand: double quoted", testSplitDoubleQuoted),
+  ("splitCommand: single quoted", testSplitSingleQuoted),
+  ("splitCommand: dq backslash escape", testSplitDoubleQuotedBackslash),
+  ("splitCommand: dq backslash-n", testSplitDoubleQuotedBackslashN),
+  ("splitCommand: sq no escape", testSplitSingleQuotedNoEscape),
+  ("splitCommand: empty double quotes", testSplitEmptyDoubleQuotes),
+  ("splitCommand: empty single quotes", testSplitEmptySingleQuotes),
+  ("splitCommand: quoted concatenation", testSplitQuotedConcat),
+  ("splitCommand: mixed quotes in arg", testSplitMixedQuotesInArg),
+  ("splitCommand: unclosed double quote", testSplitUnclosedDoubleQuote),
+  ("splitCommand: unclosed single quote", testSplitUnclosedSingleQuote),
+  ("splitCommand: just quotes", testSplitQuotedEmpty),
+  ("splitCommand: backslash in double quotes", testSplitBackslashInDoubleQuotes),
+  ("splitCommand: multiple quoted args", testSplitMultipleQuotedArgs),
+  ("splitCommand: path with spaces", testSplitPathWithSpaces),
+  ("splitCommand: consecutive spaces", testSplitConsecutiveSpaces),
+  ("splitCommand: tabs and spaces", testSplitTabsAndSpaces),
+]
+
+public def runDocSourceConfigTests : IO Nat := do
+  IO.println "Running doc source config tests..."
+  let mut failures := 0
+  for (name, test) in docSourceConfigTests do
+    IO.print s!"  {name}: "
+    try
+      test
+      IO.println "ok"
+    catch e =>
+      IO.println s!"FAIL\n    {e}"
+      failures := failures + 1
+  return failures
diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index ab43b0b7..e52c9c1e 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/src/verso-manual/VersoManual.lean
@@ -42,6 +42,7 @@ import VersoManual.Literate
 import VersoManual.Marginalia
 import VersoManual.Bibliography
 import VersoManual.Table
+import VersoManual.DB
 
 open Lean (Name NameMap Json ToJson FromJson quote)
 
diff --git a/src/verso-manual/VersoManual/DB.lean b/src/verso-manual/VersoManual/DB.lean
new file mode 100644
index 00000000..d4599092
--- /dev/null
+++ b/src/verso-manual/VersoManual/DB.lean
@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import VersoManual.DB.Config
+import VersoManual.DB.Convert
+import VersoManual.DB.Query
+import VersoManual.DB.Docstring
diff --git a/src/verso-manual/VersoManual/DB/Config.lean b/src/verso-manual/VersoManual/DB/Config.lean
new file mode 100644
index 00000000..f617036a
--- /dev/null
+++ b/src/verso-manual/VersoManual/DB/Config.lean
@@ -0,0 +1,192 @@
+/-
+Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import Lake.Toml
+
+/-! # Doc Source Configuration
+
+Parsing and code generation for `doc-sources.toml`, which declares which packages' documentation
+should be built by the `docSource` Lake package facet.
+
+The `[[require]]` entries use the same field names as `lakefile.toml`.
+-/
+
+namespace Verso.Genre.Manual.DocSource
+
+open Lake.Toml
+
+/-- Dependency entry from `doc-sources.toml`, mirroring `[[require]]` in `lakefile.toml`. -/
+structure Require where
+  /-- The package name (must match the name declared in its lakefile). -/
+  name : String
+  /-- Git repository URL. -/
+  git : Option String := none
+  /-- Git revision (branch, tag, or commit hash). -/
+  rev : Option String := none
+  /-- Local filesystem path (relative to the project root). -/
+  path : Option System.FilePath := none
+  /-- Subdirectory within the repository. -/
+  subDir : Option String := none
+deriving Repr, BEq, Inhabited
+
+/-- Parsed contents of a `doc-sources.toml` file. -/
+structure Config where
+  /-- Package dependencies whose documentation should be built. -/
+  require : Array Require := #[]
+  /--
+  Which library targets to document. Defaults to default library targets of all required
+  packages.
+  -/
+  libraries : Array String := #[]
+  /-- Shell commands to run in the managed workspace before building (e.g., `lake exe cache get`). -/
+  setup : Array String := #[]
+deriving Repr, BEq, Inhabited
+
+/-- Extracts a `String` from a TOML `Value`, or `none` if it's not a string. -/
+private def tomlString? : Value → Option String
+  | .string _ s => some s
+  | _ => none
+
+/--
+Extracts an `Array String` from a TOML array of strings. Non-string elements are silently
+skipped.
+-/
+private def tomlStringArray? : Value → Option (Array String)
+  | .array _ vs => some <| vs.filterMap tomlString?
+  | _ => none
+
+/-- Parses a single `[[require]]` entry from a TOML table value. -/
+def Require.ofToml (v : Value) : Except String Require := do
+  match v with
+  | .table' _ t =>
+    let name ← match t.find? `name with
+      | some v => match tomlString? v with
+        | some s => pure s
+        | none => throw "[[require]] entry 'name' field must be a string"
+      | none => throw "[[require]] entry is missing the required 'name' field"
+    let git := t.find? `git >>= tomlString?
+    let rev := t.find? `rev >>= tomlString?
+    let path := t.find? `path >>= tomlString? |>.map System.FilePath.mk
+    let subDir := t.find? `subDir >>= tomlString?
+    pure { name, git, rev, path, subDir }
+  | _ => throw "[[require]] entry must be a table"
+
+/-- Parses a `Config` from a TOML `Table`. -/
+def Config.ofToml (table : Table) : Except String Config := do
+  let require ← match table.find? `require with
+    | some (.array _ vs) => vs.mapM Require.ofToml
+    | some _ => throw "'require' must be an array of tables ([[require]])"
+    | none => pure #[]
+  let libraries := match table.find? `libraries with
+    | some v => tomlStringArray? v |>.getD #[]
+    | none => #[]
+  let setup := match table.find? `setup with
+    | some v => tomlStringArray? v |>.getD #[]
+    | none => #[]
+  pure { require, libraries, setup }
+
+/-- Loads and parses a `doc-sources.toml` file. -/
+def Config.load (filePath : System.FilePath) : IO Config := do
+  let input ← IO.FS.readFile filePath
+  let ictx := Lean.Parser.mkInputContext input filePath.toString
+  match (← Lake.Toml.loadToml ictx |>.toBaseIO) with
+  | .ok table =>
+    match Config.ofToml table with
+    | .ok config => pure config
+    | .error e => throw <| .userError s!"Error parsing {filePath}: {e}"
+  | .error msgs =>
+    let msgStrs ← msgs.toList.mapM fun msg => msg.data.toString
+    throw <| .userError s!"Error parsing {filePath}:\n{"\n".intercalate msgStrs}"
+
+/--
+Splits a command string into an executable name and arguments, respecting single and double
+quotes. Backslash escapes the next character inside double quotes. Unmatched quotes are
+treated as if closed at the end of the string.
+-/
+def splitCommand (cmd : String) : Option (String × Array String) := do
+  let mut args : Array String := #[]
+  let mut cur : String := ""
+  -- Track whether the current word contains any content (including empty quotes)
+  let mut inWord := false
+  let mut i := 0
+  let chars := cmd.toList
+  while i < chars.length do
+    let c := chars[i]!
+    if c == '\'' then
+      -- Single-quoted: everything up to closing ' is literal
+      inWord := true
+      i := i + 1
+      while i < chars.length && chars[i]! != '\'' do
+        cur := cur.push chars[i]!
+        i := i + 1
+      -- skip closing quote (or end of string)
+      i := i + 1
+    else if c == '"' then
+      -- Double-quoted: backslash escapes the next character
+      inWord := true
+      i := i + 1
+      while i < chars.length && chars[i]! != '"' do
+        if chars[i]! == '\\' && i + 1 < chars.length then
+          i := i + 1
+          cur := cur.push chars[i]!
+        else
+          cur := cur.push chars[i]!
+        i := i + 1
+      -- skip closing quote (or end of string)
+      i := i + 1
+    else if c == ' ' || c == '\t' then
+      if inWord then
+        args := args.push cur
+        cur := ""
+        inWord := false
+      i := i + 1
+    else
+      cur := cur.push c
+      inWord := true
+      i := i + 1
+  if inWord then
+    args := args.push cur
+  match args.toList with
+  | [] => none
+  | exe :: rest => some (exe, rest.toArray)
+
+/-- Generates a `require` declaration in lakefile.lean syntax for a single dependency. -/
+def Require.toLakefileEntry (r : Require) (projectDir : System.FilePath) : String :=
+  let name := s!"require «{r.name}»"
+  match r.git, r.path with
+  | some url, _ =>
+    -- Resolve relative git URLs against the project root, since the generated
+    -- lakefile lives in the managed workspace, not the project root.
+    let absUrl := if System.FilePath.isAbsolute ⟨url⟩ || (url.splitOn "://").length > 1 then url
+                  else (projectDir / url).toString
+    let revPart := r.rev.map (s!" @ \"{·}\"") |>.getD ""
+    let subDirPart := r.subDir.map (s!" / \"{·}\"") |>.getD ""
+    s!"{name} from git\n  \"{absUrl}\"{revPart}{subDirPart}\n"
+  | _, some path =>
+    -- Resolve relative paths against the project root to produce absolute paths,
+    -- since the generated lakefile lives in the managed workspace, not the project root.
+    let absPath := if path.isAbsolute then path else projectDir / path
+    s!"{name} from \"{absPath}\"\n"
+  | none, none =>
+    -- No source specified — Lake will look it up in the registry
+    s!"{name}\n"
+
+/--
+Generates a complete `lakefile.lean` for the managed doc-gen workspace.
+
+`config` is the parsed `doc-sources.toml` (or `none` for a core-only build).
+`docgen4Dir` is the absolute path to the doc-gen4 package checkout.
+`projectDir` is the absolute path to the user's project root.
+-/
+def generateLakefile (config : Option Config)
+    (docgen4Dir : System.FilePath) (projectDir : System.FilePath) : String :=
+  let header := "import Lake\nopen Lake DSL\n\npackage «docgen-workspace»\n\n"
+  let docgenReq := s!"require «doc-gen4» from git\n  \"{docgen4Dir}\"\n\n"
+  let userReqs := match config with
+    | some cfg => cfg.require.map (·.toLakefileEntry projectDir) |>.toList |> String.join
+    | none => ""
+  header ++ docgenReq ++ userReqs
+
+end Verso.Genre.Manual.DocSource
diff --git a/src/verso-manual/VersoManual/DB/Convert.lean b/src/verso-manual/VersoManual/DB/Convert.lean
new file mode 100644
index 00000000..9988f8c0
--- /dev/null
+++ b/src/verso-manual/VersoManual/DB/Convert.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import DocGen4.RenderedCode
+import SubVerso.Highlighting.Highlighted
+
+/-! # RenderedCode → Highlighted Conversion
+
+Doc-gen4 stores types as `RenderedCode` (`TaggedText RenderedCode.Tag`) binary blobs. Verso renders
+all code using SubVerso's `Highlighted` type. This module converts between them.
+
+The conversion is lossy: `RenderedCode` does not carry hover info, variable types, or go-to-definition
+targets. The visual rendering is the same — tokens that were keywords, string literals, or constant
+references are tagged appropriately for syntax highlighting and linking.
+-/
+
+namespace Verso.Genre.Manual.DB
+
+open DocGen4 (RenderedCode SortFormer)
+open SubVerso.Highlighting (Highlighted Token)
+
+/-- Extract plain text content from a `RenderedCode` tree, discarding all tags. -/
+partial def renderedCodeText : RenderedCode → String
+  | .text s => s
+  | .tag _ inner => renderedCodeText inner
+  | .append xs => String.join (xs.toList.map renderedCodeText)
+
+/--
+Convert a `RenderedCode` value (from doc-gen4's database) to a `Highlighted` value (for Verso's
+rendering pipeline). Tags are mapped as follows:
+
+- `.keyword` → `Token.Kind.keyword` (no name or docs)
+- `.string` → `Token.Kind.str`
+- `.const name` → `Token.Kind.const` (with signature and docstring from `constInfo` if available)
+- `.sort` → `Token.Kind.sort` (no docs)
+- `.otherExpr` → plain `Highlighted.text` (no semantic info)
+
+The `constInfo` parameter provides hover data for known constants: a map from `Name` to
+`(signature, docstring?)`.
+-/
+partial def renderedCodeToHighlighted (constInfo : Lean.NameMap (String × Option String) := {})
+    : RenderedCode → Highlighted
+  | .text s => .text s
+  | .tag t inner =>
+    let content := renderedCodeText inner
+    match t with
+    | .keyword => .token ⟨.keyword none none none, content⟩
+    | .string => .token ⟨.str content, content⟩
+    | .const name =>
+      let (sig, doc?) := constInfo.find? name |>.getD ("", none)
+      .token ⟨.const name sig doc? false none, content⟩
+    | .sort _former => .token ⟨.sort none, content⟩
+    | .otherExpr => renderedCodeToHighlighted constInfo inner
+  | .append xs => .seq (xs.map (renderedCodeToHighlighted constInfo))
+
+/-- Collect all constant names referenced in a `RenderedCode` tree. -/
+partial def renderedCodeConstNames (acc : Lean.NameSet := {}) : RenderedCode → Lean.NameSet
+  | .text _ => acc
+  | .tag (.const name) inner => renderedCodeConstNames (acc.insert name) inner
+  | .tag _ inner => renderedCodeConstNames acc inner
+  | .append xs => xs.foldl (init := acc) fun a x => renderedCodeConstNames a x
+
+end Verso.Genre.Manual.DB
diff --git a/src/verso-manual/VersoManual/DB/Docstring.lean b/src/verso-manual/VersoManual/DB/Docstring.lean
new file mode 100644
index 00000000..3348435a
--- /dev/null
+++ b/src/verso-manual/VersoManual/DB/Docstring.lean
@@ -0,0 +1,164 @@
+/-
+Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import VersoManual.DB.Query
+import VersoManual.Docstring
+import VersoManual.Markdown
+
+import Verso.Doc.Elab.Block
+import Verso.Doc.Elab.Monad
+import Verso.Doc.ArgParse
+import Verso.Doc.PointOfInterest
+
+import MD4Lean
+
+/-! # DB-Backed Docstring Command
+
+A `{dbDocstring}` block command that reads documentation data from a doc-gen4 SQLite database rather
+than from the Lean `Environment`. Produces the same `Block.docstring` output as the existing
+environment-based `{docstring}` command, so the HTML/TeX rendering pipeline works unchanged.
+-/
+
+open Lean
+open Verso.Doc.Elab.PartElabM
+open Verso.Code
+open Verso.ArgParse
+open SubVerso.Highlighting
+
+namespace Verso.Genre.Manual.DB
+
+/-- Locate the doc-gen4 database path relative to the current working directory. -/
+private def getDbPath : IO System.FilePath := do
+  let cwd ← IO.currentDir
+  return cwd / ".lake" / "build" / "verso-doc-db" / ".lake" / "build" / "api-docs.db"
+
+
+private structure DBDocstringConfig where
+  name : Ident × Name
+  allowMissing : Bool
+  hideFields : Bool := false
+  hideStructureConstructor : Bool := false
+  label : Option String := none
+
+section
+variable {m} [Monad m] [MonadOptions m] [MonadEnv m] [MonadLiftT CoreM m] [MonadError m]
+  [MonadLog m] [AddMessageContext m] [Lean.Elab.MonadInfoTree m] [MonadLiftT MetaM m]
+
+private def DBDocstringConfig.parse : ArgParse m DBDocstringConfig :=
+  DBDocstringConfig.mk <$>
+    .positional `name .documentableName <*>
+    .flagM `allowMissing (verso.docstring.allowMissing.get <$> getOptions)
+      "Warn instead of error on missing docstrings (defaults to value of option `verso.docstring.allowMissing)" <*>
+    .flag `hideFields false <*>
+    .flag `hideStructureConstructor false <*>
+    .named `label .string true
+
+instance : FromArgs DBDocstringConfig m := ⟨DBDocstringConfig.parse⟩
+
+end
+
+private def getExtras (name : Name) (declType : Block.Docstring.DeclType) :
+    Verso.Doc.Elab.DocElabM (Array Term) :=
+  match declType with
+  | .structure isClass constructor? _ fieldInfo parents _ => do
+    let ctorRow : Option Term ← constructor?.mapM fun constructor => do
+      let header := if isClass then "Instance Constructor" else "Constructor"
+      let sigDesc : Array Term ←
+        if let some docs := constructor.docstring? then
+          let some mdAst := MD4Lean.parse docs
+            | throwError "Failed to parse docstring as Markdown"
+          mdAst.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders))
+        else pure (#[] : Array Term)
+      let sig ← `(Verso.Doc.Block.other (Verso.Genre.Manual.Block.internalSignature $(quote constructor.hlName) none) #[$sigDesc,*])
+      ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$sig])
+
+    let parentsRow : Option Term ← do
+      if parents.isEmpty then pure none
+      else
+        let header := "Extends"
+        let inh ← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.inheritance $(quote name) $(quote parents)) #[])
+        some <$> ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$inh])
+
+    let fieldsRow : Option Term ← do
+      let header := if isClass then "Methods" else "Fields"
+      let fieldInfo := fieldInfo.filter (·.subobject?.isNone)
+      let fieldSigs : Array Term ← fieldInfo.mapM fun i => do
+        let inheritedFrom : Option Nat :=
+          i.fieldFrom.head?.bind (fun n => parents.findIdx? (·.name == n.name))
+        let sigDesc : Array Term ←
+          if let some docs := i.docString? then
+            let some mdAst := MD4Lean.parse docs
+              | throwError "Failed to parse docstring as Markdown"
+            mdAst.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders))
+          else
+            pure (#[] : Array Term)
+        ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.fieldSignature $(quote i.visibility) $(quote i.fieldName) $(quote i.type) $(quote inheritedFrom) $(quote <| parents.map (·.parent))) #[$sigDesc,*])
+      if fieldSigs.isEmpty then pure none
+      else some <$> ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$fieldSigs,*])
+
+    pure <| ctorRow.toArray ++ parentsRow.toArray ++ fieldsRow.toArray
+  | .inductive ctors .. => do
+    let ctorSigs : Array Term ←
+      ctors.mapM fun c => do
+        let sigDesc ←
+          if let some docs := c.docstring? then
+            let some mdAst := MD4Lean.parse docs
+              | throwError "Failed to parse docstring as Markdown"
+            mdAst.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders))
+          else pure (#[] : Array Term)
+        ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.constructorSignature $(quote c.signature)) #[$sigDesc,*])
+    pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection "Constructors") #[$ctorSigs,*])]
+  | _ => pure #[]
+
+open Verso.Genre.Manual.Markdown in
+open Verso.Doc.Elab in
+@[block_command]
+def dbDocstring : BlockCommandOf DBDocstringConfig
+  | ⟨(x, name), allowMissing, hideFields, hideCtor, customLabel⟩ => do
+    let opts : Options → Options :=
+      (verso.docstring.allowMissing.set · allowMissing)
+    withOptions opts do
+      Doc.PointOfInterest.save (← getRef) name.toString (detail? := some "Documentation")
+
+      -- Locate and open the database
+      let dbPath ← getDbPath
+      unless ← dbPath.pathExists do
+        throwErrorAt x m!"Documentation database not found at '{dbPath}'. Run `lake build` to generate it."
+
+      -- Look up the declaration
+      let some docInfo ← lookupDocInfo dbPath name
+        | throwErrorAt x m!"'{name}' not found in the documentation database."
+
+      let info := docInfo.toInfo
+      let ci ← constInfoMap dbPath docInfo
+
+      -- Extract and parse docstring
+      let blockStx ← do
+        match docStringOfDoc? info.doc with
+        | none => pure #[]
+        | some docs =>
+          let some ast := MD4Lean.parse docs
+            | throwErrorAt x "Failed to parse docstring as Markdown"
+          ast.blocks.mapM (blockFromMarkdown · (handleHeaders := strongEmphHeaders))
+
+      -- Check deprecation
+      let isDeprecated := info.attrs.any (·.startsWith "deprecated")
+      if !(← Docstring.getAllowDeprecated) && isDeprecated then
+        Lean.logError m!"'{name}' is deprecated.\n\nSet option 'verso.docstring.allowDeprecated' to 'true' to allow documentation for deprecated names."
+
+      -- Build DeclType from DocInfo
+      let declType := buildDeclType docInfo (hideFields := hideFields) (hideStructureConstructor := hideCtor) ci
+
+      -- Build Signature (includes declaration name)
+      let signature := signatureOfInfo info ci
+
+      -- Build extras for structures and inductives
+      let extras ← getExtras name declType
+
+      ``(Verso.Doc.Block.other
+          (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature) $(quote customLabel) $(quote (#[] : Array Name)))
+          #[$(blockStx ++ extras),*])
+
+end Verso.Genre.Manual.DB
diff --git a/src/verso-manual/VersoManual/DB/Query.lean b/src/verso-manual/VersoManual/DB/Query.lean
new file mode 100644
index 00000000..c8a3f82c
--- /dev/null
+++ b/src/verso-manual/VersoManual/DB/Query.lean
@@ -0,0 +1,349 @@
+/-
+Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import DocGen4.DB
+import DocGen4.DB.VersoDocString
+import DocGen4.Process.Base
+import SQLite
+
+import VersoManual.DB.Convert
+import VersoManual.Docstring
+
+/-! # DB Querying and Type Reconstruction
+
+High-level API for querying the doc-gen4 database and converting the results into Verso's
+documentation types (`DeclType`, `Signature`, `DocName`, `FieldInfo`, `ParentInfo`).
+-/
+
+namespace Verso.Genre.Manual.DB
+
+open Lean
+open DocGen4 (RenderedCode)
+open DocGen4.Process (DocInfo NameInfo)
+open DocGen4.DB (ReadDB openForReading builtinDocstringValues)
+open SubVerso.Highlighting (Highlighted Token)
+open Verso.Genre.Manual (Signature)
+open Verso.Genre.Manual.Block.Docstring (DeclType DocName FieldInfo ParentInfo Visibility)
+
+/-- Extract a markdown docstring from a doc-gen4 `NameInfo.doc` field. -/
+def docStringOfDoc? (doc : Option (String ⊕ VersoDocString)) : Option String :=
+  doc.bind fun
+    | .inl md => some md
+    | .inr v => some (DocGen4.Process.versoDocToMarkdown v)
+
+/-- Build a `DocName` from a doc-gen4 `NameInfo`.
+When `showNamespace` is `true` (the default), the full qualified name is displayed.
+When `false`, only the last component is shown (used for inductive constructors).
+The `sigOverride` parameter allows providing a custom hover signature string (e.g., with named
+parameters for structure constructors). -/
+def docNameOfNameInfo (ni : NameInfo)
+    (constInfo : Lean.NameMap (String × Option String) := {})
+    (showNamespace : Bool := true)
+    (sigOverride : Option String := none) : DocName :=
+  let docstring? := docStringOfDoc? ni.doc
+  let sigStr := sigOverride.getD s!"{ni.name} : {renderedCodeText ni.type}"
+  let displayName := if showNamespace then ni.name.toString else ni.name.getString!
+  let nameHl := Highlighted.token ⟨.const ni.name sigStr docstring? false none, displayName⟩
+  { name := ni.name
+    hlName := nameHl
+    signature := .seq #[nameHl, .text " : ", renderedCodeToHighlighted constInfo ni.type]
+    docstring? }
+
+/-- Build a `Signature` from a doc-gen4 `Info`, including the declaration name. -/
+def signatureOfInfo (info : DocGen4.Process.Info)
+    (constInfo : Lean.NameMap (String × Option String) := {}) : Signature :=
+  let docstring? := docStringOfDoc? info.doc
+  let sigStr := s!"{info.name} : {renderedCodeText info.type}"
+  let nameHl := Highlighted.token ⟨.const info.name sigStr docstring? false none, info.name.toString⟩
+  let argsHl := info.args.map fun arg =>
+    Highlighted.seq #[.text " ", renderedCodeToHighlighted constInfo arg.binder]
+  let sepHl := Highlighted.text " : "
+  let typeHl := renderedCodeToHighlighted constInfo info.type
+  let sig := Highlighted.seq (#[nameHl] ++ argsHl ++ #[sepHl, typeHl])
+  { wide := sig, narrow := sig }
+
+/--
+Extract the parent structure name from a `RenderedCode` type by finding the first `.const` tag.
+Falls back to `.anonymous` if no constant reference is found.
+-/
+private partial def parentNameOfRenderedCode : RenderedCode → Name
+  | .text _ => .anonymous
+  | .tag (.const name) _ => name
+  | .tag _ inner => parentNameOfRenderedCode inner
+  | .append xs => xs.foldl (init := .anonymous) fun acc x =>
+    if acc != .anonymous then acc else parentNameOfRenderedCode x
+
+/-- Convert doc-gen4's `StructureParentInfo` array to Verso's `ParentInfo` array. -/
+def convertParents (parents : Array DocGen4.Process.StructureParentInfo)
+    (constInfo : Lean.NameMap (String × Option String) := {}) : Array ParentInfo :=
+  parents.mapIdx fun i p => {
+    projFn := p.projFn
+    name := parentNameOfRenderedCode p.type
+    parent := renderedCodeToHighlighted constInfo p.type
+    index := i
+  }
+
+/--
+Convert a doc-gen4 `Process.FieldInfo` to Verso's `Block.Docstring.FieldInfo`.
+
+Some fields are simplified because the database doesn't carry the full information:
+- `subobject?` is always `none`
+- `binderInfo` is always `BinderInfo.default`
+- `autoParam` is always `false`
+- `visibility` is always `.public`
+
+For inherited fields (`isDirect = false`), the `fieldFrom` list is populated by matching the
+field's projection function name prefix against parent structure names. This enables the
+"Inherited from" display and checkbox-based parent field filtering in the HTML output.
+-/
+def convertFieldInfo (field : DocGen4.Process.FieldInfo)
+    (parents : Array ParentInfo)
+    (constInfo : Lean.NameMap (String × Option String) := {}) : FieldInfo :=
+  let fieldNameStr := field.name.getString!
+  let docString? := docStringOfDoc? field.doc
+  let sigStr := s!"{field.name} : {renderedCodeText field.type}"
+  let fieldName :=
+    Highlighted.token ⟨.const field.name sigStr docString? true none, fieldNameStr⟩
+  let fieldFrom : List DocName :=
+    if field.isDirect then []
+    else
+      -- For inherited fields, determine which parent owns this field by matching
+      -- the field's projection function name prefix against parent names.
+      -- E.g., field `Verso.Genre.Manual.HtmlAssets.extraCss` → parent `HtmlAssets`
+      let fieldPrefix := field.name.getPrefix
+      match parents.find? (·.name == fieldPrefix) with
+      | some parent =>
+        let parentDocName : DocName := {
+          name := parent.name
+          hlName := .token ⟨.const parent.name "" none false none, parent.name.toString⟩
+          signature := parent.parent
+          docstring? := none
+        }
+        [parentDocName]
+      | none => []
+  {
+    fieldName
+    fieldFrom
+    type := renderedCodeToHighlighted constInfo field.type
+    projFn := field.name
+    subobject? := none
+    binderInfo := .default
+    autoParam := false
+    docString?
+    visibility := .public
+  }
+
+/-- Build a pretty constructor hover signature from a structure's fields.
+Groups consecutive fields with the same type, e.g. `(shortTitle shortContextTitle : Option String)`.
+Returns a string like `Struct.mk (field1 : Type1) (field2 field3 : Type2) : Struct`.
+
+NOTE: This is a workaround because doc-gen4 currently stores the structure constructor as `NameInfo`
+(without args). Once doc-gen4 is changed to store the constructor as `Info` (with pretty-printed
+binder args), this function should be replaced by directly using the constructor's `args` field. -/
+private def prettyCtorSig (ctorName : Name) (structName : Name)
+    (fields : Array DocGen4.Process.FieldInfo) : String :=
+  let resultType := structName.toString
+  if fields.isEmpty then
+    s!"{ctorName} : {resultType}"
+  else Id.run do
+    -- Group consecutive fields with the same rendered type
+    let mut groups : Array (Array String × String) := #[]
+    for field in fields do
+      let typeStr := renderedCodeText field.type
+      let fieldName := field.name.getString!
+      match groups.back? with
+      | some (names, t) =>
+        if t == typeStr then
+          groups := groups.pop.push (names.push fieldName, t)
+        else
+          groups := groups.push (#[fieldName], typeStr)
+      | none =>
+        groups := groups.push (#[fieldName], typeStr)
+    let params := groups.map fun (names, typeStr) =>
+      let nameStr := " ".intercalate names.toList
+      s!"({nameStr} : {typeStr})"
+    let paramStr := "\n  ".intercalate params.toList
+    s!"{ctorName} {paramStr} : {resultType}"
+
+private def buildStructureDeclType (isClass : Bool) (info : DocGen4.Process.StructureInfo)
+    (hideFields : Bool) (hideStructureConstructor : Bool)
+    (constInfo : Lean.NameMap (String × Option String) := {}) : DeclType :=
+  let ctorSig := prettyCtorSig info.ctor.name info.toInfo.name info.fieldInfo
+  let ctor? :=
+    if hideStructureConstructor then none
+    else some (docNameOfNameInfo info.ctor constInfo (sigOverride := some ctorSig))
+  let fieldNames :=
+    if hideFields then #[]
+    else info.fieldInfo.map (·.name)
+  let parents := convertParents info.parents constInfo
+  let fieldInfo :=
+    if hideFields then #[]
+    else info.fieldInfo.map (convertFieldInfo · parents constInfo)
+  .structure isClass ctor? fieldNames fieldInfo parents #[]
+
+/--
+Reconstruct a `DeclType` from a doc-gen4 `DocInfo`.
+
+For structures and classes, converts constructor, field, and parent information.
+For inductives, converts constructor `DocName` values.
+For definitions, opaques, axioms: extracts safety information.
+-/
+def buildDeclType (docInfo : DocInfo) (hideFields : Bool) (hideStructureConstructor : Bool)
+    (constInfo : Lean.NameMap (String × Option String) := {}) : DeclType :=
+  match docInfo with
+  | .axiomInfo info =>
+    .axiom (if info.isUnsafe then .unsafe else .safe)
+  | .theoremInfo _ =>
+    .theorem
+  | .opaqueInfo info =>
+    .opaque info.definitionSafety
+  | .definitionInfo info =>
+    .def (if info.isUnsafe then .unsafe else .safe)
+  | .instanceInfo info =>
+    .def (if info.isUnsafe then .unsafe else .safe)
+  | .inductiveInfo info =>
+    let ctors := info.ctors.toArray.map fun ctor =>
+      docNameOfNameInfo ctor.toNameInfo constInfo (showNamespace := false)
+    .inductive ctors 0 false
+  | .structureInfo info =>
+    buildStructureDeclType false info hideFields hideStructureConstructor constInfo
+  | .classInfo info =>
+    buildStructureDeclType true info hideFields hideStructureConstructor constInfo
+  | .classInductiveInfo info =>
+    let ctors := info.ctors.toArray.map fun ctor =>
+      docNameOfNameInfo ctor.toNameInfo constInfo (showNamespace := false)
+    .inductive ctors 0 false
+  | .ctorInfo _info =>
+    .other
+
+/-- Build a `NameMap` of hover data for constants directly contained in a `DocInfo`
+(the declaration itself, its fields, constructors, etc.). -/
+private def localConstInfoMap (docInfo : DocInfo) : Lean.NameMap (String × Option String) :=
+  let info := docInfo.toInfo
+  let sig := s!"{info.name} : {renderedCodeText info.type}"
+  let m : Lean.NameMap (String × Option String) :=
+    ({} : Lean.NameMap _).insert info.name (sig, docStringOfDoc? info.doc)
+  match docInfo with
+  | .inductiveInfo ind =>
+    ind.ctors.foldl (init := m) fun m c =>
+      m.insert c.name (s!"{c.name} : {renderedCodeText c.type}", docStringOfDoc? c.doc)
+  | .structureInfo s =>
+    let ctorSig := prettyCtorSig s.ctor.name info.name s.fieldInfo
+    let m := m.insert s.ctor.name (ctorSig, docStringOfDoc? s.ctor.doc)
+    s.fieldInfo.foldl (init := m) fun m f =>
+      m.insert f.name (s!"{f.name} : {renderedCodeText f.type}", docStringOfDoc? f.doc)
+  | .classInfo s =>
+    let ctorSig := prettyCtorSig s.ctor.name info.name s.fieldInfo
+    let m := m.insert s.ctor.name (ctorSig, docStringOfDoc? s.ctor.doc)
+    s.fieldInfo.foldl (init := m) fun m f =>
+      m.insert f.name (s!"{f.name} : {renderedCodeText f.type}", docStringOfDoc? f.doc)
+  | _ => m
+
+/-- Collect all `RenderedCode` values from a `DocInfo` (type, args, fields, constructors, parents). -/
+private def allRenderedCodes (docInfo : DocInfo) : Array RenderedCode :=
+  let info := docInfo.toInfo
+  let codes := #[info.type] ++ info.args.map (·.binder)
+  match docInfo with
+  | .inductiveInfo ind =>
+    codes ++ ind.ctors.toArray.map (·.type)
+  | .structureInfo s =>
+    codes ++ #[s.ctor.type] ++ s.fieldInfo.map (·.type) ++ s.parents.map (·.type)
+  | .classInfo s =>
+    codes ++ #[s.ctor.type] ++ s.fieldInfo.map (·.type) ++ s.parents.map (·.type)
+  | _ => codes
+
+/-- Collect all constant names referenced in any `RenderedCode` of a `DocInfo`. -/
+private def referencedConstNames (docInfo : DocInfo) : Lean.NameSet :=
+  (allRenderedCodes docInfo).foldl (init := {}) fun acc rc =>
+    renderedCodeConstNames acc rc
+
+/--
+Query the database for type and docstring hover data for a set of constant names.
+Returns a `NameMap` of `(typeString, docstring?)` suitable for use as `constInfo`.
+-/
+private def queryConstHoverData (dbPath : System.FilePath) (names : Lean.NameSet) :
+    IO (Lean.NameMap (String × Option String)) := do
+  let sqlite ← SQLite.openWith dbPath .readonly
+  let typeStmt ← sqlite.prepare
+    "SELECT type, module_name, position FROM name_info WHERE name = ?"
+  let mdDocStmt ← sqlite.prepare
+    "SELECT text FROM declaration_markdown_docstrings WHERE module_name = ? AND position = ?"
+  let versoDocStmt ← sqlite.prepare
+    "SELECT content FROM declaration_verso_docstrings WHERE module_name = ? AND position = ?"
+  let mut result : Lean.NameMap (String × Option String) := {}
+  have : SQLite.Blob.FromBinary VersoDocString := DocGen4.DB.versoDocStringFromBinary builtinDocstringValues
+  for name in names do
+    typeStmt.bind 1 name.toString
+    if ← typeStmt.step then
+      let typeBlob ← typeStmt.columnBlob 0
+      let moduleName ← typeStmt.columnText 1
+      let position ← typeStmt.columnInt64 2
+      -- Look up docstring: try markdown first, then verso
+      let mut doc? : Option String := none
+      mdDocStmt.bind 1 moduleName
+      mdDocStmt.bind 2 position
+      if ← mdDocStmt.step then
+        doc? := some (← mdDocStmt.columnText 0)
+      mdDocStmt.reset
+      mdDocStmt.clearBindings
+      if doc?.isNone then
+        versoDocStmt.bind 1 moduleName
+        versoDocStmt.bind 2 position
+        if ← versoDocStmt.step then
+          let blob ← versoDocStmt.columnBlob 0
+          match SQLite.Blob.fromBinary (α := VersoDocString) blob with
+          | Except.ok vds =>
+            doc? := some (DocGen4.Process.versoDocToMarkdown vds)
+          | Except.error _ => pure ()
+        versoDocStmt.reset
+        versoDocStmt.clearBindings
+      match SQLite.Blob.fromBinary (α := RenderedCode) typeBlob with
+      | Except.ok rc =>
+        let sig := s!"{name} : {renderedCodeText rc}"
+        result := result.insert name (sig, doc?)
+      | Except.error _ =>
+        pure ()
+    typeStmt.reset
+    typeStmt.clearBindings
+  return result
+
+/--
+Build a complete `NameMap` of hover data for a `DocInfo`, including both locally-defined names
+(the declaration, its fields/constructors) and externally-referenced constants (looked up in the DB).
+-/
+def constInfoMap (dbPath : System.FilePath) (docInfo : DocInfo) :
+    IO (Lean.NameMap (String × Option String)) := do
+  let local_ := localConstInfoMap docInfo
+  let referenced := referencedConstNames docInfo
+  -- Only query the DB for names not already in the local map
+  let mut missing : Lean.NameSet := {}
+  for name in referenced do
+    unless local_.contains name do
+      missing := missing.insert name
+  if missing.isEmpty then return local_
+  let external ← queryConstHoverData dbPath missing
+  -- Merge: local takes precedence
+  return external.foldl (init := local_) fun m name val =>
+    if m.contains name then m else m.insert name val
+
+/--
+Open the doc-gen4 database at the given path and look up a declaration by name.
+
+Returns `none` if the name is not found. Throws on IO errors (missing file, corrupt DB).
+-/
+def lookupDocInfo (dbPath : System.FilePath) (name : Name) :
+    IO (Option DocInfo) := do
+  let db ← openForReading dbPath builtinDocstringValues
+  let moduleNames ← db.getModuleNames
+  let name2ModIdx ← db.buildName2ModIdx moduleNames
+  let some modIdx := name2ModIdx[name]?
+    | return none
+  let modName := moduleNames[modIdx.toNat]!
+  let mod ← db.loadModule modName
+  return mod.members.findSome? fun
+    | .docInfo di => if di.toInfo.name == name then some di else none
+    | _ => none
+
+end Verso.Genre.Manual.DB
diff --git a/src/verso-manual/VersoManual/DB/Setup.lean b/src/verso-manual/VersoManual/DB/Setup.lean
new file mode 100644
index 00000000..36131069
--- /dev/null
+++ b/src/verso-manual/VersoManual/DB/Setup.lean
@@ -0,0 +1,142 @@
+/-
+Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import VersoManual.DB.Config
+
+/-! # Doc Source Workspace Setup
+
+Executable that manages the doc-gen4 build workspace. Called by the `docSource` Lake package facet.
+
+Usage: `verso-docgen-setup <workspace-dir> <docgen4-dir> <project-dir> [toml-path]`
+
+This executable:
+1. Parses `doc-sources.toml` (if provided and exists)
+2. Generates a `lakefile.lean` and `lean-toolchain` in the managed workspace
+3. Runs any configured setup commands
+4. Runs `lake build` to produce `api-docs.db`
+5. Verifies the database was produced
+-/
+
+open Verso.Genre.Manual.DocSource
+
+/--
+Lake environment variables to clear when spawning a child `lake` process, to avoid inheriting
+the parent Lake's workspace configuration.
+-/
+private def lakeVars : Array String :=
+  #["LAKE", "LAKE_HOME", "LAKE_PKG_URL_MAP",
+    "LEAN_SYSROOT", "LEAN_AR", "LEAN_PATH", "LEAN_SRC_PATH",
+    "LEAN_GITHASH",
+    "ELAN_TOOLCHAIN", "DYLD_LIBRARY_PATH", "LD_LIBRARY_PATH"]
+
+/-- Environment variable settings that unset all Lake variables and disable doc-gen4 source links. -/
+private def cleanEnv : Array (String × Option String) :=
+  lakeVars.map (·, none) ++ #[("DOCGEN_SRC", some "file")]
+
+/-- Reads the `lean-toolchain` file from a directory. -/
+private def readToolchain (dir : System.FilePath) : IO String := do
+  let tcPath := dir / "lean-toolchain"
+  unless ← tcPath.pathExists do
+    throw <| .userError s!"lean-toolchain not found at {tcPath}"
+  let contents ← IO.FS.readFile tcPath
+  return contents.trimAscii.toString
+
+/-- Runs a shell command in the given directory, printing output and throwing on failure. -/
+private def runCmd (cmd : String) (args : Array String) (cwd : System.FilePath) : IO Unit := do
+  IO.println s!"  Running: {cmd} {" ".intercalate args.toList}"
+  let result ← IO.Process.output {
+    cmd, args, cwd := some cwd
+    env := cleanEnv
+  }
+  unless result.stdout.isEmpty do IO.print result.stdout
+  unless result.stderr.isEmpty do IO.eprint result.stderr
+  unless result.exitCode == 0 do
+    throw <| .userError s!"Command '{cmd}' exited with code {result.exitCode}"
+
+/-- Checks for a toolchain mismatch between the project and any path dependencies. -/
+private def checkToolchainMismatch
+    (projectDir : System.FilePath) (config : Config) : IO (Option String) := do
+  let ourTc ← readToolchain projectDir
+  for req in config.require do
+    if let some path := req.path then
+      let depDir := if path.isAbsolute then path else projectDir / path
+      let depTcPath := depDir / "lean-toolchain"
+      if ← depTcPath.pathExists then
+        let depTc ← IO.FS.readFile depTcPath
+        let depTc := depTc.trimAscii.toString
+        if depTc != ourTc then
+          return some s!"Toolchain mismatch: this project uses '{ourTc}' but '{req.name}' uses '{depTc}'. The documented library must build with the same toolchain as your Verso project."
+  return none
+
+def main (args : List String) : IO UInt32 := do
+  -- Parse arguments
+  let (wsDir, docgen4Dir, projectDir, tomlPath?) ← match args with
+    | [ws, dg, proj, toml] =>
+      let r : System.FilePath × System.FilePath × System.FilePath × Option System.FilePath :=
+        (⟨ws⟩, ⟨dg⟩, ⟨proj⟩, some ⟨toml⟩)
+      pure r
+    | [ws, dg, proj] =>
+      let r : System.FilePath × System.FilePath × System.FilePath × Option System.FilePath :=
+        (⟨ws⟩, ⟨dg⟩, ⟨proj⟩, none)
+      pure r
+    | _ =>
+      IO.eprintln "Usage: verso-docgen-setup <workspace-dir> <docgen4-dir> <project-dir> [toml-path]"
+      return 1
+
+  -- Parse doc-sources.toml if provided and exists
+  let config? ← do
+    if let some (tomlPath : System.FilePath) := tomlPath? then
+      if ← tomlPath.pathExists then
+        some <$> Config.load tomlPath
+      else
+        pure none
+    else
+      pure none
+
+  -- Create workspace directory
+  IO.FS.createDirAll wsDir
+
+  -- Write lakefile.lean
+  let lakefileContent := generateLakefile config? docgen4Dir projectDir
+  IO.FS.writeFile (wsDir / "lakefile.lean") lakefileContent
+  IO.println s!"Wrote {wsDir / "lakefile.lean"}"
+
+  -- Write lean-toolchain
+  let toolchain ← readToolchain projectDir
+  IO.FS.writeFile (wsDir / "lean-toolchain") (toolchain ++ "\n")
+  IO.println s!"Wrote {wsDir / "lean-toolchain"} ({toolchain})"
+
+  -- Run setup commands
+  if let some config := config? then
+    for cmd in config.setup do
+      if let some (exe, cmdArgs) := splitCommand cmd then
+        runCmd exe cmdArgs wsDir
+
+  -- Run lake build
+  let libraries := config?.map (·.libraries) |>.getD #[]
+  let targets := if libraries.isEmpty
+    then #[":docInfo"]
+    else libraries.map (· ++ ":docInfo")
+
+  IO.println s!"Building documentation sources..."
+  try
+    runCmd "lake" (#["build"] ++ targets) wsDir
+  catch e =>
+    -- On build failure, check for toolchain mismatch
+    if let some config := config? then
+      if let some mismatchMsg ← checkToolchainMismatch projectDir config then
+        IO.eprintln s!"Note: {mismatchMsg}"
+    throw e
+
+  -- Verify the database was produced inside the sub-workspace's build directory.
+  let dbPath := wsDir / ".lake" / "build" / "api-docs.db"
+  unless ← dbPath.pathExists do
+    IO.eprintln s!"Documentation database not found at {dbPath} after build."
+    IO.eprintln "This may indicate an incompatible doc-gen4 version or misconfigured library targets."
+    IO.eprintln s!"Try running 'cd {wsDir} && lake build' manually to diagnose."
+    return 1
+
+  IO.println s!"Documentation database ready at {dbPath}"
+  return 0