Conversion from Lean nodes to LaTeX.

@[reducible, inline]

abbrev Architect.Latex : Type

Equations

• Architect.Latex = String

We convert nodes to LaTeX.

The output provides the following macros:

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

The structure of the output of a module A with nodes b and c is:

A.tex
A/b.tex
A/c.tex

The first is a header file that defines the macro \inputleannode{name}, which simply inputs A/name.tex. The rest are artifact files that contain the LaTeX of each node.

def Architect.Latex.input (file : System.FilePath) : Latex

Equations

• Architect.Latex.input file = "\\input{" ++ "/".intercalate file.components ++ "}"

def Architect.preprocessLatex (s : String) : String

Equations

• Architect.preprocessLatex s = s

structure Architect.InferredUses : Type

• uses : Array String
• leanOk : Bool

def Architect.InferredUses.empty : InferredUses

Equations

• Architect.InferredUses.empty = { uses := #[], leanOk := true }

def Architect.InferredUses.merge (inferredUsess : Array InferredUses) : InferredUses

Equations

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

def Architect.NodePart.inferUses {m : Type → Type} [Monad m] [Lean.MonadEnv m] (part : NodePart) (latexLabel : String) (used : Lean.NameSet) : m InferredUses

Equations

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

def Architect.Node.inferUses {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (node : Node) : m (InferredUses × InferredUses)

Infer the used constants of a node as (statement uses, proof uses).

Equations

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

def Architect.NodePart.toLatex {m : Type → Type} [Monad m] (part : NodePart) (allParts : Array NodePart := #[part]) (inferredUses : InferredUses) (title : Option String := none) (additionalContent defaultText : String := "") : m Latex

Merges and converts an array of NodePart to LaTeX. It is assumed that part ∈ allParts.

Equations

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

def Architect.NodeWithPos.toLatex {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (node : NodeWithPos) : m Latex

Equations

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

structure Architect.LatexArtifact : Type

LatexArtifact represents an auxiliary output file for a single node, containing its label (which is its filename) and content.

• id : String
• content : Latex

structure Architect.LatexOutput : Type

LatexOutput represents the extracted LaTeX from a module, consisting of a header file and auxiliary files.

• header : System.FilePath → Latex

  The header file requires the path to the artifacts directory.

• artifacts : Array LatexArtifact

def Architect.NodeWithPos.toLatexArtifact {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (node : NodeWithPos) : m LatexArtifact

Equations

• node.toLatexArtifact = do let __do_lift ← node.toLatex pure { id := node.latexLabel, content := __do_lift }

def Architect.BlueprintContent.toLatex {m : Type → Type} [Monad m] : BlueprintContent → m Latex

Equations

• (Architect.BlueprintContent.node n).toLatex = pure ("\\inputleannode{" ++ n.latexLabel ++ "}")
• (Architect.BlueprintContent.modDoc d).toLatex = pure d.doc

def Architect.latexPreamble {m : Type → Type} [Monad m] : m Latex

Equations

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

def Architect.moduleToLatexOutput (module : Lean.Name) : Lean.CoreM LatexOutput

Convert imported module to LaTeX (header file, artifact files).

Equations

• Architect.moduleToLatexOutput module = do let contents ← Architect.getBlueprintContents module Architect.moduleToLatexOutputAux✝ module contents

def Architect.mainModuleToLatexOutput : Lean.CoreM LatexOutput

Convert current module to LaTeX (header file, artifact files).

Equations

• Architect.mainModuleToLatexOutput = do let contents ← Architect.getMainModuleBlueprintContents let __do_lift ← Lean.getMainModule Architect.moduleToLatexOutputAux✝ __do_lift contents

def Architect.show_blueprint : Lean.ParserDescr

Shows the blueprint LaTeX of the current module (#show_blueprint) or a blueprint node (#show_blueprint lean_name or #show_blueprint "latex_label").

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Architect.mainModuleToJson : Lean.CoreM Lean.Json

Equations

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

def Architect.show_blueprint_json : Lean.ParserDescr

Shows the blueprint JSON of the current module (#show_blueprint_json) or a single Lean declaration (#show_blueprint_json name).

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Architect.outputLatexResults (basePath : System.FilePath) (module : Lean.Name) (latex : LatexOutput) : IO (Array System.FilePath)

Write latex to the appropriate blueprint tex file. Returns the list of paths to auxiliary output files (note: the returned paths are currently discarded).

Equations

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

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

Write json to the appropriate blueprint json file.

Equations

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

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