From 91891fc4fd29132c19046493358d9fec04447c10 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Tue, 15 Feb 2022 11:12:17 +0000 Subject: [PATCH 1/5] Generate relative paths for documentation. We keep track of the current nesting depth in our Context, and use this to generate the correct relative path to the root. --- DocGen4/Output.lean | 29 ++++++++++++++++++----------- DocGen4/Output/Base.lean | 15 +++++++++++---- Main.lean | 10 ++++------ 3 files changed, 33 insertions(+), 21 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 4f549c2..21f28a6 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -61,21 +61,24 @@ def sourceLinker : IO (Name → Option DeclarationRange → String) := do | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}" | none => basic -def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do - let config := { root := root, result := result, currentName := none, sourceLinker := ←sourceLinker} - let basePath := FilePath.mk "." / "build" / "doc" - let indexHtml := ReaderT.run index config - let notFoundHtml := ReaderT.run notFound config +def htmlOutput (result : AnalyzerResult) : IO Unit := do + let basePath := FilePath.mk "./build/doc/" + let config := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker} FS.createDirAll basePath FS.createDirAll (basePath / "find") + let indexHtml := ReaderT.run index config + let notFoundHtml := ReaderT.run notFound config let mut declList := #[] - for (_, mod) in result.moduleInfo.toArray do + for (module, mod) in result.moduleInfo.toArray do for decl in filterMapDocInfo mod.members do - let findHtml := ReaderT.run (findRedirectHtml decl.getName) config let findDir := basePath / "find" / decl.getName.toString + let findFile := (findDir / "index.html") + -- path: 'basePath/find/decl.getName.toString' + let config := { config with depthToRoot := 2 } + let findHtml := ReaderT.run (findRedirectHtml decl.getName) config FS.createDirAll findDir - FS.writeFile (findDir / "index.html") findHtml.toString + FS.writeFile findFile findHtml.toString let obj := Json.mkObj [("name", decl.getName.toString), ("description", decl.getDocString.getD "")] declList := declList.push obj let json := Json.arr declList @@ -88,10 +91,14 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do FS.writeFile (basePath / "search.js") searchJs FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs for (module, content) in result.moduleInfo.toArray do + let fileDir := moduleNameToDirectory basePath module + let filePath := moduleNameToFile basePath module + -- 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 := module.components.dropLast.length } let moduleHtml := ReaderT.run (moduleToHtml content) config - let path := moduleNameToFile basePath module - FS.createDirAll $ moduleNameToDirectory basePath module - FS.writeFile path moduleHtml.toString + FS.createDirAll $ fileDir + FS.writeFile filePath moduleHtml.toString end DocGen4 diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 68812a8..0723518 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -14,10 +14,9 @@ open scoped DocGen4.Jsx open Lean System Widget Elab structure SiteContext where - root : String result : AnalyzerResult + depthToRoot: Nat currentName : Option Name - -- Generates a URL pointing to the source of the given module Name sourceLinker : Name → Option DeclarationRange → String def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name} @@ -25,7 +24,13 @@ def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := abbrev HtmlT := ReaderT SiteContext abbrev HtmlM := HtmlT Id -def getRoot : HtmlM String := do pure (←read).root +def getRoot : HtmlM String := do + let rec go: Nat -> String + | 0 => "./" + | Nat.succ n' => "../" ++ go n' + let d <- SiteContext.depthToRoot <$> read + return (go d) + 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 @@ -35,12 +40,14 @@ def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : H def moduleNameToLink (n : Name) : HtmlM String := do let parts := n.components.map Name.toString - pure $ (←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" + pure $ (<- getRoot) ++ (parts.intersperse "/").foldl (. ++ ·) "" ++ ".html" def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath := let parts := n.components.map Name.toString FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html" + + def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath := let parts := n.components.dropLast.map Name.toString basePath / parts.foldl (· / ·) (FilePath.mk ".") diff --git a/Main.lean b/Main.lean index 13e530b..062cf6b 100644 --- a/Main.lean +++ b/Main.lean @@ -3,15 +3,13 @@ import Lean open DocGen4 Lean IO -def main (args : List String) : IO Unit := do - if args.isEmpty then - IO.println "Usage: doc-gen4 root/url/ Module1 Module2 ..." +def main (modules : List String) : IO Unit := do + if modules.isEmpty then + IO.println "Usage: doc-gen4 Module1 Module2 ..." IO.Process.exit 1 return - let root := args.head! - let modules := args.tail! let path ← lakeSetupSearchPath (←getLakePath) modules.toArray IO.println s!"Loading modules from: {path}" let doc ← load $ modules.map Name.mkSimple IO.println "Outputting HTML" - htmlOutput doc root + htmlOutput doc From f5b9e0276674b153a213509fb2db8d8d79e0aebc Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 7 Apr 2022 00:44:49 +0100 Subject: [PATCH 2/5] modify deploy_docs to not need relative path --- deploy_docs.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deploy_docs.sh b/deploy_docs.sh index 2f77858..d9d89bc 100755 --- a/deploy_docs.sh +++ b/deploy_docs.sh @@ -23,7 +23,7 @@ fi # generate the docs cd $1 -../$2/build/bin/doc-gen4 /mathlib4_docs/ Mathlib +../$2/build/bin/doc-gen4 Mathlib if [ "$3" = "true" ]; then cd .. From 9570f25312ac0a5773f5ee33490ae2d0f2c48655 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 7 Apr 2022 00:48:12 +0100 Subject: [PATCH 3/5] cleanup code --- DocGen4/Output.lean | 10 ---------- Main.lean | 2 -- 2 files changed, 12 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index f4dd4d5..3d901c8 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -93,24 +93,14 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String let mut declList := #[] for (module, mod) in result.moduleInfo.toArray do for decl in filterMapDocInfo mod.members do --- <<<<<<< HEAD let name := decl.getName.toString - -- let findDir := basePath / "find" / ma,e - -- let findFile := (findDir / "index.html") let config := { config with depthToRoot := 2 } - -- let findHtml := ReaderT.run (findRedirectHtml decl.getName) config - -- FS.createDirAll findDir - -- FS.writeFile findFile findHtml.toString - -- let obj := Json.mkObj [("name", decl.getName.toString), ("description", decl.getDocString.getD "")] --- ======= let doc := decl.getDocString.getD "" - -- let root := module.getRoot 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)] --- >>>>>>> upstream/main declList := declList.push obj let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml diff --git a/Main.lean b/Main.lean index 88a0640..8bb1187 100644 --- a/Main.lean +++ b/Main.lean @@ -5,7 +5,6 @@ import Cli open DocGen4 Lean Cli def runDocGenCmd (p : Parsed) : IO UInt32 := do - -- let root := p.positionalArg! "root" |>.as! String let modules : List String := p.variableArgsAs! String |>.toList let res ← lakeSetup modules match res with @@ -22,7 +21,6 @@ def docGenCmd : Cmd := `[Cli| "A documentation generator for Lean 4." ARGS: - -- root : String; "The root URL to generate the HTML for (will be relative in the future)" ...modules : String; "The modules to generate the HTML for" ] From 10ed2d489d8c8300f230aaccdcbdc6e54473d213 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 7 Apr 2022 00:49:05 +0100 Subject: [PATCH 4/5] update README --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 7c343a5..7e1f829 100644 --- a/README.md +++ b/README.md @@ -4,10 +4,10 @@ Document Generator for Lean 4 ## Usage You can call `doc-gen4` from the top of a Lake project like this: ```sh -$ /path/to/doc-gen4 / Module +$ /path/to/doc-gen4 Module ``` -Where the `/` is the root URL the HTML will refer to and `Module` is one or -more of the top level modules you want to document. + +where `Module` is one or more of the top level modules you want to document. The tool will then proceed to compile the project using lake (if that hasn't happened yet), analyze it and put the result in `./build/doc`. You could e.g. host the files locally with the built-in Python webserver: From 4bc149a1fb1980b4219ac32130780c14e920e158 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 7 Apr 2022 00:53:06 +0100 Subject: [PATCH 5/5] Fix diff nits --- DocGen4/Output.lean | 2 +- DocGen4/Output/Base.lean | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 3d901c8..5483cfe 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -91,7 +91,7 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String FS.createDirAll (basePath / "semantic") let mut declList := #[] - for (module, mod) in result.moduleInfo.toArray do + for (_, mod) in result.moduleInfo.toArray do for decl in filterMapDocInfo mod.members do let name := decl.getName.toString let config := { config with depthToRoot := 2 } diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index a1e82b7..2bae54a 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -40,14 +40,12 @@ def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : H def moduleNameToLink (n : Name) : HtmlM String := do let parts := n.components.map Name.toString - pure $ (<- getRoot) ++ (parts.intersperse "/").foldl (. ++ ·) "" ++ ".html" + pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath := let parts := n.components.map Name.toString FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html" - - def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath := let parts := n.components.dropLast.map Name.toString basePath / parts.foldl (· / ·) (FilePath.mk ".")