feat: much more documentation

doc/UsersGuide/Basic.lean

@@ -1,5 +1,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
+-/
 import VersoManual
 import UsersGuide.Markup
+import UsersGuide.Websites
+import UsersGuide.Manuals
+import UsersGuide.Elab
+import UsersGuide.Extensions
+import UsersGuide.Output
 
 open Verso.Genre Manual
 
@@ -12,106 +22,92 @@ shortTitle := "Documentation with Verso"
 authors := ["David Thrane Christiansen"]
 %%%
 
-
-Documentation can take many forms:
-
-
- * References
+:::paragraph
+Verso is a tool for writing about Lean.
+Or, rather, it is a framework for constructing such tools, together with concrete tools that use this framework.
+Technical writing can take many forms, including but not limited to:
+ * Reference manuals
  * Tutorials
- * Etc
-
-{include 0 UsersGuide.Markup}
-
-# Genres
-%%%
-tag := "genres"
-%%%
+ * Web pages
+ * Academic papers
+:::
 
+All of these genres have common concerns, such as displaying Lean code, including tests to prevent bit-rot of the text, and linking to other resources.
+However, they are also very different.
+Some have a very linear structure, while others combine date-based content with an unordered set of pages.
+Some should generate highly interactive output, while others should generate PDFs that can be turned into published papers books.
 
-:::paragraph
-Documentation comes in many forms, and no one system is suitable for representing all of them.
-The needs of software documentation writers are not the same as the needs of textbook authors, researchers writing papers, bloggers, or poets.
-Thus, Lean's documentation system supports multiple {deftech}_genres_, each of which consists of:
+Verso consists of the following components:
 
- * A global view of a document's structure, whether it be a document with subsections, a collection of interrelated documents such as a web site, or a single file of text
- * A representation of cross-cutting state such as cross-references to figures, index entries, and named theorems
- * Additions to the structure of the document - for instance, the blog genre supports the inclusion of raw HTML, and the manual genre supports grouping multiple top-level blocks into a single logical paragraph
- * Procedures for resolving cross references and rendering the document to one or more output formats
-
-All genres use the same markup syntax, and they can share extensions to the markup language that don't rely on incompatible document structure additions.
-Mixing incompatible features results in an ordinary Lean type error.
-:::
+: Markup language
 
+  Verso's {ref "verso-markup"}[markup language] is a simplified variant of Markdown.
+  It is also an alternative concrete syntax for Lean itself, so Verso documents are just Lean files.
+  Just as TeX, Sphinx, and Scribble allow their languages to be extended using their own programming languages, Verso's markup language is extensible.
+  Define a Lean function at the top of a file, and use it in the text of that very same file.
 
-# Docstrings
-%%%
-tag := "docstrings"
-%%%
+: Extensible document structure
 
-Docstrings can be included using the `docstring` directive. For instance,
+  All Verso documents can contain a set of {ref "elaboration"}[common elements], such as paragraphs, emphasized text, or images.
+  They also share a hierarchical structure of sections and subsections.
+  These types are extensible by individual genres.
 
-```
-{docstring List.forM}
-```
+: Elaboration and rendering framework
 
-results in
+  Verso provides a shared paradigm for converting text written by an author into readable output.
+  Different genres will produce different output formats, but they don't need to reinvent the wheel in order to resolve cross-references, and they can benefit from shared libraries for producing output in various formats.
 
-{docstring List.forM}
+: Cross-reference management
 
-## More Docstring Examples
-%%%
-tag := "more-docstring-examples"
-shortTitle := "More Docstrings"
-%%%
+  Verso includes a common paradigm for representing the documented items, and a format for sharing cross-reference databases between genres that emit HTML, which enables links and cross-references to be automatically inserted and maintained.
 
-Here are some docstrings as rendered by Verso.
-They include heuristic elaboration of code items in their Markdown that attempts to guess what was meant.
+: Lean rendering
 
-{docstring Lean.Syntax}
+  Verso includes facilities for elaborating and displaying Lean code in documents.
+  In HTML output, this code is rendered with toggleable proof states, hovers, and hyperlinks.
+  It's also highlighted accurately, which is impossible with regexp-based highlighting due to Lean's syntactic extensibility.
 
-{docstring List}
+  The [`SubVerso`](https://github.com/leanprover/subverso) helper library allows Verso documents to process Lean code written in any version of Lean, starting with `4.0.0`.
+  This makes it possible to write a document that compares and contrasts versions, or to decouple upgrades to the Lean version used in a project from the Lean version used in the document that describes it.
 
-{docstring String}
+: Utility libraries
 
-{docstring Subtype}
+  Verso includes utility libraries that can be used by genres to provide features such as full-text search of HTML content.
+  These libraries have no additional build-time dependencies, avoiding the complications of staying up to date with multiple library ecosystems at once.
 
-{docstring OfNat}
 
-{docstring Monad}
 
-{docstring Float (label := "type") (hideFields := true) (hideStructureConstructor := true)}
+# Genres
+%%%
+tag := "genres"
+%%%
 
-{docstring Array.forM}
 
-{docstring Array.forRevM}
+:::paragraph
+Documentation comes in many forms, and no one system is suitable for representing all of them.
+The needs of software documentation writers are not the same as the needs of textbook authors, researchers writing papers, bloggers, or poets.
+Thus, Verso supports multiple {deftech}_genres_, each of which consists of:
 
-:::tactic "induction"
-:::
+ * A global view of a document's structure, whether it be a document with subsections, a collection of interrelated documents such as a web site, or a single file of text
+ * A representation of cross-cutting state such as cross-references to figures, index entries, and named theorems
+ * Additions to the structure of the document - for instance, the blog genre supports the inclusion of raw HTML, and the manual genre supports grouping multiple top-level blocks into a single logical paragraph
+ * Procedures for resolving cross references and rendering the document to one or more output formats
 
-:::tactic "simp"
+All genres use the same {ref "verso-markup"}[markup syntax], and they can share extensions to the markup language that don't rely on incompatible document structure additions.
+Mixing incompatible features results in an ordinary Lean type error.
 :::
 
+{include 0 UsersGuide.Markup}
 
-{docstring Nat}
-
-{optionDocs pp.deepTerms.threshold}
-
-{docstring Thunk}
+{include 0 UsersGuide.Elab}
 
-# Technical Terminology
-%%%
-shortTitle := "Glossary"
-tag := "tech-terms"
-%%%
+{include 0 UsersGuide.Extensions}
 
-The `deftech` role can be used to annotate the definition of a {tech}[technical term].
-Elsewhere in the document, `tech` can be used to annotate a use site of a technical term.
-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.
+{include 0 UsersGuide.Output}
 
-{docstring deftech}
+{include 0 UsersGuide.Websites}
 
-{docstring tech}
+{include 0 UsersGuide.Manuals}
 
 # Index
 %%%

doc/UsersGuide/Elab.lean

@@ -0,0 +1,104 @@
+/-
+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 Verso.Syntax
+import VersoManual
+
+open Verso Genre Manual
+
+open Verso.Genre.Manual.InlineLean
+
+#doc (Manual) "Building Documents" =>
+%%%
+tag := "build-process"
+%%%
+
+
+Verso is a general framework for implementing documentation tools, and this flexibility means that the details of the process described in this section may differ for specific tools.
+
+A Verso document passes through the following steps on its way from its author to its readers:
+1. The author writes the document's text in {ref "verso-markup"}[Verso's markup language], which is parsed to Lean's own {name Lean.Syntax}`Syntax` type
+2. The document is elaborated to a representation as a Lean data structure
+3. The resulting Lean code is compiled to an executable
+4. When run, the executable resolves cross-references and computes other globally-scoped metadata in a step referred to as the traversal pass
+5. Next, the executable generates the output
+
+
+# Elaboration
+%%%
+tag := "elaboration"
+%%%
+
+During the elaboration process, Verso's markup language is converted into its internal representation as a Lean inductive type.
+When Verso's elaborator encounters an {ref "elab-extensions"}[extension point], it consults an internal table to select an implementation of the extension, and delegates to it.
+Other syntax is translated into the appropriate constructors of Verso's data.
+
+All Verso documents are parameterized by their {tech}[genre]:
+
+{docstring Verso.Doc.Genre}
+
+Each document consists of a {name Verso.Doc.Part}`Part`.
+The part's title is the title of the entire document.
+
+{docstring Verso.Doc.Part}
+
+{name Verso.Doc.Part}`Part`s contain {name Verso.Doc.Block}`Block`s:
+
+{docstring Verso.Doc.Block}
+
+{name Verso.Doc.Block}`Block`s contain {name Verso.Doc.Inline}`Inline`s:
+
+{docstring Verso.Doc.Inline}
+
+The {name Verso.Doc.Part.metadata}`metadata` field of {name Verso.Doc.Part}`Part` typically gets its value from a metadata block written by the author, though it may be assigned more information during traversal.
+The {name Verso.Doc.Block.other}`Block.other` and {name Verso.Doc.Inline.other}`Inline.other` constructors typically result from elaborating {ref "elab-extensions"}[extension points].
+
+# Compilation
+%%%
+tag := "compilation"
+%%%
+
+After elaboration, the document is compiled into an executable program.
+Each genre provides a `main` function that will carry out the remainder of the steps.
+Usually, this `main` function can be applied to the part that represents the whole document; however, genres that don't have a strict linear order (such as the {ref "website"}[website genre]) will provide their own means of configuring the document's layout.
+The `main` function typically also takes configuration parameters both in the code and on the command line, such as which output formats to generate or customizations to the generated output.
+
+# Traversal
+%%%
+tag := "traversal"
+%%%
+
+Because they are Lean values, Verso documents adhere to the structure of Lean programs in general.
+In particular, Lean doesn't support cyclic import graphs.
+It's common, however, for technical writing to include cyclic references; two sections that describe different aspects of something will frequently refer to one another.
+Similarly, a bibliography that's generated from a database needs a global view of a document to include only those works which are, in fact, cited.
+
+The {deftech}_traversal_ phase occurs at runtime, before generating output.
+During the traversal phase, the document is repeatedly traversed from beginning to end, and metadata is accumulated into a table.
+The document may also be modified during traversal; this allows the title of a section to be inserted into a cross-reference.
+This traversal is repeated until the resulting document and metadata tables are not modified; it fails if a set number of passes are executed that result in modifications each time.
+
+Verso provides a general-purpose traversal mechanism for {name Verso.Doc.Part}`Part`, {name Verso.Doc.Block}`Block`, and {name Verso.Doc.Inline}`Inline` that genres may use.
+{name Verso.Doc.Genre.TraverseState}`Genre.TraverseState` contains the genre-specific information that's accumulated during traversal, while {name Verso.Doc.Genre.TraverseContext}`Genre.TraverseContext` provides a means of tracking the surrounding document context.
+To use this framework, genres should define instances of {name Verso.Doc.Traverse}`Traverse`, which specifies the traversal of a genre's custom elements.
+Additionally, instances of {name Verso.Doc.TraversePart}`GenrePart` and {name Verso.Doc.TraverseBlock}`GenreBlock` specify how traversal keeps track of the current position in a document.
+
+{docstring Verso.Doc.Traverse}
+
+{docstring Verso.Doc.TraversePart}
+
+{docstring Verso.Doc.TraverseBlock}
+
+# Output Generation
+%%%
+tag := "output-gen"
+%%%
+
+Following traversal, the readable version of the document is generated.
+This may be in any format; each {tech}[genre] defines its supported formats.
+
+Additionally, genres that emit HTML may generate a serialized version of their cross-reference database.
+This can be used to automatically maintain the links that implement cross-references between Verso documents: if content moves, rebuilding the linking document is sufficient to fix the link.

doc/UsersGuide/Extensions.lean

@@ -0,0 +1,106 @@
+/-
+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 Verso.Syntax
+import VersoManual
+
+open Verso Genre Manual
+open InlineLean
+
+#doc (Manual) "Extensions" =>
+%%%
+tag := "extensions"
+htmlSplit := .never
+%%%
+
+Verso's markup language features four extension points:
+ * {tech}[Roles]
+ * {tech}[Directives]
+ * {tech}[Code blocks]
+ * {tech}[Commands]
+
+These can be used to extend Verso to support new documentation features.
+
+# Syntax
+%%%
+tag := "extension-syntax"
+%%%
+
+All four extension points share a common syntax.
+They are invoked by name, with a sequence of arguments.
+These arguments may be positional or by name, and their values may be identifiers, string literals, or numbers.
+
+:::paragraph
+In this example, the directive `syntax` is invoked with the positional argument `term` and the named argument `title` set to `"Example"`.
+It contains a descriptive paragraph and the code block `grammar`, which is invoked with no arguments:
+````
+:::syntax term (title := example)
+This is an example grammar:
+```grammar
+term ::= term "<+-+>" term
+```
+:::
+````
+:::
+
+:::paragraph
+More formally, an invocation of an extension should match this grammar:
+```
+CALL := IDENT ARG*
+ARG := VAL | "(" IDENT ":=" VAL ")"
+VAL := IDENT | STRING | NUM
+```
+A `CALL` may occur after an opening fence on a code block.
+It is mandatory after the opening colons of a directive, in the opening curly braces of a role, or in a command.
+:::
+
+# Elaborating Extensions
+%%%
+tag := "elab-extensions"
+%%%
+
+Each kind of extension has a table that maps names to expanders.
+An {deftech}_expander_ converts Verso's syntax to Lean terms.
+When the elaborator encounters a code block, role, directive, or command invocation, it resolves the name and looks up an expander in the table.
+Expanders are attempted until one of them either throws an error or succeeds.
+Expanders use the monad {name Verso.Doc.Elab.DocElabM}`DocElabM`, which is an extension of Lean's term elaboration monad {name Lean.Elab.Term.TermElabM}`TermElabM` with document-specific features.
+Expanders first {ref "ArgParse"}[parse] their arguments into a suitable configuration type, typically via a {name Verso.ArgParse.FromArgs}`FromArgs` instance, after which they return Lean syntax.
+
+There are two ways to associate an expander with a name: the `@[code_block]`, `@[role]`, `@[directive]`, and `@[block_command]` attributes (preferred) or the `@[code_block_expander]`, `@[role_expander]`, and `@[directive_expander]` attributes.
+Using the former attributes results in an expander that invokes the argument parser automatically, and they enable Verso to automatically compute usage information from a {name Verso.ArgParse.FromArgs}`FromArgs` instance.
+The latter are lower-level, and require manual parsing of arguments.
+
+## Parsing Arguments
+%%%
+tag := "ArgParse"
+%%%
+
+This grammar is fairly restrictive, so each extension is responsible for parsing their arguments in order to afford sufficient flexibility.
+Arguments are parsed via instances of {name Verso.ArgParse.FromArgs}`FromArgs`:
+
+{docstring Verso.ArgParse.FromArgs}
+
+Implementations of {name Verso.ArgParse.FromArgs.fromArgs}`FromArgs.fromArgs` specify parsers written using {name Verso.ArgParse}`ArgParse`:
+
+{docstring Verso.ArgParse}
+
+Individual argument values are matched using {name Verso.ArgParse.ValDesc}`ValDesc`:
+
+{docstring Verso.ArgParse.ValDesc}
+
+A canonical value description for a Lean type can be registered via an instance of {name Verso.ArgParse.FromArgVal}`FromArgVal`:
+
+{docstring Verso.ArgParse.FromArgVal}
+
+
+In addition to the constructors of {name Verso.ArgParse}`ArgParse`, the {name}`Applicative` and {name}`Functor` instances are important, as well as the following helpers:
+
+{docstring Verso.ArgParse.namedD}
+
+{docstring Verso.ArgParse.positional'}
+
+{docstring Verso.ArgParse.named'}
+
+{docstring Verso.ArgParse.namedD'}