Skip to content

Upload Docs

Upload Docs #269

Workflow file for this run

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/[email protected]
with:
script: |
var artifacts = await github.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.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 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
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/
cp -r docs-new target-releases/$NAME
cd target-releases/
rm -f latest
ln -s $NAME latest
python3 genversions.py
git add .
git commit -m "Update docs for $NAME"
git push
else
echo "Ignored run"
fi