Merge pull request #39 from bollu/feb-21-relative-paths-manual-depth

Add support for relative paths
main
Henrik Böving 2022-04-07 08:29:01 +02:00 committed by GitHub
commit 00837fd089
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 28 additions and 18 deletions

View File

@ -80,8 +80,8 @@ def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option
| some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
| none => basic
def htmlOutput (result : AnalyzerResult) (root : String) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do
let config := { root := root, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash}
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"
let indexHtml := ReaderT.run index config
let findHtml := ReaderT.run find config
@ -94,8 +94,10 @@ def htmlOutput (result : AnalyzerResult) (root : String) (ws : Lake.Workspace) (
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 }
let doc := decl.getDocString.getD ""
let link := root ++ s!"semantic/{decl.getName.hash}.xml#"
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)]
@ -116,7 +118,8 @@ def htmlOutput (result : AnalyzerResult) (root : String) (ws : Lake.Workspace) (
FS.writeFile declarationDataPath json.compress
FS.writeFile (basePath / "declaration-data.timestamp") <| toString (←declarationDataPath.metadata).modified.sec
FS.writeFile (basePath / "site-root.js") (siteRootJs.replace "{siteRoot}" config.root)
let root := Id.run <| ReaderT.run (getRoot) config
FS.writeFile (basePath / "site-root.js") (siteRootJs.replace "{siteRoot}" root)
FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs
FS.writeFile (basePath / "nav.js") navJs
FS.writeFile (basePath / "find" / "find.js") findJs
@ -125,10 +128,14 @@ def htmlOutput (result : AnalyzerResult) (root : String) (ws : Lake.Workspace) (
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

View File

@ -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

View File

@ -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
@ -13,7 +12,7 @@ def runDocGenCmd (p : Parsed) : IO UInt32 := do
IO.println s!"Loading modules from: {←searchPathRef.get}"
let doc ← load $ modules.map Name.mkSimple
IO.println "Outputting HTML"
htmlOutput doc root ws leanHash
htmlOutput doc ws leanHash
pure 0
| Except.error rc => pure rc
@ -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"
]

View File

@ -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:

View File

@ -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 ..