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.

def

Verso.Genre.Manual : Genre
Verso.Genre.Manual : Genre

A genre for writing reference manuals and other book-like documents.

structure

Verso.Genre.Manual.PartMetadata : Type
Verso.Genre.Manual.PartMetadata : Type

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

Verso.Genre.Manual.HtmlSplitMode : Type
Verso.Genre.Manual.HtmlSplitMode : 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

Verso.Genre.Manual.Block : Type
Verso.Genre.Manual.Block : Type

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

Verso.Genre.Manual.Inline : Type
Verso.Genre.Manual.Inline : Type

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

Verso.Genre.Manual.BlockDescr : Type
Verso.Genre.Manual.BlockDescr : Type

Implementations of all the operations needed to use a block.

Constructor

Verso.Genre.Manual.BlockDescr.mk

Extends

HtmlAssets

Fields

extraCss : Std.HashSet CSS

Inherited from

HtmlAssets

extraJs : Std.HashSet JS

Inherited from

HtmlAssets

extraJsFiles : Std.HashSet JsFile

Inherited from

HtmlAssets

extraCssFiles : Std.HashSet CssFile

Inherited from

HtmlAssets

extraDataFiles : Std.HashSet DataFile

Inherited from

HtmlAssets

licenseInfo : Std.HashSet LicenseInfo

Inherited from

HtmlAssets

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

Verso.Genre.Manual.InlineDescr : Type
Verso.Genre.Manual.InlineDescr : Type

Implementations of all the operations needed to use an inline element.

Constructor

Verso.Genre.Manual.InlineDescr.mk

Extends

HtmlAssets

Fields

extraCss : Std.HashSet CSS

Inherited from

HtmlAssets

extraJs : Std.HashSet JS

Inherited from

HtmlAssets

extraJsFiles : Std.HashSet JsFile

Inherited from

HtmlAssets

extraCssFiles : Std.HashSet CssFile

Inherited from

HtmlAssets

extraDataFiles : Std.HashSet DataFile

Inherited from

HtmlAssets

licenseInfo : Std.HashSet LicenseInfo

Inherited from

HtmlAssets

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?

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

Verso.Genre.Manual.HtmlAssets : Type
Verso.Genre.Manual.HtmlAssets : Type

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

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

Verso.Genre.Manual.HtmlAssets.combine (assets moreAssets : HtmlAssets) :
  HtmlAssets
Verso.Genre.Manual.HtmlAssets.combine
  (assets moreAssets : HtmlAssets) :
  HtmlAssets

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 PUnit
List.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, where e is an expression instead of a variable, generalizes e in the goal, and then performs induction on the resulting variable.
induction e using r allows the user to specify the principle of induction that should be used. Here r should be a term whose result type must be of the form C t, where C is a bound variable and t is a (possibly empty) sequence of bound variables
induction e generalizing z₁ ... zₙ, where z₁ ... zₙ are variables in the local context, generalizes over z₁ ... 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 tactic tac₁ for the zero case, and tac₂ for the succ case.

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.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

Verso.Genre.Manual.deftech : Elab.RoleExpanderOf DefTechArgs
Verso.Genre.Manual.deftech :
  Elab.RoleExpanderOf DefTechArgs

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

Verso.Genre.Manual.tech : Elab.RoleExpanderOf TechArgs
Verso.Genre.Manual.tech :
  Elab.RoleExpanderOf TechArgs

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

Verso.Genre.Manual.LicenseInfo : Type
Verso.Genre.Manual.LicenseInfo : Type

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

Verso.Genre.Manual.licenseInfo : Elab.BlockCommandOf Unit
Verso.Genre.Manual.licenseInfo :
  Elab.BlockCommandOf Unit

Displays the open-source licenses of components used to build the document.