[nongnu] elpa/proof-general e8dadc6ea7: feat: Auto-deploy doc of PG master (#664)

[ELPA Syncer]

branch: elpa/proof-general
commit e8dadc6ea7d94e355c39776ad7940c8daaa659a6
Author: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Commit: GitHub <noreply@github.com>

    feat: Auto-deploy doc of PG master (#664)
---
 .github/workflows/deploy-doc.yml | 88 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 88 insertions(+)

diff --git a/.github/workflows/deploy-doc.yml b/.github/workflows/deploy-doc.yml
new file mode 100644
index 0000000000..9ea0058ef4
--- /dev/null
+++ b/.github/workflows/deploy-doc.yml
@@ -0,0 +1,88 @@
+name: Documentation
+
+on:
+  push:
+    branches:
+      # All these must be protected branches so $GHA_PG_DEPLOY_KEY is available
+      - 'master'
+      # Maybe add a similar trigger for tags (if repo secrets can be retrieved)
+
+jobs:
+  deploy-doc:
+    runs-on: ubuntu-latest
+
+    strategy:
+      matrix:
+        emacs_version:
+          # Update if need be:
+          - 27.1
+      # don't cancel all in-progress jobs if one matrix job fails:
+      fail-fast: false
+
+    steps:
+      - uses: purcell/setup-emacs@master
+        with:
+          version: ${{ matrix.emacs_version }}
+
+      - run: emacs --version
+
+      - name: Install makeinfo
+        run: sudo apt-get update -y -q && sudo DEBIAN_FRONTEND=noninteractive 
apt-get install -y -q --no-install-recommends texinfo texi2html
+
+      - name: Checkout PG
+        uses: actions/checkout@v3
+        with:
+          path: 'PG'
+          # Assuming this workflow is only triggerred for branches and tags
+          ref: ${{ github.ref_name }}
+
+      - name: Checkout proofgeneral.github.io
+        uses: actions/checkout@v3
+        with:
+          repository: 'ProofGeneral/proofgeneral.github.io'
+          ref: 'master'
+          path: 'gh-pages'
+
+      - name: Build doc
+        run: |
+          set -x
+          pushd PG
+          commit_PG=$(git rev-parse --verify HEAD)
+          echo "Commit ${commit_PG}:"
+          git describe --all --long --abbrev=40 --always --dirty
+          pushd ../gh-pages/doc
+          git config user.name "ProofGeneral Bot"
+          git config user.email "37002148+proofbot@users.noreply.github.com"
+          make BRANCH="${GITHUB_REF_NAME}"
+          git commit -m 'Auto-Update {userman, adaptingman}' \
+            -m "href: https://github.com/ProofGeneral/PG/commit/${commit_PG}";
+          popd
+          popd
+
+      - name: Disable Host key verification
+        # this workaround should ideally be replaced with a ssh-keyscan based 
solution
+        run: |
+          mkdir -p -m 700 ~/.ssh
+          echo "StrictHostKeyChecking no" >> ~/.ssh/config
+
+      - name: Push doc
+        env:
+          GHA_PG_DEPLOY_KEY: ${{ secrets.GHA_PG_DEPLOY_KEY }}
+        run: |
+          [ -n "$GHA_PG_DEPLOY_KEY" ]
+          eval $(ssh-agent -s)
+          mkdir -p -m 700 ~/.ssh
+          echo "$GHA_PG_DEPLOY_KEY" | ssh-add -
+          set -x
+          pushd gh-pages
+          export branch=master  # useful for debug purpose
+          if [ "$branch" != master ]; then git checkout -b "$branch"; fi
+          git remote add deploy 
git@github.com:ProofGeneral/proofgeneral.github.io.git
+          git remote -v
+          git describe --all --long --abbrev=40 --always --dirty
+          git branch -avv
+          git rev-parse --verify HEAD
+          git push deploy HEAD:"$branch"
+          popd
+          rm -fr ~/.ssh || :
+          ssh-add -D || :