Upload Docs #779
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Upload Docs | |
| on: | |
| workflow_run: | |
| workflows: ["CI"] | |
| types: | |
| - completed | |
| jobs: | |
| upload-docs: | |
| name: upload-docs | |
| runs-on: ubuntu-latest | |
| continue-on-error: true | |
| if: github.repository == 'cvc5/cvc5' && github.event.workflow_run.conclusion == 'success' | |
| steps: | |
| - name: Setup git config | |
| run: | | |
| git config --global user.email "docbot@cvc5" | |
| git config --global user.name "DocBot" | |
| - name: Download artifact | |
| uses: actions/github-script@v7 | |
| with: | |
| script: | | |
| var artifacts = await github.rest.actions.listWorkflowRunArtifacts({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| run_id: ${{github.event.workflow_run.id }}, | |
| }); | |
| var matchArtifact = artifacts.data.artifacts.filter((artifact) => { | |
| return artifact.name == "documentation" | |
| })[0]; | |
| var download = await github.rest.actions.downloadArtifact({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| artifact_id: matchArtifact.id, | |
| archive_format: 'zip', | |
| }); | |
| var fs = require('fs'); | |
| fs.writeFileSync('${{github.workspace}}/download.zip', Buffer.from(download.data)); | |
| - name: Unpack artifact | |
| run: unzip download.zip -d docs-new/ | |
| - name: Check for broken links | |
| continue-on-error: true | |
| run: | | |
| python3 -m pip install linkchecker | |
| linkchecker --check-extern docs-new/index.html | |
| # This workflow is run for commits in PRs (from branches in forks), commits | |
| # (from branches in main repo, usually main branch) and tags. Unfortunately, | |
| # there are only two properties in the github context that can be used here: | |
| # - workflow_run.event is "pull_request" for PRs and "push" otherwise | |
| # - workflow_run.head_branch contains the branch or tag name | |
| # We can not reliably identify a tag from that, so we simply match the | |
| # head_branch against the naming pattern of our tags ("cvc5-*"). To prevent PRs | |
| # with a matching branch name to be recognized as tags, we proceed as follows: | |
| # - handle PRs (event == "pull_request") | |
| # - handle tags (head_branch == "cvc5-*") | |
| # - rest are regular commits | |
| - name: Setup Context | |
| run: | | |
| HASH=${{ github.event.workflow_run.head_commit.id }} | |
| ISRELEASE=false | |
| if [ "${{ github.event.workflow_run.event }}" == "pull_request" ] ; then | |
| NAME=$(cat docs-new/prnum) | |
| rm docs-new/prnum | |
| echo "Identified PR #$NAME (from $HASH)" | |
| NAME="pr$NAME" | |
| elif [ "${{ startsWith(github.event.workflow_run.head_branch, 'cvc5-') }}" == "true" ] ; then | |
| ISRELEASE=true | |
| NAME=${{ github.event.workflow_run.head_branch }} | |
| echo "Identified tag $NAME" | |
| elif [ "${{ github.event.workflow_run.event }}" == "push" ] ; then | |
| NAME=${{ github.event.workflow_run.head_branch }} | |
| echo "Identified branch $NAME" | |
| fi | |
| echo "NAME=$NAME" >> $GITHUB_ENV | |
| echo "HASH=$HASH" >> $GITHUB_ENV | |
| echo "ISRELEASE=$ISRELEASE" >> $GITHUB_ENV | |
| - name: Update versions | |
| continue-on-error: true | |
| run: | | |
| python3 -m pip install beautifulsoup4 lxml | |
| eval $(ssh-agent -s) | |
| ssh-add - <<< "${{ secrets.CVC5_DOCS_RELEASE_TOKEN }}" | |
| git clone [email protected]:cvc5/docs.git target-releases/ | |
| TARGET_DIR= | |
| if [ "$ISRELEASE" = true ]; then | |
| TARGET_DIR=target-releases/$NAME | |
| else | |
| TARGET_DIR=target-releases/cvc5-main | |
| fi | |
| cp -r docs-new "${TARGET_DIR}" | |
| pushd target-releases/ | |
| python3 genversions.py | |
| popd | |
| cp -rf "${TARGET_DIR}" docs-new | |
| - name: Update docs | |
| continue-on-error: true | |
| run: | | |
| if [ -n "$NAME" ]; then | |
| eval $(ssh-agent -s) | |
| ssh-add - <<< "${{ secrets.CVC5_DOCS_TOKEN }}" | |
| git clone [email protected]:cvc5/docs-ci.git target/ | |
| cp -r docs-new target/docs-$NAME-$HASH | |
| cd target/ | |
| isdiff=$(diff -r -x "*.zip" docs-main/ docs-$NAME-$HASH >&2; echo $?; exit 0) | |
| if [[ ("$ISRELEASE" != true) && ($isdiff = 0) ]] | |
| then | |
| echo "Ignored run, documentation is the same as for current main" | |
| else | |
| rm -f docs-$NAME | |
| ln -s docs-$NAME-$HASH docs-$NAME | |
| git add docs-$NAME docs-$NAME-$HASH | |
| python3 genindex.py | |
| git add README.md | |
| git commit -m "Update docs for $NAME" | |
| git push | |
| fi | |
| else | |
| echo "Ignored run" | |
| fi | |
| - name: Update docs for release | |
| continue-on-error: true | |
| run: | | |
| if [ "$ISRELEASE" = true ]; then | |
| eval $(ssh-agent -s) | |
| ssh-add - <<< "${{ secrets.CVC5_DOCS_RELEASE_TOKEN }}" | |
| cd target-releases/ | |
| rm -f latest | |
| ln -s $NAME latest | |
| git add . | |
| git commit -m "Update docs for $NAME" | |
| git push | |
| else | |
| echo "Ignored run" | |
| fi |