[Merged by Bors] - feat(CI): add emoji to maintainer merge'd PRs also

.github/workflows/zulip_emoji_maintainer_merge.yaml

@@ -0,0 +1,34 @@
+on:
+  pull_request:
+    types: [labeled, unlabeled]
+jobs:
+  set_pr_emoji:
+    if: github.event.label.name == 'maintainer-merge'
+    runs-on: ubuntu-latest
+    steps:
+    - name: Checkout mathlib repository
+      uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      with:
+          sparse-checkout: |
+            scripts/zulip_emoji_merge_delegate.py
+
+    - name: Set up Python
+      uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+      with:
+        python-version: '3.x'
+
+    - name: Install dependencies
+      run: |
+        python -m pip install --upgrade pip
+        pip install zulip
+
+    - name: Add or remove emoji
+      env:
+        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+        ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
+        ZULIP_SITE: https://leanprover.zulipchat.com
+        PR_NUMBER: ${{ github.event.number}}
+        LABEL_STATUS: ${{ github.event.action }}
+      run: |
+        printf $'Running the python script with pr "%s"\n' "$PR_NUMBER"
+        python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$PR_NUMBER"

scripts/zulip_emoji_merge_delegate.py

@@ -72,6 +72,7 @@
     has_bors = any(reaction['emoji_name'] == 'bors' for reaction in reactions)
     has_merge = any(reaction['emoji_name'] == 'merge' for reaction in reactions)
     has_awaiting_author = any(reaction['emoji_name'] == 'writing' for reaction in reactions)
+    has_maintainer_merge = any(reaction['emoji_name'] == 'hammer' for reaction in reactions)
     has_closed = any(reaction['emoji_name'] == 'closed-pr' for reaction in reactions)
     first_in_thread = hashPR.search(message['subject']) and message['display_recipient'] == 'PR reviews' and message['subject'] not in first_by_subject
     first_by_subject[message['subject']] = message['id']
@@ -105,6 +106,13 @@
                 "emoji_name": "merge"
             })
             print(f"result: '{result}'")
+        if has_maintainer_merge:
+            print('Removing maintainer-merge')
+            result = client.remove_reaction({
+                "message_id": message['id'],
+                "emoji_name": "hammer"
+            })
+            print(f"result: '{result}'")
         if has_awaiting_author:
             print('Removing awaiting-author')
             result = client.remove_reaction({
@@ -137,6 +145,12 @@
                 "message_id": message['id'],
                 "emoji_name": "peace_sign"
             })
+        elif 'maintainer-merge' == LABEL:
+            print('adding maintainer-merge')
+            client.add_reaction({
+                "message_id": message['id'],
+                "emoji_name": "hammer"
+            })
         elif LABEL == 'labeled':
             print('adding awaiting-author')
             client.add_reaction({