maintainer_merge_comment.yml

name: Maintainer merge (comment)

on:
  issue_comment:
    types: [created, edited]

jobs:
  ping_zulip:
    name: Ping maintainers on Zulip
    if: github.event.issue.pull_request && (startsWith(github.event.comment.body, 'maintainer merge') || contains(toJSON(github.event.comment.body), '\nmaintainer merge'))
    runs-on: ubuntu-latest
    steps:
      - name: Check whether user is part of mathlib-reviewers team
        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.

      - uses: actions/checkout@v4
        with:
          ref: master
      - name: Determine Zulip topic
        id: determine_topic
        run: |
          ./scripts/get_tlabel.sh "${PR}" >> "$GITHUB_OUTPUT"
        env:
          PR:  /repos/leanprover-community/mathlib4/issues/${{ github.event.issue.number }}
          GH_TOKEN: ${{secrets.GITHUB_TOKEN}}

      - name: Send message on Zulip
        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: |
            ${{ format('{0} requested a maintainer merge from comment on PR [#{1}]({2}):', github.event.comment.user.login, github.event.issue.number, github.event.issue.html_url ) }}

            > ${{ github.event.issue.title }}

      - name: Add comment to PR
        uses: GrantBirki/comment@v2
        with:
          issue-number: ${{ github.event.issue.number }}
          body: |
            🚀 Pull request has been placed on the maintainer queue by ${{ github.event.comment.user.login }}.
      - name: Add label to PR
        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'] });