diff options
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/docs_cleanup.yml | 61 | ||||
| -rw-r--r-- | .github/workflows/docs_update.yml | 108 |
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 |