A genre for writing reference manuals and other book-like documents.
7. Manuals and Books
Verso's 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.
structure
Metadata for the manual
Constructor
Verso.Genre.Manual.PartMetadata.mk
Fields
shortTitle : Option String
A shorter title to be shown in titlebars and tables of contents.
shortContextTitle : Option String
A shorter title to be shown in breadcrumbs for search results. Should typically be at least as
short as shortTitle.
authors : List String
The book's authors
authorshipNote : Option String
An extra note to show after the author list
date : Option String
The publication date
tag : Option Tag
The main tag for the part, used for cross-references.
file : Option String
If this part ends up as the root of a file, use this name for it
id : Option InternalId
The internal unique ID, which is automatically assigned during traversal.
number : Bool
Should this section be numbered? If false, then it's like \section* in LaTeX
draft : Bool
If true, the part is only rendered in draft mode.
assignedNumber : Option Numbering
Which number has been assigned? This field is set during traversal.
htmlToc : Bool
If true, this part will display a list of subparts that are separate HTML pages.
htmlSplit : HtmlSplitMode
How should this document be split when rendering multi-page HTML output?
inductive type
When rendering multi-page HTML, should splitting pages follow the depth setting?
Constructors
default : HtmlSplitMode
Follow the main setting
never : HtmlSplitMode
Do not split here nor in child parts
The Manual genre's block and inline element types are extensible.
In the document, they consist of instances of Manual.Block and Manual.Inline, respectively:
structure
A custom block. The name field should correspond to an entry in the block descriptions table.
Constructor
Verso.Genre.Manual.Block.mk
Fields
name : Lean.Name
A unique name that identifies the block.
id : Option InternalId
A unique ID, assigned during traversal.
data : Lean.Json
Data saved by elaboration, potentially updated during traversal, and used to render output. This is the primary means of communicating information about a block between phases.
properties : NameMap String
A registry for properties that can be used to create ad-hoc protocols for coordination between block elements in extensions.
structure
A custom inline. The name field should correspond to an entry in the block descriptions table.
Constructor
Verso.Genre.Manual.Inline.mk
Fields
name : Lean.Name
A unique name that identifies the inline.
id : Option InternalId
The internal unique ID, which is automatically assigned during traversal.
data : Lean.Json
Data saved by elaboration, potentially updated during traversal, and used to render output. This is the primary means of communicating information about a block between phases.
The fields Block.name and Inline.name are used to look up concrete implementations of traversal and output generation in run-time tables that contain descriptions:
structure
Implementations of all the operations needed to use a block.
Constructor
Verso.Genre.Manual.BlockDescr.mk
Extends
Fields
features : HtmlFeatures
Inherited from
Which bundled features should be included?
extraCss : Std.HashSet CSS
Inherited from
Extra CSS to be included inline into every <head> via <style> tags
extraJs : Std.HashSet JS
Inherited from
Extra JS to be included inline into every <head> via <script> tags
extraJsFiles : Std.HashSet JsFile
Inherited from
Extra JS to be written to the filesystem in the Verso data directory and loaded by each <head>
extraCssFiles : Std.HashSet CssFile
Inherited from
Extra CSS to be written to the filesystem in the Verso data directory and loaded by each <head>
extraDataFiles : Std.HashSet DataFile
Inherited from
Extra files to be placed in the Verso data directory
licenseInfo : Std.HashSet LicenseInfo
Inherited from
Open-source licenses, to be collected for display in the final document.
init : TraverseState → TraverseState
All registered initializers are called in the state prior to the first traversal.
traverse : BlockTraversal Manual
How the traversal phase should process this block
toHtml : Option (BlockToHtml Manual (ReaderT Multi.AllRemotes (ReaderT ExtensionImpls IO)))
How to generate HTML. If none, generating HTML from a document that contains this block will fail.
localContentItem : InternalId → Lean.Json → Array (Doc.Block Manual) → Except String (Array (String × Output.Html))
Should this block be an entry in the page-local ToC? If so, how should it be represented?
Entries should be returned as a preference-ordered array of representations. Each representation consists of a string and some HTML; the string should represent the HTML's content if all formatting were stripped. Items are compared for string equality, with later suggestions used in case of overlap, but the HTML is what's displayed. Exceptions are logged as errors during HTML generation.
The empty array means that the block should not be included.
toTeX : Option (BlockToTeX Manual (ReaderT ExtensionImpls IO))
How to generate TeX. If none, generating TeX from a document that contains this block will fail.
usePackages : List String
Required TeX \usepackage lines
preamble : List String
Required items in the TeX preamble
structure
Implementations of all the operations needed to use an inline element.
Constructor
Verso.Genre.Manual.InlineDescr.mk
Extends
Fields
features : HtmlFeatures
Inherited from
Which bundled features should be included?
extraCss : Std.HashSet CSS
Inherited from
Extra CSS to be included inline into every <head> via <style> tags
extraJs : Std.HashSet JS
Inherited from
Extra JS to be included inline into every <head> via <script> tags
extraJsFiles : Std.HashSet JsFile
Inherited from
Extra JS to be written to the filesystem in the Verso data directory and loaded by each <head>
extraCssFiles : Std.HashSet CssFile
Inherited from
Extra CSS to be written to the filesystem in the Verso data directory and loaded by each <head>
extraDataFiles : Std.HashSet DataFile
Inherited from
Extra files to be placed in the Verso data directory
licenseInfo : Std.HashSet LicenseInfo
Inherited from
Open-source licenses, to be collected for display in the final document.
init : TraverseState → TraverseState
All registered initializers are called in the state prior to the first traversal.
traverse : InlineTraversal Manual
Given the contents of the data field of the corresponding Manual.Inline and the contained
inline elements, carry out the traversal pass.
In addition to updating the cross-reference state through the available monadic effects, a
traversal may additionally replace the element with another one. This can be used to e.g. emit
a cross-reference once the target becomes available in the state. To replace the element,
return some. To leave it as is, return none.
toHtml : Option (InlineToHtml Manual (ReaderT Multi.AllRemotes (ReaderT ExtensionImpls IO)))
How to generate HTML. If none, generating HTML from a document that contains this inline will fail.
localContentItem : InternalId → Lean.Json → Array (Doc.Inline Manual) → Except String (Array (String × Output.Html))
Should this inline be an entry in the page-local ToC? If so, how should it be represented?
Entries should be returned as a preference-ordered array of representations. Each representation consists of a string and some HTML; the string should represent the HTML's content if all formatting were stripped. Items are compared for string equality, with later suggestions used in case of overlap, but the HTML is what's displayed.
The empty array means that the inline should not be included.
toTeX : Option (InlineToTeX Manual (ReaderT ExtensionImpls IO))
How to generate TeX. If none, generating TeX from a document that contains this inline will fail.
usePackages : List String
Required TeX \usepackage lines
preamble : List String
Required items in the TeX preamble
Typically, the inline_extension and block_extension commands are used to simultaneously define an element and its descriptor, registering them for use by manualMain.
The type HtmlAssets contains CSS and JavaScript code.
Manual.TraverseState, Manual.BlockDescr, and Manual.InlineDescr all inherit from this structure.
During traversal, HTML assets are collected; they are all included in the final rendered document.
structure
A collection of HTML assets that can be initialized in the manual configuration and enlarged by custom elements during traversal.
Constructor
Verso.Genre.Manual.HtmlAssets.mk
Fields
features : HtmlFeatures
Which bundled features should be included?
extraCss : Std.HashSet CSS
Extra CSS to be included inline into every <head> via <style> tags
extraJs : Std.HashSet JS
Extra JS to be included inline into every <head> via <script> tags
extraJsFiles : Std.HashSet JsFile
Extra JS to be written to the filesystem in the Verso data directory and loaded by each <head>
extraCssFiles : Std.HashSet CssFile
Extra CSS to be written to the filesystem in the Verso data directory and loaded by each <head>
extraDataFiles : Std.HashSet DataFile
Extra files to be placed in the Verso data directory
licenseInfo : Std.HashSet LicenseInfo
Open-source licenses, to be collected for display in the final document.
Use HtmlAssets.combine to combine multiple assets.
def
Combines two sets of HTML assets.
If moreAssets contains named file assets whose names conflict with those in assets,
then the version in assets is used.
7.1. Tags and References
The Manual genre maintains a table of link targets for various namespaces, such as documented constants, documented syntax, technical terminology, and sections.
In this table, domain-specific names are mapped to their documentation location.
For items such as document sections that don't have a clear, unambiguous, globally-unique name, Verso requires such a name to be manually specified before it is in the table.
Extensions and parts for which names should be manually specified take a tag parameter.
Specifying a tag has the following benefits:
-
The item is included in the quick-jump box and the index.
-
The tag can be used to construct permalinks that will continue to work even if the document is reorganized, so long as the tag is maintained.
-
The item can be linked to automatically from other documents.
Tags should be specified for all sections that the author considers to have a stable identity.
7.2. Paragraphs
The paragraph directive indicates that a sequence of blocks form a logical paragraph.
Verso's markup language shares one key limitation with Markdown and HTML: bulleted lists and code blocks cannot be contained within paragraphs.
However, there's no a priori reason to reject this, and many real documents include lists in paragraphs.
When using the paragraph directive, HTML output wraps the contents in a suitable element that causes their internal margins to be a bit smaller, and TeX output omits the blank line that would signal a paragraph break to TeX.
7.3. Docstrings
Docstrings can be included using the docstring directive. For instance,
{docstring List.forM}
results in
def
List.forM.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnitList.forM.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnit
Applies the monadic action f to every element in the list, in order.
List.mapM is a variant that collects results. List.forA is a variant that works on any
Applicative.
The docstring command takes a positional parameter which is the documented name.
It also accepts the following optional named parameters:
-
allowMissing : Bool If
true, missing docstrings are a warning rather than an error.-
hideFields : Bool If
true, fields or methods of structures or classes are not shown.-
hideStructureConstructor : Bool If
true, constructors of structures or classes are not shown.-
label : String A label to show instead of the default.
The tactic directive and the optionDocs command can be used to show documentation for tactics and compiler options, respectively.
:::tactic "induction" :::
results in
tactic
induction
Assuming x is a variable in the local context with an inductive type,
induction x applies induction on x to the main goal,
producing one goal for each constructor of the inductive type,
in which the target is replaced by a general instance of that constructor
and an inductive hypothesis is added for each recursive argument to the constructor.
If the type of an element in the local context depends on x,
that element is reverted and reintroduced afterward,
so that the inductive hypothesis incorporates that hypothesis as well.
For example, given n : Nat and a goal with a hypothesis h : P n and target Q n,
induction n produces one goal with hypothesis h : P 0 and target Q 0,
and one goal with hypotheses h : P (Nat.succ a) and ih₁ : P a → Q a and target Q (Nat.succ a).
Here the names a and ih₁ are chosen automatically and are not accessible.
You can use with to provide the variables names for each constructor.
-
induction e, whereeis an expression instead of a variable, generalizesein the goal, and then performs induction on the resulting variable. -
induction e using rallows the user to specify the principle of induction that should be used. Herershould be a term whose result type must be of the formC t, whereCis a bound variable andtis a (possibly empty) sequence of bound variables -
induction e generalizing z₁ ... zₙ, wherez₁ ... zₙare variables in the local context, generalizes overz₁ ... zₙbefore applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized. -
Given
x : Nat,induction x with | zero => tac₁ | succ x' ih => tac₂uses tactictac₁for thezerocase, andtac₂for thesucccase.
and
{optionDocs pp.deepTerms.threshold}
results in
option
pp.deepTerms.threshold
Default value: 50
(pretty printer) when pp.deepTerms is false, the depth at which terms start being replaced with ⋯
7.3.1. Docstrings From doc-gen4 (Experimental)
Ordinarily, the 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 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 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.
7.3.1.1. 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).
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.
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]
7.3.1.2. Usage
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
7.3.1.3. 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.
7.3.1.4. 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.
7.4. Technical Terminology
The deftech role can be used to annotate the definition of a technical term.
Elsewhere in the document, tech can be used to annotate a use site of a technical term.
A 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.
def
Defines a technical term.
Internally, these definitions are saved according to a key that is derived by stripping formatting
information from the arguments in args, and then normalizing the resulting string by:
-
lowercasing it
-
replacing trailing
"ies"with"y" -
replacing consecutive runs of whitespace and/or hyphens with a single space
Call with (normalize := false) to disable normalization, and (key := some k) to use k instead
of the automatically-derived key.
Uses of tech use the same process to derive a key, and the key is matched against the deftech table.
def
Emits a reference to a technical term defined with deftech.
Internally, these terms are found according to a key that is derived by stripping formatting
information from the arguments in args, and then normalizing the resulting string by:
-
lowercasing it
-
replacing trailing
"ies"with"y" -
replacing consecutive runs of whitespace and/or hyphens with a single space
Call with (normalize := false) to disable normalization, and (key := some k) to use k instead
of the automatically-derived key.
7.5. Open-Source Licenses
To facilitate providing appropriate credit to the authors of open-source JavaScript, CSS, and HTML libraries used to render a Verso document, inline and block elements can specify the licenses of components that they include in their rendered output.
This is done using the licenseInfo field that BlockDescr and InlineDescr inherit from HtmlAssets.
These contain a LicenseInfo:
structure
A description of an open-source license used by a frontend component that's included in generated HTML. This is used to create an attribution page.
Constructor
Verso.Genre.Manual.LicenseInfo.mk
Fields
identifier : String
SPDX license identifier
dependency : String
Dependency name. This is used in a header, and for alphabetical sorting.
howUsed : Option String
How is the dependency used? This can give better credit.
Examples:
-
"The display of mathematical formulae is powered by KaTeX."
-
"The graphs are rendered using Chart.js."
link : Option String
A link target used to credit the dependency's author
text : Array (Option String × String)
The license or notice text in plain text, divided into sections with optional headers.
The licenseInfo command displays the licenses for all components that were included in the generated document:
def
Displays the open-source licenses of components used to build the document.