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