Move docs upload to a different workflow (#6512)

This PR (finally, I hope) uses a proper setup for uploading the documentation. One of the CI jobs generates the documentation and stores it in an artifact. Another workflow is triggered (via workflow_run) and then uploads this artifact. Only this setup seems to properly work for PR builds.

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 92e4dca44b67d76fa067c882e126c7b4f4d60b43..cc5b0e995d024c4303a2ee4027c50dc1e5c668cc 100644 (file)
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -1,9 +1,8 @@
-on: [push, pull_request, pull_request_target]
+on: [push, pull_request]
 name: CI
 
 jobs:
   build:
-    if: ${{ github.event_name == 'push' || github.event_name == 'pull_request' }}
     strategy:
       matrix:
         include:
@@ -220,7 +219,11 @@ jobs:
 
     - name: Build Documentation
       if: matrix.build-documentation
-      run: make -j2 docs-gh
+      run: |
+        make -j2 docs-gh
+        if [ "${{ github.event_name }}" == "pull_request" ] ; then
+          echo "${{ github.event.number }}" > docs/sphinx-gh/prnum
+        fi
       working-directory: build
     
     - name: Store Documentation
@@ -229,67 +232,3 @@ jobs:
       with:
         name: documentation
         path: build/docs/sphinx-gh/
-
-  upload-docs:
-    if: github.event_name == 'push' || github.event_name == 'pull_request_target'
-    name: upload-docs
-    runs-on: ubuntu-latest
-    continue-on-error: true
-    needs: build
-    steps:
-      - 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: Setup Context
-        run: |
-          if [ "${{ github.event_name }}" == "push" ] ; then
-            NAME=$(echo "${GITHUB_REF}" | sed "s,refs/heads/,,")
-            HASH=${{ github.sha }}
-            echo "Identified branch $NAME"
-          elif [ "${{ github.event_name }}" == "pull_request_target" ] ; then
-            NAME="${{ github.event.number }}"
-            HASH="${{ github.event.pull_request.head.sha }}"
-            echo "Identified PR #$NAME (from $HASH)"
-            NAME="pr$NAME"
-          fi
-          echo "NAME=$NAME" >> $GITHUB_ENV
-          echo "HASH=$HASH" >> $GITHUB_ENV
-
-      - name: Clone Documentation Repository
-        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: Fetch artifact
-        uses: actions/download-artifact@v2
-        with:
-          name: documentation
-          path: docs-new
-
-      - name: Update docs
-        continue-on-error: true
-        env:
-            SSH_AUTH_SOCK: /tmp/ssh_agent.sock
-        run: |
-          if [ -n "$NAME" ]; then
-            mv docs-new target/docs-$NAME-$HASH
-            cd target/
-            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
-          else
-            echo "Ignored run"
-          fi

diff --git a/.github/workflows/docs_cleanup.yml b/.github/workflows/docs_cleanup.yml
index 0260b64748e1a9f1943ac303c8689623c512c8ec..67b5f6b4ac0ab26f23c8d222ac9b07bab0ec82b7 100644 (file)
--- a/.github/workflows/docs_cleanup.yml
+++ b/.github/workflows/docs_cleanup.yml
@@ -45,8 +45,10 @@ jobs:
           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
+          if [ -n "$last" ]; then
+            git rebase -Xtheirs --onto $first $last
+            git log
+          fi
       
       - name: Push
         env:

diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml
new file mode 100644 (file)
index 0000000..5b5ee32
--- /dev/null
+++ b/.github/workflows/docs_upload.yml
@@ -0,0 +1,89 @@
+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'
+    steps:
+      - 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 Documentation Repository
+        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: Download artifact
+        uses: actions/github-script@v3.1.0
+        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: Setup Context
+        run: |
+          HASH=${{ github.event.workflow_run.head_commit.id }}
+          if [ "${{ 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
+
+      - name: Update docs
+        continue-on-error: true
+        env:
+            SSH_AUTH_SOCK: /tmp/ssh_agent.sock
+        run: |
+          if [ -n "$NAME" ]; then
+            mv docs-new target/docs-$NAME-$HASH
+            cd target/
+            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
+          else
+            echo "Ignored run"
+          fi