From 1b81bfd7d12bb86260457fa25f366d1f1846ab91 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 15 Aug 2025 16:59:20 +0200 Subject: [PATCH 1/2] feat: much more documentation --- doc/UsersGuide/Basic.lean | 136 +++++++++--------- doc/UsersGuide/Elab.lean | 104 ++++++++++++++ doc/UsersGuide/Extensions.lean | 106 ++++++++++++++ doc/UsersGuide/Manuals.lean | 162 +++++++++++++++++++++ doc/UsersGuide/Markup.lean | 102 ++++++++----- doc/UsersGuide/Output.lean | 125 ++++++++++++++++ doc/UsersGuide/Websites.lean | 78 ++++++++++ src/verso-blog/VersoBlog.lean | 19 +++ src/verso-blog/VersoBlog/Basic.lean | 79 ++++++++++ src/verso-blog/VersoBlog/Site.lean | 9 ++ src/verso-blog/VersoBlog/Template.lean | 15 +- src/verso-blog/VersoBlog/Theme.lean | 38 +++++ src/verso-manual/VersoManual.lean | 9 +- src/verso-manual/VersoManual/Basic.lean | 87 ++++++++++- src/verso-manual/VersoManual/License.lean | 3 + src/verso-manual/VersoManual/Table.lean | 2 +- src/verso/Verso/Doc.lean | 168 ++++++++++++++++++---- src/verso/Verso/Doc/ArgParse.lean | 121 +++++++++++----- src/verso/Verso/Doc/Elab/Monad.lean | 2 +- src/verso/Verso/Output/Html.lean | 52 ++++++- src/verso/Verso/Output/TeX.lean | 31 ++-- 21 files changed, 1249 insertions(+), 199 deletions(-) create mode 100644 doc/UsersGuide/Elab.lean create mode 100644 doc/UsersGuide/Extensions.lean create mode 100644 doc/UsersGuide/Manuals.lean create mode 100644 doc/UsersGuide/Output.lean create mode 100644 doc/UsersGuide/Websites.lean diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean index d6d126d73..523e5b79e 100644 --- a/doc/UsersGuide/Basic.lean +++ b/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 %%% diff --git a/doc/UsersGuide/Elab.lean b/doc/UsersGuide/Elab.lean new file mode 100644 index 000000000..0b0b670a0 --- /dev/null +++ b/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. diff --git a/doc/UsersGuide/Extensions.lean b/doc/UsersGuide/Extensions.lean new file mode 100644 index 000000000..d6f0970cb --- /dev/null +++ b/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'} diff --git a/doc/UsersGuide/Manuals.lean b/doc/UsersGuide/Manuals.lean new file mode 100644 index 000000000..db73d7e47 --- /dev/null +++ b/doc/UsersGuide/Manuals.lean @@ -0,0 +1,162 @@ +/- +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 +import VersoBlog + +open Verso Genre Manual + +open InlineLean +open Verso.Doc + +#doc (Manual) "Manuals and Books" => +%%% +tag := "manual" +htmlSplit := .never +%%% + +Verso's {name}`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. + +{docstring Manual} + +{docstring Manual.PartMetadata} + +{docstring Manual.HtmlSplitMode} + +The {name}`Manual` genre's block and inline element types are extensible. +In the document, they consist of instances of {name}`Manual.Block` and {name}`Manual.Inline`, respectively: + +{docstring Manual.Block} + +{docstring Manual.Inline} + +The fields {name}`Block.name` and {name Manual.Inline.name}`Inline.name` are used to look up concrete implementations of traversal and output generation in run-time tables that contain descriptions: + +{docstring Manual.BlockDescr} + +{docstring Manual.InlineDescr} + +Typically, the `inline_extension` and `block_extension` commands are used to simultaneously define an element and its descriptor, registering them for use by {name}`manualMain`. + +# Tags and References +%%% +tag := "manual-tags" +%%% + +The {name}`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. + +:::paragraph +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. +::: + +# Paragraphs +%%% +tag := "paragraph-directive" +%%% + +The {name}`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 {name}`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. + +# Docstrings +%%% +tag := "docstrings" +%%% + +Docstrings can be included using the `docstring` directive. For instance, + +``` +{docstring List.forM} +``` + +results in + +{docstring List.forM} + +The {name}`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. + +::::paragraph +The {name}`tactic` directive and the {name}`optionDocs` command can be used to show documentation for tactics and compiler options, respectively. + +``` +:::tactic "induction" +::: +``` + +results in + +:::tactic "induction" +::: + +and + +``` +{optionDocs pp.deepTerms.threshold} +``` + +results in + +{optionDocs pp.deepTerms.threshold} +:::: + + +# Technical Terminology +%%% +shortTitle := "Glossary" +tag := "tech-terms" +%%% + +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. + +{docstring deftech} + +{docstring tech} + + +# Open-Source Licenses +%%% +tag := "oss-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 {name}`BlockDescr.licenseInfo` and {name}`InlineDescr.licenseInfo` fields. +These contain a {name}`LicenseInfo`: + +{docstring LicenseInfo} + +The {name}`licenseInfo` command displays the licenses for all components that were included in the generated document: + +{docstring licenseInfo} diff --git a/doc/UsersGuide/Markup.lean b/doc/UsersGuide/Markup.lean index 73781c8c3..044e82234 100644 --- a/doc/UsersGuide/Markup.lean +++ b/doc/UsersGuide/Markup.lean @@ -1,3 +1,8 @@ +/- +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 @@ -178,7 +183,7 @@ r#" .markup-example > .content > .syntax, .markup-example > .content > .result { flex: 1; - padding: var(--verso--box-padding); + padding: 0 var(--verso--box-padding); position: relative; width: calc(50% - calc(4 * var(--verso--box-padding))); } @@ -189,7 +194,7 @@ r#" .markup-example > .content > .syntax > .title, .markup-example > .content > .result > .title { font-family: var(--verso-structure-font-family); - padding: var(--verso--box-padding); + padding: 0; font-size: 0.875rem; } @@ -329,6 +334,7 @@ def markupPreviewPre : CodeBlockExpanderOf MarkupPreviewConfig #doc (Manual) "Verso Markup" => %%% tag := "verso-markup" +htmlSplit := .never %%% Lean's documentation markup language is a close relative of Markdown, but it's not identical to it. @@ -338,12 +344,25 @@ Lean's documentation markup language is a close relative of Markdown, but it's n tag := "markup-design-principles" %%% - 1. Syntax errors - fail fast rather than producing unexpected output or having complicated rules - 2. Reduce lookahead - parsing should succeed or fail as locally as possible - 3. Extensibility - there should be dedicated features for compositionally adding new kinds of content, rather than relying on a collection of ad-hoc textual subformats - 4. Assume Unicode - Lean users are used to entering Unicode directly and have good tools for it, so there's no need to support alternative textual syntaxes for characters not on keyboards such as em dashes or typographical quotes - 5. Markdown compatibility - benefit from existing muscle memory and familiarity when it doesn't lead to violations of the other principles - 6. Pandoc and Djot compatibility - when Markdown doesn't have a syntax for a feature, attempt to be compatible with Pandoc Markdown or Djot +: Syntax errors + + Fail fast rather than producing unexpected output or having complicated rules. + +: Reduce lookahead + + Parsing should succeed or fail as locally as possible. + +: Extensibility + + There should be dedicated features for compositionally adding new kinds of content, rather than relying on a collection of ad-hoc textual subformats. + +: Assume Unicode + + Lean users are used to entering Unicode directly and have good tools for it, so there's no need to support alternative textual syntaxes for characters not on keyboards such as em dashes or typographical quotes. + +: Markdown compatibility + + Users benefit from existing muscle memory and familiarity when it doesn't lead to violations of the other principles. # Syntax %%% @@ -352,24 +371,22 @@ tag := "markup-syntax" Like Markdown, Lean's markup has three primary syntactic categories: -: Inline elements - The ordinary content of written text, such as text itself, bold or emphasized text, and hyperlinks. +: Document structure + + Headers, footnote definitions, and named links give greater structure to a document. They may not be nested inside of blocks. + : Block elements The main organization of written text, including paragraphs, lists, and quotations. Some blocks may be nested: for example, lists may contain other lists. -: Document structure +: Inline elements - Headers, footnote definitions, and named links give greater structure to a document. They may not be nested inside of blocks. + The ordinary content of written text, such as text itself, bold or emphasized text, and hyperlinks. -## Description -%%% -tag := "markup-syntax-description" -%%% -### Document Structure +## Document Structure %%% tag := "document-structure" %%% @@ -403,7 +420,7 @@ Metadata blocks begin and end with `%%%`, and they contain any syntax that would ::: -### Block Syntax +## Block Syntax %%% tag := "block-syntax" %%% @@ -449,7 +466,7 @@ This is a new paragraph. ``` ::: -#### Lists +### Lists %%% tag := "list-syntax" %%% @@ -664,7 +681,7 @@ A description item is a line that starts with zero or more spaces, followed by a ``` ::: -#### Quotes +### Quotes %%% tag := "quote-syntax" %%% @@ -701,7 +718,7 @@ But not this one. ``` ::: -#### Code Blocks +### Code Blocks %%% tag := "code-block-syntax" %%% @@ -789,9 +806,9 @@ def x : String := 5 ::: When a code block has a name, then the name is resolved in the current Lean namespace and used to select an implementation. -TODO ref extensions chapter (todo) +The {ref "extensions"}[chapter on Verso markup extensions] has more details on this process. -#### Directives +### Directives %%% tag := "directive-syntax" %%% @@ -801,7 +818,7 @@ Directives begin with three or more colons and a name with zero or more argument They may contain any number of blocks, which must be indented at least as much as the colons. Nested directives must begin and end with strictly fewer colons than the surrounding directives. -TODO ref extensions chapter (todo) +The {ref "extensions"}[chapter on Verso markup extensions] describes the processing of directives in more detail. This is an empty directive: :::markupPreview "Directives" @@ -832,14 +849,14 @@ This is a paragraph ``` ::: -#### Commands +### Commands %%% tag := "command-block-syntax" %%% A line that consists of only a set of curly braces that contain a name and zero or more arguments is a command. The name is used to select an implementation for the command, which is then invoked during elaboration. -TODO ref extensions chapter (todo) +The {ref "extensions"}[chapter on Verso markup extensions] has more details on this process. :::markupPreview "Commands" ``` @@ -851,7 +868,7 @@ TODO ref extensions chapter (todo) ::: -### Inline Syntax +## Inline Syntax %%% tag := "inline-syntax" %%% @@ -1044,14 +1061,14 @@ This one takes a single inline code element without needing square brackets: ::: :::: -## Differences from Markdown +# Differences from Markdown %%% tag := "differences-from-markdown" %%% This is a quick "cheat sheet" for those who are used to Markdown, documenting the differences. -### Syntax Errors +## Syntax Errors %%% tag := "syntax-errors" %%% @@ -1061,7 +1078,7 @@ Similarly, Markdown specifies that unmatched delimiters (such as `*` or `_`) sho This is based on the principle that, for long-form technical writing, it's better to catch typos while writing than while reviewing the text later. -### Reduced Lookahead +## Reduced Lookahead %%% tag := "reduced-lookahead" %%% @@ -1069,7 +1086,7 @@ tag := "reduced-lookahead" In Markdown, whether `[this][here]` is a link depends on whether `here` is defined as a link reference target somewhere in the document. In Lean's markup, it is always a link, and it is an error if `here` is not defined as a link target. -### Header Nesting +## Header Nesting %%% tag := "header-nesting" %%% @@ -1078,10 +1095,31 @@ In Lean's markup, every document already has a title, so there's no need to use Additionally, all documents are required to use `#` for their top-level header, `##` for the next level, and so forth, because a single file may represent a section, a chapter, or even a whole book. Authors should not need to maintain a global mapping from header levels to document structures, so Lean's markup automatically assigns these based on the structure of the document. -### Genre-Specific Extensions +## Genre-Specific Extensions %%% tag := "genre-specific-extensions" %%% Markdown has no standard way for specific tools or styles of writing to express domain- or {ref "genres"}[genre]-specific concepts. Lean's markup provides standard syntaxes to use for this purpose, enabling compositional extensions. + +## Fewer Unused Features +%%% +tag := "removed-md-features" +%%% + +Markdown has a number of features that are rarely used in practice. +They have been removed from Verso to reduce surprises while using it and make documents more predictable. +This includes: + * the distinction between [tight](https://spec.commonmark.org/0.31.2/#tight) and [loose](https://spec.commonmark.org/0.31.2/#loose) lists, + * [four-space indentation](https://spec.commonmark.org/0.31.2/#indented-code-blocks) to create code blocks, + * [Setext-style headers](https://spec.commonmark.org/0.31.2/#setext-headings), indicated with underlines instead of leading hash marks (`#`), + * [hard line break syntax](https://spec.commonmark.org/0.31.2/#hard-line-breaks), + * and [HTML entities and character references](https://spec.commonmark.org/0.31.2/#entity-and-numeric-character-references) + +Other Markdown features don't make sense for non-HTML output, and can be implemented by a {tech}[genre] using code blocks or directives. +They have also been removed from Verso. +In particular, this includes [HTML blocks](https://spec.commonmark.org/0.31.2/#html-blocks), [raw HTML](https://spec.commonmark.org/0.31.2/#raw-html) and [thematic breaks](https://spec.commonmark.org/0.31.2/#thematic-breaks). + +Finally, some Markdown features are used by a minority of authors, and make sense in all backends, but were not deemed worth the complexity budget. +In particular, this includes [auto-links](https://spec.commonmark.org/0.31.2/#autolinks). diff --git a/doc/UsersGuide/Output.lean b/doc/UsersGuide/Output.lean new file mode 100644 index 000000000..73bdba854 --- /dev/null +++ b/doc/UsersGuide/Output.lean @@ -0,0 +1,125 @@ +/- +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 +import VersoBlog + +open Verso Genre Manual + +open Verso.Genre.Blog (Page Post) + +open InlineLean +open Verso.Doc + +open Verso.Output + +#doc (Manual) "Output Formats" => +%%% +tag := "outputs" +htmlSplit := .never +%%% + +Verso provides genre authors with tools for generating HTML and TeX code via embedded languages that reduce the syntactic overhead of constructing ASTs. +These libraries may also be used by authors of extensions to the {name}`Manual` genre, who need to define how each new element should be rendered to each supported backend. + +# HTML +%%% +tag := "output-html" +%%% + +Verso's {name}`Html` type represents HTML documents. +They are typically produced using an embedded DSL that is available when the namespace `Verso.Output.Html` is opened. + +{docstring Html} + +{docstring Html.empty} + +{docstring Html.fromArray} + +{docstring Html.fromList} + +{docstring Html.append} + +{docstring Html.visitM} + +{docstring Html.format} + +{docstring Html.asString} + +HTML documents are written in double curly braces, in a syntax very much like HTML itself. +The differences are: + * Double curly braces escape back to Lean. This can be done for HTML elements, attribute values, or whole sets of attributes. + * Text content is written as Lean string literals to facilitate precise control over whitespace. + * Interpolated Lean strings (with `s!`) may be used in any context that expects a string. + +For example, this definition creates a `