maintainer_bors.yml

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 }}
      COMMENT_EVENT: ${{ github.event.comment.body }}
      COMMENT_REVIEW: ${{ github.event.review.body }}
      PR_NUMBER: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
      HAS_DELEGATED_LABEL: ${{ contains(github.event.issue.labels.*.name, 'delegated') }}
    name: Add ready-to-merge or delegated label
    runs-on: ubuntu-latest
    if: github.repository == 'leanprover-community/mathlib4'
    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}"
          if [ "${AUTHOR}" == 'mathlib-bors[bot]' ] && [ "${HAS_DELEGATED_LABEL}" == 'true' ]
          then
            m_or_d="$(printf '%s' "${COMMENT}" |
              sed -n 's=^Build failed:=delegated=p' | head -1)"
          else
            m_or_d="$(printf '%s' "${COMMENT}" |
              sed -n 's=^bors  *\(merge\|r+\) *$=ready-to-merge=p; s=^bors  *\(delegate\|d+\|d\=\).*=delegated=p' | head -1)"
          fi

          remove_labels="$(printf '%s' "${COMMENT}" |
            sed -n 's=^bors  *\(merge\|r\|d\)- *$=remove-labels=p' | head -1)"

          printf $'"bors delegate" or "bors merge" found? \'%s\'\n' "${m_or_d}"
          printf $'"bors r-" or "bors d-" found? \'%s\'\n' "${remove_labels}"
          printf $'AUTHOR: \'%s\'\n' "${AUTHOR}"
          printf $'PR_NUMBER: \'%s\'\n' "${PR_NUMBER}"
          printf $'%s' "${PR_NUMBER}" | hexdump -cC

          printf $'mOrD=%s\n' "${m_or_d}" >> "${GITHUB_OUTPUT}"
          printf $'removeLabels=%s\n' "${remove_labels}" >> "${GITHUB_OUTPUT}"
          if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] ||
             [ "${AUTHOR}" == 'leanprover-community-bot-assistant' ] ||
             [ "${AUTHOR}" == 'mathlib-bors[bot]' ]
          then
            printf $'bot=true\n'
            printf $'bot=true\n' >> "${GITHUB_OUTPUT}"
            BOT='true'
          else
            printf $'bot=false\n'
            printf $'bot=false\n' >> "${GITHUB_OUTPUT}"
            BOT='false'
          fi

          # write an artifact with all data needed below if we don't have access to necessary secrets
          if [[ -z '${{ secrets.TRIAGE_TOKEN }}' ]]
          then
            printf 'No access to secrets, writing to file.\n'
            jq -n \
              --arg author "${AUTHOR}" \
              --arg pr_number "${PR_NUMBER}" \
              --arg comment "${COMMENT}" \
              --arg bot "${BOT}" \
              --arg remove_labels "${remove_labels}" \
              --arg m_or_d "${m_or_d}" \
              '{
                author: $author,
                pr_number: $pr_number,
                comment: $comment,
                bot: $bot,
                remove_labels: $remove_labels,
                m_or_d: $m_or_d,
              }' > artifact-data.json
            echo "Generated JSON artifact:"
            cat artifact-data.json

            printf 'secrets=' >> "${GITHUB_OUTPUT}"
            exit 0
          else
            printf 'secrets=true\n' >> "${GITHUB_OUTPUT}"
          fi

      # upload artifact if we have no access to secrets
      - if: ${{ steps.merge_or_delegate.outputs.secrets == '' &&
          (! steps.merge_or_delegate.outputs.mOrD == '' || ! steps.merge_or_delegate.outputs.removeLabels == '') }}
        name: Upload artifact
        uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
        with:
          name: workflow-data
          path: artifact-data.json
          retention-days: 5

      # Run the following steps only if we have access to secrets / write perms on GITHUB_TOKEN
      - name: Check whether user is a mathlib admin
        id: user_permission
        if: ${{ ! steps.merge_or_delegate.outputs.secrets == '' &&
          (! steps.merge_or_delegate.outputs.mOrD == '' || ! steps.merge_or_delegate.outputs.removeLabels == '') }}
        uses: actions-cool/check-user-permission@7b90a27f92f3961b368376107661682c441f6103 # v2.3.0
        with:
          require: 'admin'

      - name: Add ready-to-merge or delegated label
        id: add_label
        if: ${{ ! steps.merge_or_delegate.outputs.secrets == '' &&
          (! steps.merge_or_delegate.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.merge_or_delegate.outputs.bot == 'true' )) }}
        uses: octokit/request-action@dad4362715b7fb2ddedf9772c8670824af564f0d # v2.4.0
        with:
          route: POST /repos/:repository/issues/:issue_number/labels
          # Unexpected input warning from the following is expected:
          # https://github.com/octokit/request-action?tab=readme-ov-file#warnings
          repository: ${{ github.repository }}
          issue_number: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
          labels: '["${{ steps.merge_or_delegate.outputs.mOrD }}"]'
        env:
          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}

      - if: ${{ ! steps.merge_or_delegate.outputs.secrets == '' &&
          (! 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" and "maintainer-merge"
        # 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: |
          for label in awaiting-author maintainer-merge; do
            curl --request DELETE \
              --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/${label}" \
              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
          done

      - name: On bors r/d-, remove ready-to-merge or delegated label
        if: ${{ ! steps.merge_or_delegate.outputs.secrets == '' &&
          (! steps.merge_or_delegate.outputs.removeLabels == '' &&
          steps.user_permission.outputs.require-result == 'true') }}
        # 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: |
          for label in ready-to-merge delegated; do
            curl --request DELETE \
              --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/${label}" \
              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
          done

      - name: Set up Python
        if: ${{ ! steps.merge_or_delegate.outputs.secrets == '' &&
          (! steps.merge_or_delegate.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.merge_or_delegate.outputs.bot == 'true' )) }}
        uses: actions/setup-python@83679a892e2d95755f2dac6acb0bfd1e9ac5d548 # v6.1.0
        with:
          python-version: '3.x'

      - name: Install dependencies
        if: ${{ ! steps.merge_or_delegate.outputs.secrets == '' &&
          (! steps.merge_or_delegate.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.merge_or_delegate.outputs.bot == 'true' )) }}
        run: |
          python -m pip install --upgrade pip
          pip install zulip

      - if: ${{ ! steps.merge_or_delegate.outputs.secrets == '' &&
          (! steps.merge_or_delegate.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.merge_or_delegate.outputs.bot == 'true' )) }}
        uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
        with:
          ref: master
          sparse-checkout: |
            scripts/zulip_emoji_reactions.py

      - name: update zulip emoji reactions
        if: ${{ ! steps.merge_or_delegate.outputs.secrets == '' &&
          (! steps.merge_or_delegate.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.merge_or_delegate.outputs.bot == 'true' )) }}
        env:
          ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
          ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
          ZULIP_SITE: https://leanprover.zulipchat.com
        run: |
          python scripts/zulip_emoji_reactions.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"