diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index ad55818..ba1ad2f 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -25,6 +25,14 @@ jobs: run: | lake build + - name: Checkout and compile LeanInk + run: | + cd ../ + git clone https://github.com/hargonix/LeanInk + cd LeanInk + git checkout doc-gen + lake build + - name: Checkout and compile mathlib4 run: | cd ../ @@ -40,7 +48,7 @@ jobs: deploy="false" fi cd ../ - ./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "$deploy" + ./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "$deploy" "LeanInk" env: MATHLIB4_DOCS_KEY: ${{ secrets.MATHLIB4_DOCS_KEY }} github_repo: ${{ github.repository }} diff --git a/README.md b/README.md index 7e1f829..4ca3074 100644 --- a/README.md +++ b/README.md @@ -10,6 +10,10 @@ $ /path/to/doc-gen4 Module where `Module` is one or more of the top level modules you want to document. The tool will then proceed to compile the project using lake (if that hasn't happened yet), analyze it and put the result in `./build/doc`. + +You can optionally provide the path to a `LeanInk` binary using the `--ink` flag which will make +the tool produce `Alectryon` style rendered output along the usual documentation. + You could e.g. host the files locally with the built-in Python webserver: ```sh $ cd build/doc && python -m http.server diff --git a/deploy_docs.sh b/deploy_docs.sh index d9d89bc..3eec3b8 100755 --- a/deploy_docs.sh +++ b/deploy_docs.sh @@ -23,7 +23,7 @@ fi # generate the docs cd $1 -../$2/build/bin/doc-gen4 Mathlib +../$2/build/bin/doc-gen4 --ink ../$4/build/bin/leanInk Mathlib if [ "$3" = "true" ]; then cd ..