Rework website publishing workflow

The previous one turned out not to work because GH Actions
lacked permissions to access an external repo from a script.

The new workflow goes in two stages:

1. Generate website
2. Publish website

Generate website stage does the following:

1. Check out the website repo and save all the snapshots
   in a separate directory
2. Generate the website from the current commit the CI runs
   against
3. Move the previous snapshots to the output directory of
   the documentation generation run

Publish website step utilizes a 3rd party GitHub Action.

Author: anatoliykmetyuk

.github/workflows/ci.yaml

@@ -308,10 +308,18 @@ jobs:
           key: ${{ runner.os }}-general-${{ hashFiles('**/build.sbt') }}
           restore-keys: ${{ runner.os }}-general-
 
-      - name: Nightly Documentation
+      - name: Generate Website
         run: |
           ./project/scripts/genDocs -doc-snapshot
 
+      - name: Deploy Website
+        uses: peaceiris/actions-gh-pages@v3
+        with:
+          personal_token: ${{ secrets.BOT_TOKEN }}
+          publish_dir: docs/_site
+          external_repository: lampepfl/dotty-website
+          publish_branch: gh-pages
+
   publish_release:
     runs-on: self-hosted
     container: lampepfl/dotty:2020-04-24
@@ -452,10 +460,18 @@ jobs:
           key: ${{ runner.os }}-general-${{ hashFiles('**/build.sbt') }}
           restore-keys: ${{ runner.os }}-general-
 
-      - name: Nightly Documentation
+      - name: Generate Website
         run: |
           ./project/scripts/genDocs -doc-snapshot
 
+      - name: Deploy Website
+        uses: peaceiris/actions-gh-pages@v3
+        with:
+          personal_token: ${{ secrets.BOT_TOKEN }}
+          publish_dir: docs/_site
+          external_repository: lampepfl/dotty-website
+          publish_branch: gh-pages
+
   publish_sbt_release:
     runs-on: self-hosted
     container: lampepfl/dotty:2020-04-24

project/scripts/genDocs

@@ -1,66 +1,38 @@
 #!/usr/bin/env bash
 
-# Usage:
-# BOT_TOKEN=<dotty-bot password> ./genDocs [-doc-snapshot]
-
 set -e
-GENDOC_EXTRA_ARGS=$@
-
-# set extended glob, needed for rm everything but x
-shopt -s extglob
+shopt -s extglob # needed for rm everything but x
+echo "Working directory: $PWD"
 
-# make sure that BOT_TOKEN is set
-if [ -z "$BOT_TOKEN" ]; then
-    echo "Error: BOT_TOKEN env unset, unable to push without password" 1>&2
-    exit 1
+GENDOC_EXTRA_ARGS=$@
+GIT_HEAD=$(git rev-parse HEAD) # save current head for commit message in gh-pages
+PREVIOUS_SNAPSHOTS_DIR="$PWD/../prev_snapshots"
+SCRIPT_DIR="(cd "$(dirname "${BASH_SOURCE[0]}")" >& /dev/null && pwd)"
+SITE_OUT_DIR="$PWD/docs/_site"
+
+### Obtain the previous versions of the website ###
+if [ -d "$PREVIOUS_SNAPSHOTS_DIR" ]; then
+  rm -rf "$PREVIOUS_SNAPSHOTS_DIR"
 fi
 
-echo "Working directory: $PWD"
+mkdir -pv "$PREVIOUS_SNAPSHOTS_DIR"
+git remote add doc-remote "https://github.com/lampepfl/dotty-website.git"
+git fetch doc-remote gh-pages
+git checkout gh-pages
+(cp -vr 0.*/ "$PREVIOUS_SNAPSHOTS_DIR"; true)  # Don't fail if no `0.*` found to copy
+git checkout "$GIT_HEAD"
 
+### Generate the current snapshot of the website ###
 # this command will generate docs in $PWD/docs/_site
-SBT="$(cd "$(dirname "${BASH_SOURCE[0]}")" >& /dev/null && pwd)/sbt"
+SBT="$SCRIPT_DIR/sbt"
 "$SBT" "dotty-bootstrapped/genDocs $GENDOC_EXTRA_ARGS"
 
 # make sure that the previous command actually succeeded
-if [ ! -d "$PWD/docs/_site" ]; then
-    echo "Output directory did not exist: $PWD/docs/_site" 1>&2
-    exit 1
+if [ ! -d "$SITE_OUT_DIR" ]; then
+  echo "Output directory did not exist: $SITE_OUT_DIR" 1>&2
+  exit 1
 fi
 
-# save current head for commit message in gh-pages
-GIT_HEAD=$(git rev-parse HEAD)
-
-
-# set up remote and github credentials
-git remote add doc-remote "https://dotty-bot:$BOT_TOKEN@github.com/lampepfl/dotty-website.git"
-git config user.name "dotty-bot"
-git config user.email "dotty-bot@d-d.me"
-
-# check out correct branch
-git fetch doc-remote gh-pages
-git checkout gh-pages
-
-# save the old snapshots to the newly generated site
-# This command must never fail since failures short-circuit the script
-# The reason for failure is that no folder matches "0.*" pattern
-# because snapshots may not be generated yet
-(mv 0.*/ $PWD/docs/_site; true)
-
-# move newly generated _site dir to $PWD
-mv $PWD/docs/_site .
-
-# remove everything BUT _site dir
-rm -rf !(_site)
-
-# copy new contents to $PWD
-mv _site/* .
-
-# remove now empty _site dir
-rm -rf _site
-
-# add all contents of $PWD to commit
-git add -A
-git commit -m "Update gh-pages site for $GIT_HEAD" || echo "nothing new to commit"
-
-# push to doc-remote
-git push doc-remote || echo "couldn't push, since nothing was added"
+### Move previous versions' snapshots to _site ###
+mv -v "$PREVIOUS_SNAPSHOTS_DIR"/* "$SITE_OUT_DIR"
+rm -rf "$PREVIOUS_SNAPSHOTS_DIR"