Loading the analysis result of a module.

def Architect.envOfImports (imports : Array Lean.Name) : IO Lean.Environment

This is copied from DocGen4.envOfImports.

Equations

• Architect.envOfImports imports = do Architect.envOfImports.unsafe_impl_2✝ Lean.importModules (Array.map (fun (x : Lean.Name) => { module := x }) imports) Lean.Options.empty 0 #[] true true

def Architect.runEnvOfImports {α : Type} (imports : Array Lean.Name) (options : Lean.Options) (x : Lean.CoreM α) : IO α

This is copied from DocGen4.load, except for separate handling of options.

Equations

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

def Architect.latexOutputOfImportModule (module : Lean.Name) (options : Lean.Options) : IO LatexOutput

Outputs the blueprint of a module.

Equations

• Architect.latexOutputOfImportModule module options = Architect.runEnvOfImports #[module] options (Architect.moduleToLatexOutput module)

def Architect.jsonOfImportModule (module : Lean.Name) (options : Lean.Options) : IO Lean.Json

Outputs the JSON data for the blueprint of a module.

Equations

• Architect.jsonOfImportModule module options = Architect.runEnvOfImports #[module] options (Architect.moduleToJson module)

def Architect.progressOfImportModules (modules : Array Lean.Name) (options : Lean.Options) (localOnly : Bool := false) : IO ProgressReport

Computes blueprint progress report across modules. If localOnly is true, only counts nodes defined in the given modules. Otherwise, also includes nodes from all their imports.

Equations

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

def Architect.statusOfImportModules (modules : Array Lean.Name) (constName : Lean.Name) (options : Lean.Options) : IO StatusReport

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

Equations

• Architect.statusOfImportModules modules constName options = Architect.runEnvOfImports modules options (Architect.computeStatus constName)

def Architect.incompleteOfImportModules (modules : Array Lean.Name) (options : Lean.Options) (localOnly : Bool := false) : IO IncompleteReport

Computes incomplete blueprint nodes across modules. If localOnly is true, only considers nodes defined in the given modules.

Equations

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

def Architect.impactOfImportModules (modules : Array Lean.Name) (constName : Lean.Name) (options : Lean.Options) (localOnly : Bool := false) : IO ImpactReport

Computes the impact of formalizing a specific blueprint node across modules. If localOnly is true, only considers nodes defined in the given modules.

Equations

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