Fix docs upload once again (#7997)

This PR finally sorts out the ambiguity of different commits from PRs, tags and regular branches (fingers crossed).

diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml
index d23d3ea68d7fac52f62dd7527d64ae61f2c4edcd..38a6432a548257a6482b1ae2c6df76f2ad12b160 100644 (file)
--- a/.github/workflows/docs_upload.yml
+++ b/.github/workflows/docs_upload.yml
@@ -48,25 +48,37 @@ jobs:
           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 master) 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 }}
-          ISTAG=${{ github.ref_name != github.event.workflow_run.head_branch }}
-          if [ "$ISTAG" = true ] ; then
+          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"
-          elif [ "${{ 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"
           fi
           echo "NAME=$NAME" >> $GITHUB_ENV
           echo "HASH=$HASH" >> $GITHUB_ENV
-          echo "ISTAG=$ISTAG" >> $GITHUB_ENV
+          echo "ISRELEASE=$ISRELEASE" >> $GITHUB_ENV
 
       - name: Update docs
         continue-on-error: true
@@ -81,7 +93,7 @@ jobs:
 
             isdiff=$(diff -r -x "*.zip" docs-master/ docs-$NAME-$HASH >&2; echo $?; exit 0)
 
-            if [[ ("$ISTAG" != true) && ($isdiff = 0) ]]
+            if [[ ("$ISRELEASE" != true) && ($isdiff = 0) ]]
             then
               echo "Ignored run, documentation is the same as for current master"
             else
@@ -102,7 +114,7 @@ jobs:
       - name: Update docs for release
         continue-on-error: true
         run: |
-          if [ "$ISTAG" = true ]; then
+          if [ "$ISRELEASE" = true ]; then
             eval $(ssh-agent -s)
             ssh-add - <<< "${{ secrets.CVC5_DOCS_RELEASE_TOKEN }}"