def DocGen4.Output.basePathComponent : String

Equations

• DocGen4.Output.basePathComponent = "doc"

def DocGen4.Output.basePath (buildDir : System.FilePath) : System.FilePath

Equations

• DocGen4.Output.basePath buildDir = buildDir / { toString := DocGen4.Output.basePathComponent }

def DocGen4.Output.srcBasePath (buildDir : System.FilePath) : System.FilePath

Equations

• DocGen4.Output.srcBasePath buildDir = DocGen4.Output.basePath buildDir / { toString := "src" }

def DocGen4.Output.declarationsBasePath (buildDir : System.FilePath) : System.FilePath

Equations

• DocGen4.Output.declarationsBasePath buildDir = buildDir / { toString := "doc-data" }

structure DocGen4.Output.BibItem : Type

The structure representing a processed bibitem.

• citekey : String

  The cite key as in the bib file.

• tag : String

  The tag generated by bib processor, e.g. [Doe12]. Should be plain text and should not be escaped.

• html : String

  The HTML generated by bib processor, e.g. John Doe. <i>Test</i>. 2012.

• plaintext : String

  The plain text form of html field. Should not be escaped.

@[implicit_reducible]

instance DocGen4.Output.instFromJsonBibItem : Lean.FromJson BibItem

Equations

• DocGen4.Output.instFromJsonBibItem = { fromJson? := DocGen4.Output.instFromJsonBibItem.fromJson }

def DocGen4.Output.instFromJsonBibItem.fromJson : Lean.Json → Except String BibItem

Equations

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

@[implicit_reducible]

instance DocGen4.Output.instToJsonBibItem : Lean.ToJson BibItem

Equations

• DocGen4.Output.instToJsonBibItem = { toJson := DocGen4.Output.instToJsonBibItem.toJson }

def DocGen4.Output.instToJsonBibItem.toJson : BibItem → Lean.Json

Equations

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

structure DocGen4.Output.BackrefItem : Type

The structure representing a backref item.

• citekey : String

  The cite key as in the bib file.

• modName : Lean.Name

  The name of the module.

• funName : String

  The name of the function, as a string. It is empty if the backref is in modstring.

• index : Nat

  The index of the backref in that module, starting from zero.

@[implicit_reducible]

instance DocGen4.Output.instFromJsonBackrefItem : Lean.FromJson BackrefItem

Equations

• DocGen4.Output.instFromJsonBackrefItem = { fromJson? := DocGen4.Output.instFromJsonBackrefItem.fromJson }

def DocGen4.Output.instFromJsonBackrefItem.fromJson : Lean.Json → Except String BackrefItem

Equations

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

@[implicit_reducible]

instance DocGen4.Output.instToJsonBackrefItem : Lean.ToJson BackrefItem

Equations

• DocGen4.Output.instToJsonBackrefItem = { toJson := DocGen4.Output.instToJsonBackrefItem.toJson }

def DocGen4.Output.instToJsonBackrefItem.toJson : BackrefItem → Lean.Json

Equations

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

@[implicit_reducible]

instance DocGen4.Output.instInhabitedBackrefItem : Inhabited BackrefItem

Equations

• DocGen4.Output.instInhabitedBackrefItem = { default := DocGen4.Output.instInhabitedBackrefItem.default }

structure DocGen4.Output.SiteBaseContext : Type

The context used in the BaseHtmlM monad for HTML templating.

• buildDir : System.FilePath

  The build directory (provided by lake).

• hierarchy : Hierarchy

  The module hierarchy as a tree structure.

• depthToRoot : Nat

  How far away we are from the page root, used for relative links to the root.

• currentName : Option Lean.Name

  The name of the current module if there is one, there exist a few pages that don't have a module name.

• refs : Array BibItem

  The list of references, as an array.

@[reducible, inline]

abbrev DocGen4.Output.DeclarationDecoratorFn : Type

Declaration decorator function type: given a module name, declaration name, and declaration kind, returns optional extra HTML to inject into the declaration's rendering. This enables external tools to add badges, links, or other decorations to declarations.

Equations

• DocGen4.Output.DeclarationDecoratorFn = (Lean.Name → Lean.Name → String → Array DocGen4.Html)

def DocGen4.Output.defaultDeclarationDecorator : DeclarationDecoratorFn

The default declaration decorator that produces no extra HTML.

Equations

• DocGen4.Output.defaultDeclarationDecorator x✝² x✝¹ x✝ = #[]

structure DocGen4.Output.SiteContext : Type

The read-only context used in the HtmlM monad for HTML templating.

• result : Process.AnalyzerResult

  The full analysis result from the Process module.

• sourceLinker : Lean.Name → Option Lean.DeclarationRange → String

  A function to link declaration names to their source URLs, usually Github ones.

• refsMap : Std.HashMap String BibItem

  The references as a map.

• declarationDecorator : DeclarationDecoratorFn

  A function to decorate declarations with extra HTML (e.g., verification badges). Receives (moduleName, declarationName, declarationKind) and returns extra HTML. Defaults to producing no extra HTML.

structure DocGen4.Output.SiteState : Type

The writable state used in the HtmlM monad for HTML templating.

• backrefs : Array BackrefItem

  The list of back references, as an array.

• errors : String

  The errors occurred during the process.

def DocGen4.Output.setCurrentName (name : Lean.Name) (ctx : SiteBaseContext) : SiteBaseContext

Equations

• DocGen4.Output.setCurrentName name ctx = { buildDir := ctx.buildDir, hierarchy := ctx.hierarchy, depthToRoot := ctx.depthToRoot, currentName := some name, refs := ctx.refs }

@[reducible, inline]

abbrev DocGen4.Output.BaseHtmlT (m : Type → Type u_1) (α : Type) : Type u_1

Equations

• DocGen4.Output.BaseHtmlT = ReaderT DocGen4.Output.SiteBaseContext

@[reducible, inline]

abbrev DocGen4.Output.BaseHtmlM (α : Type) : Type

Equations

• DocGen4.Output.BaseHtmlM = DocGen4.Output.BaseHtmlT Id

@[reducible, inline]

abbrev DocGen4.Output.HtmlT (m : Type → Type u_1) (α : Type) : Type u_1

Equations

• DocGen4.Output.HtmlT m = StateT DocGen4.Output.SiteState (ReaderT DocGen4.Output.SiteContext (DocGen4.Output.BaseHtmlT m))

@[reducible, inline]

abbrev DocGen4.Output.HtmlM (α : Type) : Type

Equations

• DocGen4.Output.HtmlM = DocGen4.Output.HtmlT Id

def DocGen4.Output.HtmlT.run {m : Type → Type u_1} {α : Type} (x : HtmlT m α) (state : SiteState) (ctx : SiteContext) (baseCtx : SiteBaseContext) : m (α × SiteState)

Equations

• x.run state ctx baseCtx = ReaderT.run ((StateT.run x state).run ctx) baseCtx

def DocGen4.Output.HtmlM.run {α : Type} (x : HtmlM α) (state : SiteState) (ctx : SiteContext) (baseCtx : SiteBaseContext) : α × SiteState

Equations

• x.run state ctx baseCtx = (ReaderT.run ((StateT.run x state).run ctx) baseCtx).run

@[implicit_reducible]

instance DocGen4.Output.instMonadLiftHtmlMHtmlTOfMonad {m : Type → Type u_1} [Monad m] : MonadLift HtmlM (HtmlT m)

Equations

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

@[implicit_reducible]

instance DocGen4.Output.instMonadLiftBaseHtmlMBaseHtmlTOfMonad {m : Type → Type u_1} [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m)

Equations

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

def DocGen4.Output.addBackref (citekey funName : String) : HtmlM BackrefItem

Add a backref of the given citekey and funName to current document, and returns it.

Equations

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

def DocGen4.Output.addError (err : String) : HtmlM Unit

Add an error message to errors of current document.

Equations

• DocGen4.Output.addError err = modify fun (cfg : DocGen4.Output.SiteState) => { backrefs := cfg.backrefs, errors := cfg.errors ++ err ++ "\n" }

def DocGen4.Output.getRoot : BaseHtmlM String

Obtains the root URL as a relative one to the current depth.

Equations

• DocGen4.Output.getRoot = do let d ← DocGen4.Output.SiteBaseContext.depthToRoot <$> read pure (DocGen4.Output.getRoot.go d)

def DocGen4.Output.getRoot.go : Nat → String

Equations

• DocGen4.Output.getRoot.go 0 = "./"
• DocGen4.Output.getRoot.go n'.succ = "../" ++ DocGen4.Output.getRoot.go n'

def DocGen4.Output.getHierarchy : BaseHtmlM Hierarchy

Equations

• DocGen4.Output.getHierarchy = do let __do_lift ← read pure __do_lift.hierarchy

def DocGen4.Output.getCurrentName : BaseHtmlM (Option Lean.Name)

Equations

• DocGen4.Output.getCurrentName = do let __do_lift ← read pure __do_lift.currentName

def DocGen4.Output.getResult : HtmlM Process.AnalyzerResult

Equations

• DocGen4.Output.getResult = do let __do_lift ← read pure __do_lift.result

def DocGen4.Output.getSourceUrl (module : Lean.Name) (range : Option Lean.DeclarationRange) : HtmlM String

Equations

• DocGen4.Output.getSourceUrl module range = do let __do_lift ← read pure (__do_lift.sourceLinker module range)

def DocGen4.Output.getDeclarationDecorator : HtmlM DeclarationDecoratorFn

Equations

• DocGen4.Output.getDeclarationDecorator = do let __do_lift ← read pure __do_lift.declarationDecorator

def DocGen4.Output.templateExtends {α β : Type u_1} {m : Type u_1 → Type u_2} [Bind m] (base : α → m β) (new : m α) : m β

If a template is meant to be extended because it for example only provides the header but no real content this is the way to fill the template with content. This is untyped so HtmlM and BaseHtmlM can be mixed.

Equations

• DocGen4.Output.templateExtends base new = new >>= base

def DocGen4.Output.templateLiftExtends {α β : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Bind m] [MonadLiftT n m] (base : α → n β) (new : m α) : m β

Equations

• DocGen4.Output.templateLiftExtends base new = new >>= monadLift ∘ base

def DocGen4.Output.moduleNameToLink (n : Lean.Name) : BaseHtmlM String

Returns the doc-gen4 link to a module name.

If n is a locally-documented module (present in the site Hierarchy), the result is a relative path to that module's generated HTML. Otherwise — i.e. the module belongs to an external library that doc-gen4 did not analyze — the result is a link to the corresponding page on the external documentation site (see DocGen4.Output.External).

Equations

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

def DocGen4.Output.moduleToHtmlLink (module : Lean.Name) : BaseHtmlM Html

Returns the HTML doc-gen4 link to a module name.

Equations

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

def DocGen4.Output.moduleNameToFile (n : Lean.Name) : System.FilePath

Returns the path to the HTML file that contains information about a module.

Equations

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

The following section contains all the statically included files that are used in documentation generation, notably JS and CSS ones.

def DocGen4.Output.styleCss : String

Equations

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

def DocGen4.Output.faviconSvg : String

Equations

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

def DocGen4.Output.declarationDataCenterJs : String

Equations

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

def DocGen4.Output.colorSchemeJs : String

Equations

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

def DocGen4.Output.jumpSrcJs : String

Equations

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

def DocGen4.Output.navJs : String

Equations

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

def DocGen4.Output.expandNavJs : String

Equations

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

def DocGen4.Output.howAboutJs : String

Equations

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

def DocGen4.Output.searchJs : String

Equations

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

def DocGen4.Output.instancesJs : String

Equations

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

def DocGen4.Output.importedByJs : String

Equations

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

def DocGen4.Output.findJs : String

Equations

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

def DocGen4.Output.mathjaxConfigJs : String

Equations

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

def DocGen4.Output.declNameToLink (name : Lean.Name) : HtmlM String

Returns the doc-gen4 link to a declaration name.

Equations

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

def DocGen4.Output.declNameToHtmlLink (name : Lean.Name) : HtmlM Html

Returns the HTML doc-gen4 link to a declaration name.

Equations

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

def DocGen4.Output.breakWithin (name : String) : Array Html

Returns a name splitted into parts. Together with "break_within" CSS class this helps browser to break a name nicely.

Equations

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

def DocGen4.Output.declNameToHtmlBreakWithinLink (name : Lean.Name) : HtmlM Html

Returns the HTML doc-gen4 link to a declaration name with "break_within" set as class.

Equations

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

def DocGen4.Output.splitWhitespaces (s : String) : String × String × String

Equations

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

partial def DocGen4.Output.renderedCodeToHtmlAux (code : RenderedCode) : HtmlM (Bool × Array Html)

Converts RenderedCode to HTML with declaration links.

Returns (hasAnchor, html) where hasAnchor indicates if the result contains an <a> tag. This is tracked to avoid creating nested anchors (which is invalid HTML).

For .const name tags, it first checks whether the name is a valid link target (that is, a non-private name in name2ModIdx). If so, it links directly to that name. If not, it applies Lean.privateToUserName? to convert internal private names to user-facing names (e.g., _private.Init.Prelude.0.Foo.helper → Foo.helper) and then tries:

1. Auxiliary name removal (findLinkableParent): Strip trailing components that start with _ or are numeric (e.g., Foo.bar._proof_2 → Foo.bar). This handles auto-generated auxiliary names like match discriminant functions (Foo.bar.match_1 → Foo.bar).
2. Module link: For private names where no declaration was found, extract the module name from the private prefix and link to the module page (e.g., _private.Init.Prelude.0.Foo → module Init.Prelude). moduleNameToLink itself decides local-vs-external.
3. External fallback: Emit <a href={externalDeclLink nameToSearch}> — the external Mathlib find redirect resolves the owning module client-side. The user-facing name (post privateToUserName?) is used so private internal names are not leaked into the URL. See DocGen4.Output.External for the URL form, and docs/dev/design/external-linking.md for the rationale.

def DocGen4.Output.renderedCodeToHtmlAux.fn (html : Array Html) : Array Html

Equations

• DocGen4.Output.renderedCodeToHtmlAux.fn html = #[DocGen4.Html.element "span" true (#[].push ("class", "fn")) (#[] ++ html)]

def DocGen4.Output.renderedCodeToHtml (code : RenderedCode) : HtmlM (Array Html)

Convert RenderedCode to HTML with declaration links.

Equations

• DocGen4.Output.renderedCodeToHtml code = Prod.snd <$> DocGen4.Output.renderedCodeToHtmlAux code

def DocGen4.Output.infoFormatToHtml (i : Lean.Widget.CodeWithInfos) : HtmlM (Array Html)

Equations

• DocGen4.Output.infoFormatToHtml i = DocGen4.Output.renderedCodeToHtml (DocGen4.renderTagged i)

def DocGen4.Output.baseHtmlHeadDeclarations : BaseHtmlM (Array Html)

Equations

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