Document generator for my Bookshelf project
 
 
 
 
Go to file
Henrik Böving 84a116ac43 chore: update toolchain 2022-12-13 19:37:28 +01:00
.github/workflows ci: also run on scheduled builds 2022-10-06 22:10:53 +02:00
DocGen4 chore: update toolchain 2022-12-03 17:43:12 +01:00
static fix: minor style improvements 2022-11-06 13:53:23 +01:00
.gitignore chore: update toolchain 2022-12-02 17:55:27 +01:00
DocGen4.lean chore: update toolchain 2022-08-11 18:30:28 +02:00
LICENSE Initial commit 2021-11-10 17:41:28 -08:00
Main.lean chore: toolchain upgrade (#82) 2022-10-05 12:05:58 +02:00
README.md feat: implement facet 2022-08-11 22:58:25 +02:00
deploy_docs.sh chore: toolchain upgrade (#82) 2022-10-05 12:05:58 +02:00
lake-manifest.json chore: update toolchain 2022-12-03 17:43:12 +01:00
lakefile.lean chore: update toolchain 2022-12-03 17:43:12 +01:00
lean-toolchain chore: update toolchain 2022-12-13 19:37:28 +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.