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] [Lean.MonadOptions 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] [Lean.MonadOptions 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.isMathlibOk {m : Type → Type} [Monad m] [Lean.MonadEnv m] (name : Lean.Name) : m Bool

Equations

• Architect.isMathlibOk name = do let __do_lift ← Lean.getEnv pure (Architect.isLibraryDecl __do_lift name)

def Architect.Node.isLeanOk {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (node : Node) : m Bool

Whether a node is sorry-free (both statement and proof have no sorryAx).

Equations

• node.isLeanOk = do let __discr ← node.inferUses match __discr with | (stmtUses, proofUses) => pure (stmtUses.leanOk && proofUses.leanOk)

structure Architect.ProgressStats : Type

Progress statistics for blueprint nodes.

• total : Nat
• sorryFree : Nat
• containsSorry : Nat
• notReady : Nat

@[implicit_reducible]

instance Architect.instToStringProgressStats : ToString ProgressStats

Equations

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

structure Architect.ProgressReport : Type

Progress report with aggregate stats and optional per-module breakdown.

• aggregate : ProgressStats
• byModule : Array (Lean.Name × ProgressStats)
• showByModule : Bool

@[implicit_reducible]

instance Architect.instToStringProgressReport : ToString ProgressReport

Equations

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

def Architect.ProgressStats.merge (a b : ProgressStats) : ProgressStats

Equations

• a.merge b = { total := a.total + b.total, sorryFree := a.sorryFree + b.sorryFree, containsSorry := a.containsSorry + b.containsSorry, notReady := a.notReady + b.notReady }

def Architect.ProgressStats.empty : ProgressStats

Equations

• Architect.ProgressStats.empty = { total := 0, sorryFree := 0, containsSorry := 0, notReady := 0 }

def Architect.computeProgress {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (nodes : Array Node) : m ProgressStats

Compute progress statistics for an array of blueprint nodes. Categories are mutually exclusive: a node is either formalized (sorry-free), incomplete (contains sorry), or not ready. These three sum to total.

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] [Lean.MonadOptions 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] [Lean.MonadOptions 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 Lean.Parser.Category.blueprintProgressOpt : Category

Shows blueprint progress statistics.

• #blueprint_progress shows project-wide statistics with per-module breakdown.
• #blueprint_progress nobreakdown shows project-wide statistics without breakdown.
• #blueprint_progress local shows current module statistics with per-module breakdown.
• #blueprint_progress local nobreakdown shows current module statistics without breakdown.

Equations

• Lean.Parser.Category.blueprintProgressOpt = { }

def Architect.blueprintProgressOpt.quot : Lean.ParserDescr

Equations

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

def Architect.blueprintProgressOptLocal : Lean.ParserDescr

Equations

• Architect.blueprintProgressOptLocal = Lean.ParserDescr.node `Architect.blueprintProgressOptLocal 1022 (Lean.ParserDescr.nonReservedSymbol "local" false)

def Architect.blueprintProgressOptNobreakdown : Lean.ParserDescr

Equations

• Architect.blueprintProgressOptNobreakdown = Lean.ParserDescr.node `Architect.blueprintProgressOptNobreakdown 1024 (Lean.ParserDescr.symbol "nobreakdown")

def Architect.blueprint_progress : Lean.ParserDescr

Equations

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

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

Equations

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

inductive Architect.NodeStatus : Type

Classification of a single blueprint node's formalization status.

• formalized : NodeStatus
• incomplete : NodeStatus
• notReady : NodeStatus

@[implicit_reducible]

instance Architect.instToStringNodeStatus : ToString NodeStatus

Equations

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

structure Architect.NodeEntry : Type

A blueprint node entry with status and dependency completion data. Used uniformly for blocking deps, reverse deps, unblocked nodes, and incomplete nodes.

• name : Lean.Name
• status : NodeStatus
• depDone : Nat
• depTotal : Nat
• module : Lean.Name

structure Architect.DepFracWidths : Type

Column widths for aligned dep-fraction formatting.

• dw : Nat
• tw : Nat
• pw : Nat

def Architect.DepFracWidths.compute (entries : Array NodeEntry) : DepFracWidths

Compute dep-fraction column widths from an array of NodeEntry.

Equations

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

def Architect.fmtDepFrac (done total : Nat) (w : DepFracWidths) : String

Format a dependency fraction with aligned / and % columns.

Equations

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

def Architect.fmtNodeEntryListMsg (entries : Array NodeEntry) (header : Lean.MessageData) : Lean.MessageData

Format a list of NodeEntry as aligned MessageData rows: name frac status (for interactive).

Equations

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

def Architect.classifyNode {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (node : Node) : m NodeStatus

Classify a single blueprint node as formalized, incomplete, or not ready.

Equations

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

structure Architect.StatusReport : Type

Status report for a specific blueprint node and its dependency subtree.

• name : Lean.Name
• selfStatus : NodeStatus
• depStats : ProgressStats
• blocking : Array NodeEntry

def Architect.formatStatusReport (r : StatusReport) : String

Equations

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

@[implicit_reducible]

instance Architect.instToStringStatusReport : ToString StatusReport

Equations

• Architect.instToStringStatusReport = { toString := Architect.formatStatusReport }

@[implicit_reducible]

instance Architect.instToMessageDataStatusReport : Lean.ToMessageData StatusReport

Equations

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

def Architect.computeStatus {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (name : Lean.Name) : m StatusReport

Compute the formalization status of a specific blueprint node and its dependency subtree.

Equations

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

def Architect.blueprint_status : Lean.ParserDescr

Shows formalization status of a specific blueprint node and its dependency subtree.

• #blueprint_status name shows the status of name and its transitive dependencies.

Equations

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

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

Equations

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

structure Architect.IncompleteReport : Type

Report listing all incomplete blueprint nodes.

• nodes : Array NodeEntry

@[implicit_reducible]

instance Architect.instToStringIncompleteReport : ToString IncompleteReport

Equations

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

@[implicit_reducible]

instance Architect.instToMessageDataIncompleteReport : Lean.ToMessageData IncompleteReport

Equations

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

def Architect.collectIncomplete {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (moduleNodes : Array (Lean.Name × Array Node)) : m IncompleteReport

Collect all incomplete blueprint nodes with their dependency completion fraction.

Equations

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

def Architect.blueprintIncompleteOpt.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.blueprintIncompleteOpt : Category

Shows incomplete blueprint nodes sorted by dependency completion.

• #blueprint_incomplete shows incomplete nodes across all modules.
• #blueprint_incomplete local shows incomplete nodes in the current module only.

Equations

• Lean.Parser.Category.blueprintIncompleteOpt = { }

def Architect.blueprintIncompleteOptLocal : Lean.ParserDescr

Equations

• Architect.blueprintIncompleteOptLocal = Lean.ParserDescr.node `Architect.blueprintIncompleteOptLocal 1022 (Lean.ParserDescr.nonReservedSymbol "local" false)

def Architect.blueprint_incomplete : Lean.ParserDescr

Equations

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

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

Equations

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

structure Architect.ImpactReport : Type

Impact report: reverse dependencies and nodes that would be unblocked.

• name : Lean.Name
• selfStatus : NodeStatus
• reverseDeps : Array NodeEntry
• wouldUnblock : Array NodeEntry

def Architect.formatImpactReport (r : ImpactReport) : String

Equations

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

@[implicit_reducible]

instance Architect.instToStringImpactReport : ToString ImpactReport

Equations

• Architect.instToStringImpactReport = { toString := Architect.formatImpactReport }

@[implicit_reducible]

instance Architect.instToMessageDataImpactReport : Lean.ToMessageData ImpactReport

Equations

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

def Architect.computeImpact {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (targetName : Lean.Name) (moduleNodes : Array (Lean.Name × Array Node)) : m ImpactReport

Compute the impact of formalizing a specific blueprint node: which nodes depend on it and which would become actionable.

Equations

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

def Lean.Parser.Category.blueprintImpactOpt : Category

Shows the impact of formalizing a specific blueprint node: which nodes depend on it and which would become actionable.

• #blueprint_impact name searches all imported modules.
• #blueprint_impact name local searches only the current module.

Equations

• Lean.Parser.Category.blueprintImpactOpt = { }

def Architect.blueprintImpactOpt.quot : Lean.ParserDescr

Equations

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

def Architect.blueprintImpactOptLocal : Lean.ParserDescr

Equations

• Architect.blueprintImpactOptLocal = Lean.ParserDescr.node `Architect.blueprintImpactOptLocal 1022 (Lean.ParserDescr.nonReservedSymbol "local" false)

def Architect.blueprint_impact : Lean.ParserDescr

Equations

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

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