From 279df925558d8248f16a45f05c22cdb7de4daacd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 May 2022 20:36:35 +0200 Subject: [PATCH 01/19] refactor: restructure the modules --- DocGen4.lean | 3 --- DocGen4/Output/Base.lean | 2 +- DocGen4/Output/Index.lean | 2 +- DocGen4/Output/Navbar.lean | 2 +- DocGen4/Output/NotFound.lean | 2 +- DocGen4/Output/Template.lean | 2 +- DocGen4/{ => Output}/ToHtmlFormat.lean | 0 DocGen4/Process.lean | 4 ++-- DocGen4/{ => Process}/Attributes.lean | 0 DocGen4/{ => Process}/Hierarchy.lean | 0 10 files changed, 7 insertions(+), 10 deletions(-) rename DocGen4/{ => Output}/ToHtmlFormat.lean (100%) rename DocGen4/{ => Process}/Attributes.lean (100%) rename DocGen4/{ => Process}/Hierarchy.lean (100%) diff --git a/DocGen4.lean b/DocGen4.lean index e91e7c7..0ae1c74 100644 --- a/DocGen4.lean +++ b/DocGen4.lean @@ -3,10 +3,7 @@ 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.Hierarchy import DocGen4.Process import DocGen4.Load -import DocGen4.ToHtmlFormat import DocGen4.IncludeStr import DocGen4.Output -import DocGen4.Attributes diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 4aef3b9..66bb358 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -5,7 +5,7 @@ Authors: Henrik Böving -/ import DocGen4.Process import DocGen4.IncludeStr -import DocGen4.ToHtmlFormat +import DocGen4.Output.ToHtmlFormat namespace DocGen4 namespace Output diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean index e0342b6..d31ea3d 100644 --- a/DocGen4/Output/Index.lean +++ b/DocGen4/Output/Index.lean @@ -3,7 +3,7 @@ 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.ToHtmlFormat +import DocGen4.Output.ToHtmlFormat import DocGen4.Output.Template namespace DocGen4 diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 7d00102..c9cb196 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ import Lean -import DocGen4.ToHtmlFormat +import DocGen4.Output.ToHtmlFormat import DocGen4.Output.Base namespace DocGen4 diff --git a/DocGen4/Output/NotFound.lean b/DocGen4/Output/NotFound.lean index a700963..c5161c4 100644 --- a/DocGen4/Output/NotFound.lean +++ b/DocGen4/Output/NotFound.lean @@ -3,7 +3,7 @@ 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.ToHtmlFormat +import DocGen4.Output.ToHtmlFormat import DocGen4.Output.Template namespace DocGen4 diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index aed65c7..33d7c59 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -3,7 +3,7 @@ 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.ToHtmlFormat +import DocGen4.Output.ToHtmlFormat import DocGen4.Output.Navbar namespace DocGen4 diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/Output/ToHtmlFormat.lean similarity index 100% rename from DocGen4/ToHtmlFormat.lean rename to DocGen4/Output/ToHtmlFormat.lean diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index d815f96..3ce8d3b 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -9,8 +9,8 @@ import Lean.PrettyPrinter import Std.Data.HashMap import Lean.Meta.SynthInstance -import DocGen4.Hierarchy -import DocGen4.Attributes +import DocGen4.Process.Hierarchy +import DocGen4.Process.Attributes namespace DocGen4 diff --git a/DocGen4/Attributes.lean b/DocGen4/Process/Attributes.lean similarity index 100% rename from DocGen4/Attributes.lean rename to DocGen4/Process/Attributes.lean diff --git a/DocGen4/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean similarity index 100% rename from DocGen4/Hierarchy.lean rename to DocGen4/Process/Hierarchy.lean From 5fd076530e9d4bf7c0dbfadae91c71de65bdb512 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 May 2022 20:41:45 +0200 Subject: [PATCH 02/19] doc: IncludeStr --- DocGen4/IncludeStr.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/DocGen4/IncludeStr.lean b/DocGen4/IncludeStr.lean index afc3ceb..d9ac0f9 100644 --- a/DocGen4/IncludeStr.lean +++ b/DocGen4/IncludeStr.lean @@ -27,6 +27,11 @@ partial def traverseDir (f : FilePath) (p : FilePath → IO Bool) : IO (Option F syntax (name := includeStr) "include_str" str : term +/-- +Provides a way to include the contents of a file at compile time as a String. +This is used to include things like the CSS and JS in the binary so we +don't have to carry them around as files. +-/ @[termElab includeStr] def includeStrImpl : TermElab := λ stx expectedType? => do let str := stx[1].isStrLit?.get! let srcPath := (FilePath.mk (← read).fileName) From c05a9cf5e517109fa99f5e648e27dee4b146a61e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 May 2022 20:45:12 +0200 Subject: [PATCH 03/19] doc: Load --- DocGen4/Load.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 841891a..e86694b 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -13,6 +13,11 @@ namespace DocGen4 open Lean System Std 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 (imports : List String) : IO (Except UInt32 (Lake.Workspace × String)) := do let (leanInstall?, lakeInstall?) ← Lake.findInstall? let res ← StateT.run Lake.Cli.loadWorkspace {leanInstall?, lakeInstall?} |>.toIO' @@ -28,6 +33,10 @@ def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × Str pure $ Except.ok (ws, lean.githash) | Except.error rc => pure $ Except.error rc +/-- +Load a list of modules from the current Lean search path into an `Environment` +to process for documentation. +-/ def load (imports : List Name) : IO AnalyzerResult := do let env ← importModules (List.map (Import.mk · false) imports) Options.empty -- TODO parameterize maxHeartbeats From 43f778652362bb9f917ba6d010889507fe88f4a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 May 2022 20:48:26 +0200 Subject: [PATCH 04/19] refactor: pull source linker into submodule --- DocGen4/Output.lean | 64 +---------------------------- DocGen4/Output/SourceLinker.lean | 70 ++++++++++++++++++++++++++++++++ 2 files changed, 71 insertions(+), 63 deletions(-) create mode 100644 DocGen4/Output/SourceLinker.lean diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 7919f67..8d99535 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -12,74 +12,12 @@ import DocGen4.Output.Module import DocGen4.Output.NotFound import DocGen4.Output.Find import DocGen4.Output.Semantic +import DocGen4.Output.SourceLinker namespace DocGen4 open Lean Std IO System Output - -/- -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 - pure s!"https://github.com/{url}" - else if url.endsWith ".git" then - pure $ url.dropRight 4 - else - pure url - -def getProjectGithubUrl : IO String := do - let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]} - if out.exitCode != 0 then - throw <| IO.userError <| "git exited with code " ++ toString out.exitCode - pure out.stdout.trimRight - -def getProjectCommit : IO String := do - let out ← IO.Process.output {cmd := "git", args := #["rev-parse", "HEAD"]} - if out.exitCode != 0 then - throw <| IO.userError <| "git exited with code " ++ toString out.exitCode - pure out.stdout.trimRight - -def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option DeclarationRange → String) := do - -- Compute a map from package names to source URL - let mut gitMap := Std.mkHashMap - let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl) - let projectCommit ← getProjectCommit - gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit) - for pkg in ws.packageArray do - for dep in pkg.dependencies do - let value := match dep.src with - | Lake.Source.git url commit => (getGithubBaseUrl url, commit) - -- TODO: What do we do here if linking a source is not possible? - | _ => ("https://example.com", "master") - gitMap := gitMap.insert dep.name value - - pure $ λ 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 ∨ root == `Std then - s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean" - else - match ws.packageForModule? module with - | some pkg => - let (baseUrl, commit) := gitMap.find! pkg.name - s!"{baseUrl}/blob/{commit}/{path}.lean" - | none => "https://example.com" - - match range with - | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}" - | none => basic - def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash} let basePath := FilePath.mk "." / "build" / "doc" diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean new file mode 100644 index 0000000..b50c961 --- /dev/null +++ b/DocGen4/Output/SourceLinker.lean @@ -0,0 +1,70 @@ +import Lean +import Lake + +namespace DocGen4.Output + +open Lean + +/- +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 + pure s!"https://github.com/{url}" + else if url.endsWith ".git" then + pure $ url.dropRight 4 + else + pure url + +def getProjectGithubUrl : IO String := do + let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]} + if out.exitCode != 0 then + throw <| IO.userError <| "git exited with code " ++ toString out.exitCode + pure out.stdout.trimRight + +def getProjectCommit : IO String := do + let out ← IO.Process.output {cmd := "git", args := #["rev-parse", "HEAD"]} + if out.exitCode != 0 then + throw <| IO.userError <| "git exited with code " ++ toString out.exitCode + pure out.stdout.trimRight + +def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option DeclarationRange → String) := do + -- Compute a map from package names to source URL + let mut gitMap := Std.mkHashMap + let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl) + let projectCommit ← getProjectCommit + gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit) + for pkg in ws.packageArray do + for dep in pkg.dependencies do + let value := match dep.src with + | Lake.Source.git url commit => (getGithubBaseUrl url, commit) + -- TODO: What do we do here if linking a source is not possible? + | _ => ("https://example.com", "master") + gitMap := gitMap.insert dep.name value + + pure $ λ 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 ∨ root == `Std then + s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean" + else + match ws.packageForModule? module with + | some pkg => + let (baseUrl, commit) := gitMap.find! pkg.name + s!"{baseUrl}/blob/{commit}/{path}.lean" + | none => "https://example.com" + + match range with + | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}" + | none => basic + +end DocGen4.Output From 653c67e9b7b307bef3ffa93948cdff8d80c8858f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 May 2022 20:52:54 +0200 Subject: [PATCH 05/19] doc: SourceLinker --- DocGen4/Output/SourceLinker.lean | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean index b50c961..3152dd0 100644 --- a/DocGen4/Output/SourceLinker.lean +++ b/DocGen4/Output/SourceLinker.lean @@ -5,12 +5,14 @@ namespace DocGen4.Output 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 + +TODO: This function is quite brittle and very Github specific, we can probably do better. -/ def getGithubBaseUrl (gitUrl : String) : String := Id.run do @@ -24,18 +26,29 @@ def getGithubBaseUrl (gitUrl : String) : String := Id.run do else pure url +/-- +Obtain the Github URL of a project by parsing the origin remote. +-/ def getProjectGithubUrl : IO String := do let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]} if out.exitCode != 0 then throw <| IO.userError <| "git exited with code " ++ toString out.exitCode pure out.stdout.trimRight +/-- +Obtain the git commit hash of the project that is currently getting analyzed. +-/ def getProjectCommit : IO String := do let out ← IO.Process.output {cmd := "git", args := #["rev-parse", "HEAD"]} if out.exitCode != 0 then throw <| IO.userError <| "git exited with code " ++ toString out.exitCode pure 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) (leanHash : String): IO (Name → Option DeclarationRange → String) := do -- Compute a map from package names to source URL let mut gitMap := Std.mkHashMap From 0b8f7a1397ddb4d4fbd717c09debe1d0c6ca7017 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 May 2022 20:54:42 +0200 Subject: [PATCH 06/19] doc: Output top level module --- DocGen4/Output.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 8d99535..feedfda 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -16,8 +16,12 @@ import DocGen4.Output.SourceLinker namespace DocGen4 -open Lean Std IO System Output +open Lean IO System Output +/-- +The main entrypoint for outputting the documentation HTML based on an +`AnalyzerResult`. +-/ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash} let basePath := FilePath.mk "." / "build" / "doc" From bdd4a5f61211a0e8e10b5f1fe01654e55fd899d4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 May 2022 21:05:17 +0200 Subject: [PATCH 07/19] doc: Output.Base --- DocGen4/Output/Base.lean | 63 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 59 insertions(+), 4 deletions(-) diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 66bb358..3cedc79 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -7,16 +7,31 @@ import DocGen4.Process import DocGen4.IncludeStr import DocGen4.Output.ToHtmlFormat -namespace DocGen4 -namespace Output +namespace DocGen4.Output open scoped DocGen4.Jsx open Lean System Widget Elab +/-- +The context used in the `HtmlM` monad for HTML templating. +-/ structure SiteContext where + /-- + The full analysis result from the Process module. + -/ result : AnalyzerResult + /-- + 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 + /-- + A function to link declaration names to their source URLs, usually Github ones. + -/ sourceLinker : Name → Option DeclarationRange → String def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name} @@ -24,6 +39,9 @@ def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := abbrev HtmlT := ReaderT SiteContext abbrev HtmlM := HtmlT Id +/-- +Obtains the root URL as a relative one to the current depth. +-/ def getRoot : HtmlM String := do let rec go: Nat -> String | 0 => "./" @@ -35,22 +53,40 @@ 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 +/-- +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. +-/ def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := new >>= base +/-- +Returns the doc-gen4 link to a module name. +-/ def moduleNameToLink (n : Name) : HtmlM String := do let parts := n.components.map Name.toString pure $ (← 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" @@ -60,11 +96,26 @@ section Static def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js" 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] pure $ (←moduleNameToLink module) ++ "#" ++ 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 @@ -72,6 +123,11 @@ def splitWhitespaces (s : String) : (String × String × String) := Id.run do 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 | TaggedText.text t => pure #[Html.escape t] @@ -93,5 +149,4 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)] | _ => pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)] -end Output -end DocGen4 +end DocGen4.Output From e0bf4ad28c4187070410fbc67f01af03a3f22463 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 May 2022 21:07:44 +0200 Subject: [PATCH 08/19] doc: Output/Definition --- DocGen4/Output/Definition.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean index 3e0b146..6be1639 100644 --- a/DocGen4/Output/Definition.lean +++ b/DocGen4/Output/Definition.lean @@ -7,12 +7,18 @@ namespace Output open scoped DocGen4.Jsx open Lean Widget -/- This is basically an arbitrary number that seems to work okay. -/ +/-- This is basically an arbitrary number that seems to work okay. -/ def equationLimit : Nat := 200 def equationToHtml (c : CodeWithInfos) : HtmlM Html := do pure
  • [←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 : DefinitionInfo) : HtmlM (Array Html) := do if let some eqs := i.equations then let equationsHtml ← eqs.mapM equationToHtml From 20e136bb270b39a1d8adc30cbe333124011d0e06 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 May 2022 21:40:22 +0200 Subject: [PATCH 09/19] refactor: centralized methods for internal linking infrastructure --- DocGen4/Output/Base.lean | 21 +++++++++++++ DocGen4/Output/Class.lean | 2 +- DocGen4/Output/Module.lean | 61 ++++++++++++++++++++++++++++++-------- DocGen4/Output/Navbar.lean | 4 +-- 4 files changed, 73 insertions(+), 15 deletions(-) diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 3cedc79..cdcbca6 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -67,6 +67,12 @@ def moduleNameToLink (n : Name) : HtmlM 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 + pure {module.toString} + /-- Returns the path to the HTML file that contains information about a module. -/ @@ -104,6 +110,21 @@ def declNameToLink (name : Name) : HtmlM String := do let module := res.moduleNames[res.name2ModIdx.find! name] pure $ (←moduleNameToLink module) ++ "#" ++ name.toString +/-- +Returns the HTML doc-gen4 link to a declaration name. +-/ +def declNameToHtmlLink (name : Name) : HtmlM Html := do + let link ← declNameToLink name + pure {name.toString} + +/-- +Returns the HTML doc-gen4 link to a declaration name with "break_within" +set as class. +-/ +def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do + let link ← declNameToLink name + pure {name.toString} + /-- In Lean syntax declarations the following pattern is quite common: ``` diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean index 00fd252..e39a424 100644 --- a/DocGen4/Output/Class.lean +++ b/DocGen4/Output/Class.lean @@ -8,7 +8,7 @@ open scoped DocGen4.Jsx open Lean def classInstanceToHtml (name : Name) : HtmlM Html := do - pure
  • {name.toString}
    • + pure
  • {←declNameToHtmlLink name}
    • def classInstancesToHtml (instances : Array Name) : HtmlM Html := do let instancesHtml ← instances.mapM classInstanceToHtml diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 062a3ca..a9efe14 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -19,6 +19,10 @@ namespace Output open scoped DocGen4.Jsx open Lean +/-- +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) @@ -37,19 +41,27 @@ def argToHtml (arg : Arg) : HtmlM Html := do else pure html +/-- +Render the structures this structure extends from as HTML so it can be +added to the top level. +-/ def structureInfoHeader (s : 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 := {parent.toString} + let link ← declNameToHtmlBreakWithinLink parent let inner := Html.element "span" true #[("class", "fn")] #[link] let html:= Html.element "span" false #[("class", "decl_parent")] #[inner] parents := parents.push html nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray pure 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 {doc.getKindDescription} @@ -63,7 +75,6 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do for arg in doc.getArgs do nodes := nodes.push (←argToHtml arg) - -- TODO: dedup this match doc with | DocInfo.structureInfo i => nodes := nodes.append (←structureInfoHeader i) | DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i.toStructureInfo) @@ -73,6 +84,9 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType) pure
    [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 @@ -114,12 +128,20 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do +/-- +Rendering a module doc string, that is the ones with an ! after the opener +as HTML. +-/ def modDocToHtml (module : Name) (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 @@ -130,10 +152,9 @@ def declarationToNavLink (module : Name) : Html := {module.toString} --- TODO: Similar functions are used all over the place, we should dedup them -def moduleToNavLink (module : Name) : HtmlM Html := do - pure {module.toString} - +/-- +Returns the list of all imports this module does. +-/ def getImports (module : Name) : HtmlM (Array Name) := do let res ← getResult let some idx := res.moduleNames.findIdx? (. == module) | unreachable! @@ -144,6 +165,17 @@ def getImports (module : Name) : HtmlM (Array Name) := do imports := imports.push (res.moduleNames.get! i) pure 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 (λ i => do pure
  • {←moduleToHtmlLink i}
    • ) + +/-- +Returns a list of all modules this module is imported by. +-/ def getImportedBy (module : Name) : HtmlM (Array Name) := do let res ← getResult let some idx := res.moduleNames.findIdx? (. == module) | unreachable! @@ -154,15 +186,17 @@ def getImportedBy (module : Name) : HtmlM (Array Name) := do impBy := impBy.push (res.moduleNames.get! i) pure impBy +/-- +Sort the list of all modules this one is imported by, linkify it +and return the HTML. +-/ def importedByHtml (moduleName : Name) : HtmlM (Array Html) := do let imports := (←getImportedBy moduleName) |>.qsort Name.lt - imports.mapM (λ i => do pure
  • {←moduleToNavLink i}
    • ) - - -def importsHtml (moduleName : Name) : HtmlM (Array Html) := do - let imports := (←getImports moduleName) |>.qsort Name.lt - imports.mapM (λ i => do pure
  • {←moduleToNavLink i}
    • ) + imports.mapM (λ i => do pure
  • {←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 : Module) : HtmlM Html := withReader (setCurrentName module.name) do let memberDocs ← module.members.mapM (λ i => moduleMemberToHtml module.name i) let memberNames := filterMapDocInfo module.members |>.map DocInfo.getName diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index c9cb196..3db6033 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -15,7 +15,7 @@ open scoped DocGen4.Jsx def moduleListFile (file : Name) : HtmlM Html := do pure
    - {file.toString} + {←moduleToHtmlLink file}
    partial def moduleListDir (h : Hierarchy) : HtmlM Html := do @@ -31,7 +31,7 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do [if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]> { if (←getResult).moduleInfo.contains h.getName then - Html.element "summary" true #[] #[{h.getName.toString}] + Html.element "summary" true #[] #[←moduleToHtmlLink h.getName] else {h.getName.toString} } From 94ce87d11a390f4d50d614d03dac5b4f621cafe8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 May 2022 21:49:25 +0200 Subject: [PATCH 10/19] doc: Output.Navbar --- DocGen4/Output/Navbar.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 3db6033..bec70af 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -18,6 +18,9 @@ def moduleListFile (file : Name) : HtmlM Html := do {←moduleToHtmlLink file} +/-- +Build the HTML tree representing the module hierarchy. +-/ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do let children := Array.mk (h.getChildren.toList.map Prod.snd) let dirs := children.filter (λ c => c.getChildren.toList.length != 0) @@ -39,6 +42,9 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do [fileNodes] +/-- +Return a list of top level modules, linkified and rendered as HTML +-/ def moduleList : HtmlM Html := do let hierarchy := (←getResult).hierarchy let mut list := Array.empty @@ -46,6 +52,9 @@ def moduleList : HtmlM Html := 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 pure