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..10f1c48 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -19,7 +19,7 @@ Sets up a lake workspace for the current project. Furthermore initialize the Lean search path with the path to the proper compiler from lean-toolchain as well as all the dependencies. -/ -def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × String)) := do +def lakeSetup (imports : List String) : IO (Except UInt32 Lake.Workspace) := do let (leanInstall?, lakeInstall?) ← Lake.findInstall? match ←(EIO.toIO' $ Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with | .ok config => @@ -30,16 +30,23 @@ def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × Str let ctx ← Lake.mkBuildContext ws (ws.root.buildImportsAndDeps imports *> pure ()) |>.run Lake.MonadLog.eio ctx initSearchPath (←findSysroot) ws.leanPaths.oleanPath - pure $ Except.ok (ws, libraryLeanGitHash) + pure $ Except.ok ws | .error err => throw $ IO.userError err.toString +def envOfImports (imports : List Name) : IO Environment := do + importModules (imports.map (Import.mk · false)) Options.empty + +def loadInit (imports : List Name) : IO Hierarchy := do + let env ← envOfImports imports + pure $ Hierarchy.fromArray env.header.moduleNames + /-- 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 - let env ← importModules (List.map (Import.mk · false) imports) Options.empty +def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy) := do + let env ← envOfImports task.getLoad IO.println "Processing modules" let config := { -- TODO: parameterize maxHeartbeats @@ -49,6 +56,7 @@ 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 task) config { env := env } {} {} end DocGen4 diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index fe24651..c690c04 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -11,86 +11,103 @@ 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, +def basePath := FilePath.mk "." / "build" / "doc" +def srcBasePath := basePath / "src" + +def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do + let findBasePath := basePath / "find" + + -- Base structure + FS.createDirAll basePath + FS.createDirAll (basePath / "find") + FS.createDirAll srcBasePath + + -- All the doc-gen static stuff + let indexHtml := ReaderT.run index config |>.toString + let notFoundHtml := ReaderT.run notFound config |>.toString + let docGenStatic := #[ + ("style.css", styleCss), + ("declaration-data.js", declarationDataCenterJs), + ("nav.js", navJs), + ("how-about.js", howAboutJs), + ("search.js", searchJs), + ("mathjax-config.js", mathjaxConfigJs), + ("index.html", indexHtml), + ("404.html", notFoundHtml) + ] + for (fileName, content) in docGenStatic do + FS.writeFile (basePath / fileName) content + + let findHtml := ReaderT.run find { config with depthToRoot := 1 } |>.toString + let findStatic := #[ + ("index.html", findHtml), + ("find.js", findJs) + ] + for (fileName, content) in findStatic do + FS.writeFile (findBasePath / fileName) content + + let alectryonStatic := #[ + ("alectryon.css", alectryonCss), + ("alectryon.js", alectryonJs), + ("docutils_basic.css", docUtilsCss), + ("pygments.css", pygmentsCss) + ] + + for (fileName, content) in alectryonStatic do + FS.writeFile (srcBasePath / fileName) content + +def DocInfo.toJson (module : Name) (info : DocInfo) : HtmlM Json := do + let name := info.getName.toString + let doc := info.getDocString.getD "" + let docLink ← declNameToLink info.getName + let sourceLink ← getSourceUrl module info.getDeclarationRange + pure $ Json.mkObj [("name", name), ("doc", doc), ("docLink", docLink), ("sourceLink", sourceLink)] + +def Process.Module.toJson (module : Module) : HtmlM (Array Json) := do + let mut jsonDecls := #[] + for decl in filterMapDocInfo module.members do + let json ← DocInfo.toJson module.name decl + jsonDecls := jsonDecls.push json + pure jsonDecls + +def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do + let config : SiteContext := { result := result, - currentName := none, - sourceLinker := ←sourceLinker ws leanHash + sourceLinker := ←sourceLinker ws leanInkEnabled := inkPath.isSome } - 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 + + FS.createDirAll basePath + -- 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 - FS.createDirAll basePath - FS.createDirAll (basePath / "find") - FS.createDirAll (basePath / "semantic") - FS.createDirAll srcBasePath - - let mut declList := #[] + let mut declMap := HashMap.empty 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 + let topLevelMod := mod.name.getRoot + let jsonDecls := Module.toJson mod |>.run config baseConfig + let currentModDecls := declMap.findD topLevelMod #[] + declMap := declMap.insert topLevelMod (currentModDecls ++ jsonDecls) - FS.writeFile (basePath / "semantic" / "docgen4.xml") <| toString <| Id.run <| ReaderT.run schemaXml config - - FS.writeFile (basePath / "index.html") indexHtml.toString - FS.writeFile (basePath / "404.html") notFoundHtml.toString - FS.writeFile (basePath / "find" / "index.html") findHtml.toString - - 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 - 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 + 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 +115,40 @@ 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 + } + +def htmlOutputFinalize (baseConfig : SiteBaseContext) : IO Unit := do + htmlOutputSetup baseConfig + + let mut topLevelModules := #[] + for entry in ←System.FilePath.readDir basePath do + if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then + let module := entry.fileName.drop "declaration-data-".length |>.dropRight ".bmp".length + topLevelModules := topLevelModules.push (Json.str module) + + -- The root JSON for find + FS.writeFile (basePath / "declaration-data.bmp") (Json.arr topLevelModules).compress + +/-- +The main entrypoint for outputting the documentation HTML based on an +`AnalyzerResult`. +-/ +def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do + let baseConfig := getSimpleBaseContext hierarchy + htmlOutputResults baseConfig result ws inkPath + htmlOutputFinalize baseConfig + 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