Add CI jobs to build docs (#6413)

This PR adds CI jobs to automatically build documentation for branches on the main repository and for pull request.
The first job builds the documentation for every push and pr and stores the generated documentation in cvc5.github.io/docs-ci. All versions are stored and for every branch and PR a symbolic link to the most recent version is maintained.
Note that the PR jobs are run by the pull_request_target trigger that allows access to repository secrets, but runs in the context of the target branch and we thus need to (carefully!) pull in the relevant changes manually.
The second job runs once a week and prunes the docs-ci repository: all directories that have not been touched for a month are removed, and all commits older than a month are squashed into a single commit. This retains the full history for the last month, but effectively removes everything older than that.

2 files changed, 169 insertions, 0 deletions

diff --git a/.github/workflows/docs_cleanup.yml b/.github/workflows/docs_cleanup.yml
new file mode 100644
index 000000000..0260b6474
--- /dev/null
+++ b/.github/workflows/docs_cleanup.yml
@@ -0,0 +1,61 @@
+name: documentation cleanup
+on:
+  schedule:
+    - cron: '0 1 * * SUN'
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Install Packages
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y python3 python3-jinja2
+
+      - name: Setup Deploy Key
+        env:
+            SSH_AUTH_SOCK: /tmp/ssh_agent.sock
+        run: |
+            ssh-agent -a $SSH_AUTH_SOCK > /dev/null
+            ssh-add - <<< "${{ secrets.CVC5_DOCS_TOKEN }}"
+
+      - name: Clone docs repo
+        env:
+            SSH_AUTH_SOCK: /tmp/ssh_agent.sock
+        run: |
+          git config --global user.email "docbot@cvc5"
+          git config --global user.name "DocBot"
+          git clone git@github.com:cvc5/docs-ci.git target/
+      
+      - name: Remove stale docs
+        run: |
+          cd target
+          for file in `find ./ -maxdepth 1 -name "docs-*"`; do
+            mod=`git log -1 HEAD --pretty="%ci" $file`
+            touch -d "$mod" $file
+          done
+          find ./ -maxdepth 1 -name "docs-*" -mtime +7 -exec git rm -r {} +
+          git commit -m "Prune docs" || echo "Nothing to prune"
+
+      - name: Squash old commits
+        env:
+            SSH_AUTH_SOCK: /tmp/ssh_agent.sock
+        run: |
+          cd target
+          git log
+          first=`git rev-list --max-parents=0 HEAD`
+          last=`git rev-list --until=1.month.ago -n1 HEAD`
+          git rebase -Xtheirs --onto $first $last
+          git log
+      
+      - name: Push
+        env:
+            SSH_AUTH_SOCK: /tmp/ssh_agent.sock
+        run: |
+          cd target
+
+          python3 genindex.py
+          git add README.md
+          git commit -m "Update README.md"
+
+          git push -f
diff --git a/.github/workflows/docs_update.yml b/.github/workflows/docs_update.yml
new file mode 100644
index 000000000..c51246ee0
--- /dev/null
+++ b/.github/workflows/docs_update.yml
@@ -0,0 +1,108 @@
+name: documentation update
+on:
+  push:
+    paths:
+    - '.github/**'
+    - 'docs/**'
+    - 'examples/**'
+    - 'src/api/**'
+  pull_request_target:
+    paths:
+    - '.github/**'
+    - 'docs/**'
+    - 'examples/**'
+    - 'src/api/**'
+
+# When run by pull_request_target (in comparison to pull_request), the action
+# has access to the repository secrets so that we can push the generated docs.
+# To allow this, the action is run in the context of the master branch instead
+# of the PR. We therefore obtain the changes from the PR manually,
+# but need to be very careful to not pull any changes to files that are executed
+# during configuration or build. At the same time, we try to include as many
+# files as possible that may change how the documentations looks like.
+# To ensure this, we only checkout a very selected set of files from the PR
+# branch:
+# - docs/**.(bib|rst)
+# - src/api/**.(cpp|h|java|py)
+# - examples/**.(cpp|h|java|py|smt2)
+# In particular, we should not checkout any CMakeLists.txt files or any python
+# files used by sphinx.
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: Install Packages
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y \
+            build-essential \
+            libgmp-dev \
+            doxygen \
+            python3-docutils python3-jinja2
+          python3 -m pip install \
+            setuptools toml pytest \
+            sphinxcontrib-bibtex sphinx-tabs sphinx-rtd-theme \
+            breathe
+          python3 -m pip install \
+            Cython==0.29.* --install-option="--no-cython-compile"
+          echo "$(python3 -m site --user-base)/bin" >> $GITHUB_PATH
+      
+      - name: Checkout PR
+        run: |
+          git config --global user.email "docbot@cvc5"
+          git config --global user.name "DocBot"
+          if [ "${{ github.event_name }}" == "push" ] ; then
+            NAME=$(echo "${GITHUB_REF}" | sed "s,refs/heads/,,")
+            echo "Identified branch $NAME"
+          elif [ "${{ github.event_name }}" == "pull_request_target" ] ; then
+            NAME="${{ github.event.number }}"
+            PRHASH="${{ github.event.pull_request.head.sha }}"
+            echo "Identified PR #$NAME (from $PRHASH)"
+            NAME="pr$NAME"
+            # be careful here, see explanation above!
+            git fetch
+            git checkout "${PRHASH}" -- \
+              `git ls-tree "${PRHASH}" --name-only -r docs/ | grep -E ".*\.(rst|bib)"` \
+              `git ls-tree "${PRHASH}" --name-only -r src/api/ | grep -E ".*\.(h|cpp|java|py)"` \
+              `git ls-tree "${PRHASH}" --name-only -r examples/ | grep -E ".*\.(h|cpp|java|py|smt2)"`
+          fi
+          echo "NAME=$NAME" >> $GITHUB_ENV
+
+      - name: Configure
+        run: ./configure.sh production --docs --all-bindings
+
+      - name: Build
+        run: make -j2 docs-gh
+        working-directory: build
+
+      - name: Setup Deploy Key
+        env:
+            SSH_AUTH_SOCK: /tmp/ssh_agent.sock
+        run: |
+            ssh-agent -a $SSH_AUTH_SOCK > /dev/null
+            ssh-add - <<< "${{ secrets.CVC5_DOCS_TOKEN }}"
+
+      - name: Update docs
+        continue-on-error: true
+        env:
+            SSH_AUTH_SOCK: /tmp/ssh_agent.sock
+        run: |
+          git clone git@github.com:cvc5/docs-ci.git target/
+          if [ -n "$NAME" ]; then
+            rsync -a --delete build/docs/sphinx-gh/ target/docs-$NAME-${{ github.sha }}
+            cd target/
+            rm -f docs-$NAME
+            ln -s docs-$NAME-${{ github.sha }} docs-$NAME
+            git add docs-$NAME docs-$NAME-${{ github.sha }}
+
+            python3 genindex.py
+            git add README.md
+            git commit -m "Update docs for $NAME"
+
+            git push
+          else
+            echo "Ignored run"
+          fi