chore(.github/workflows): add delegated tag on comment (#7251)

This automation should hopefully add the "delegated" tag if a maintainer types `bors d+` or `bors d=`. (In fact, it will apply the label if it sees any line starting with `bors d`, since `bors delegate+`, etc. are also allowed).
leanprover-community · Apr 22, 2021 · 6deafc2 · 6deafc2
1 parent f68645f
commit 6deafc2
Show file tree

Hide file tree

Showing 2 changed files with 140 additions and 6 deletions.
diff --git a/.github/workflows/add_label_from_comment.yml b/.github/workflows/add_label_from_comment.yml
@@ -1,12 +1,12 @@
-name: Add "ready-to-merge" label from comment
+name: Add "ready-to-merge" and "delegated" label from comment
 
 on:
   issue_comment:
     types: [created]
 
 jobs:
-  add_label:
-    name: Add label
+  add_ready_to_merge_label:
+    name: Add ready-to-merge label
     if: (toJSON(github.event.issue.pull_request) != 'null') && (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\r\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\r\nbors merge'))
     runs-on: ubuntu-latest
     steps:
@@ -74,3 +74,70 @@ jobs:
           curl --request DELETE \
             --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-author \
             --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+
+  add_delegated_label:
+    name: Add delegated label
+    if: (toJSON(github.event.issue.pull_request) != 'null') && (startsWith(github.event.comment.body, 'bors d') || contains(toJSON(github.event.comment.body), '\r\nbors d')
+    runs-on: ubuntu-latest
+    steps:
+      - uses: octokit/request-action@v2.x
+        name: Get PR head
+        id: get_pr_head
+        with:
+          route: GET /repos/:repository/pulls/:pull_number
+          repository: ${{ github.repository }}
+          pull_number: ${{ github.event.issue.number }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      # Parse steps.get_pr_head.outputs.data, since it is a string
+      - id: parse_pr_head
+        name: Parse PR head
+        uses: gr2m/get-json-paths-action@v1.x
+        with:
+          json: ${{ steps.get_pr_head.outputs.data }}
+          head_user: 'head.user.login'
+
+      # we skip the rest if this PR is from a fork,
+      # since the GITHUB_TOKEN doesn't have write perms
+      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
+        uses: octokit/request-action@v2.x
+        name: Get comment author
+        id: get_user
+        with:
+          route: GET /repos/:repository/collaborators/:username/permission
+          repository: ${{ github.repository }}
+          username: ${{ github.event.comment.user.login }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      # Parse steps.get_user.outputs.data, since it is a string
+      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
+        id: parse_user
+        name: Parse comment author permission
+        uses: gr2m/get-json-paths-action@v1.x
+        with:
+          json: ${{ steps.get_user.outputs.data }}
+          permission: 'permission'
+
+      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+        uses: octokit/request-action@v2.x
+        id: add_label
+        name: Add label
+        with:
+          route: POST /repos/:repository/issues/:issue_number/labels
+          repository: ${{ github.repository }}
+          issue_number: ${{ github.event.issue.number }}
+          labels: '["delegated"]'
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+        id: remove_labels
+        name: Remove "awaiting-review"
+        # we use curl rather than octokit/request-action so that the job won't fail
+        # (and send an annoying email) if the labels don't exist
+        run: |
+          curl --request DELETE \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-review \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
diff --git a/.github/workflows/add_label_from_review.yml b/.github/workflows/add_label_from_review.yml
@@ -1,12 +1,12 @@
-name: Add "ready-to-merge" label from PR review
+name: Add "ready-to-merge" and "delegated" label from PR review
 
 on:
   pull_request_review:
     types: [submitted]
 
 jobs:
-  add_label:
-    name: Add label
+  add_ready_to_merge_label:
+    name: Add ready-to-merge label
     if: (startsWith(github.event.review.body, 'bors r+') || contains(toJSON(github.event.review.body), '\r\nbors r+') || startsWith(github.event.review.body, 'bors merge') || contains(toJSON(github.event.review.body), '\r\nbors merge'))
     runs-on: ubuntu-latest
     steps:
@@ -74,3 +74,70 @@ jobs:
           curl --request DELETE \
             --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/awaiting-author \
             --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+            
+  add_delegated_label:
+    name: Add delegated label
+    if: (startsWith(github.event.review.body, 'bors d') || contains(toJSON(github.event.review.body), '\r\nbors d')
+    runs-on: ubuntu-latest
+    steps:
+      - uses: octokit/request-action@v2.x
+        name: Get PR head
+        id: get_pr_head
+        with:
+          route: GET /repos/:repository/pulls/:pull_number
+          repository: ${{ github.repository }}
+          pull_number: ${{ github.event.pull_request.number }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      # Parse steps.get_pr_head.outputs.data, since it is a string
+      - id: parse_pr_head
+        name: Parse PR head
+        uses: gr2m/get-json-paths-action@v1.x
+        with:
+          json: ${{ steps.get_pr_head.outputs.data }}
+          head_user: 'head.user.login'
+
+      # we skip the rest if this PR is from a fork,
+      # since the GITHUB_TOKEN doesn't have write perms
+      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
+        uses: octokit/request-action@v2.x
+        name: Get comment author
+        id: get_user
+        with:
+          route: GET /repos/:repository/collaborators/:username/permission
+          repository: ${{ github.repository }}
+          username: ${{ github.event.review.user.login }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      # Parse steps.get_user.outputs.data, since it is a string
+      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
+        id: parse_user
+        name: Parse comment author permission
+        uses: gr2m/get-json-paths-action@v1.x
+        with:
+          json: ${{ steps.get_user.outputs.data }}
+          permission: 'permission'
+
+      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+        uses: octokit/request-action@v2.x
+        id: add_label
+        name: Add label
+        with:
+          route: POST /repos/:repository/issues/:issue_number/labels
+          repository: ${{ github.repository }}
+          issue_number: ${{ github.event.pull_request.number }}
+          labels: '["delegated"]'
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+        id: remove_labels
+        name: Remove "awaiting-review"
+        # we use curl rather than octokit/request-action so that the job won't fail
+        # (and send an annoying email) if the labels don't exist
+        run: |
+          curl --request DELETE \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/awaiting-review \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'