leanprover · david-christiansen · Feb 27, 2026 · Mar 1, 2026 · Mar 6, 2026 · Mar 27, 2026
diff --git a/.github/workflows/copyright-header.yml b/.github/workflows/copyright-header.yml
@@ -15,10 +15,22 @@ jobs:
 
             - name: Verify .lean files start with a copyright header.
               run: |
-                  FILES=$(find ./src ./test-projects -path ./src/tests/interactive -prune -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;)
-                  if [ -n "$FILES" ]; then
+                  OFFENDING=()
+                  while IFS= read -r -d '' file; do
+                    if ! head -1 "$file" | grep -q '^/-$'; then
+                      OFFENDING+=("$file")
+                    elif ! head -2 "$file" | tail -1 | grep -q '^Copyright'; then
+                      OFFENDING+=("$file")
+                    fi
+                  done < <(find ./src ./test-projects \
+                    -path ./src/tests/interactive -prune -o \
+                    -path '*/.lake' -prune -o \
+                    -path './test-projects/literate-*' -prune -o \
+                    -type f -name "*.lean" -print0)
+
+                  if [ ${#OFFENDING[@]} -gt 0 ]; then
                     echo "Found .lean files which do not have a copyright header:"
-                    echo "$FILES"
+                    printf '%s\n' "${OFFENDING[@]}"
                     exit 1
                   else
                     echo "All copyright headers present."

diff --git a/doc-sources.toml b/doc-sources.toml
@@ -0,0 +1,3 @@
+# These are the libraries documented in the Verso User's Guide
+libraries = ["Verso", "VersoManual", "VersoBlog"]
+include_core = true
diff --git a/doc/UsersGuide.lean b/doc/UsersGuide.lean
@@ -1,3 +1,4 @@
+module
 import VersoManual
 
 import UsersGuide.Basic
diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean
@@ -3,7 +3,8 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
-import VersoManual
+module
+public import VersoManual
 import UsersGuide.Markup
 import UsersGuide.Websites
 import UsersGuide.Manuals

diff --git a/doc/UsersGuide/Elab.lean b/doc/UsersGuide/Elab.lean
@@ -3,11 +3,13 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
-
+module
 import Lean.DocString.Syntax
-import VersoManual
+public import VersoManual
 
-open Verso Genre Manual
+open Verso Genre
+open Verso.Genre.Manual hiding docstring tactic conv
+open Verso.Genre.Manual.DocGen
 
 open Verso.Genre.Manual.InlineLean
 

diff --git a/doc/UsersGuide/Extensions.lean b/doc/UsersGuide/Extensions.lean
@@ -3,10 +3,13 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
+module
 import Lean.DocString.Syntax
-import VersoManual
+public import VersoManual
 
-open Verso Genre Manual
+open Verso Genre
+open Verso.Genre.Manual hiding docstring tactic conv
+open Verso.Genre.Manual.DocGen
 open InlineLean
 
 #doc (Manual) "Extensions" =>

diff --git a/doc/UsersGuide/Literate.lean b/doc/UsersGuide/Literate.lean
@@ -3,8 +3,9 @@ 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
 -/
+module
 import Lean.DocString.Syntax
-import VersoManual
+public import VersoManual
 import VersoBlog
 
 open Verso Genre Manual

diff --git a/doc/UsersGuide/Manuals.lean b/doc/UsersGuide/Manuals.lean
@@ -3,15 +3,20 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
+module
 import Lean.DocString.Syntax
-import VersoManual
+public import VersoManual
 import VersoBlog
 
-open Verso Genre Manual
+open Verso Genre
+open Verso.Genre.Manual hiding docstring tactic conv
+open Verso.Genre.Manual.DocGen
 
 open InlineLean
 open Verso.Doc
 
+set_option pp.rawOnError true
+
 #doc (Manual) "Manuals and Books" =>
 %%%
 tag := "manual"
@@ -23,6 +28,7 @@ It supports generating both HTML and PDFs via LaTeX, but the PDF support is rela
 
 {docstring Manual}
 
+
 {docstring Manual.PartMetadata}
 
 {docstring Manual.HtmlSplitMode}
@@ -143,6 +149,83 @@ results in
 ::::
 
 
+## Docstrings From `doc-gen4` (Experimental)
+%%%
+tag := "docgen-docstrings"
+%%%
+
+:::paragraph
+Ordinarily, the {name Verso.Genre.Manual.docstring}`docstring` command extracts documentation directly from the Lean environment.
+This requires that the documented library be imported into the Verso document, which has two drawbacks:
+
+ * Declarations from Verso itself and its dependencies are present in the environment alongside the documented library, making it difficult to distinguish the two.
+ * When using the module system, docstrings are saved in the server `.olean`, and are not available when building at the command line.
+  This means that complicated documents written in Verso cannot get the benefits of the module system, such as improved incremental rebuilds and less memory use.
+ * Documentation does not necessarily have a global view of the package being documented, making it difficult to automatically take care of cross-cutting concerns such as listing all instances of a type class.
+:::
+
+The {name}`DocGen.docstring` command is an experimental alternative implementation that displays docstrings extracted by `doc-gen4` rather than from the Lean environment.
+It produces the same output as the standard {name Verso.Genre.Manual.docstring}`docstring` command.
+
+Before the text that includes the docstrings is built, `doc-gen4` is invoked to produce a SQLite database that includes the documented declarations.
+Then, each page of documentation reads this database during elaboration.
+
+### Setup
+
+To use docstrings from `doc-gen4`, two pieces of configuration are needed:
+ * The documentation extraction tool must be configured to include the correct libraries.
+ * Lake needs to run this tool prior to building the documetnation.
+
+The extraction tool is configured in a file called `doc-sources.toml` in the root of the package in which documentation is written.
+It contains two fields: `libraries` is an array of strings, each of which is a library's module root, and `include_core` is a Boolean that determines whether the Lean standard library and metaprogramming API are included (defaulting to `true`).
+
+:::paragraph
+For example, to include `MyLib` and `MyOtherLib` along with the Lean standard library, use this file:
+```
+libraries = ["MyLib", "MyOtherLib"]
+```
+:::
+
+To instruct Lake to build the documentation database before building the document that refers to it, add a `needs` field to the documentation in the Lake configuration file.
+In particular, the package facet `docSource` uses the package's `doc-sources.toml` to create the database.
+To avoid problems with circularity, the library that contains the documentation should not be in `doc-sources.toml`.
+
+:::paragraph
+For example, a suitable `needs` field may look like this, where `MyDocs` is a document written in the manual genre:
+
+```
+lean_lib MyDocs where
+  needs := #[`@:docSource]
+```
+:::
+
+### Usage
+
+:::paragraph
+The `docstring` command and the `tactic` and `conv` directives have equivalents based on the database.
+These equivalents have the same API as the environment-based versions, but they are in the `Verso.Genre.Manual.DocGen` namespace.
+The indended mode of use is that the original commands should be hidden when opening the `Verso.Genre.Manual` namespace.
+For example:
+```
+open Verso Genre
+open Verso.Genre.Manual hiding docstring tactic conv
+open Verso.Genre.Manual.DocGen
+```
+:::
+
+### Editor Experience
+
+Before the first `lake build`, `DocGen.docstring` commands show an error directing you to run `lake build`.
+After the documentation data has been generated, the editor is fully responsive.
+If you change the documented library, running `lake build` again updates the data.
+
+### Coexistence with Environment-Based Commands
+
+The doc-gen-sourced commands live in the `Verso.Genre.Manual.DocGen` namespace and do not replace the standard commands.
+Projects that document declarations available in their own environment can continue to use `docstring` with no changes.
+Both sets of commands produce the same block types, so they can coexist within a single document if needed.
+
+
 # Technical Terminology
 %%%
 shortTitle := "Glossary"
@@ -158,7 +241,6 @@ References to technical terms are valid both before and after their definition s
 
 {docstring tech}
 
-
 # Open-Source Licenses
 %%%
 tag := "oss-licenses"

diff --git a/doc/UsersGuide/Markup.lean b/doc/UsersGuide/Markup.lean
@@ -3,14 +3,21 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
+module
 import Lean.DocString.Syntax
+public import Verso.Doc.Elab.Monad
+public meta import Verso.Parser
+import Verso
 import VersoManual
+public import VersoManual.Basic
+import VersoManual.InlineLean.LongLines
+public meta import VersoManual.InlineLean.LongLines
 
 set_option guard_msgs.diff true
 
 open Verso Genre Manual
 
-section
+meta section
 open Lean
 open Lean.Doc.Syntax
 
@@ -129,7 +136,7 @@ partial def preview (stx : Syntax) : m Std.Format :=
       throwErrorAt stx "Didn't understand {Verso.SyntaxUtils.ppSyntax stx} for preview"
 end
 
-block_extension MarkupExample (title : String) where
+public block_extension MarkupExample (title : String) where
   data := title
   traverse _ _ _ := pure none
   toHtml := some fun _goI goB _id data contents => open Verso.Output.Html in do
@@ -266,23 +273,23 @@ open Lean
 open ArgParse
 open Doc.Elab
 
-structure MarkupPreviewConfig where
+public structure MarkupPreviewConfig where
   title : StrLit
 
-instance : FromArgs MarkupPreviewConfig DocElabM where
+public meta instance : FromArgs MarkupPreviewConfig DocElabM where
   fromArgs := MarkupPreviewConfig.mk <$> .positional `title .strLit
 
 end
 
-private def withNl (s : String) : String := if s.endsWith "\n" then s else s.push '\n'
+private meta def withNl (s : String) : String := if s.endsWith "\n" then s else s.push '\n'
 
 
 open Verso Doc Elab in
 open Lean Elab in
 open Verso.Parser in
 open Lean.Doc.Syntax in
 @[directive]
-def markupPreview : DirectiveExpanderOf MarkupPreviewConfig
+public meta def markupPreview : DirectiveExpanderOf MarkupPreviewConfig
   | {title}, contents => do
     let #[blk1, blk2] := contents.filter nonempty
       | throwError "Expected precisely two code blocks, got {contents.filter nonempty}"
@@ -324,7 +331,7 @@ where
 open Lean Verso Doc Elab in
 open Verso.Parser in
 @[code_block markupPreview]
-def markupPreviewPre : CodeBlockExpanderOf MarkupPreviewConfig
+public meta def markupPreviewPre : CodeBlockExpanderOf MarkupPreviewConfig
   | {title}, contents => do
 
     let stx ← blocks {} |>.parseString contents.getString

diff --git a/doc/UsersGuide/Output.lean b/doc/UsersGuide/Output.lean
@@ -3,11 +3,14 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
+module
 import Lean.DocString.Syntax
-import VersoManual
+public import VersoManual
 import VersoBlog
 
-open Verso Genre Manual
+open Verso Genre
+open Verso.Genre.Manual hiding docstring tactic conv
+open Verso.Genre.Manual.DocGen
 
 open Verso.Genre.Blog (Page Post)
 

diff --git a/doc/UsersGuide/Releases.lean b/doc/UsersGuide/Releases.lean
@@ -3,8 +3,8 @@ Copyright (c) 2026 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Emilio J. Gallego Arias
 -/
-
-import VersoManual
+module
+public import VersoManual
 
 import UsersGuide.Releases.«v4_29_0»
 import UsersGuide.Releases.«v4_28_0»

diff --git a/doc/UsersGuide/Releases/v4_28_0.lean b/doc/UsersGuide/Releases/v4_28_0.lean
@@ -3,8 +3,8 @@ Copyright (c) 2026 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Emilio J. Gallego Arias
 -/
-
-import VersoManual
+module
+public import VersoManual
 
 open Verso.Genre
 

diff --git a/doc/UsersGuide/Releases/v4_29_0.lean b/doc/UsersGuide/Releases/v4_29_0.lean
@@ -3,8 +3,8 @@ Copyright (c) 2026 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Emilio J. Gallego Arias
 -/
-
-import VersoManual
+module
+public import VersoManual
 
 open Verso.Genre Manual
 
@@ -18,6 +18,8 @@ file := "v4.29.0"
 * Fix Verso folding ranges / TOC for Lean.Doc syntax and #doc (#768)
 * Align Blog inline Lean role naming with Manual; add `{lean}` and deprecate `{leanInline}` (#762)
 * A zero-config {ref "literate429"}[literate programming] feature was added in [#809](https://github.com/leanprover/verso/pull/809).
+* A {ref "docgen429"}[`doc-gen4`-based backend for extracted API docs] was added in [#776](https://github.com/leanprover/verso/pull/776).
+
 
 # Literate Programming
 %%%
@@ -27,3 +29,14 @@ tag := "literate429"
 PR [#809](https://github.com/leanprover/verso/pull/809) added support for a simple literate programming system, in which module docstrings are rendered as the text of a page.
 While no configuration is necessary to use it, aside from adding Verso as a dependency, some configuration is possible in order to customize aspects of the display.
 See {ref "literate"}[its section in this guide] for more details.
+
+# Docstrings via `doc-gen4`
+%%%
+tag := "docgen429"
+%%%
+
+PR [#776](https://github.com/leanprover/verso/pull/776) implements an alternative backend for the docstring features in the manual genre.
+Instead of retrieving them from the in-memory Lean environment, they can be read from a SQLite database dumped by `doc-gen4`.
+This allows manuals written in Verso to use the Lean module system, which eliminates docstrings from environments for performance reasons, and it can enable features that require a global perspective, such as lists of instances.
+This very document now uses this new feature and has enabled the module system.
+See {ref "docgen-docstrings"}[its section in this guide] for more details.
diff --git a/doc/UsersGuide/Websites.lean b/doc/UsersGuide/Websites.lean
@@ -3,11 +3,15 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
+module
 import Lean.DocString.Syntax
-import VersoManual
-import VersoBlog
+public import VersoManual
+public meta import VersoManual.DB
+meta import VersoBlog
 
-open Verso Genre Manual
+open Verso Genre
+open Verso.Genre.Manual hiding docstring tactic conv
+open Verso.Genre.Manual.DocGen
 
 open Verso.Genre.Blog (Page Post)
 
@@ -44,7 +48,7 @@ However, their metadata are different:
 tag := "blogMain"
 %%%
 
-Blogs should have an executable that invokes `blogMain` on the appropriate {ref "site-config"}[site and theme], forwarding on command-line arguments.
+Blogs should have an executable that invokes {name Verso.Genre.Blog.blogMain}`blogMain` on the appropriate {ref "site-config"}[site and theme], forwarding on command-line arguments.
 It is responsible for {ref "traversal"}[traversing] the site and generating the HTML.
 
 {docstring Blog.blogMain}