Require that PR head matches that of diff when merging

Due to the limitations imposed by by using both `pull_request_target` and `issue_comment` events to trigger the
"Manage PRs" workflow, the PR diff used for the validation is procured via a GitHub API request.

It is necessary to check that the pull request state matches that of the diff, which is achieved via the `sha` parameter
of the GitHub API request used to merge. This can not be determined from the `github` context provided by GitHub Actions
to the workflow for either of the trigger events, so the pull request metadata is requested from the GitHub API at the
same time as the diff.

This situation requires different handling by the `merge-fail` job. Fortunately, the two failure causes result in
different values from the merge request workflow step's `status` output.

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
@@ -433,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
@@ -502,8 +521,24 @@ 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'
+        if: >
+          needs.merge.outputs.status != '405' &&
+          needs.merge.outputs.status != '409'
         run: exit 1 # Trigger the `unexpected-fail` job
 
   not-submission: