def DocGen4.collectBackrefs (buildDir : System.FilePath) : IO (Array Output.BackrefItem)

Equations

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

def DocGen4.htmlOutputSetup (config : Output.SiteBaseContext) (tacticInfo : Array (Process.TacticInfo Html)) : IO Unit

Equations

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

@[reducible, inline]

abbrev DocGen4.SourceLinkerFn : Type

Custom source linker type: given an optional source URL and module name, returns a function from declaration range to URL

Equations

• DocGen4.SourceLinkerFn = (Option String → Lean.Name → Option Lean.DeclarationRange → String)

def DocGen4.htmlOutputResultsParallel (baseConfig : Output.SiteBaseContext) (dbPath : System.FilePath) (linkCtx : DB.LinkingContext) (targetModules : Array Lean.Name := linkCtx.moduleNames) (sourceLinker? : Option SourceLinkerFn := none) (declarationDecorator? : Option Output.DeclarationDecoratorFn := none) : IO (Array System.FilePath × Array Output.JsonModule)

Generates HTML for all modules in parallel. Each task loads its module from DB, renders HTML, and writes output files. The linking context provides cross-module linking without loading all module data upfront. When targetModules is provided, only those modules are rendered (but linking uses all modules).

Equations

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

def DocGen4.getSimpleBaseContext (buildDir : System.FilePath) (hierarchy : Hierarchy) : IO Output.SiteBaseContext

Equations

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

def DocGen4.htmlOutputIndex (baseConfig : Output.SiteBaseContext) (modules : Array Output.JsonModule) (tacticInfo : Array (Process.TacticInfo Html)) : IO Unit

Equations

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

def DocGen4.headerDataOutput (buildDir : System.FilePath) : IO Unit

Equations

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

def DocGen4.htmlPathToModuleName (docDir htmlPath : System.FilePath) : Option Lean.Name

Converts an HTML file path to a module name: doc/A/B/C.html -> A.B.C.

Equations

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

def DocGen4.scanModuleHtmlFiles (docDir : System.FilePath) : IO (Array Lean.Name)

Scans for existing module HTML files under docDir.

Equations

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

partial def DocGen4.scanModuleHtmlFiles.scanDir (docDir : System.FilePath) (skipFiles skipDirs : List String) (dir : System.FilePath) : IO (Array Lean.Name)

def DocGen4.updateNavbarFromDisk (buildDir : System.FilePath) : IO Unit

Rebuilds navbar.html by scanning existing HTML files on disk. This enables incremental builds where subsequent builds include HTML modules from previous builds.

Equations

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