3. Building Documents🔗

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 Verso's markup language, which is parsed to Lean's own 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

1. 3.1. Elaboration
2. 3.2. Compilation
3. 3.3. Traversal
4. 3.4. Output Generation