From 93f32971ec83cbb27ec0aa64dcb8e643709bf39a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 6 Jan 2022 22:55:29 +0100
Subject: [PATCH] feat: CI and auto documentation preview for mathlib4

---
 .github/workflows/build.yml | 47 +++++++++++++++++++++++++++++++++++++
 deploy_docs.sh              | 41 ++++++++++++++++++++++++++++++++
 2 files changed, 88 insertions(+)
 create mode 100644 .github/workflows/build.yml
 create mode 100755 deploy_docs.sh

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
new file mode 100644
index 0000000..ad55818
--- /dev/null
+++ b/.github/workflows/build.yml
@@ -0,0 +1,47 @@
+name: build and deploy docs
+
+on:
+  schedule:
+    - cron: '0 */2 * * *' # every 2 hours
+  push:
+  pull_request:
+
+jobs:
+  build:
+    name: build and deploy docs
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repo
+        uses: actions/checkout@v2
+
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: compile doc-gen4
+        run: |
+          lake build
+
+      - name: Checkout and compile mathlib4
+        run: |
+          cd ../
+          git clone https://github.com/leanprover-community/mathlib4
+          cd mathlib4
+          lake build
+
+      - name: generate and deploy docs
+        run: |
+          if [ "$github_repo" = "leanprover/doc-gen4" ] && [ "$github_ref" = "refs/heads/main" ]; then
+            deploy="true"
+          else
+            deploy="false"
+          fi
+          cd ../
+          ./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "$deploy"
+        env:
+          MATHLIB4_DOCS_KEY: ${{ secrets.MATHLIB4_DOCS_KEY }}
+          github_repo: ${{ github.repository }}
+          github_ref: ${{ github.ref }}
diff --git a/deploy_docs.sh b/deploy_docs.sh
new file mode 100755
index 0000000..6e28e87
--- /dev/null
+++ b/deploy_docs.sh
@@ -0,0 +1,41 @@
+# Arguments:
+# $1 : path to mathlib4 from working directory
+# $2 : path to doc-gen4 from working directory
+# $3 : whether to deploy
+
+set -e
+set -x
+
+cd $1
+mathlib_short_git_hash="$(git log -1 --pretty=format:%h)"
+
+cd ../$2
+docgen_git_hash="$(git log -1 --pretty=format:%h)"
+
+cd ../
+
+git clone "https://github.com/leanprover-community/mathlib4_docs.git" mathlib4_docs
+
+# skip if docs for this commit have already been generated
+if [ "$(cd mathlib4_docs && git log -1 --pretty=format:%s)" == "automatic update to mathlib4 $mathlib_short_git_hash using doc-gen4 $docgen_git_hash" ]; then
+  exit 0
+fi
+
+# generate the docs
+cd $1
+../$2/build/bin/doc-gen4 Mathlib
+
+if [ "$3" = "true" ]; then
+  rm -rf mathlib4_docs/docs/
+  cp -r "$1/build/doc" mathlib4_docs/docs
+  mkdir ~/.ssh
+  echo "$MATHLIB4_DOCS_KEY" > ~/.ssh/id_ed25519
+  cd mathlib4_docs/docs
+  git remote set-url origin "git@github.com:leanprover-community/mathlib4_docs.git"
+  git config user.email "hargonix@gmail.com"
+  git config user.name "doc-gen4-bot"
+  git add -A .
+  git checkout --orphan master2
+  git commit -m "automatic update to mathlib4 $mathlib_short_git_hash using doc-gen4 $docgen_git_hash"
+  git push -f origin HEAD:master
+fi