Skip to content

Commit

Permalink
doc: notes on sharing
Browse files Browse the repository at this point in the history
  • Loading branch information
hargoniX committed Nov 11, 2024
1 parent 68943ae commit b181b72
Showing 1 changed file with 12 additions and 0 deletions.
12 changes: 12 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@
Document Generator for Lean 4

## Usage
Please do read the entire usage section once before executing commands as it might safe you some time.

`doc-gen4` is easiest to use via its custom Lake facet. The currently recommended setup for
this is that you create a nested project for documentation building inside of your lake project.
To do this:
Expand Down Expand Up @@ -38,6 +40,16 @@ If you have multiple libraries you want to generate full documentation for:
lake build Test:docs YourLibraryName:docs
```

If your library has additional dependencies this setup is not going to share the builds of the
dependencies by default. To do this run the following from `docbuild` before building docs:
```sh
mkdir -p .lake/packages
for package_path in ../.lake/packages/*; do
package=$(basename $package_path)
ln -s ../../../.lake/packages/$package .lake/packages/$package
done
```

Note that `doc-gen4` currently always generates documentation for `Lean`, `Init`, `Lake` and `Std`
in addition to the provided targets.

Expand Down

0 comments on commit b181b72

Please sign in to comment.