Skip to content

Commit

Permalink
doc: more notes on sharing
Browse files Browse the repository at this point in the history
  • Loading branch information
hargoniX committed Nov 11, 2024
1 parent b181b72 commit 8add673
Showing 1 changed file with 12 additions and 3 deletions.
15 changes: 12 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,6 @@
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 All @@ -28,7 +26,18 @@ rev = "main"
```
.lake/
```
4. Run `lake update` within `docbuild` to pin `doc-gen4` and its dependencies to the chosen versions.
4. If you want to build docs right away and you have extra dependencies you need to run the
following script from within `docbuild` to share build products with your parent project.
Note that as `docbuild/.lake` is not going to be tracked by git you also need to run this
before building docs every time
```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
```
5. Run `lake update` within `docbuild` to pin `doc-gen4` and its dependencies to the chosen versions.

After this setup step you can generate documentation for an entire library and all files imported
by that library using the following command within `docbuild`:
Expand Down

0 comments on commit 8add673

Please sign in to comment.