add_label_from_review.yml

name: Add "ready-to-merge" and "delegated" label from PR review

on:
  pull_request_review:
    types: [submitted]

jobs:
  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), '\nbors r+') || startsWith(github.event.review.body, 'bors merge') || contains(toJSON(github.event.review.body), '\nbors merge'))
    runs-on: ubuntu-latest
    steps:
      - id: user_permission
        uses: actions-cool/check-user-permission@v2
        with:
          require: 'write'
          token: ${{ secrets.TRIAGE_TOKEN }}

      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.review.user.login == 'leanprover-community-mathlib4-bot') || (github.event.review.user.login == 'leanprover-community-bot-assistant')
        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: '["ready-to-merge"]'
        env:
          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}

      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.review.user.login == 'leanprover-community-mathlib4-bot') || (github.event.review.user.login == 'leanprover-community-bot-assistant')
        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/${{ github.event.pull_request.number }}/labels/awaiting-author \
            --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'

  add_delegated_label:
    name: Add delegated label
    if: (startsWith(github.event.review.body, 'bors d') || contains(toJSON(github.event.review.body), '\nbors d'))
    runs-on: ubuntu-latest
    steps:
      - id: user_permission
        uses: actions-cool/check-user-permission@v2
        with:
          require: 'write'
          token: ${{ secrets.TRIAGE_TOKEN }}

      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.review.user.login == 'leanprover-community-mathlib4-bot') || (github.event.review.user.login == 'leanprover-community-bot-assistant')
        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.TRIAGE_TOKEN }}