docs_upload.yml

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 git@github.com: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 git@github.com: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