diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 4412ec5..5483cfe 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -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 diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 2f84500..2bae54a 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,7 +40,7 @@ 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 diff --git a/Main.lean b/Main.lean index e8b2d82..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 @@ -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" ] 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: 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 ..