feat: update CI and README

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

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

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