@[reducible, inline]

abbrev DocGen4.Process.MarkdownDocstring : Type

Represents a non-verso docstring; these will be rendered using Output.docStringToHtml.

Equations

• DocGen4.Process.MarkdownDocstring = String

inductive DocGen4.Process.ModuleMember : Type

Member of a module, either a declaration or some module doc string.

• docInfo (info : DocInfo) : ModuleMember
• modDoc (doc : Lean.ModuleDoc) : ModuleMember

@[implicit_reducible]

instance DocGen4.Process.instInhabitedModuleMember : Inhabited ModuleMember

Equations

• DocGen4.Process.instInhabitedModuleMember = { default := DocGen4.Process.instInhabitedModuleMember.default }

structure DocGen4.Process.TacticInfo (textType : Type) : Type

Information about a tactic declaration which will be rendered on the Tactics page.

This datastructure contains slightly different contents compared to a TacticDoc to make it easily serializable as JSON. It is designed to be easy to instantiate, using { tacticDoc with ... }.

• internalName : Lean.Name

  The name of the canonical parser for the tactic

• userName : String

  The user-facing name to display (typically the first keyword token)

• tags : Array Lean.Name

  The tags that have been applied to the tactic

• docString : textType

  The docstring for the tactic, including any extension docstrings.

• definingModule : Lean.Name

  Name of the module where the tactic is declared.

@[implicit_reducible]

instance DocGen4.Process.instFromJsonTacticInfo {textType✝ : Type} [Lean.FromJson textType✝] : Lean.FromJson (TacticInfo textType✝)

Equations

• DocGen4.Process.instFromJsonTacticInfo = { fromJson? := DocGen4.Process.instFromJsonTacticInfo.fromJson }

def DocGen4.Process.instFromJsonTacticInfo.fromJson {textType✝ : Type} [Lean.FromJson textType✝] : Lean.Json → Except String (TacticInfo textType✝)

Equations

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

def DocGen4.Process.instToJsonTacticInfo.toJson {textType✝ : Type} [Lean.ToJson textType✝] : TacticInfo textType✝ → Lean.Json

Equations

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

@[implicit_reducible]

instance DocGen4.Process.instToJsonTacticInfo {textType✝ : Type} [Lean.ToJson textType✝] : Lean.ToJson (TacticInfo textType✝)

Equations

• DocGen4.Process.instToJsonTacticInfo = { toJson := DocGen4.Process.instToJsonTacticInfo.toJson }

structure DocGen4.Process.Module : Type

A Lean module.

• name : Lean.Name

  Name of the module.

• members : Array ModuleMember

  All members of the module, sorted according to their line numbers.

• imports : Array Lean.Name
• tactics : Array (TacticInfo MarkdownDocstring)

  Tactics declared in this module.

@[implicit_reducible]

instance DocGen4.Process.instInhabitedModule : Inhabited Module

Equations

• DocGen4.Process.instInhabitedModule = { default := DocGen4.Process.instInhabitedModule.default }

structure DocGen4.Process.AnalyzerResult : Type

The result of running a full doc-gen analysis on a project.

• name2ModIdx : Std.HashMap Lean.Name Lean.ModuleIdx

  The map from module names to indices of the moduleNames array.

• moduleNames : Array Lean.Name

  The list of all modules, accessible nicely via name2ModIdx.

• moduleInfo : Std.HashMap Lean.Name Module

  A map from module names to information about these modules.

• containedNames : Std.HashMap Lean.Name (Std.HashSet Lean.Name)

  For each rendered declaration, the set of names whose declaration ranges are contained within it. Used to determine whether auto-generated projections should receive anchor IDs in the HTML output.

  This field is only populated when the result is read from the database. Prior to that, it is empty.

@[implicit_reducible]

instance DocGen4.Process.instInhabitedAnalyzerResult : Inhabited AnalyzerResult

Equations

• DocGen4.Process.instInhabitedAnalyzerResult = { default := DocGen4.Process.instInhabitedAnalyzerResult.default }

def DocGen4.Process.ModuleMember.getDeclarationRange : ModuleMember → Lean.DeclarationRange

Equations

• (DocGen4.Process.ModuleMember.docInfo i).getDeclarationRange = i.getDeclarationRange
• (DocGen4.Process.ModuleMember.modDoc i).getDeclarationRange = i.declarationRange

def DocGen4.Process.ModuleMember.order (l r : ModuleMember) : Bool

An order for module members, based on their declaration range.

Equations

• l.order r = l.getDeclarationRange.pos.lt r.getDeclarationRange.pos

def DocGen4.Process.ModuleMember.getName : ModuleMember → Lean.Name

Equations

• (DocGen4.Process.ModuleMember.docInfo i).getName = i.getName
• (DocGen4.Process.ModuleMember.modDoc i).getName = Lean.Name.anonymous

def DocGen4.Process.ModuleMember.getDocString : ModuleMember → Option (String ⊕ Lean.VersoDocString)

Equations

• (DocGen4.Process.ModuleMember.docInfo i).getDocString = i.getDocString
• (DocGen4.Process.ModuleMember.modDoc i).getDocString = some (Sum.inl i.doc)

def DocGen4.Process.ModuleMember.shouldRender : ModuleMember → Bool

Equations

• (DocGen4.Process.ModuleMember.docInfo i).shouldRender = i.shouldRender
• (DocGen4.Process.ModuleMember.modDoc i).shouldRender = true

inductive DocGen4.Process.AnalyzeTask : Type

• analyzePrefixModules (topLevel : Lean.Name) : AnalyzeTask
• analyzeConcreteModules (modules : Array Lean.Name) : AnalyzeTask

def DocGen4.Process.AnalyzeTask.getLoad (task : AnalyzeTask) : Array Lean.Name

Equations

• (DocGen4.Process.AnalyzeTask.analyzePrefixModules topLevel).getLoad = #[topLevel]
• (DocGen4.Process.AnalyzeTask.analyzeConcreteModules modules).getLoad = modules

def DocGen4.Process.collectTactics (module : Lean.Name) (env : Lean.Environment) : Lean.MetaM (Array (TacticInfo MarkdownDocstring))

Collect tactic info for pages to display in addition to the module docs.

Equations

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

def DocGen4.Process.getAllModuleDocs (relevantModules : Array Lean.Name) : Lean.MetaM (Std.HashMap Lean.Name Module)

Equations

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

def DocGen4.Process.mkOptions : IO DocGenOptions

Equations

• DocGen4.Process.mkOptions = do let __do_lift ← liftM (IO.getEnv "DISABLE_EQUATIONS") match __do_lift with | some "1" => pure { genEquations := false } | x => pure { }

def DocGen4.Process.process (task : AnalyzeTask) : Lean.MetaM AnalyzerResult

Run the doc-gen analysis on all modules that are loaded into the Environment of this MetaM run and mentioned by the AnalyzeTask.

Equations

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

def DocGen4.Process.filterDocInfo {α : Type} [Std.Iterator α Id ModuleMember] (ms : Std.Iter ModuleMember) : Std.Iter DocInfo

Equations

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