Here, we convert nodes and docstrings to LaTeX. The main difficulty is converting Markdown to LaTeX, which we describe below.

@[reducible, inline]

abbrev BlueprintGen.Latex : Type

Equations

• BlueprintGen.Latex = String

We convert docstrings of declarations and modules to LaTeX. Besides the usual Markdown features, we also support citations using square brackets and references using inline code, by having custom commands and postprocessing steps, as follows:

1. Using MD4Lean, we parse the markdown.
2. If possible, we convert bracketed citations (e.g. [taylorwiles]) to \cite{taylorwiles} commands.
3. If possible, we convert inline code with a constant (e.g. abc) to \ref{abc} commands.
4. We convert the markdown to LaTeX macro definitions as output.

TODO: Support doc-gen4 style named citations like [abc][def].

The output provides the following macros:

• \inputleannode{name}: Inputs the theorem or definition with Lean name name.
• \inputleanmodule{Module}: Inputs the entire module (containing nodes and module docstrings) with module name Module.s

The long-term goal for blueprint-gen is to migrate to Verso and not have to output to LaTeX at all. Here, this would mean using docstring parsing from Verso instead (which similarly uses MD4Lean to parse the docstrings), and it has support for elaborating code blocks. However, AFAIK it currently does not support citations in docstrings.

opaque BlueprintGen.blueprint.bracketedCitations : Lean.Option Bool

opaque BlueprintGen.blueprint.refCommand : Lean.Option String

opaque BlueprintGen.blueprint.citeCommand : Lean.Option String

def BlueprintGen.escapeForLatexBasic (s : String) : String

Escapes a string in LaTeX for all LaTeX environments (text, math, leancode, links, etc.).

Equations

• BlueprintGen.escapeForLatexBasic s = (s.replace "#" "\\#").replace "%" "\\%"

def BlueprintGen.escapeForLatexText (s : String) : String

Escapes a string in LaTeX for text.

Equations

• BlueprintGen.escapeForLatexText s = ((BlueprintGen.escapeForLatexBasic s).replace "_" "\\_").replace "^" "\\^{}"

def BlueprintGen.postprocessMarkdownText {m : Type → Type} [Monad m] [Lean.MonadOptions m] (s : String) : m String

Escape # and convert brackets [taylorwiles] to \cite{taylorwiles} commands.

Equations

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

partial def BlueprintGen.postprocessMarkdownText.findAllEnclosed (s : String) (bracketStart bracketEnd : Char) (notFollowedBy : Char → Bool) (i : String.Pos := 0) (ret : Array String := ∅) : Array String

def BlueprintGen.removeNameFirstComponent : Lean.Name → Option Lean.Name

Equations

• BlueprintGen.removeNameFirstComponent (Lean.Name.anonymous.str str) = some Lean.Name.anonymous
• BlueprintGen.removeNameFirstComponent (Lean.Name.anonymous.num i) = some Lean.Name.anonymous
• BlueprintGen.removeNameFirstComponent (p.str s) = Option.map (fun (p : Lean.Name) => p.str s) (BlueprintGen.removeNameFirstComponent p)
• BlueprintGen.removeNameFirstComponent (p.num i) = Option.map (fun (p : Lean.Name) => p.num i) (BlueprintGen.removeNameFirstComponent p)
• BlueprintGen.removeNameFirstComponent Lean.Name.anonymous = none

def BlueprintGen.parseMarkdown (markdown : String) : Option MD4Lean.Document

Equations

• BlueprintGen.parseMarkdown markdown = MD4Lean.parse markdown (MD4Lean.MD_DIALECT_GITHUB ||| MD4Lean.MD_FLAG_LATEXMATHSPANS ||| MD4Lean.MD_FLAG_NOHTML)

def BlueprintGen.markdownToLatex {m : Type → Type} [Monad m] [Lean.MonadOptions m] (markdown : String) : m Latex

Parse and convert markdown to LaTeX using MD4Lean with postprocessing steps as above.

Equations

• BlueprintGen.markdownToLatex markdown = match BlueprintGen.parseMarkdown markdown with | none => pure markdown | some doc => BlueprintGen.markdownToLatex.documentToLatex doc

def BlueprintGen.markdownToLatex.documentToLatex {m : Type → Type} [Monad m] [Lean.MonadOptions m] (doc : MD4Lean.Document) : m Latex

Equations

• BlueprintGen.markdownToLatex.documentToLatex doc = do let __do_lift ← Array.mapM BlueprintGen.markdownToLatex.blockToLatex doc.blocks pure ("\n\n".intercalate __do_lift.toList)

partial def BlueprintGen.markdownToLatex.blockToLatex {m : Type → Type} [Monad m] [Lean.MonadOptions m] (block : MD4Lean.Block) : m Latex

partial def BlueprintGen.markdownToLatex.textToLatex {m : Type → Type} [Monad m] [Lean.MonadOptions m] (text : MD4Lean.Text) : m Latex

def BlueprintGen.markdownToLatex.attrTextToLatex (attrText : MD4Lean.AttrText) : Latex

Equations

• BlueprintGen.markdownToLatex.attrTextToLatex (MD4Lean.AttrText.normal content) = BlueprintGen.escapeForLatexBasic content
• BlueprintGen.markdownToLatex.attrTextToLatex (MD4Lean.AttrText.entity content) = BlueprintGen.escapeForLatexBasic content
• BlueprintGen.markdownToLatex.attrTextToLatex MD4Lean.AttrText.nullchar = ""

partial def BlueprintGen.markdownToLatex.itemToLatex {m : Type → Type} [Monad m] [Lean.MonadOptions m] (item : MD4Lean.Li MD4Lean.Block) : m Latex

def BlueprintGen.moduleToRelPath (module : Lean.Name) (ext : String) : System.FilePath

Equations

• BlueprintGen.moduleToRelPath module ext = Lean.modToFilePath { toString := "module" } module ext

def BlueprintGen.libraryToRelPath (library : Lean.Name) (ext : String) : System.FilePath

Equations

• BlueprintGen.libraryToRelPath library ext = (System.mkFilePath ["library", library.toString false]).addExtension ext

def BlueprintGen.NodePart.toLatex {m : Type → Type} [Monad m] [Lean.MonadOptions m] (part : NodePart) (title : Option String) (additionalContent : String) : m Latex

Equations

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

def BlueprintGen.NodeWithPos.toLatex {m : Type → Type} [Monad m] [Lean.MonadOptions m] (node : NodeWithPos) : m Latex

Equations

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

def BlueprintGen.NodeWithPos.toLatexHeader {m : Type → Type} [Monad m] [Lean.MonadOptions m] (node : NodeWithPos) : m Latex

Equations

• node.toLatexHeader = do let latex ← node.toLatex pure ("\\newleannode{" ++ node.name.toString ++ "}{" ++ latex ++ "}")

def BlueprintGen.BlueprintContent.toLatex {m : Type → Type} [Monad m] [Lean.MonadOptions m] : BlueprintContent → m Latex

Equations

• (BlueprintGen.BlueprintContent.node n).toLatex = pure ("\\inputleannode{" ++ n.name.toString ++ "}")
• (BlueprintGen.BlueprintContent.modDoc d).toLatex = BlueprintGen.markdownToLatex d.doc

def BlueprintGen.latexPreamble {m : Type → Type} [Monad m] [Lean.MonadOptions m] : m Latex

Equations

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

def BlueprintGen.moduleToLatexHeader (module : Lean.Name) : Lean.CoreM Latex

Convert imported module to LaTeX.

Equations

• BlueprintGen.moduleToLatexHeader module = do let contents ← BlueprintGen.getBlueprintContents module BlueprintGen.moduleToLatexHeaderAux✝ module contents

def BlueprintGen.mainModuleToLatexHeader : Lean.CoreM Latex

Convert current module to LaTeX (for debugging).

Equations

• BlueprintGen.mainModuleToLatexHeader = do let contents ← BlueprintGen.getMainModuleBlueprintContents let __do_lift ← Lean.getMainModule BlueprintGen.moduleToLatexHeaderAux✝ __do_lift contents

def BlueprintGen.show_blueprint : Lean.ParserDescr

Shows the blueprint LaTeX of the current module for debugging.

Equations

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

def BlueprintGen.elabShowBlueprint : Lean.Elab.Command.CommandElab

Equations

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

def BlueprintGen.NodeWithPos.toJson (node : NodeWithPos) : Lean.Json

Equations

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

def BlueprintGen.BlueprintContent.toJson : BlueprintContent → Lean.Json

Equations

• (BlueprintGen.BlueprintContent.node n).toJson = Lean.Json.mkObj [("type", Lean.Json.str "node"), ("data", Lean.toJson n.toJson)]
• (BlueprintGen.BlueprintContent.modDoc d).toJson = Lean.Json.mkObj [("type", Lean.Json.str "moduleDoc"), ("data", Lean.toJson d.doc)]

def BlueprintGen.moduleToJson (module : Lean.Name) : Lean.CoreM Lean.Json

Equations

• BlueprintGen.moduleToJson module = do let __do_lift ← BlueprintGen.getBlueprintContents module pure (Lean.Json.arr (Array.map BlueprintGen.BlueprintContent.toJson __do_lift))

def BlueprintGen.mainModuleToJson : Lean.CoreM Lean.Json

Equations

• BlueprintGen.mainModuleToJson = do let __do_lift ← BlueprintGen.getMainModuleBlueprintContents pure (Lean.Json.arr (Array.map BlueprintGen.BlueprintContent.toJson __do_lift))

def BlueprintGen.show_blueprint_json : Lean.ParserDescr

Shows the blueprint JSON of the current module for debugging.

Equations

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

def BlueprintGen.elabShowBlueprintJson : Lean.Elab.Command.CommandElab

Equations

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

def BlueprintGen.outputResultsWithExt (basePath : System.FilePath) (module : Lean.Name) (content ext : String) : IO Unit

Write the result content to the appropriate blueprint file with extension ext ("tex" or "json").

Equations

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

def BlueprintGen.outputLatexResults (basePath : System.FilePath) (module : Lean.Name) (latex : Latex) : IO Unit

Write latex to the appropriate blueprint tex file.

Equations

• BlueprintGen.outputLatexResults basePath module latex = BlueprintGen.outputResultsWithExt basePath module latex "tex"

def BlueprintGen.outputJsonResults (basePath : System.FilePath) (module : Lean.Name) (json : Lean.Json) : IO Unit

Write json to the appropriate blueprint json file.

Equations

• BlueprintGen.outputJsonResults basePath module json = BlueprintGen.outputResultsWithExt basePath module json.pretty "json"

def BlueprintGen.outputLibraryLatex (basePath : System.FilePath) (library : Lean.Name) (modules : Array Lean.Name) : IO Unit

Write to an appropriate index tex file that \inputs all modules in a library.

Equations

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

def BlueprintGen.outputLibraryJson (basePath : System.FilePath) (library : Lean.Name) (modules : Array Lean.Name) : IO Unit

Write to an appropriate index json file containing paths to json files of all modules in a library.

Equations

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