From 63468c8c645e281d7b40332cff1c37b6efe6e879 Mon Sep 17 00:00:00 2001 From: "Anne C.A. Baanen" Date: Mon, 5 Jan 2026 16:37:37 +0100 Subject: [PATCH] feat: sublibrary for adding supplement pages and sections This PR adds a library `SubDocGen` that defines a pair of environment extensions, and helper functions for adding definitions to these extensions. In a follow-up PR, these extensions will be used to render supplement pages, in addition to API documentation. For example, Mathlib can generate an overview of all library notes, Stacks tags and `norm_num` extensions, without having to program support specifically into DocGen for each of them. The environment extensions need to be imported by projects in order to add to the supplement, so I define it as its own library rather than a piece of DocGen itself. The main open question I have right now is Verso support. The entries of the environment extension are intentionally dependent on the type of (doc)string they contain, so switching them out all at once should be easy. I wonder if it would be better to instead have two extensions: one storing Markdown strings and one for storing Verso strings. --- SubDocGen.lean | 161 +++++++++++++++++++++++++++++++++++++++++++++++++ lakefile.lean | 3 + 2 files changed, 164 insertions(+) create mode 100644 SubDocGen.lean diff --git a/SubDocGen.lean b/SubDocGen.lean new file mode 100644 index 00000000..5c555322 --- /dev/null +++ b/SubDocGen.lean @@ -0,0 +1,161 @@ +/- +Copyright (c) 2025 Anne Baanen. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anne Baanen +-/ +module + +public meta import Lean.Elab.Command +public import Lean.EnvExtension +public import Lean.Meta.Basic + +/-! +# Library for adding supplementary pages to the DocGen output. + +In addition to the pages listing declarations, DocGen can output supplementary pages. +Each page is made up of an introduction followed by a sequence of sections. +These sections can be added individually through metaprogramming, for example when adding an +attribute to a declaration. + +The main user interface for adding pages and sections can be found in the commands +`register_supplement_page` and `register_supplement_section`; these correspond to +`SubDocGen.registerSupplementPage` and `SubDocGen.registerSupplementSection` respectively. +-/ + +namespace SubDocGen + +open Lean Meta + +/-- A docstring formatted in Markdown. -/ +public abbrev MarkdownDocstring := String + +/-- A section out of a `SupplementPage`. -/ +public structure SupplementSection (textFormat : Type) where + /-- Human-readable title of the section. -/ + name : String + + /-- Main contents of this section. -/ + text : textFormat + + /-- Module where this section is defined. Will be set by `registerSupplementSection`. -/ + definingModule : Option Name + /-- Declaration(s) relating to this section. + + For example, a tactic might link here to its implementation. + -/ + relatedDecls : Array Name +deriving FromJson, ToJson + +/-- +A page to be rendered in addition to the module docs. + +Pages have some introductory text, followed by headered sections. +-/ +public structure SupplementPage (textFormat : Type) where + /-- Human-readable name of the page. -/ + name : String + /-- Page introduction. -/ + intro : textFormat + + /-- Module where this page is defined. Will be set by `registerSupplementPage`. -/ + definingModule : Option Name + /-- Sections of the page. Will be computed by DocGen during processing of the supplement pages. -/ + sections : Array (SupplementSection textFormat) + +/-- A section out of a `SupplementPage`, plus information on where to place the section. -/ +public structure SupplementSectionEntry (textFormat) extends SupplementSection textFormat where + /-- Identifies the page to which this section belongs. -/ + pageKey : String +deriving FromJson, ToJson + +/-- A page to be rendered in addition to the module docs, plus information on +where to find its sections. -/ +public structure SupplementPageEntry (textFormat) extends SupplementPage textFormat where + /-- A unique identifier for this page, used to associate sections declared in downstream modules. -/ + key : String +deriving FromJson, ToJson + +/-- This environment extension allows adding supplement pages that will be rendered by DocGen. +Add entries using the `SubDocGen.registerSupplementPage` function or +`register_supplement_page` command. +-/ +-- Pages are stored as a `HashMap` for easy existence checking. +public meta initialize supplementPageExt : SimplePersistentEnvExtension (SupplementPageEntry MarkdownDocstring) + (Std.HashMap String (SupplementPageEntry MarkdownDocstring)) ← + registerSimplePersistentEnvExtension { + addImportedFn as := as.foldl (fun m as => m.insertMany (as.map fun a => (a.key, a))) {} + addEntryFn m a := m.insert a.key a + } + +/-- This environment extension allows adding sections to supplement pages. +Add entries using the `SubDocGen.registerSupplementSection` function or +`register_supplement_section` command. + +See also `SubDocGen.supplementPageExt`. +-/ +-- Sections are stored as an array since they are all scanned through per-module anyway. +public meta initialize supplementSectionExt : SimplePersistentEnvExtension (SupplementSectionEntry MarkdownDocstring) + (Array (SupplementSectionEntry MarkdownDocstring)) ← + registerSimplePersistentEnvExtension { + addImportedFn as := as.flatten + addEntryFn as a := as.push a + } + +variable {m} [Monad m] [MonadEnv m] [MonadError m] + +/-- Add a page (with perhaps some predefined sections) to the DocGen supplement. +This function is the interface for metaprograms: the command `register_supplement_page` is the +basic wrapper for users. + +Page keys should be unique. If not, this function throws an error. + +Further sections to this page can be added by calling `registerSupplementSection`. +-/ +public meta def registerSupplementPage (page : SupplementPageEntry MarkdownDocstring) : m Unit := do + if (supplementPageExt.getState (← getEnv)).contains page.key then + throwError m!"registerSupplementPage: there is already a page with key `{page.key}`." + modifyEnv (supplementPageExt.addEntry · { page with definingModule := (← getEnv).header.mainModule }) + +/-- Add a section to a page in the DocGen supplement. +This function is the interface for metaprograms: the command `register_supplement_section` is the +basic wrapper for users. + +The page that this section appears in should first be declared using `registerSupplementPage`. +If not, this function throws an error. +-/ +public meta def registerSupplementSection (sec : SupplementSectionEntry MarkdownDocstring) : m Unit := do + if !(supplementPageExt.getState (← getEnv)).contains sec.pageKey then + throwError m!"registerSupplementSection: no page has been declared with key `{sec.pageKey}`." + modifyEnv (supplementSectionExt.addEntry · { sec with definingModule := (← getEnv).header.mainModule }) + +open Elab Command in +/-- `register_supplement_page key "Page Title" /-- Introduction text -/` +adds a page to the DocGen supplement under the given key. + +In metaprograms, you can call `registerSupplementPage` directly. +-/ +elab "register_supplement_page " name:ident ppSpace title:str ppSpace dc:docComment : command => do + registerSupplementPage { + key := name.getId.toString + name := title.getString + intro := dc.getDocString + definingModule := none + sections := #[] + } + +open Elab Command in +/-- `register_supplement_section pageKey "Section Title" /-- Introduction text -/` +adds a section to the `pageKey` page in the DocGen supplement. + +In metaprograms, you can call `registerSupplementSection` directly. +-/ +elab "register_supplement_section " pageKey:ident ppSpace title:str ppSpace dc:docComment : command => do + registerSupplementSection { + pageKey := pageKey.getId.toString + name := title.getString + text := dc.getDocString + definingModule := none + relatedDecls := #[] + } + +end SubDocGen diff --git a/lakefile.lean b/lakefile.lean index 8e61872b..d0d7aaea 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,6 +5,9 @@ package «doc-gen4» lean_lib DocGen4 +lean_lib SubDocGen where + leanOptions := #[⟨`experimental.module, true⟩] + @[default_target] lean_exe «doc-gen4» { root := `Main