diff --git a/DocGen4.lean b/DocGen4.lean
new file mode 100644
index 0000000..09a4641
--- /dev/null
+++ b/DocGen4.lean
@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.Process
+import DocGen4.Load
+import DocGen4.Output
+import DocGen4.LeanInk
diff --git a/DocGen4/LeanInk.lean b/DocGen4/LeanInk.lean
new file mode 100644
index 0000000..c4b326a
--- /dev/null
+++ b/DocGen4/LeanInk.lean
@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.LeanInk.Process
+import DocGen4.LeanInk.Output
diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean
new file mode 100644
index 0000000..ae23832
--- /dev/null
+++ b/DocGen4/LeanInk/Output.lean
@@ -0,0 +1,215 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving, Xubai Wang
+-/
+import DocGen4.Output.Base
+import DocGen4.Output.ToHtmlFormat
+import Lean.Data.Json
+import LeanInk.Annotation.Alectryon
+
+namespace LeanInk.Annotation.Alectryon
+
+open DocGen4 Output
+open scoped DocGen4.Jsx
+
+structure AlectryonContext where
+ counter : Nat
+
+abbrev AlectryonT := StateT AlectryonContext
+abbrev AlectryonM := AlectryonT HtmlM
+
+def getNextButtonLabel : AlectryonM String := do
+ let val ← get
+ let newCounter := val.counter + 1
+ set { val with counter := newCounter }
+ return s!"plain-lean4-lean-chk{val.counter}"
+
+def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do
+ pure
+
+
+def Token.processSemantic (t : Token) : Html :=
+ match t.semanticType with
+ | some "Name.Attribute" => {t.raw}
+ | some "Name.Variable" => {t.raw}
+ | some "Keyword" => {t.raw}
+ | _ => Html.text t.raw
+
+def Token.toHtml (t : Token) : AlectryonM Html := do
+ -- Right now t.link is always none from LeanInk, ignore it
+ -- TODO: render docstring
+ let mut parts := #[]
+ if let some tyi := t.typeinfo then
+ parts := parts.push <| ← tyi.toHtml
+
+ parts := parts.push t.processSemantic
+
+ pure
+ -- TODO: Show rest of token
+
+ [parts]
+
+
+def Contents.toHtml : Contents → AlectryonM Html
+ | .string value =>
+ pure
+
+ {value}
+
+ | .experimentalTokens values => do
+ let values ← values.mapM Token.toHtml
+ pure
+
+ [values]
+
+
+def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do
+ let mut hypParts := #[[h.names.intersperse ", " |>.map Html.text |>.toArray]]
+ if h.body.snd != "" then
+ hypParts := hypParts.push
+
+ :=
+ [← infoFormatToHtml h.body.fst]
+
+ hypParts := hypParts.push
+
+ :
+ [← infoFormatToHtml h.type.fst]
+
+
+ pure
+
+ [hypParts]
+
+
+def Goal.toHtml (g : Goal) : AlectryonM Html := do
+ let mut hypotheses := #[]
+ for hyp in g.hypotheses do
+ let rendered ← hyp.toHtml
+ hypotheses := hypotheses.push rendered
+ hypotheses := hypotheses.push
+ let conclusionHtml ←
+ match g.conclusion with
+ | .typed info _ => infoFormatToHtml info
+ | .untyped str => pure #[Html.text str]
+
+ pure
+
+
+ [hypotheses]
+
+
+ {g.name}
+
+
+ [conclusionHtml]
+
+
+
+def Message.toHtml (m : Message) : AlectryonM Html := do
+ pure
+
+ -- TODO: This might have to be done in a fancier way
+ {m.contents}
+
+
+def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
+ let messages :=
+ if s.messages.size > 0 then
+ #[
+
+ [← s.messages.mapM Message.toHtml]
+
+ ]
+ else
+ #[]
+
+ let goals :=
+ if s.goals.size > 0 then
+ -- TODO: Alectryon has a "alectryon-extra-goals" here, implement it
+ #[
+
+ [← s.goals.mapM Goal.toHtml]
+
+ ]
+ else
+ #[]
+
+ let buttonLabel ← getNextButtonLabel
+
+ pure
+
+
+
+
+ [messages]
+ [goals]
+
+
+
+def Text.toHtml (t : Text) : AlectryonM Html := t.contents.toHtml
+
+def Fragment.toHtml : Fragment → AlectryonM Html
+ | .text value => value.toHtml
+ | .sentence value => value.toHtml
+
+def baseHtml (content : Array Html) : AlectryonM Html := do
+ let banner :=
+
+ Built with doc-gen4, running Lean4.
+ Bubbles () indicate interactive fragments: hover for details, tap to reveal contents.
+ Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
+ On Mac, use Cmd instead of Ctrl.
+
+
+ pure
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ {banner}
+
+ [content]
+
+
+
+
+
+def annotationsToFragments (as : List Annotation.Annotation) : AnalysisM (List Fragment) := do
+ let config ← read
+ annotateFileWithCompounds [] config.inputFileContents as
+
+-- TODO: rework monad mess
+def renderAnnotations (as : List Annotation.Annotation) : HtmlT AnalysisM Html := do
+ let fs ← annotationsToFragments as
+ let (html, _) ← fs.mapM Fragment.toHtml >>= (baseHtml ∘ List.toArray) |>.run { counter := 0 }
+ return html
+
+end LeanInk.Annotation.Alectryon
diff --git a/DocGen4/LeanInk/Process.lean b/DocGen4/LeanInk/Process.lean
new file mode 100644
index 0000000..3a826f8
--- /dev/null
+++ b/DocGen4/LeanInk/Process.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+import LeanInk.Analysis
+import LeanInk.Annotation
+import DocGen4.LeanInk.Output
+import DocGen4.Output.Base
+
+namespace DocGen4.Process.LeanInk
+
+open Lean
+open DocGen4.Output
+
+def docGenOutput (as : List LeanInk.Annotation.Annotation) : HtmlT LeanInk.AnalysisM UInt32 := do
+ let some modName ← getCurrentName | unreachable!
+ let srcHtml ← LeanInk.Annotation.Alectryon.renderAnnotations as
+ let srcDir := moduleNameToDirectory srcBasePath modName
+ let srcPath := moduleNameToFile srcBasePath modName
+ IO.FS.createDirAll srcDir
+ IO.FS.writeFile srcPath srcHtml.toString
+ return 0
+
+def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do
+ let ctx ← readThe SiteContext
+ let baseCtx ← readThe SiteBaseContext
+ let outputFn := (docGenOutput · |>.run ctx baseCtx)
+ return ← LeanInk.Analysis.runAnalysis {
+ name := "doc-gen4"
+ genOutput := outputFn
+ }
+
+def execAux (config : LeanInk.Configuration) : HtmlT IO UInt32 := do
+ execAuxM.run (← readThe SiteContext) (← readThe SiteBaseContext) |>.run config
+
+@[implemented_by enableInitializersExecution]
+private def enableInitializersExecutionWrapper : IO Unit := return ()
+
+def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do
+ let contents ← IO.FS.readFile sourceFilePath
+ let config := {
+ inputFilePath := sourceFilePath
+ inputFileContents := contents
+ lakeFile := none
+ verbose := false
+ prettifyOutput := true
+ experimentalTypeInfo := true
+ experimentalDocString := true
+ experimentalSemanticType := true
+ }
+ enableInitializersExecutionWrapper
+ if (← execAux config) != 0 then
+ throw <| IO.userError s!"Analysis for \"{sourceFilePath}\" failed!"
+
+end DocGen4.Process.LeanInk
diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
new file mode 100644
index 0000000..fc2ef09
--- /dev/null
+++ b/DocGen4/Load.lean
@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+
+import Lean
+import Lake
+import Lake.CLI.Main
+import DocGen4.Process
+import Lean.Data.HashMap
+
+namespace DocGen4
+
+open Lean System IO
+/--
+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 : IO (Except UInt32 Lake.Workspace) := do
+ let (leanInstall?, lakeInstall?) ← Lake.findInstall?
+ let config := Lake.mkLoadConfig.{0} {leanInstall?, lakeInstall?}
+ match ←(EIO.toIO' config) with
+ | .ok config =>
+ let ws : Lake.Workspace ← Lake.loadWorkspace config
+ |>.run Lake.MonadLog.eio
+ |>.toIO (λ _ => IO.userError "Failed to load Lake workspace")
+ 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 (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy) := do
+ let env ← envOfImports task.getLoad
+ IO.println "Processing modules"
+ let config := {
+ -- TODO: parameterize maxHeartbeats
+ maxHeartbeats := 100000000,
+ options := ⟨[(`pp.tagAppFns, true)]⟩,
+ -- TODO: Figure out whether this could cause some bugs
+ fileName := default,
+ fileMap := default,
+ }
+
+ Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}
+
+def loadCore : IO (Process.AnalyzerResult × Hierarchy) := do
+ load <| .loadAll [`Init, `Lean]
+
+end DocGen4
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
new file mode 100644
index 0000000..f21c609
--- /dev/null
+++ b/DocGen4/Output.lean
@@ -0,0 +1,151 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+import Lake
+import DocGen4.Process
+import DocGen4.Output.Base
+import DocGen4.Output.Index
+import DocGen4.Output.Module
+import DocGen4.Output.NotFound
+import DocGen4.Output.Find
+import DocGen4.Output.SourceLinker
+import DocGen4.Output.Search
+import DocGen4.Output.ToJson
+import DocGen4.Output.FoundationalTypes
+import DocGen4.LeanInk.Process
+import Lean.Data.HashMap
+
+namespace DocGen4
+
+open Lean IO System Output Process
+
+def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
+ let findBasePath := basePath / "find"
+
+ -- Base structure
+ FS.createDirAll basePath
+ FS.createDirAll findBasePath
+ FS.createDirAll srcBasePath
+ FS.createDirAll declarationsBasePath
+
+ -- All the doc-gen static stuff
+ let indexHtml := ReaderT.run index config |>.toString
+ let notFoundHtml := ReaderT.run notFound config |>.toString
+ let foundationalTypesHtml := ReaderT.run foundationalTypes config |>.toString
+ let navbarHtml := ReaderT.run navbar config |>.toString
+ let searchHtml := ReaderT.run search config |>.toString
+ let docGenStatic := #[
+ ("style.css", styleCss),
+ ("declaration-data.js", declarationDataCenterJs),
+ ("nav.js", navJs),
+ ("how-about.js", howAboutJs),
+ ("search.html", searchHtml),
+ ("search.js", searchJs),
+ ("mathjax-config.js", mathjaxConfigJs),
+ ("instances.js", instancesJs),
+ ("importedBy.js", importedByJs),
+ ("index.html", indexHtml),
+ ("foundational_types.html", foundationalTypesHtml),
+ ("404.html", notFoundHtml),
+ ("navbar.html", navbarHtml)
+ ]
+ 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 htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT IO Unit := do
+ for (_, mod) in result.moduleInfo.toArray do
+ let jsonDecls ← Module.toJson mod
+ FS.writeFile (declarationsBasePath / s!"declaration-data-{mod.name}.bmp") (toJson jsonDecls).compress
+
+def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (ink : Bool) : IO Unit := do
+ let config : SiteContext := {
+ result := result,
+ sourceLinker := ← SourceLinker.sourceLinker ws
+ leanInkEnabled := ink
+ }
+
+ FS.createDirAll basePath
+ FS.createDirAll declarationsBasePath
+
+ -- 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
+
+ discard <| htmlOutputDeclarationDatas result |>.run config baseConfig
+
+ 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 baseConfig := { baseConfig with
+ depthToRoot := modName.components.dropLast.length
+ currentName := some modName
+ }
+ let moduleHtml := moduleToHtml module |>.run config baseConfig
+ FS.createDirAll fileDir
+ FS.writeFile filePath moduleHtml.toString
+ if ink then
+ if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" module.name then
+ 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 baseConfig := {baseConfig with depthToRoot := modName.components.length }
+ Process.LeanInk.runInk inputPath |>.run config baseConfig
+
+def getSimpleBaseContext (hierarchy : Hierarchy) : IO SiteBaseContext := do
+ return {
+ depthToRoot := 0,
+ currentName := none,
+ hierarchy
+ projectGithubUrl := ← SourceLinker.getProjectGithubUrl
+ projectCommit := ← SourceLinker.getProjectCommit
+ }
+
+def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
+ htmlOutputSetup baseConfig
+
+ let mut index : JsonIndex := { }
+ for entry in ←System.FilePath.readDir declarationsBasePath do
+ if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then
+ let fileContent ← FS.readFile entry.path
+ let .ok jsonContent := Json.parse fileContent | unreachable!
+ let .ok (module : JsonModule) := fromJson? jsonContent | unreachable!
+ index := index.addModule module |>.run baseConfig
+
+ let finalJson := toJson index
+ -- The root JSON for find
+ FS.writeFile (declarationsBasePath / "declaration-data.bmp") finalJson.compress
+
+/--
+The main entrypoint for outputting the documentation HTML based on an
+`AnalyzerResult`.
+-/
+def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (ink : Bool) : IO Unit := do
+ let baseConfig ← getSimpleBaseContext hierarchy
+ htmlOutputResults baseConfig result ws ink
+ htmlOutputIndex baseConfig
+
+end DocGen4
+
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
new file mode 100644
index 0000000..d02bf99
--- /dev/null
+++ b/DocGen4/Output/Base.lean
@@ -0,0 +1,277 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.Process
+import DocGen4.Output.ToHtmlFormat
+
+namespace DocGen4.Output
+
+open scoped DocGen4.Jsx
+open Lean System Widget Elab Process
+
+def basePath := FilePath.mk "." / "build" / "doc"
+def srcBasePath := basePath / "src"
+def declarationsBasePath := basePath / "declarations"
+
+/--
+The context used in the `BaseHtmlM` monad for HTML templating.
+-/
+structure SiteBaseContext where
+
+ /--
+ The module hierarchy as a tree structure.
+ -/
+ hierarchy : Hierarchy
+ /--
+ How far away we are from the page root, used for relative links to the root.
+ -/
+ depthToRoot: Nat
+ /--
+ The name of the current module if there is one, there exist a few
+ pages that don't have a module name.
+ -/
+ currentName : Option Name
+ /--
+ The Github URL of the project that we are building docs for.
+ -/
+ projectGithubUrl : String
+ /--
+ The commit of the project that we are building docs for.
+ -/
+ projectCommit : String
+
+/--
+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.
+ -/
+ sourceLinker : Name → Option DeclarationRange → String
+ /--
+ Whether LeanInk is enabled
+ -/
+ leanInkEnabled : Bool
+
+def setCurrentName (name : Name) (ctx : SiteBaseContext) := {ctx with currentName := some name}
+
+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
+
+instance [Monad m] : MonadLift HtmlM (HtmlT m) where
+ monadLift x := do return x.run (← readThe SiteContext) (← readThe SiteBaseContext)
+
+instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where
+ monadLift x := do return x.run (← readThe SiteBaseContext)
+
+/--
+Obtains the root URL as a relative one to the current depth.
+-/
+def getRoot : BaseHtmlM String := do
+ let rec go: Nat -> String
+ | 0 => "./"
+ | Nat.succ n' => "../" ++ go n'
+ let d <- SiteBaseContext.depthToRoot <$> read
+ return (go d)
+
+def getHierarchy : BaseHtmlM Hierarchy := do return (← read).hierarchy
+def getCurrentName : BaseHtmlM (Option Name) := do return (← read).currentName
+def getResult : HtmlM AnalyzerResult := do return (← read).result
+def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do return (← read).sourceLinker module range
+def leanInkEnabled? : HtmlM Bool := do return (← read).leanInkEnabled
+def getProjectGithubUrl : BaseHtmlM String := do return (← read).projectGithubUrl
+def getProjectCommit : BaseHtmlM String := do return (← read).projectCommit
+
+/--
+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 {α β} {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) : BaseHtmlM String := do
+ let parts := n.components.map Name.toString
+ return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+
+/--
+Returns the HTML doc-gen4 link to a module name.
+-/
+def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do
+ return {module.toString}
+
+/--
+Returns the LeanInk link to a module name.
+-/
+def moduleNameToInkLink (n : Name) : BaseHtmlM String := do
+ let parts := "src" :: n.components.map Name.toString
+ return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+
+/--
+Returns the path to the HTML file that contains information about a module.
+-/
+def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
+ let parts := n.components.map Name.toString
+ FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"
+
+/--
+Returns the directory of the HTML file that contains information about a module.
+-/
+def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
+ let parts := n.components.dropLast.map Name.toString
+ basePath / parts.foldl (· / ·) (FilePath.mk ".")
+
+section Static
+/-!
+The following section contains all the statically included files that
+are used in documentation generation, notably JS and CSS ones.
+-/
+ def styleCss : String := include_str "../../static/style.css"
+ def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
+ def navJs : String := include_str "../../static/nav.js"
+ def howAboutJs : String := include_str "../../static/how-about.js"
+ def searchJs : String := include_str "../../static/search.js"
+ def instancesJs : String := include_str "../../static/instances.js"
+ def importedByJs : String := include_str "../../static/importedBy.js"
+ def findJs : String := include_str "../../static/find/find.js"
+ def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"
+
+ def alectryonCss : String := include_str "../../static/alectryon/alectryon.css"
+ def alectryonJs : String := include_str "../../static/alectryon/alectryon.js"
+ def docUtilsCss : String := include_str "../../static/alectryon/docutils_basic.css"
+ def pygmentsCss : String := include_str "../../static/alectryon/pygments.css"
+end Static
+
+/--
+Returns the doc-gen4 link to a declaration name.
+-/
+def declNameToLink (name : Name) : HtmlM String := do
+ let res ← getResult
+ let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
+ return (← moduleNameToLink module) ++ "#" ++ name.toString
+
+/--
+Returns the HTML doc-gen4 link to a declaration name.
+-/
+def declNameToHtmlLink (name : Name) : HtmlM Html := do
+ return {name.toString}
+
+/--
+Returns the LeanInk link to a declaration name.
+-/
+def declNameToInkLink (name : Name) : HtmlM String := do
+ let res ← getResult
+ let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
+ return (← moduleNameToInkLink module) ++ "#" ++ name.toString
+
+/--
+Returns a name splitted into parts.
+Together with "break_within" CSS class this helps browser to break a name
+nicely.
+-/
+def breakWithin (name: String) : (Array Html) :=
+ name.splitOn "."
+ |> .map (fun (s: String) => {s})
+ |> .intersperse "."
+ |> List.toArray
+
+/--
+Returns the HTML doc-gen4 link to a declaration name with "break_within"
+set as class.
+-/
+def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do
+ return
+ [breakWithin name.toString]
+
+
+/--
+In Lean syntax declarations the following pattern is quite common:
+```
+syntax term " + " term : term
+```
+that is, we place spaces around the operator in the middle. When the
+`InfoTree` framework provides us with information about what source token
+corresponds to which identifier it will thus say that `" + "` corresponds to
+`HAdd.hadd`. This is however not the way we want this to be linked, in the HTML
+only `+` should be linked, taking care of this is what this function is
+responsible for.
+-/
+def splitWhitespaces (s : String) : (String × String × String) := Id.run do
+ let front := "".pushn ' ' <| s.offsetOfPos (s.find (!Char.isWhitespace ·))
+ let mut s := s.trimLeft
+ let back := "".pushn ' ' (s.length - s.offsetOfPos (s.find Char.isWhitespace))
+ s := s.trimRight
+ (front, s, back)
+
+/--
+Turns a `CodeWithInfos` object, that is basically a Lean syntax tree with
+information about what the identifiers mean, into an HTML object that links
+to as much information as possible.
+-/
+partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
+ match i with
+ | .text t => return #[Html.escape t]
+ | .append tt => tt.foldlM (fun acc t => do return acc ++ (← infoFormatToHtml t)) #[]
+ | .tag a t =>
+ match a.info.val.info with
+ | Info.ofTermInfo i =>
+ let cleanExpr := i.expr.consumeMData
+ match cleanExpr with
+ | .const name _ =>
+ -- TODO: this is some very primitive blacklisting but real Blacklisting needs MetaM
+ -- find a better solution
+ if (← getResult).name2ModIdx.contains name then
+ match t with
+ | .text t =>
+ let (front, t, back) := splitWhitespaces <| Html.escape t
+ let elem := {t}
+ return #[Html.text front, elem, Html.text back]
+ | _ =>
+ return #[[← infoFormatToHtml t]]
+ else
+ return #[[← infoFormatToHtml t]]
+ | .sort _ =>
+ match t with
+ | .text t =>
+ let mut sortPrefix :: rest := t.splitOn " " | unreachable!
+ let sortLink := {sortPrefix}
+ if rest != [] then
+ rest := " " :: rest
+ return #[sortLink, Html.text <| String.join rest]
+ | _ =>
+ return #[[← infoFormatToHtml t]]
+ | _ =>
+ return #[[← infoFormatToHtml t]]
+ | _ => return #[[← infoFormatToHtml t]]
+
+def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do
+ return #[
+ ,
+ ,
+ ,
+ ,
+ ,
+
+ ]
+
+end DocGen4.Output
diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean
new file mode 100644
index 0000000..521afc3
--- /dev/null
+++ b/DocGen4/Output/Class.lean
@@ -0,0 +1,22 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Structure
+import DocGen4.Process
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean
+
+def classInstancesToHtml (className : Name) : HtmlM Html := do
+ pure
+
+ Instances
+
+
+
+def classToHtml (i : Process.ClassInfo) : HtmlM (Array Html) := do
+ structureToHtml i
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/ClassInductive.lean b/DocGen4/Output/ClassInductive.lean
new file mode 100644
index 0000000..746b005
--- /dev/null
+++ b/DocGen4/Output/ClassInductive.lean
@@ -0,0 +1,14 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Class
+import DocGen4.Output.Inductive
+import DocGen4.Process
+
+
+namespace DocGen4
+namespace Output
+
+def classInductiveToHtml (i : Process.ClassInductiveInfo) : HtmlM (Array Html) := do
+ inductiveToHtml i
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean
new file mode 100644
index 0000000..c468ceb
--- /dev/null
+++ b/DocGen4/Output/Definition.lean
@@ -0,0 +1,51 @@
+import DocGen4.Output.Template
+import DocGen4.Output.DocString
+import DocGen4.Process
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean Widget
+
+/-- This is basically an arbitrary number that seems to work okay. -/
+def equationLimit : Nat := 200
+
+def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
+ return
[← infoFormatToHtml c]
+
+/--
+Attempt to render all `simp` equations for this definition. At a size
+defined in `equationLimit` we stop trying since they:
+- are too ugly to read most of the time
+- take too long
+-/
+def equationsToHtml (i : Process.DefinitionInfo) : HtmlM (Array Html) := do
+ if let some eqs := i.equations then
+ let equationsHtml ← eqs.mapM equationToHtml
+ let filteredEquationsHtml := equationsHtml.filter (·.textLength < equationLimit)
+ if equationsHtml.size ≠ filteredEquationsHtml.size then
+ return #[
+
+ Equations
+
+
One or more equations did not get rendered due to their size.
+ [filteredEquationsHtml]
+
+
+ ]
+ else
+ return #[
+
+ Equations
+
+ [filteredEquationsHtml]
+
+
+ ]
+ else
+ return #[]
+
+end Output
+end DocGen4
+
diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
new file mode 100644
index 0000000..ef75d76
--- /dev/null
+++ b/DocGen4/Output/DocString.lean
@@ -0,0 +1,216 @@
+import CMark
+import DocGen4.Output.Template
+import Lean.Data.Parsec
+import UnicodeBasic
+
+open Lean Xml Parser Parsec DocGen4.Process
+
+namespace DocGen4
+namespace Output
+
+/-- Auxiliary function for `splitAround`. -/
+@[specialize] partial def splitAroundAux (s : String) (p : Char → Bool) (b i : String.Pos) (r : List String) : List String :=
+ if s.atEnd i then
+ let r := (s.extract b i)::r
+ r.reverse
+ else
+ let c := s.get i
+ if p c then
+ let i := s.next i
+ splitAroundAux s p i i (c.toString::s.extract b (i-⟨1⟩)::r)
+ else
+ splitAroundAux s p b (s.next i) r
+
+/--
+ Similar to `Stirng.split` in Lean core, but keeps the separater.
+ e.g. `splitAround "a,b,c" (fun c => c = ',') = ["a", ",", "b", ",", "c"]`
+-/
+def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux s p 0 0 []
+
+instance : Inhabited Element := ⟨"", Lean.RBMap.empty, #[]⟩
+
+/-- Parse an array of Xml/Html document from String. -/
+def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof
+
+/--
+ Generate id for heading elements, with the following rules:
+
+ 1. Characters in `letter`, `mark`, `number` and `symbol` unicode categories are preserved.
+ 2. Any sequences of Characters in `punctuation`, `separator` and `other` categories are replaced by a single dash.
+ 3. Cases (upper and lower) are preserved.
+ 4. Xml/Html tags are ignored.
+-/
+partial def xmlGetHeadingId (el : Xml.Element) : String :=
+ elementToPlainText el |> replaceCharSeq unicodeToDrop "-"
+ where
+ elementToPlainText el := match el with
+ | (Element.Element _ _ contents) =>
+ "".intercalate (contents.toList.map contentToPlainText)
+ contentToPlainText c := match c with
+ | Content.Element el => elementToPlainText el
+ | Content.Comment _ => ""
+ | Content.Character s => s
+ replaceCharSeq pattern replacement s :=
+ s.split pattern
+ |>.filter (!·.isEmpty)
+ |> replacement.intercalate
+ unicodeToDrop (c : Char) : Bool :=
+ let cats := [
+ Unicode.GeneralCategory.P, -- punctuation
+ Unicode.GeneralCategory.Z, -- separator
+ Unicode.GeneralCategory.C -- other
+ ]
+ cats.any (Unicode.isInGeneralCategory c)
+
+/--
+ This function try to find the given name, both globally and in current module.
+
+ For global search, a precise name is need. If the global search fails, the function
+ tries to find a local one that ends with the given search name.
+-/
+def nameToLink? (s : String) : HtmlM (Option String) := do
+ let res ← getResult
+ if let some name := Lean.Syntax.decodeNameLit ("`" ++ s) then
+ -- with exactly the same name
+ if res.name2ModIdx.contains name then
+ declNameToLink name
+ -- module name
+ else if res.moduleNames.contains name then
+ moduleNameToLink name
+ -- find similar name in the same module
+ else
+ match (← getCurrentName) with
+ | some currentName =>
+ match res.moduleInfo.find! currentName |>.members |> filterDocInfo |>.find? (sameEnd ·.getName name) with
+ | some info =>
+ declNameToLink info.getName
+ | _ => return none
+ | _ => return none
+ else
+ return none
+ where
+ -- check if two names have the same ending components
+ sameEnd n1 n2 :=
+ List.zip n1.componentsRev n2.componentsRev
+ |>.all fun ⟨a, b⟩ => a == b
+
+/--
+ Extend links with following rules:
+
+ 1. if the link starts with `##`, a name search is used and will panic if not found
+ 2. if the link starts with `#`, it's treated as id link, no modification
+ 3. if the link starts with `http`, it's an absolute one, no modification
+ 4. otherwise it's a relative link, extend it with base url
+-/
+def extendLink (s : String) : HtmlM String := do
+ -- for intra doc links
+ if s.startsWith "##" then
+ if let some link ← nameToLink? (s.drop 2) then
+ return link
+ else
+ panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported"
+ -- for id
+ else if s.startsWith "#" then
+ return s
+ -- for absolute and relative urls
+ else if s.startsWith "http" then
+ return s
+ else return ((← getRoot) ++ s)
+
+/-- Add attributes for heading. -/
+def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Element) : HtmlM Element := do
+ match el with
+ | Element.Element name attrs contents => do
+ let id := xmlGetHeadingId el
+ let anchorAttributes := Lean.RBMap.empty
+ |>.insert "class" "hover-link"
+ |>.insert "href" s!"#{id}"
+ let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"]
+ let newAttrs := attrs
+ |>.insert "id" id
+ |>.insert "class" "markdown-heading"
+ let newContents := (←
+ contents.mapM (fun c => match c with
+ | Content.Element e => return Content.Element (← modifyElement e)
+ | _ => pure c))
+ |>.push (Content.Character " ")
+ |>.push (Content.Element anchor)
+ return ⟨ name, newAttrs, newContents⟩
+
+/-- Extend anchor links. -/
+def extendAnchor (el : Element) : HtmlM Element := do
+ match el with
+ | Element.Element name attrs contents =>
+ let newAttrs ← match attrs.find? "href" with
+ | some href => pure (attrs.insert "href" (← extendLink href))
+ | none => pure attrs
+ return ⟨ name, newAttrs, contents⟩
+
+/-- Automatically add intra documentation link for inline code span. -/
+def autoLink (el : Element) : HtmlM Element := do
+ match el with
+ | Element.Element name attrs contents =>
+ let mut newContents := #[]
+ for c in contents do
+ match c with
+ | Content.Character s =>
+ newContents := newContents ++ (← splitAround s unicodeToSplit |>.mapM linkify).join
+ | _ => newContents := newContents.push c
+ return ⟨ name, attrs, newContents ⟩
+ where
+ linkify s := do
+ let link? ← nameToLink? s
+ match link? with
+ | some link =>
+ let attributes := Lean.RBMap.empty.insert "href" link
+ return [Content.Element <| Element.Element "a" attributes #[Content.Character s]]
+ | none =>
+ let sHead := s.dropRightWhile (· != '.')
+ let sTail := s.takeRightWhile (· != '.')
+ let link'? ← nameToLink? sTail
+ match link'? with
+ | some link' =>
+ let attributes := Lean.RBMap.empty.insert "href" link'
+ return [
+ Content.Character sHead,
+ Content.Element <| Element.Element "a" attributes #[Content.Character sTail]
+ ]
+ | none =>
+ return [Content.Character s]
+ unicodeToSplit (c : Char) : Bool :=
+ let cats := [
+ Unicode.GeneralCategory.Z, -- separator
+ Unicode.GeneralCategory.C -- other
+ ]
+ cats.any (Unicode.isInGeneralCategory c)
+
+/-- Core function of modifying the cmark rendered docstring html. -/
+partial def modifyElement (element : Element) : HtmlM Element :=
+ match element with
+ | el@(Element.Element name attrs contents) => do
+ -- add id and class to
+ if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then
+ addHeadingAttributes el modifyElement
+ -- extend relative href for
+ else if name = "a" then
+ extendAnchor el
+ -- auto link for inline
+ else if name = "code" then
+ autoLink el
+ -- recursively modify
+ else
+ let newContents ← contents.mapM fun c => match c with
+ | Content.Element e => return Content.Element (← modifyElement e)
+ | _ => pure c
+ return ⟨ name, attrs, newContents ⟩
+
+/-- Convert docstring to Html. -/
+def docStringToHtml (s : String) : HtmlM (Array Html) := do
+ let rendered := CMark.renderHtml s
+ match manyDocument rendered.mkIterator with
+ | Parsec.ParseResult.success _ res =>
+ res.mapM fun x => do return Html.text <| toString (← modifyElement x)
+ | _ => return #[Html.text rendered]
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Find.lean b/DocGen4/Output/Find.lean
new file mode 100644
index 0000000..aa81f15
--- /dev/null
+++ b/DocGen4/Output/Find.lean
@@ -0,0 +1,22 @@
+import DocGen4.Output.Template
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean
+
+def find : BaseHtmlM Html := do
+ pure
+
+
+
+
+
+
+
+
+
+end Output
+end DocGen4
+
diff --git a/DocGen4/Output/FoundationalTypes.lean b/DocGen4/Output/FoundationalTypes.lean
new file mode 100644
index 0000000..2297570
--- /dev/null
+++ b/DocGen4/Output/FoundationalTypes.lean
@@ -0,0 +1,51 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Inductive
+
+namespace DocGen4.Output
+
+open scoped DocGen4.Jsx
+
+def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundational Types") do
+ pure <|
+
+
+
Foundational Types
+
+
Some of Lean's types are not defined in any Lean source files (even the prelude) since they come from its foundational type theory. This page provides basic documentation for these types.
+
For a more in-depth explanation of Lean's type theory, refer to
+ TPiL.
+
+
+
Sort u
+
Sort u is the type of types in Lean, and Sort u : Sort (u + 1).
+ {← instancesForToHtml `_builtin_sortu}
+
+
Type u
+
Type u is notation for Sort (u + 1).
+ {← instancesForToHtml `_builtin_typeu}
+
+
Prop
+
Prop is notation for Sort 0.
+ {← instancesForToHtml `_builtin_prop}
+
+
Pi types, {"(a : α) → β a"}
+
The type of dependent functions is known as a pi type.
+ Non-dependent functions and implications are a special case.
+
Note that these can also be written with the alternative notations:
+
+
∀ a : α, β a, conventionally used where β a : Prop.
+
(a : α) → β a
+
α → γ, possible only if β a = γ for all a.
+
+
Lean also permits ASCII-only spellings of the three variants:
+
+
forall a : A, B a for {"∀ a : α, β a"}
+
(a : A) -> B a, for (a : α) → β a
+
A -> B, for α → β
+
+
Note that despite not itself being a function, (→) is available as infix notation for
+ {"fun α β, α → β"}.
+ -- TODO: instances for pi types
+
+
+end DocGen4.Output
diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean
new file mode 100644
index 0000000..afa4eb5
--- /dev/null
+++ b/DocGen4/Output/Index.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.Output.Template
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
+ pure <|
+
+
+
+
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
new file mode 100644
index 0000000..0afeaf6
--- /dev/null
+++ b/DocGen4/Output/Inductive.lean
@@ -0,0 +1,39 @@
+import DocGen4.Output.Template
+import DocGen4.Output.DocString
+import DocGen4.Process
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean
+
+def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
+ pure
+
+ Instances For
+
+
+
+def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
+ let shortName := c.name.componentsRev.head!.toString
+ let name := c.name.toString
+ if let some doc := c.doc then
+ let renderedDoc ← docStringToHtml doc
+ pure
+
+
[renderedDoc]
+ {shortName} : [← infoFormatToHtml c.type]
+
+ else
+ pure
+
+ {shortName} : [← infoFormatToHtml c.type]
+
+
+def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do
+ let constructorsHtml :=
[← i.ctors.toArray.mapM ctorToHtml]
+ return #[constructorsHtml]
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Instance.lean b/DocGen4/Output/Instance.lean
new file mode 100644
index 0000000..78f098d
--- /dev/null
+++ b/DocGen4/Output/Instance.lean
@@ -0,0 +1,8 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Definition
+
+namespace DocGen4
+namespace Output
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
new file mode 100644
index 0000000..dd673e5
--- /dev/null
+++ b/DocGen4/Output/Module.lean
@@ -0,0 +1,216 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.Output.Template
+import DocGen4.Output.Inductive
+import DocGen4.Output.Structure
+import DocGen4.Output.Class
+import DocGen4.Output.Definition
+import DocGen4.Output.Instance
+import DocGen4.Output.ClassInductive
+import DocGen4.Output.DocString
+import DocGen4.Process
+import Lean.Data.Xml.Parser
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean Process
+
+/--
+Render an `Arg` as HTML, adding opacity effects etc. depending on what
+type of binder it has.
+-/
+def argToHtml (arg : Arg) : HtmlM Html := do
+ let (l, r, implicit) := match arg.binderInfo with
+ | BinderInfo.default => ("(", ")", false)
+ | BinderInfo.implicit => ("{", "}", true)
+ | BinderInfo.strictImplicit => ("⦃", "⦄", true)
+ | BinderInfo.instImplicit => ("[", "]", true)
+ let mut nodes := #[Html.text s!"{l}{arg.name.toString} : "]
+ nodes := nodes.append (← infoFormatToHtml arg.type)
+ nodes := nodes.push r
+ let inner := [nodes]
+ let html := Html.element "span" false #[("class", "decl_args")] #[inner]
+ if implicit then
+ return {html}
+ else
+ return html
+
+/--
+Render the structures this structure extends from as HTML so it can be
+added to the top level.
+-/
+def structureInfoHeader (s : Process.StructureInfo) : HtmlM (Array Html) := do
+ let mut nodes := #[]
+ if s.parents.size > 0 then
+ nodes := nodes.push extends
+ let mut parents := #[]
+ for parent in s.parents do
+ let link ← declNameToHtmlBreakWithinLink parent
+ let inner := {link}
+ let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
+ parents := parents.push html
+ nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray
+ return nodes
+
+/--
+Render the general header of a declaration containing its declaration type
+and name.
+-/
+def docInfoHeader (doc : DocInfo) : HtmlM Html := do
+ let mut nodes := #[]
+ nodes := nodes.push <| Html.element "span" false #[("class", "decl_kind")] #[doc.getKindDescription]
+ nodes := nodes.push
+
+ {← declNameToHtmlBreakWithinLink doc.getName}
+
+ for arg in doc.getArgs do
+ nodes := nodes.push (← argToHtml arg)
+
+ match doc with
+ | DocInfo.structureInfo i => nodes := nodes.append (← structureInfoHeader i)
+ | DocInfo.classInfo i => nodes := nodes.append (← structureInfoHeader i)
+ | _ => nodes := nodes
+
+ nodes := nodes.push <| Html.element "span" true #[("class", "decl_args")] #[" :"]
+ nodes := nodes.push
[← infoFormatToHtml doc.getType]
+ return
[nodes]
+
+/--
+The main entry point for rendering a single declaration inside a given module.
+-/
+def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
+ -- basic info like headers, types, structure fields, etc.
+ let docInfoHtml ← match doc with
+ | DocInfo.inductiveInfo i => inductiveToHtml i
+ | DocInfo.structureInfo i => structureToHtml i
+ | DocInfo.classInfo i => classToHtml i
+ | DocInfo.classInductiveInfo i => classInductiveToHtml i
+ | _ => pure #[]
+ -- rendered doc stirng
+ let docStringHtml ← match doc.getDocString with
+ | some s => docStringToHtml s
+ | none => pure #[]
+ -- extra information like equations and instances
+ let extraInfoHtml ← match doc with
+ | DocInfo.classInfo i => pure #[← classInstancesToHtml i.name]
+ | DocInfo.definitionInfo i => equationsToHtml i
+ | DocInfo.instanceInfo i => equationsToHtml i.toDefinitionInfo
+ | DocInfo.classInductiveInfo i => pure #[← classInstancesToHtml i.name]
+ | DocInfo.inductiveInfo i => pure #[← instancesForToHtml i.name]
+ | DocInfo.structureInfo i => pure #[← instancesForToHtml i.name]
+ | _ => pure #[]
+ let attrs := doc.getAttrs
+ let attrsHtml :=
+ if attrs.size > 0 then
+ let attrStr := "@[" ++ String.intercalate ", " doc.getAttrs.toList ++ "]"
+ #[Html.element "div" false #[("class", "attributes")] #[attrStr]]
+ else
+ #[]
+ let leanInkHtml :=
+ if ← leanInkEnabled? then
+ #[
+
+
+/--
+Rendering a module doc string, that is the ones with an ! after the opener
+as HTML.
+-/
+def modDocToHtml (mdoc : ModuleDoc) : HtmlM Html := do
+ pure
+
+ [← docStringToHtml mdoc.doc]
+
+
+/--
+Render a module member, that is either a module doc string or a declaration
+as HTML.
+-/
+def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := do
+ match member with
+ | ModuleMember.docInfo d => docInfoToHtml module d
+ | ModuleMember.modDoc d => modDocToHtml d
+
+def declarationToNavLink (module : Name) : Html :=
+
+
+/--
+Returns the list of all imports this module does.
+-/
+def getImports (module : Name) : HtmlM (Array Name) := do
+ let res ← getResult
+ return res.moduleInfo.find! module |>.imports
+
+/--
+Sort the list of all modules this one is importing, linkify it
+and return the HTML.
+-/
+def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
+ let imports := (← getImports moduleName).qsort Name.lt
+ imports.mapM (fun i => do return
{← moduleToHtmlLink i}
)
+
+/--
+Render the internal nav bar (the thing on the right on all module pages).
+-/
+def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
+ pure
+
+
+/--
+The main entry point to rendering the HTML for an entire module.
+-/
+def moduleToHtml (module : Process.Module) : HtmlM Html := withTheReader SiteBaseContext (setCurrentName module.name) do
+ let relevantMembers := module.members.filter Process.ModuleMember.shouldRender
+ let memberDocs ← relevantMembers.mapM (moduleMemberToHtml module.name)
+ let memberNames := filterDocInfo relevantMembers |>.map DocInfo.getName
+ templateLiftExtends (baseHtmlGenerator module.name.toString) <| pure #[
+ ← internalNav memberNames module.name,
+ Html.element "main" false #[] memberDocs
+ ]
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
new file mode 100644
index 0000000..4280864
--- /dev/null
+++ b/DocGen4/Output/Navbar.lean
@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.Output.Base
+
+namespace DocGen4
+namespace Output
+
+open Lean
+open scoped DocGen4.Jsx
+
+def moduleListFile (file : Name) : BaseHtmlM Html := do
+ return
+
+/--
+Build the HTML tree representing the module hierarchy.
+-/
+partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do
+ let children := Array.mk (h.getChildren.toList.map Prod.snd)
+ let dirs := children.filter (fun c => c.getChildren.toList.length != 0)
+ let files := children.filter (fun c => Hierarchy.isFile c && c.getChildren.toList.length = 0)
+ |>.map Hierarchy.getName
+ let dirNodes ← dirs.mapM moduleListDir
+ let fileNodes ← files.mapM moduleListFile
+ let moduleLink ← moduleNameToLink h.getName
+ let summary :=
+ if h.isFile then
+ {s!"{h.getName.getString!} ({file})"}
+ else
+ {h.getName.getString!}
+
+ pure
+
+ {summary}
+ [dirNodes]
+ [fileNodes]
+
+
+/--
+Return a list of top level modules, linkified and rendered as HTML
+-/
+def moduleList : BaseHtmlM Html := do
+ let hierarchy ← getHierarchy
+ let mut list := Array.empty
+ for (_, cs) in hierarchy.getChildren do
+ list := list.push <| ← moduleListDir cs
+ return
[list]
+
+/--
+The main entry point to rendering the navbar on the left hand side.
+-/
+def navbar : BaseHtmlM Html := do
+ pure
+
+
+ [← baseHtmlHeadDeclarations]
+
+
+
+
+
+
+
+
+
+
+
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/NotFound.lean b/DocGen4/Output/NotFound.lean
new file mode 100644
index 0000000..976ba06
--- /dev/null
+++ b/DocGen4/Output/NotFound.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.Output.Template
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+/--
+Render the 404 page.
+-/
+def notFound : BaseHtmlM Html := do templateExtends (baseHtml "404") <|
+ pure <|
+
+
404 Not Found
+
Unfortunately, the page you were looking for is no longer here.
+
+
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Search.lean b/DocGen4/Output/Search.lean
new file mode 100644
index 0000000..8fdbff6
--- /dev/null
+++ b/DocGen4/Output/Search.lean
@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2023 Jeremy Salwen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Salwen
+-/
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.Output.Template
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+def search : BaseHtmlM Html := do templateExtends (baseHtml "Search") <|
+ pure <|
+
+
+
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean
new file mode 100644
index 0000000..a8ef27d
--- /dev/null
+++ b/DocGen4/Output/SourceLinker.lean
@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+import Lake.Load
+
+namespace DocGen4.Output.SourceLinker
+
+open Lean
+
+/--
+Turns a Github git remote URL into an HTTPS Github URL.
+Three link types from git supported:
+- https://github.com/org/repo
+- https://github.com/org/repo.git
+- git@github.com:org/repo.git
+
+TODO: This function is quite brittle and very Github specific, we can
+probably do better.
+-/
+def getGithubBaseUrl (gitUrl : String) : String := Id.run do
+ let mut url := gitUrl
+ if url.startsWith "git@" then
+ url := url.drop 15
+ url := url.dropRight 4
+ return s!"https://github.com/{url}"
+ else if url.endsWith ".git" then
+ return url.dropRight 4
+ else
+ return url
+
+/--
+Obtain the Github URL of a project by parsing the origin remote.
+-/
+def getProjectGithubUrl (directory : System.FilePath := "." ) : IO String := do
+ let out ← IO.Process.output {
+ cmd := "git",
+ args := #["remote", "get-url", "origin"],
+ cwd := directory
+ }
+ if out.exitCode != 0 then
+ throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
+ return out.stdout.trimRight
+
+/--
+Obtain the git commit hash of the project that is currently getting analyzed.
+-/
+def getProjectCommit (directory : System.FilePath := "." ) : IO String := do
+ let out ← IO.Process.output {
+ cmd := "git",
+ args := #["rev-parse", "HEAD"]
+ cwd := directory
+ }
+ if out.exitCode != 0 then
+ throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
+ return out.stdout.trimRight
+
+/--
+Given a lake workspace with all the dependencies as well as the hash of the
+compiler release to work with this provides a function to turn names of
+declarations into (optionally positional) Github URLs.
+-/
+def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange → String) := do
+ let leanHash := ws.lakeEnv.lean.githash
+ -- Compute a map from package names to source URL
+ let mut gitMap := Lean.mkHashMap
+ let projectBaseUrl := getGithubBaseUrl (← getProjectGithubUrl)
+ let projectCommit ← getProjectCommit
+ gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit)
+ let manifest ← Lake.Manifest.loadOrEmpty ws.root.manifestFile
+ |>.run (Lake.MonadLog.eio .normal)
+ |>.toIO (fun _ => IO.userError "Failed to load lake manifest")
+ for pkg in manifest.entryArray do
+ match pkg with
+ | .git _ url rev .. => gitMap := gitMap.insert pkg.name (getGithubBaseUrl url, rev)
+ | .path _ path =>
+ let pkgBaseUrl := getGithubBaseUrl (← getProjectGithubUrl path)
+ let pkgCommit ← getProjectCommit path
+ gitMap := gitMap.insert pkg.name (pkgBaseUrl, pkgCommit)
+
+ return fun module range =>
+ let parts := module.components.map Name.toString
+ let path := (parts.intersperse "/").foldl (· ++ ·) ""
+ let root := module.getRoot
+ let basic := if root == `Lean ∨ root == `Init then
+ s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
+ else
+ match ws.packageArray.find? (·.isLocalModule module) with
+ | some pkg =>
+ match gitMap.find? pkg.name with
+ | some (baseUrl, commit) => s!"{baseUrl}/blob/{commit}/{path}.lean"
+ | none => "https://example.com"
+ | none => "https://example.com"
+
+ match range with
+ | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
+ | none => basic
+
+end DocGen4.Output.SourceLinker
diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean
new file mode 100644
index 0000000..f4ab138
--- /dev/null
+++ b/DocGen4/Output/Structure.lean
@@ -0,0 +1,51 @@
+import DocGen4.Output.Template
+import DocGen4.Output.DocString
+import DocGen4.Process
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean
+
+/--
+Render a single field consisting of its documentation, its name and its type as HTML.
+-/
+def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do
+ let shortName := f.name.componentsRev.head!.toString
+ let name := f.name.toString
+ if let some doc := f.doc then
+ let renderedDoc ← docStringToHtml doc
+ pure
+
+
[renderedDoc]
+
{s!"{shortName} "} : [← infoFormatToHtml f.type]
+
+ else
+ pure
+
+
{s!"{shortName} "} : [← infoFormatToHtml f.type]
+
+
+/--
+Render all information about a structure as HTML.
+-/
+def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do
+ let structureHtml :=
+ if Name.isSuffixOf `mk i.ctor.name then
+ (
+ [← i.fieldInfo.mapM fieldToHtml]
+
)
+ else
+ let ctorShortName := i.ctor.name.componentsRev.head!.toString
+ (
+
{s!"{ctorShortName} "} :: (
+
+ [← i.fieldInfo.mapM fieldToHtml]
+
+
)
+
)
+ return #[structureHtml]
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
new file mode 100644
index 0000000..192fb4b
--- /dev/null
+++ b/DocGen4/Output/Template.lean
@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.Output.Navbar
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+/--
+The HTML template used for all pages.
+-/
+def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do
+ let moduleConstant :=
+ if let some module := ← getCurrentName then
+ #[]
+ else
+ #[]
+ pure
+
+
+ [← baseHtmlHeadDeclarations]
+
+ {title}
+
+
+
+
+
+ [moduleConstant]
+
+
+
+
+
+
+
+
+
+
+
+