maintainer_merge.yml

name: Maintainer merge

# triggers the action when
on:
  # the PR receives a comment
  issue_comment:
    types: [created, edited]
  # 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, edited]

jobs:
  ping_zulip:
    # 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_AUTHOR: ${{ github.event.issue.user.login }}${{ github.event.pull_request.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: Ping maintainers on Zulip
    runs-on: ubuntu-latest
    steps:
      - name: Find maintainer merge/delegate
        id: merge_or_delegate
        run: |
          echo "PR author: ${PR_AUTHOR}"
          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}" |
            # captures `maintainer merge/delegate` as well as an optional `?`, ignoring subsequent spaces
            sed -n 's=^maintainer  *\(merge\|delegate\)\(?\?\) *$=\1\2=p' | head -1)"

          printf $'"maintainer delegate" or "maintainer merge" found? \'%s\'\n' "${m_or_d}"

          printf $'mOrD=%s\n' "${m_or_d}" > "${GITHUB_OUTPUT}"

      - name: Check whether user is part of mathlib-reviewers team
        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
        uses: TheModdingInquisition/actions-team-membership@v1.0
        with:
          organization: 'leanprover-community'
          team: 'mathlib-reviewers' # required. The team to check for
          token: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # required. Personal Access Token with the `read:org` permission
          comment: 'You seem to not be authorized' # optional. A comment to post if the user is not part of the team.
                                                   # This feature is only applicable in an issue (or PR) context
          exit: true # optional. If the action should exit if the user is not part of the team. Defaults to true.

      - name: Checkout
        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
        uses: actions/checkout@v4

      - name: Determine Zulip topic
        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
        id: determine_topic
        run: |
          ./scripts/get_tlabel.sh "/repos/leanprover-community/mathlib4/issues/${PR_NUMBER}" >> "$GITHUB_OUTPUT"
        env:
          GH_TOKEN: ${{secrets.GITHUB_TOKEN}}

      - name: Form the message
        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
        id: form_the_message
        run: |
          # for debugging, we print the available variables
          echo "github.event.action: '${{ github.event.action }}'"

          echo ""
          message="$(
            ./scripts/maintainer_merge_message.sh "${AUTHOR}" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${EVENT_NAME}" "${PR_NUMBER}" "${PR_URL}" "${PR_TITLE_ISSUE}${PR_TITLE_PR}" "${COMMENT_EVENT}${COMMENT_REVIEW}" "${PR_AUTHOR}"
          )"
          printf 'title<<EOF\n%s\nEOF' "${message}" | tee "$GITHUB_OUTPUT"

      - name: Send message on Zulip
        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
        uses: zulip/github-actions-zulip/send-message@v1
        with:
          api-key: ${{ secrets.ZULIP_API_KEY }}
          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
          organization-url: 'https://leanprover.zulipchat.com'
          to: 'mathlib reviewers'
          type: 'stream'
          topic: ${{ steps.determine_topic.outputs.topic }}
          content: ${{ steps.form_the_message.outputs.title }}

      - name: Add comment to PR
        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
        uses: GrantBirki/comment@v2
        with:
          # if a comment triggers the action, then `issue.number` is set
          # if a review or review comment triggers the action, then `pull_request.number` is set
          issue-number: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
          body: |
            🚀 Pull request has been placed on the maintainer queue by ${{ github.event.comment.user.login }}${{ github.event.review.user.login }}.

      - name: Add label to PR
        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
        uses: actions/github-script@v7
        with:
          github-token: ${{secrets.GITHUB_TOKEN}}
          script: |
            const { owner, repo, number: issue_number } = context.issue;
            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['maintainer-merge'] });