From f461d1e7a7161ade721c81199ec8ca7fd46173f5 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 2 May 2025 10:22:29 +0200 Subject: [PATCH 1/3] feat(CI): add emoji to maintainer merge'd PRs also The zulip bot reacts to all label changes, including arbitrary users setting that label. That seems harmless: the emoji is only informational, and the effect of false marking a PR with the label may simply be that it doesn't reviewed as well. --- .../zulip_emoji_maintainer_merge.yaml | 34 +++++++++++++++++++ scripts/zulip_emoji_merge_delegate.py | 14 ++++++++ 2 files changed, 48 insertions(+) create mode 100644 .github/workflows/zulip_emoji_maintainer_merge.yaml diff --git a/.github/workflows/zulip_emoji_maintainer_merge.yaml b/.github/workflows/zulip_emoji_maintainer_merge.yaml new file mode 100644 index 00000000000000..778dd6050c91f2 --- /dev/null +++ b/.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" diff --git a/scripts/zulip_emoji_merge_delegate.py b/scripts/zulip_emoji_merge_delegate.py index 6af3ff60d60f2e..aa500e87b09bd0 100644 --- a/scripts/zulip_emoji_merge_delegate.py +++ b/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({ From 20125e631d273b30e8a577a9b768487ce921eac4 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 2 May 2025 11:57:28 +0200 Subject: [PATCH 2/3] Also print LABEL_STATUS --- .github/workflows/zulip_emoji_awaiting_author.yaml | 2 +- .github/workflows/zulip_emoji_maintainer_merge.yaml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/zulip_emoji_awaiting_author.yaml b/.github/workflows/zulip_emoji_awaiting_author.yaml index 441218a6aef60b..6eae06b53ff7c5 100644 --- a/.github/workflows/zulip_emoji_awaiting_author.yaml +++ b/.github/workflows/zulip_emoji_awaiting_author.yaml @@ -30,5 +30,5 @@ jobs: PR_NUMBER: ${{ github.event.number}} LABEL_STATUS: ${{ github.event.action }} run: | - printf $'Running the python script with pr "%s"\n' "$PR_NUMBER" + printf $'Running the python script with pr "%s"\n' "$PR_NUMBER" "$LABEL_STATUS" python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$PR_NUMBER" diff --git a/.github/workflows/zulip_emoji_maintainer_merge.yaml b/.github/workflows/zulip_emoji_maintainer_merge.yaml index 778dd6050c91f2..7f491bbf99b032 100644 --- a/.github/workflows/zulip_emoji_maintainer_merge.yaml +++ b/.github/workflows/zulip_emoji_maintainer_merge.yaml @@ -30,5 +30,5 @@ jobs: PR_NUMBER: ${{ github.event.number}} LABEL_STATUS: ${{ github.event.action }} run: | - printf $'Running the python script with pr "%s"\n' "$PR_NUMBER" + printf $'Running the python script with pr "%s"\n' "$PR_NUMBER" "$LABEL_STATUS" python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$PR_NUMBER" From e2a5289bd7577ba7c14e7f46cb5fc8adec54c75b Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 2 May 2025 11:59:05 +0200 Subject: [PATCH 3/3] refactor: consolidate in one workflow, and rename --- ...author.yaml => zulip_emoji_labelling.yaml} | 4 ++- .../zulip_emoji_maintainer_merge.yaml | 34 ------------------- 2 files changed, 3 insertions(+), 35 deletions(-) rename .github/workflows/{zulip_emoji_awaiting_author.yaml => zulip_emoji_labelling.yaml} (82%) delete mode 100644 .github/workflows/zulip_emoji_maintainer_merge.yaml diff --git a/.github/workflows/zulip_emoji_awaiting_author.yaml b/.github/workflows/zulip_emoji_labelling.yaml similarity index 82% rename from .github/workflows/zulip_emoji_awaiting_author.yaml rename to .github/workflows/zulip_emoji_labelling.yaml index 6eae06b53ff7c5..52fae3a3b3a43b 100644 --- a/.github/workflows/zulip_emoji_awaiting_author.yaml +++ b/.github/workflows/zulip_emoji_labelling.yaml @@ -2,8 +2,10 @@ on: pull_request: types: [labeled, unlabeled] jobs: + # When a PR is (un)labelled with awaiting-author or maintainer-merge, + # add resp. remove the matching emoji reaction from zulip messages. set_pr_emoji: - if: github.event.label.name == 'awaiting-author' + if: github.event.label.name == 'awaiting-author' || github.event.label.name == 'maintainer-merge' runs-on: ubuntu-latest steps: - name: Checkout mathlib repository diff --git a/.github/workflows/zulip_emoji_maintainer_merge.yaml b/.github/workflows/zulip_emoji_maintainer_merge.yaml deleted file mode 100644 index 7f491bbf99b032..00000000000000 --- a/.github/workflows/zulip_emoji_maintainer_merge.yaml +++ /dev/null @@ -1,34 +0,0 @@ -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" "$LABEL_STATUS" - python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$PR_NUMBER"