From 25b1ddb66ba5d2174b7dca64021341175be2365b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 21 Jul 2022 01:40:04 +0200 Subject: [PATCH 1/6] feat: Preparations to split doc-gen build process --- DocGen4/LeanInk/Output.lean | 5 +- DocGen4/Load.lean | 4 +- DocGen4/Output.lean | 117 +++++++++++++++++++-------------- DocGen4/Output/Base.lean | 49 ++++++++++---- DocGen4/Output/Find.lean | 4 +- DocGen4/Output/Index.lean | 2 +- DocGen4/Output/Module.lean | 4 +- DocGen4/Output/Navbar.lean | 14 ++-- DocGen4/Output/NotFound.lean | 2 +- DocGen4/Output/Semantic.lean | 59 ----------------- DocGen4/Output/Template.lean | 4 +- DocGen4/Process/Analyze.lean | 50 +++++++++----- DocGen4/Process/Hierarchy.lean | 5 +- Main.lean | 62 ++++++++++++----- static/declaration-data.js | 48 +++++++------- 15 files changed, 233 insertions(+), 196 deletions(-) delete mode 100644 DocGen4/Output/Semantic.lean diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean index 720c4cf..b534744 100644 --- a/DocGen4/LeanInk/Output.lean +++ b/DocGen4/LeanInk/Output.lean @@ -208,14 +208,15 @@ open Lean open LeanInk.Annotation.Alectryon open scoped DocGen4.Jsx -def moduleToHtml (module : Process.Module) (inkPath : System.FilePath) (sourceFilePath : System.FilePath) : HtmlT IO Html := withReader (setCurrentName module.name) do +def moduleToHtml (module : Process.Module) (inkPath : System.FilePath) (sourceFilePath : System.FilePath) : HtmlT IO Html := withTheReader SiteBaseContext (setCurrentName module.name) do let json ← runInk inkPath sourceFilePath let fragments := fromJson? json match fragments with | .ok fragments => let render := StateT.run (LeanInk.Annotation.Alectryon.renderFragments fragments) { counter := 0 } let ctx ← read - let (html, _) := ReaderT.run render ctx + let baseCtx ← readThe SiteBaseContext + let (html, _) := render |>.run ctx baseCtx pure html | .error err => throw $ IO.userError s!"Error while parsing LeanInk Output: {err}" diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 2c62eeb..7a45ec1 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -38,7 +38,7 @@ def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × Str Load a list of modules from the current Lean search path into an `Environment` to process for documentation. -/ -def load (imports : List Name) : IO Process.AnalyzerResult := do +def load (imports : List Name) (transitiveModules : Bool) : IO (Process.AnalyzerResult × Hierarchy) := do let env ← importModules (List.map (Import.mk · false) imports) Options.empty IO.println "Processing modules" let config := { @@ -49,6 +49,6 @@ def load (imports : List Name) : IO Process.AnalyzerResult := do fileName := default, fileMap := default, } - Prod.fst <$> Meta.MetaM.toIO Process.process config { env := env} {} {} + Prod.fst <$> Meta.MetaM.toIO (Process.process imports transitiveModules) config { env := env } {} {} end DocGen4 diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index fe24651..4c34a67 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -11,86 +11,91 @@ import DocGen4.Output.Index import DocGen4.Output.Module import DocGen4.Output.NotFound import DocGen4.Output.Find -import DocGen4.Output.Semantic import DocGen4.Output.SourceLinker import DocGen4.LeanInk.Output +import Std.Data.HashMap namespace DocGen4 -open Lean IO System Output Process +open Lean IO System Output Process Std -/-- -The main entrypoint for outputting the documentation HTML based on an -`AnalyzerResult`. --/ -def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) (inkPath : Option System.FilePath) : IO Unit := do - let config := { - depthToRoot := 0, - result := result, - currentName := none, - sourceLinker := ←sourceLinker ws leanHash - leanInkEnabled := inkPath.isSome - } +def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do let basePath := FilePath.mk "." / "build" / "doc" let srcBasePath := basePath / "src" - let indexHtml := ReaderT.run index config - let findHtml := ReaderT.run find { config with depthToRoot := 1 } - let notFoundHtml := ReaderT.run notFound config - -- Rendering the entire lean compiler takes time.... - --let sourceSearchPath := ((←Lean.findSysroot) / "src" / "lean") :: ws.root.srcDir :: ws.leanSrcPath - let sourceSearchPath := ws.root.srcDir :: ws.leanSrcPath + let declarationDataPath := basePath / "declaration-data.bmp" + -- Base structure FS.createDirAll basePath FS.createDirAll (basePath / "find") - FS.createDirAll (basePath / "semantic") FS.createDirAll srcBasePath - let mut declList := #[] - for (_, mod) in result.moduleInfo.toArray do - for decl in filterMapDocInfo mod.members do - let name := decl.getName.toString - let config := { config with depthToRoot := 0 } - let doc := decl.getDocString.getD "" - let root := Id.run <| ReaderT.run (getRoot) config - let link := root ++ s!"../semantic/{decl.getName.hash}.xml#" - let docLink := Id.run <| ReaderT.run (declNameToLink decl.getName) config - let sourceLink := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config - let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("docLink", docLink), ("sourceLink", sourceLink)] - declList := declList.push obj - let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config - FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml - let json := Json.arr declList - - FS.writeFile (basePath / "semantic" / "docgen4.xml") <| toString <| Id.run <| ReaderT.run schemaXml config - + -- The three HTML files we always need + let indexHtml := ReaderT.run index config FS.writeFile (basePath / "index.html") indexHtml.toString + + let notFoundHtml := ReaderT.run notFound config FS.writeFile (basePath / "404.html") notFoundHtml.toString + + let findHtml := ReaderT.run find { config with depthToRoot := 1 } FS.writeFile (basePath / "find" / "index.html") findHtml.toString + -- The root JSON for find + let topLevelModules := config.hierarchy.getChildren.toArray.map (Json.str ∘ toString ∘ Prod.fst) + FS.writeFile declarationDataPath (Json.arr topLevelModules).compress + + -- All the static stuff FS.writeFile (basePath / "style.css") styleCss - - let declarationDataPath := basePath / "declaration-data.bmp" - FS.writeFile declarationDataPath json.compress - FS.writeFile (basePath / "declaration-data.timestamp") <| toString (←declarationDataPath.metadata).modified.sec - FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs FS.writeFile (basePath / "nav.js") navJs FS.writeFile (basePath / "find" / "find.js") findJs FS.writeFile (basePath / "how-about.js") howAboutJs FS.writeFile (basePath / "search.js") searchJs FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs + + -- All the static stuff for LeanInk FS.writeFile (srcBasePath / "alectryon.css") alectryonCss FS.writeFile (srcBasePath / "alectryon.js") alectryonJs FS.writeFile (srcBasePath / "docutils_basic.css") docUtilsCss FS.writeFile (srcBasePath / "pygments.css") pygmentsCss + +def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) (inkPath : Option System.FilePath) : IO Unit := do + let config : SiteContext := { + result := result, + sourceLinker := ←sourceLinker ws leanHash + leanInkEnabled := inkPath.isSome + } + let basePath := FilePath.mk "." / "build" / "doc" + let srcBasePath := basePath / "src" + -- Rendering the entire lean compiler takes time.... + --let sourceSearchPath := ((←Lean.findSysroot) / "src" / "lean") :: ws.root.srcDir :: ws.leanSrcPath + let sourceSearchPath := ws.root.srcDir :: ws.leanSrcPath + + let mut declMap := HashMap.empty + for (_, mod) in result.moduleInfo.toArray do + let topLevelMod := mod.name.getRoot + let mut jsonDecls := #[] + for decl in filterMapDocInfo mod.members do + let name := decl.getName.toString + let doc := decl.getDocString.getD "" + let docLink := declNameToLink decl.getName |>.run config baseConfig + IO.println s!"DOC: {docLink}" + let sourceLink := getSourceUrl mod.name decl.getDeclarationRange |>.run config baseConfig + let json := Json.mkObj [("name", name), ("doc", doc), ("docLink", docLink), ("sourceLink", sourceLink)] + jsonDecls := jsonDecls.push json + let currentModDecls := declMap.findD topLevelMod #[] + declMap := declMap.insert topLevelMod (currentModDecls ++ jsonDecls) + + for (topLevelMod, decls) in declMap.toList do + FS.writeFile (basePath / s!"declaration-data-{topLevelMod}.bmp") (Json.arr decls).compress + for (modName, module) in result.moduleInfo.toArray do let fileDir := moduleNameToDirectory basePath modName let filePath := moduleNameToFile basePath modName -- path: 'basePath/module/components/till/last.html' -- The last component is the file name, so we drop it from the depth to root. - let config := { config with depthToRoot := modName.components.dropLast.length } - let moduleHtml := ReaderT.run (moduleToHtml module) config + let baseConfig := { baseConfig with depthToRoot := modName.components.dropLast.length } + let moduleHtml := moduleToHtml module |>.run config baseConfig FS.createDirAll $ fileDir FS.writeFile filePath moduleHtml.toString if let some inkPath := inkPath then @@ -98,12 +103,28 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String IO.println s!"Inking: {modName.toString}" -- path: 'basePath/src/module/components/till/last.html' -- The last component is the file name, however we are in src/ here so dont drop it this time - let config := { config with depthToRoot := modName.components.length } - let srcHtml ← ReaderT.run (LeanInk.moduleToHtml module inkPath inputPath) config + let baseConfig := { baseConfig with depthToRoot := modName.components.length } + let srcHtml ← LeanInk.moduleToHtml module inkPath inputPath |>.run config baseConfig let srcDir := moduleNameToDirectory srcBasePath modName let srcPath := moduleNameToFile srcBasePath modName FS.createDirAll srcDir FS.writeFile srcPath srcHtml.toString +def getSimpleBaseContext (hierarchy : Hierarchy) : SiteBaseContext := + { + depthToRoot := 0, + currentName := none, + hierarchy + } + +/-- +The main entrypoint for outputting the documentation HTML based on an +`AnalyzerResult`. +-/ +def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (leanHash: String) (inkPath : Option System.FilePath) : IO Unit := do + let baseConfig := getSimpleBaseContext hierarchy + htmlOutputSetup baseConfig + htmlOutputResults baseConfig result ws leanHash inkPath + end DocGen4 diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 25fc338..daf980d 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -13,13 +13,14 @@ open scoped DocGen4.Jsx open Lean System Widget Elab Process /-- -The context used in the `HtmlM` monad for HTML templating. +The context used in the `BaseHtmlM` monad for HTML templating. -/ -structure SiteContext where +structure SiteBaseContext where + /-- - The full analysis result from the Process module. + The module hierarchy as a tree structure. -/ - result : AnalyzerResult + hierarchy : Hierarchy /-- How far away we are from the page root, used for relative links to the root. -/ @@ -29,6 +30,15 @@ structure SiteContext where pages that don't have a module name. -/ currentName : Option Name + +/-- +The context used in the `HtmlM` monad for HTML templating. +-/ +structure SiteContext where + /-- + The full analysis result from the Process module. + -/ + result : AnalyzerResult /-- A function to link declaration names to their source URLs, usually Github ones. -/ @@ -38,50 +48,63 @@ structure SiteContext where -/ leanInkEnabled : Bool -def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name} +def setCurrentName (name : Name) (ctx : SiteBaseContext) := {ctx with currentName := some name} -abbrev HtmlT := ReaderT SiteContext +abbrev BaseHtmlT := ReaderT SiteBaseContext +abbrev BaseHtmlM := BaseHtmlT Id + +abbrev HtmlT (m) := ReaderT SiteContext (BaseHtmlT m) abbrev HtmlM := HtmlT Id +def HtmlT.run (x : HtmlT m α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : m α := + ReaderT.run x ctx |>.run baseCtx + +def HtmlM.run (x : HtmlM α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : α := + ReaderT.run x ctx |>.run baseCtx |>.run + /-- Obtains the root URL as a relative one to the current depth. -/ -def getRoot : HtmlM String := do +def getRoot : BaseHtmlM String := do let rec go: Nat -> String | 0 => "./" | Nat.succ n' => "../" ++ go n' - let d <- SiteContext.depthToRoot <$> read + let d <- SiteBaseContext.depthToRoot <$> read return (go d) +def getHierarchy : BaseHtmlM Hierarchy := do pure (←read).hierarchy +def getCurrentName : BaseHtmlM (Option Name) := do pure (←read).currentName def getResult : HtmlM AnalyzerResult := do pure (←read).result -def getCurrentName : HtmlM (Option Name) := do pure (←read).currentName def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure $ (←read).sourceLinker module range def leanInkEnabled? : HtmlM Bool := do pure (←read).leanInkEnabled /-- 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. -/ -def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := +def templateExtends {α β} {m} [Bind m] (base : α → m β) (new : m α) : m β := new >>= base +def templateLiftExtends {α β} {m n} [Bind m] [MonadLift n m] (base : α → n β) (new : m α) : m β := + new >>= (monadLift ∘ base) /-- Returns the doc-gen4 link to a module name. -/ -def moduleNameToLink (n : Name) : HtmlM String := do +def moduleNameToLink (n : Name) : BaseHtmlM String := do let parts := n.components.map Name.toString pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" /-- Returns the HTML doc-gen4 link to a module name. -/ -def moduleToHtmlLink (module : Name) : HtmlM Html := do +def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do pure {module.toString} /-- Returns the LeanInk link to a module name. -/ -def moduleNameToInkLink (n : Name) : HtmlM String := do +def moduleNameToInkLink (n : Name) : BaseHtmlM String := do let parts := "src" :: n.components.map Name.toString pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" diff --git a/DocGen4/Output/Find.lean b/DocGen4/Output/Find.lean index e63507a..a787ac4 100644 --- a/DocGen4/Output/Find.lean +++ b/DocGen4/Output/Find.lean @@ -6,13 +6,13 @@ namespace Output open scoped DocGen4.Jsx open Lean -def find : HtmlM Html := do +def find : BaseHtmlM Html := do pure - + diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean index d31ea3d..6132dc8 100644 --- a/DocGen4/Output/Index.lean +++ b/DocGen4/Output/Index.lean @@ -11,7 +11,7 @@ namespace Output open scoped DocGen4.Jsx -def index : HtmlM Html := do templateExtends (baseHtml "Index") $ pure $ +def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") $ pure $

Welcome to the documentation page

diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 86d8fba..efd6a31 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -233,10 +233,10 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do /-- The main entry point to rendering the HTML for an entire module. -/ -def moduleToHtml (module : Process.Module) : HtmlM Html := withReader (setCurrentName module.name) do +def moduleToHtml (module : Process.Module) : HtmlM Html := withTheReader SiteBaseContext (setCurrentName module.name) do let memberDocs ← module.members.mapM (λ i => moduleMemberToHtml module.name i) let memberNames := filterMapDocInfo module.members |>.map DocInfo.getName - templateExtends (baseHtmlGenerator module.name.toString) $ pure #[ + templateLiftExtends (baseHtmlGenerator module.name.toString) $ pure #[ ←internalNav memberNames module.name, Html.element "main" false #[] memberDocs ] diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 0c75103..bf70e34 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -13,7 +13,7 @@ namespace Output open Lean open scoped DocGen4.Jsx -def moduleListFile (file : Name) : HtmlM Html := do +def moduleListFile (file : Name) : BaseHtmlM Html := do pure
{←moduleToHtmlLink file}
@@ -21,7 +21,7 @@ def moduleListFile (file : Name) : HtmlM Html := do /-- Build the HTML tree representing the module hierarchy. -/ -partial def moduleListDir (h : Hierarchy) : HtmlM Html := do +partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do let children := Array.mk (h.getChildren.toList.map Prod.snd) let dirs := children.filter (λ c => c.getChildren.toList.length != 0) let files := children.filter (λ c => Hierarchy.isFile c ∧ c.getChildren.toList.length = 0) @@ -30,7 +30,7 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do let fileNodes ← (files.mapM moduleListFile) let moduleLink ← moduleNameToLink h.getName let summary := - if (←getResult).moduleInfo.contains h.getName then + if h.isFile then {←moduleToHtmlLink h.getName} else {h.getName.toString} @@ -45,17 +45,17 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do /-- Return a list of top level modules, linkified and rendered as HTML -/ -def moduleList : HtmlM Html := do - let hierarchy := (←getResult).hierarchy +def moduleList : BaseHtmlM Html := do + let hierarchy ← getHierarchy let mut list := Array.empty - for (n, cs) in hierarchy.getChildren do + for (_, cs) in hierarchy.getChildren do list := list.push $ ←moduleListDir cs pure
[list]
/-- The main entry point to rendering the navbar on the left hand side. -/ -def navbar : HtmlM Html := do +def navbar : BaseHtmlM Html := do pure