Merge pull request #303 from per1234/check-head-sha

Require that PR head matches that of diff when merging

Author: per1234

.github/workflows/manage-prs.yml

@@ -42,14 +42,20 @@ jobs:
       artifact: ${{ steps.configuration.outputs.artifact }}
       path: ${{ steps.configuration.outputs.path }}
       filename: ${{ steps.configuration.outputs.filename }}
+      head: ${{ steps.head.outputs.head }}
+
+    env:
+      # See: https://docs.github.com/en/rest/reference/pulls#custom-media-types-for-pull-requests
+      DIFF_IDENTIFIER: diff
+      JSON_IDENTIFIER: raw+json
 
     steps:
       - name: Set configuration outputs
         id: configuration
         run: |
           echo "::set-output name=artifact::diff"
           echo "::set-output name=path::${{ runner.temp }}"
-          echo "::set-output name=filename::diff.txt"
+          echo "::set-output name=filename::${{ env.DIFF_IDENTIFIER }}"
 
       - name: Comment on comment trigger to provide feedback
         if: github.event_name == 'issue_comment'
@@ -67,18 +73,29 @@ jobs:
             |
             Hello! I'm checking your submission again.
 
-      - name: Get PR diff
+      - name: Get PR data
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
+          # Two API requests are necessary, one for the PR diff and another for the metadata.
           # It's necessary to reference both pull_request.number and issue.number because only one of the two are
           # defined depending on whether the workflow is triggered by PR or comment event.
-          curl \
-            --fail \
-            --output "${{ steps.configuration.outputs.path }}/${{ steps.configuration.outputs.filename }}" \
-            --header "Authorization: token $GITHUB_TOKEN" \
-            --header "Accept: application/vnd.github.v3.diff" \
-            https://api.github.com/repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }}${{ github.event.issue.number }}
+          parallel \
+            ' \
+              curl \
+                --fail \
+                --output "${{ steps.configuration.outputs.path }}/{}" \
+                --header "Authorization: token $GITHUB_TOKEN" \
+                --header "Accept: application/vnd.github.v3.{}" \
+                https://api.github.com/repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }}${{ github.event.issue.number }}
+            ' \
+            ::: \
+              ${{ env.DIFF_IDENTIFIER }} \
+              ${{ env.JSON_IDENTIFIER }}
+
+      - name: Get head SHA of diff
+        id: head
+        run: echo "::set-output name=head::$(jq -c .head.sha "${{ steps.configuration.outputs.path }}/${{ env.JSON_IDENTIFIER }}")"
 
       - name: Upload diff file to workflow artifact
         uses: actions/upload-artifact@v2
@@ -399,6 +416,7 @@ jobs:
 
   merge:
     needs:
+      - diff
       - parse
       - check-submissions-result
     # Only merge submissions that passed all checks
@@ -408,6 +426,7 @@ jobs:
     runs-on: ubuntu-latest
     outputs:
       pass: ${{ steps.merge.outcome == 'success' }}
+      status: ${{ steps.merge.outputs.status }}
 
     steps:
       - name: Approve pull request
@@ -432,6 +451,7 @@ jobs:
           owner: ${{ github.repository_owner }}
           repo: ${{ github.event.repository.name }}
           pull_number: ${{ github.event.pull_request.number }}${{ github.event.issue.number }}
+          sha: ${{ needs.diff.outputs.head }}
           merge_method: squash
 
       - name: Checkout index source branch
@@ -482,7 +502,8 @@ jobs:
     if: needs.merge.outputs.pass == 'false'
     runs-on: ubuntu-latest
     steps:
-      - name: Comment on merge failure
+      - name: Comment on merge conflict
+        if: needs.merge.outputs.status == '405'
         uses: octokit/[email protected]
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
@@ -500,6 +521,26 @@ jobs:
 
             Once that is done, it will be merged automatically.
 
+      - name: Comment on diff head/PR head mismatch
+        if: needs.merge.outputs.status == '409'
+        uses: octokit/[email protected]
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        with:
+          route: POST /repos/{owner}/{repo}/issues/{issue_number}/comments
+          owner: ${{ github.repository_owner }}
+          repo: ${{ github.event.repository.name }}
+          issue_number: ${{ github.event.pull_request.number }}${{ github.event.issue.number }}
+          body: |
+            |
+            It looks like there may have been an update to the pull request. If so, I'll check it again now.
+
+      - name: Fail on unidentified merge failure
+        if: >
+          needs.merge.outputs.status != '405' &&
+          needs.merge.outputs.status != '409'
+        run: exit 1 # Trigger the `unexpected-fail` job
+
   not-submission:
     needs:
       - parse