Docgen dump docstrings

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}

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"}

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

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,

src/tests/Tests.lean

@@ -31,3 +31,4 @@ import Tests.VersoBlog
 import Tests.VersoManual
 import Tests.Z85
 import Tests.Zip
+import Tests.DocSourceConfig