From 898496ca51987a8db762e6b468ba277cf32f2d16 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 20 Jun 2022 22:51:22 +0200
Subject: [PATCH] feat: update CI and README

---
 .github/workflows/build.yml | 10 +++++++++-
 README.md                   |  4 ++++
 deploy_docs.sh              |  2 +-
 3 files changed, 14 insertions(+), 2 deletions(-)

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