diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index b64b550..d79c658 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -14,9 +14,8 @@ namespace DocGen4 open Lean Std IO System Output -def htmlOutput (result : AnalyzerResult) : IO Unit := do - -- TODO: parameterize this - let config := { root := "/", result := result, currentName := none} +def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do + let config := { root := root, result := result, currentName := none} let basePath := FilePath.mk "./build/doc/" let indexHtml := ReaderT.run index config let notFoundHtml := ReaderT.run notFound config diff --git a/Main.lean b/Main.lean index bc5c77a..7f527a4 100644 --- a/Main.lean +++ b/Main.lean @@ -4,9 +4,10 @@ import Lean open DocGen4 Lean IO def main (args : List String) : IO Unit := do - let modules := args + 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 + htmlOutput doc root diff --git a/README.md b/README.md index d0ff1e1..7c343a5 100644 --- a/README.md +++ b/README.md @@ -4,9 +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 `Module` is one or more of the top level modules you want to document. +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. 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 d9d89bc..2f77858 100755 --- a/deploy_docs.sh +++ b/deploy_docs.sh @@ -23,7 +23,7 @@ fi # generate the docs cd $1 -../$2/build/bin/doc-gen4 Mathlib +../$2/build/bin/doc-gen4 /mathlib4_docs/ Mathlib if [ "$3" = "true" ]; then cd ..