feat(CI): merge bors (#19078)

Unify the three `bors d`, `bors merge` and `bord r+` actions into a single one.

Prefer using `TRIAGE` token for GH API quota.

.github/workflows/maintainer_bors.yml

@@ -0,0 +1,93 @@
+name: Add "ready-to-merge" and "delegated" label
+
+# triggers the action when
+on:
+  # the PR receives a comment
+  issue_comment:
+    types: [created]
+  # the PR receives a review
+  pull_request_review:
+    # whether or not it is accompanied by a comment
+    types: [submitted]
+  # the PR receives a review comment
+  pull_request_review_comment:
+    types: [created]
+
+jobs:
+  add_ready_to_merge_label:
+    # we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not
+    # both set simultaneously: depending on the event that triggers the PR, usually only one is set
+    env:
+      AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }}
+      PR_NUMBER: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
+      COMMENT_EVENT: ${{ github.event.comment.body }}
+      COMMENT_REVIEW: ${{ github.event.review.body }}
+      PR_TITLE_ISSUE: ${{ github.event.issue.title }}
+      PR_TITLE_PR: ${{ github.event.pull_request.title }}
+      PR_URL: ${{ github.event.issue.html_url }}${{ github.event.pull_request.html_url }}
+      EVENT_NAME: ${{ github.event_name }}
+    name: Add ready-to-merge or delegated label
+    runs-on: ubuntu-latest
+    steps:
+      - name: Find bors merge/delegate
+        id: merge_or_delegate
+        run: |
+          COMMENT="${COMMENT_EVENT}${COMMENT_REVIEW}"
+          # we strip `\r` since line endings from GitHub contain this character
+          COMMENT="${COMMENT//$'\r'/}"
+          # for debugging, we print some information
+          printf '%s' "${COMMENT}" | hexdump -cC
+          printf 'Comment:"%s"\n' "${COMMENT}"
+          m_or_d="$(printf '%s' "${COMMENT}" |
+            sed -n 's=^bors  *\(merge\|r+\) *$=ready-to-merge=p; s=^bors  *d.*=delegated=p' | head -1)"
+
+          printf $'"bors delegate" or "bors merge" found? \'%s\'\n' "${m_or_d}"
+
+          printf $'mOrD=%s\n' "${m_or_d}" > "${GITHUB_OUTPUT}"
+          if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] ||
+             [ "${AUTHOR}" == 'leanprover-community-bot-assistant' ]
+          then
+            printf $'bot=true\n'
+            printf $'bot=true\n' > "${GITHUB_OUTPUT}"
+          else
+            printf $'bot=false\n'
+            printf $'bot=false\n' > "${GITHUB_OUTPUT}"
+          fi
+
+      - name: Check whether user is a mathlib admin
+        id: user_permission
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
+        uses: actions-cool/check-user-permission@v2
+        with:
+          require: 'admin'
+          # review(_comment) use
+          # require: 'write'
+          # token: ${{ secrets.TRIAGE_TOKEN }}
+
+      - name: Add ready-to-merge or delegated label
+        id: add_label
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
+          ( steps.user_permission.outputs.require-result == 'true' ||
+            steps.merge_or_delegate.outputs.bot == 'true' ) }}
+        uses: octokit/[email protected]
+        with:
+          # check is this ok? was /repos/:repository/issues/:issue_number/labels
+          route: POST /repos/:repository/issues/${PR_NUMBER}/labels
+          repository: ${{ github.repository }}
+          issue_number: ${PR_NUMBER}
+          labels: '["${{ steps.merge_or_delegate.outputs.mOrD }}"]'
+        env:
+          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }} # comment uses ${{ secrets.GITHUB_TOKEN }}
+
+      - if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
+          ( steps.user_permission.outputs.require-result == 'true' ||
+            steps.merge_or_delegate.outputs.bot == 'true' ) }}
+        id: remove_labels
+        name: Remove "awaiting-author"
+        # 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/${PR_NUMBER}/labels/awaiting-author" \
+            --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+            # comment uses ${{ secrets.GITHUB_TOKEN }}