Document generator for my Bookshelf project
 
 
 
 
Go to file
F. G. Dorais 755f06fb0d fix: correct character category testing 2023-03-11 21:14:36 +01:00
.github/workflows chore: QoL updates for deploy_docs.sh 2023-01-05 00:02:41 +01:00
DocGen4 fix: correct character category testing 2023-03-11 21:14:36 +01:00
static fix implicit arg wrapping 2023-03-04 12:20:05 +01:00
.gitignore chore: update toolchain 2022-12-02 17:55:27 +01:00
DocGen4.lean chore: update toolchain and dependencies 2022-08-09 23:30:43 +02:00
LICENSE Initial commit 2021-11-10 17:41:28 -08:00
Main.lean feat: show versions in index HTML 2023-03-09 21:46:38 +01:00
README.md Add comment to README about need for copying css and js files. 2023-02-03 21:10:44 +01:00
deploy_docs.sh chore: QoL updates for deploy_docs.sh 2023-01-05 00:02:41 +01:00
lake-manifest.json refactor: switch to maintained unicode lib 2023-03-11 18:06:32 +01:00
lakefile.lean refactor: switch to maintained unicode lib 2023-03-11 18:06:32 +01:00
lean-toolchain chore: update toolchhain 2023-03-09 19:37:27 +01:00

README.md

doc-gen4

Document Generator for Lean 4

Usage

doc-gen4 is the easiest to use via its custom Lake facet, in order to do this you have to add it to your lakefile.lean like this:

meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

Then you can generate documentation for an entire library using:

lake -Kenv=dev build Test:docs

If you have multiple libraries you want to generate documentation for the recommended way right now is to run it for each library.

Development of doc-gen4

You can build docs using a modified doc-gen4 as follows: Replace the from git "..." @ "main" in the lakefile.lean with just from "..." using the path to the modified version of doc-gen4. E.g. if the path to the modified version of doc-gen4 is ../doc-gen4, it would be:

meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from "../doc-gen4"

The root of the built docs will be build/docs/index.html. However, due to the "Same Origin Policy", the generated website will be partially broken if you just open the generated html files in your browser. You need to serve them from a proper http server for it to work. An easy way to do that is to run python3 -m http.server from the build/docs directory.

Note that if you modify the .js or .css files in doc-gen4, they won't necessarily be copied over when you rebuild the documentation. You can manually copy the changes to the build/docs directory to make sure the changes appear, or just do a full recompilation (lake clean and lake build inside the doc-gen4 directory.)