ci(deploy_docs.sh): generalize for use in doc-gen CI (#2978)

This moves some installation steps out of `deploy_docs.sh` script and makes it accept several path arguments so that it can be re-used in the CI for `doc-gen`. 

The associated `doc-gen` PR: leanprover-community/doc-gen#27 will be updated after this is merged.

.github/workflows/build.yml

@@ -157,14 +157,6 @@ jobs:
           ~/.elan/bin/lean --version
           echo "::add-path::$HOME/.elan/bin"
 
-      - name: install Python
-        uses: actions/setup-python@v1
-        with:
-          python-version: 3.8
-
-      - name: install Python dependencies
-        run: python -m pip install --upgrade pip requests
-
       - name: tests
         run: |
           set -o pipefail
@@ -175,9 +167,21 @@ jobs:
           lean --recursive --export=mathlib.txt src/
           leanchecker mathlib.txt
 
+      - name: install Python
+        uses: actions/setup-python@v1
+        with:
+          python-version: 3.8
+
+      - name: install Python dependencies
+        run: python -m pip install --upgrade pip requests markdown2 toml
+
+      - name: setup doc-gen
+        run: |
+          git clone https://github.com/leanprover-community/doc-gen.git
+
       - name: generate docs
         run:
-          ./scripts/deploy_docs.sh
+          ./scripts/deploy_docs.sh "." "doc-gen" ".."
         env:
           DEPLOY_GITHUB_TOKEN: ${{ secrets.DEPLOY_GITHUB_TOKEN }}
           github_repo: ${{ github.repository }}

scripts/deploy_docs.sh

@@ -1,22 +1,27 @@
+# Arguments:
+# $1 : path to mathlib from working directory (mathlib: ".", doc-gen: "mathlib")
+# $2 : path to doc-gen from mathlib (mathlib: "doc-gen", doc-gen: "..")
+# $3 : path to mathlib from doc-gen (mathlib: "..", doc-gen: "mathlib")
+
 DEPLOY_GITHUB_USER=leanprover-community-bot
 
 set -e
 set -x
 
+cd $1
 lean_version="$(sed '/^lean_version/!d;s/.*"\(.*\)".*/\1/' leanpkg.toml)"
+mathlib_git_hash="$(git log -1 --pretty=format:%h)"
 
-git_hash="$(git log -1 --pretty=format:%h)"
-git clone https://github.com/leanprover-community/doc-gen.git
-cd doc-gen
-
-# the commit hash in leanpkg.toml is used by doc_gen.
-sed -i "s/rev = \"\S*\"/rev = \"$git_hash\"/" leanpkg.toml
+cd $2
+docgen_git_hash="$(git log -1 --pretty=format:%h)"
+# use the commit hash in mathlib's leanpkg.toml in doc_gen's leanpkg.toml
+sed -i "s/rev = \"\S*\"/rev = \"$mathlib_git_hash\"/" leanpkg.toml
+echo -e "builtin_path\npath ./src\npath $3/src" > leanpkg.path
 
-echo -e "builtin_path\npath ./src\npath ../src" > leanpkg.path
 git clone "https://$DEPLOY_GITHUB_USER:$DEPLOY_GITHUB_TOKEN@github.com/leanprover-community/mathlib_docs.git"
 
 # skip if docs for this commit have already been generated
-if [ "$(cd mathlib_docs && git log -1 --pretty=format:%s)" == "automatic update to $git_hash" ]; then
+if [ "$(cd mathlib_docs && git log -1 --pretty=format:%s)" == "automatic update to mathlib $mathlib_git_hash using doc-gen $docgen_git_hash" ]; then
   exit 0
 fi
 
@@ -27,16 +32,14 @@ rm -rf mathlib_docs/docs/
 # but this is better than trying to recompile all of mathlib.
 elan override set "$lean_version"
 
-python3 -m pip install --upgrade pip
-pip3 install markdown2 toml
-./gen_docs -w -r "../" -t "mathlib_docs/docs/"
+./gen_docs -w -r "$3/" -t "mathlib_docs/docs/"
 
-if [ "$github_repo" = "leanprover-community/mathlib" -a "$github_event" = "push" -a "$github_ref" = "refs/heads/master" ]; then
+if { [ "$github_repo" = "leanprover-community/mathlib" ] || [ "$github_repo" = "leanprover-community/doc-gen" ]; } && [ "$github_event" = "push" ] && [ "$github_ref" = "refs/heads/master" ]; then
   cd mathlib_docs/docs
   git config user.email "leanprover.community@gmail.com"
   git config user.name "leanprover-community-bot"
   git add -A .
   git checkout --orphan master2
-  git commit -m "automatic update to $git_hash"
+  git commit -m "automatic update to mathlib $mathlib_git_hash using doc-gen $docgen_git_hash"
   git push -f origin HEAD:master
 fi