Verso docstring roles

This module provides custom Verso docstring roles and code blocks used to support Verso syntax in Mathlib docstrings:

• {url} turns a code literal containing a URL into a link.

• {library_note} references a library note and checks that it exists.

• {cite} references a bibliography entry and renders custom text for it.

• The code code block records a verbatim code listing in the given language.

The roles are declared in the root namespace so that they are available in every docstring without opening a namespace.

structure Mathlib.VersoRoles.Citation : Type

A reference to a bibliography entry in docs/references.bib.

• key : String

  The citation key, as it appears in docs/references.bib.

@[instance_reducible]

instance Mathlib.VersoRoles.instTypeNameCitation : TypeName Citation

Equations

• Mathlib.VersoRoles.instTypeNameCitation = Mathlib.VersoRoles.inst✝

@[instance_reducible]

instance Mathlib.VersoRoles.instReprCitation : Repr Citation

Equations

• Mathlib.VersoRoles.instReprCitation = { reprPrec := Mathlib.VersoRoles.instReprCitation.repr }

def Mathlib.VersoRoles.instReprCitation.repr : Citation → Nat → Std.Format

Equations

• Mathlib.VersoRoles.instReprCitation.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "key" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.key)).group) " }"

structure Mathlib.VersoRoles.CodeWithLanguage : Type

A verbatim code listing together with the name of its language.

• language : String

  The language of the code listing.

@[instance_reducible]

instance Mathlib.VersoRoles.instTypeNameCodeWithLanguage : TypeName CodeWithLanguage

Equations

• Mathlib.VersoRoles.instTypeNameCodeWithLanguage = Mathlib.VersoRoles.inst✝

def Mathlib.VersoRoles.instReprCodeWithLanguage.repr : CodeWithLanguage → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Mathlib.VersoRoles.instReprCodeWithLanguage : Repr CodeWithLanguage

Equations

• Mathlib.VersoRoles.instReprCodeWithLanguage = { reprPrec := Mathlib.VersoRoles.instReprCodeWithLanguage.repr }

def Mathlib.VersoRoles.soleCode (xs : Array Lean.Doc.VersoInline) : Lean.Doc.DocM Lean.Doc.VersoCode

Extracts the single code literal from the contents of a role, such as the `x` in {role}`x`.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.VersoRoles.bibContainsKey (bib key : String) : Bool

Whether bib (the contents of docs/references.bib) contains an entry with the given key.

Equations

• One or more equations did not get rendered due to their size.

def url (xs : Lean.TSyntaxArray `Lean.Doc.Parser.inline) : Lean.Doc.DocM (Lean.Doc.Inline Lean.ElabInline)

A link to a URL.

The code literal contains the target, which is also used as the link text, as in {url}`https://leanprover.org`.

Equations

• url xs = do let s ← Mathlib.VersoRoles.soleCode xs have target : String := s.view pure (Lean.Doc.Inline.link #[Lean.Doc.Inline.text target] target)

opaque doc.verso.libraryNote.warnOnMissing : Lean.Option Bool

If doc.verso.libraryNote.warnOnMissing is enabled, a {library_note} reference that is not in scope generates a warning.

def library_note (xs : Lean.TSyntaxArray `Lean.Doc.Parser.inline) : Lean.Doc.DocM (Lean.Doc.Inline Lean.ElabInline)

A reference to a library note.

The code literal contains the note's label, as in {library_note}`partially-applied ext lemmas`. A warning is reported when no library note with this label is in scope, so that references to notes defined later are allowed. Set the option doc.verso.libraryNote.warnOnMissing to false to disable this warning.

Equations

• One or more equations did not get rendered due to their size.

def cite (key : Lean.StrLit) (xs : Lean.TSyntaxArray `Lean.Doc.Parser.inline) : Lean.Doc.DocM (Lean.Doc.Inline Lean.ElabInline)

A reference to a bibliography entry.

The positional argument is the entry's key in docs/references.bib, and the bracketed content is the text to render, as in {cite "Adamek_Rosicky_1994"}[Adámek–Rosický]. A warning is emitted when the key is not found in docs/references.bib.

TODO: this performs an O(n) lookup of bibliographic entries for every reference appearing in each docstring. For potential optimization, see: https://github.com/leanprover-community/mathlib4/pull/44135/changes#r4258754031

Equations

• One or more equations did not get rendered due to their size.

def code (language : Lean.Ident) (content : Lean.Doc.VersoCodeBlock) : Lean.Doc.DocM (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)

A verbatim code listing in the language named by the positional argument, as in ```code python.

The language is recorded for later use; the listing itself is rendered verbatim.

Equations

• code language content = pure (Lean.Doc.Block.other (Lean.ElabBlock.custom (Dynamic.mk { language := (Lean.TSyntax.getId language).toString })) #[Lean.Doc.Block.code content.view])