wip: read docstrings from doc-gen

This PR implements an alternative path to docstring rendering that
reads the necessary data from a doc-gen4 SQLite database, to work
around the fact that docstring info is no longer available in the
environment with the module system and to allow a global view of the
project for things like instance lists.

Author: david-christiansen

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,38 +22,66 @@ 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
 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}

lakefile.lean

@@ -106,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
@@ -219,19 +220,17 @@ package_facet docSource pkg : System.FilePath := do
     | none => buildDir / ".." / "packages" / "doc-gen4"
 
   exeJob.mapM fun exeFile => do
-    -- Add trace for the TOML config file so changes trigger rebuild
-    if ← tomlPath.pathExists then
-      addTrace (← fetchFileTrace tomlPath (text := true))
-
-    buildFileUnlessUpToDate' dbPath do
-      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
-      }
+    -- 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

src/tests/Tests/DocSourceConfig.lean

@@ -14,7 +14,7 @@ Tests for `Verso.Genre.Manual.DocSource.Config` — TOML parsing and lakefile ge
 open Verso.Genre.Manual.DocSource
 open Lake.Toml
 
-/-- Parse a TOML string into a `Table`. Throws on parse error. -/
+/-- 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
@@ -23,18 +23,18 @@ private def parseToml (input : String) : IO Table := do
     let msgStrs ← msgs.toList.mapM fun msg => msg.data.toString
     throw <| .userError s!"TOML parse error:\n{"\n".intercalate msgStrs}"
 
-/-- Assert that two values are equal, throwing a descriptive error if not. -/
+/-- 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}"
 
-/-- Assert that a result is an error. -/
+/-- 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}"
 
-/-- Assert that a string contains a substring. -/
+/-- 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}"

src/verso-manual/VersoManual/DB.lean

@@ -4,3 +4,6 @@ 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

src/verso-manual/VersoManual/DB/Config.lean

@@ -17,7 +17,7 @@ namespace Verso.Genre.Manual.DocSource
 
 open Lake.Toml
 
-/-- A dependency entry from `doc-sources.toml`, mirroring `[[require]]` in `lakefile.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
@@ -44,20 +44,20 @@ structure Config where
   setup : Array String := #[]
 deriving Repr, BEq, Inhabited
 
-/-- Extract a `String` from a TOML `Value`, or `none` if it's not a string. -/
+/-- 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
 
 /--
-Extract an `Array String` from a TOML array of strings. Non-string elements are silently
+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
 
-/-- Parse a single `[[require]]` entry from a TOML table value. -/
+/-- Parses a single `[[require]]` entry from a TOML table value. -/
 def Require.ofToml (v : Value) : Except String Require := do
   match v with
   | .table' _ t =>
@@ -73,7 +73,7 @@ def Require.ofToml (v : Value) : Except String Require := do
     pure { name, git, rev, path, subDir }
   | _ => throw "[[require]] entry must be a table"
 
-/-- Parse a `Config` from a TOML `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
@@ -87,7 +87,7 @@ def Config.ofToml (table : Table) : Except String Config := do
     | none => #[]
   pure { require, libraries, setup }
 
-/-- Load and parse a `doc-sources.toml` file. -/
+/-- 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
@@ -101,7 +101,7 @@ def Config.load (filePath : System.FilePath) : IO Config := do
     throw <| .userError s!"Error parsing {filePath}:\n{"\n".intercalate msgStrs}"
 
 /--
-Split a command string into an executable name and arguments, respecting single and double
+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.
 -/
@@ -152,14 +152,18 @@ def splitCommand (cmd : String) : Option (String × Array String) := do
   | [] => none
   | exe :: rest => some (exe, rest.toArray)
 
-/-- Generate a `require` declaration in lakefile.lean syntax for a single dependency. -/
+/-- 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  \"{url}\"{revPart}{subDirPart}\n"
+    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.
@@ -170,7 +174,7 @@ def Require.toLakefileEntry (r : Require) (projectDir : System.FilePath) : Strin
     s!"{name}\n"
 
 /--
-Generate a complete `lakefile.lean` for the managed doc-gen workspace.
+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.
@@ -179,7 +183,7 @@ Generate a complete `lakefile.lean` for the managed doc-gen workspace.
 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 \"{docgen4Dir}\"\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 => ""

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