Skip to content

kim-em/doc-gen4

This branch is 224 commits behind leanprover/doc-gen4:main.

Folders and files

NameName
Last commit message
Last commit date

Latest commit

Aug 18, 2023
d805539 · Aug 18, 2023
Aug 6, 2023
Aug 18, 2023
Aug 18, 2023
Dec 2, 2022
Aug 9, 2022
Nov 11, 2021
Mar 9, 2023
May 26, 2023
Aug 18, 2023
Aug 6, 2023
Aug 18, 2023
Aug 6, 2023

Repository files navigation

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 update your dependencies:

lake -Kenv=dev update

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

About

Document Generator for Lean 4

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Lean 56.2%
  • CSS 28.4%
  • JavaScript 15.2%
  • Shell 0.2%