From 4438086b2efc4fd35e94b6c110953bf0e3364bb0 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Sun, 27 Jul 2025 17:20:50 -0400 Subject: [PATCH 1/5] fix: do not remove reactions if the corresponding label is still present on the PR cf. https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/merge.2Fdelegate.20emojis.20bot/near/528289834 --- .github/workflows/zulip_emoji_labelling.yaml | 5 ++- scripts/zulip_emoji_reactions.py | 42 ++++++++++++++------ 2 files changed, 32 insertions(+), 15 deletions(-) diff --git a/.github/workflows/zulip_emoji_labelling.yaml b/.github/workflows/zulip_emoji_labelling.yaml index 8cee6d08a40f9b..80a747fef6ff68 100644 --- a/.github/workflows/zulip_emoji_labelling.yaml +++ b/.github/workflows/zulip_emoji_labelling.yaml @@ -40,6 +40,7 @@ jobs: PR_NUMBER: ${{ github.event.number}} LABEL_STATUS: ${{ github.event.action }} LABEL_NAME: ${{ github.event.label.name }} + PR_LABELS: ${{ github.event.pull_request.labels.*.name }} run: | - printf $'Running the python script with pr "%s"\n' "$PR_NUMBER" "$LABEL_STATUS" "$LABEL" - python scripts/zulip_emoji_reactions.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$LABEL_NAME" "$PR_NUMBER" + printf $'Running the python script with pr "%s"\n' "$PR_NUMBER" "$LABEL_STATUS" "$LABEL" "$PR_LABELS" + python scripts/zulip_emoji_reactions.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$LABEL_NAME" "$PR_NUMBER" "$PR_LABELS" diff --git a/scripts/zulip_emoji_reactions.py b/scripts/zulip_emoji_reactions.py index fd2f9b400082df..dd722f3cb7774f 100644 --- a/scripts/zulip_emoji_reactions.py +++ b/scripts/zulip_emoji_reactions.py @@ -2,12 +2,15 @@ import sys import zulip import re +import json # Usage: -# python scripts/zulip_emoji_reactions.py $ZULIP_API_KEY $ZULIP_EMAIL $ZULIP_SITE $ACTION $LABEL_NAME $PR_NUMBER +# python scripts/zulip_emoji_reactions.py $ZULIP_API_KEY $ZULIP_EMAIL $ZULIP_SITE $ACTION $LABEL_NAME $PR_NUMBER $PR_LABELS # The first three variables identify the lean4 Zulip chat and allow the bot to access it # (see .github/workflows/zulip_emoji_merge_delegate.yaml), # see the comment below for a description of $ACTION and $LABEL_NAME. +# $PR_LABELS is optional, but if present, should be a JSON array of label names +# (see .github/workflows/zulip_emoji_labelling.yaml) ZULIP_API_KEY = sys.argv[1] ZULIP_EMAIL = sys.argv[2] @@ -32,6 +35,15 @@ print(f"ACTION: '{ACTION}'") print(f"LABEL_NAME: '{LABEL_NAME}'") print(f"PR_NUMBER: '{PR_NUMBER}'") +try: + PR_LABELS = sys.argv[7] + print(f"Attempting to parse PR_LABELS: '{PR_LABELS}") + PR_LABELS = json.loads(PR_LABELS) + assert isinstance(PR_LABELS, list) +except: + print(f"parsing PR_LABELS failed; setting to None") + PR_LABELS = None +print(f"PR_LABELS: '{PR_LABELS}'") # Initialize Zulip client client = zulip.Client( @@ -101,14 +113,18 @@ def has_reaction(name: str) -> bool: if match: print(f"matched: '{message}'") - def remove_reaction(name: str, emoji_name: str, **kwargs) -> None: + def remove_reaction(name: str, emoji_name: str, label_name: str, **kwargs) -> None: + # We do not remove an emoji if the corresponding label is still present. print(f'Removing {name}') - result = client.remove_reaction({ - "message_id": message['id'], - "emoji_name": emoji_name, - **kwargs - }) - print(f"result: '{result}'") + if label_name not in PR_LABELS: + result = client.remove_reaction({ + "message_id": message['id'], + "emoji_name": emoji_name, + **kwargs + }) + print(f"result: '{result}'") + else: + print(f'The "{label_name}" label is present, so we will not remove the "{name}" reaction.') def add_reaction(name: str, emoji_name: str) -> None: print(f'adding {name} emoji') client.add_reaction({ @@ -131,16 +147,16 @@ def add_reaction(name: str, emoji_name: str) -> None: # If the emoji is a custom emoji, add the fields `emoji_code` and `reaction_type` as well. print("Removing previous reactions, if present.") if has_peace_sign: - remove_reaction('delegated', 'peace_sign') + remove_reaction('delegated', 'peace_sign', 'delegated') if has_bors: - remove_reaction("bors", "bors", emoji_code="22134", reaction_type="realm_emoji") + remove_reaction("bors", "bors", "ready-to-merge", emoji_code="22134", reaction_type="realm_emoji") if has_merge: - remove_reaction('merge', 'merge') + remove_reaction('merge', 'merge', "") if has_awaiting_author: - remove_reaction('awaiting-author', 'writing') + remove_reaction('awaiting-author', 'writing', 'awaiting-author') if has_closed: # 61282 was the earlier version of the emoji. - remove_reaction('closed-pr', 'closed-pr', emoji_code="61293", reaction_type="realm_emoji") + remove_reaction('closed-pr', 'closed-pr', '', emoji_code="61293", reaction_type="realm_emoji") # Apply the appropriate emoji reaction. print("Applying reactions, as appropriate.") From d46b7b35606a8a65eb16a63c57799e55bf7a8150 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Sun, 27 Jul 2025 18:57:13 -0400 Subject: [PATCH 2/5] fix lint --- .github/workflows/zulip_emoji_labelling.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/zulip_emoji_labelling.yaml b/.github/workflows/zulip_emoji_labelling.yaml index 80a747fef6ff68..63a7148588a091 100644 --- a/.github/workflows/zulip_emoji_labelling.yaml +++ b/.github/workflows/zulip_emoji_labelling.yaml @@ -40,7 +40,7 @@ jobs: PR_NUMBER: ${{ github.event.number}} LABEL_STATUS: ${{ github.event.action }} LABEL_NAME: ${{ github.event.label.name }} - PR_LABELS: ${{ github.event.pull_request.labels.*.name }} + PR_LABELS: ${{ toJSON(github.event.pull_request.labels.*.name) }} run: | printf $'Running the python script with pr "%s"\n' "$PR_NUMBER" "$LABEL_STATUS" "$LABEL" "$PR_LABELS" python scripts/zulip_emoji_reactions.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$LABEL_NAME" "$PR_NUMBER" "$PR_LABELS" From 5d7db37a178ece1fe125dcd9e3edee2440b0bd48 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Mon, 28 Jul 2025 00:47:33 -0400 Subject: [PATCH 3/5] comments --- scripts/zulip_emoji_reactions.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/scripts/zulip_emoji_reactions.py b/scripts/zulip_emoji_reactions.py index dd722f3cb7774f..dbf218970dd983 100644 --- a/scripts/zulip_emoji_reactions.py +++ b/scripts/zulip_emoji_reactions.py @@ -115,8 +115,8 @@ def has_reaction(name: str) -> bool: def remove_reaction(name: str, emoji_name: str, label_name: str, **kwargs) -> None: # We do not remove an emoji if the corresponding label is still present. - print(f'Removing {name}') if label_name not in PR_LABELS: + print(f'Removing {name}') result = client.remove_reaction({ "message_id": message['id'], "emoji_name": emoji_name, @@ -143,7 +143,11 @@ def add_reaction(name: str, emoji_name: str) -> None: # We should never remove any "this PR was migrated from a fork" reaction. - # Otherwise, remove all previous mutually exclusive emoji reactions. + # Otherwise, remove all previous mutually exclusive emoji reactions (unless + # PR_LABELS contains the corresponding label). + # Note that the 'merge' and 'closed-pr' reactions do not have a corresponding label, + # so we pass the empty string (which should never be in PR_LABELS) so that they are + # always removed. # If the emoji is a custom emoji, add the fields `emoji_code` and `reaction_type` as well. print("Removing previous reactions, if present.") if has_peace_sign: From 2fb10ffd071ee02dfc8afe8dbcf1dda4e64e4262 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Thu, 31 Jul 2025 10:04:15 -0400 Subject: [PATCH 4/5] better default value for PR_LABELS, fixes --- scripts/zulip_emoji_reactions.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/scripts/zulip_emoji_reactions.py b/scripts/zulip_emoji_reactions.py index dbf218970dd983..971f0af361d3d4 100644 --- a/scripts/zulip_emoji_reactions.py +++ b/scripts/zulip_emoji_reactions.py @@ -41,8 +41,9 @@ PR_LABELS = json.loads(PR_LABELS) assert isinstance(PR_LABELS, list) except: - print(f"parsing PR_LABELS failed; setting to None") - PR_LABELS = None + print(f"parsing PR_LABELS failed; setting to empty list") + # an empty list is a good default since we remove reactions if the label is `not in PR_LABELS` + PR_LABELS = [] print(f"PR_LABELS: '{PR_LABELS}'") # Initialize Zulip client @@ -114,7 +115,7 @@ def has_reaction(name: str) -> bool: print(f"matched: '{message}'") def remove_reaction(name: str, emoji_name: str, label_name: str, **kwargs) -> None: - # We do not remove an emoji if the corresponding label is still present. + # We only remove the emoji if the corresponding label is not present. if label_name not in PR_LABELS: print(f'Removing {name}') result = client.remove_reaction({ @@ -138,7 +139,7 @@ def add_reaction(name: str, emoji_name: str) -> None: if ACTION == "labeled": add_reaction('maintainer-merge', 'hammer') elif ACTION == "unlabeled": - remove_reaction('maintainer-merge', 'hammer') + remove_reaction('maintainer-merge', 'hammer', 'maintainer-merge') continue # We should never remove any "this PR was migrated from a fork" reaction. From 65e2684be053a08f09df09f8f46df5d0d58104c2 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Fri, 1 Aug 2025 18:47:21 -0400 Subject: [PATCH 5/5] more comments, fix logging in workflow --- .github/workflows/zulip_emoji_labelling.yaml | 2 +- scripts/zulip_emoji_reactions.py | 35 ++++++++++++-------- 2 files changed, 22 insertions(+), 15 deletions(-) diff --git a/.github/workflows/zulip_emoji_labelling.yaml b/.github/workflows/zulip_emoji_labelling.yaml index 63a7148588a091..ed859668a112fd 100644 --- a/.github/workflows/zulip_emoji_labelling.yaml +++ b/.github/workflows/zulip_emoji_labelling.yaml @@ -42,5 +42,5 @@ jobs: LABEL_NAME: ${{ github.event.label.name }} PR_LABELS: ${{ toJSON(github.event.pull_request.labels.*.name) }} run: | - printf $'Running the python script with pr "%s"\n' "$PR_NUMBER" "$LABEL_STATUS" "$LABEL" "$PR_LABELS" + printf $'Running the python script with:\nPR number: "%s"\nlabel status: "%s"\nlabel: "%s"\nPR labels: "%s"\n' "$PR_NUMBER" "$LABEL_STATUS" "$LABEL" "$PR_LABELS" python scripts/zulip_emoji_reactions.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$LABEL_NAME" "$PR_NUMBER" "$PR_LABELS" diff --git a/scripts/zulip_emoji_reactions.py b/scripts/zulip_emoji_reactions.py index 971f0af361d3d4..760608a5c8920f 100644 --- a/scripts/zulip_emoji_reactions.py +++ b/scripts/zulip_emoji_reactions.py @@ -5,11 +5,12 @@ import json # Usage: -# python scripts/zulip_emoji_reactions.py $ZULIP_API_KEY $ZULIP_EMAIL $ZULIP_SITE $ACTION $LABEL_NAME $PR_NUMBER $PR_LABELS +# python scripts/zulip_emoji_reactions.py $ZULIP_API_KEY $ZULIP_EMAIL $ZULIP_SITE $ACTION $LABEL_NAME $PR_NUMBER $LABELS_TO_KEEP # The first three variables identify the lean4 Zulip chat and allow the bot to access it # (see .github/workflows/zulip_emoji_merge_delegate.yaml), # see the comment below for a description of $ACTION and $LABEL_NAME. -# $PR_LABELS is optional, but if present, should be a JSON array of label names +# $LABELS_TO_KEEP is optional, but if present, should be a JSON array of GitHub PR label names +# Emoji reactions that correspond to these labels will not be removed # (see .github/workflows/zulip_emoji_labelling.yaml) ZULIP_API_KEY = sys.argv[1] @@ -36,15 +37,16 @@ print(f"LABEL_NAME: '{LABEL_NAME}'") print(f"PR_NUMBER: '{PR_NUMBER}'") try: - PR_LABELS = sys.argv[7] - print(f"Attempting to parse PR_LABELS: '{PR_LABELS}") - PR_LABELS = json.loads(PR_LABELS) - assert isinstance(PR_LABELS, list) + LABELS_TO_KEEP = sys.argv[7] + print(f"Attempting to parse LABELS_TO_KEEP: '{LABELS_TO_KEEP}") + LABELS_TO_KEEP = json.loads(LABELS_TO_KEEP) + assert isinstance(LABELS_TO_KEEP, list) + assert '' not in LABELS_TO_KEEP except: - print(f"parsing PR_LABELS failed; setting to empty list") - # an empty list is a good default since we remove reactions if the label is `not in PR_LABELS` - PR_LABELS = [] -print(f"PR_LABELS: '{PR_LABELS}'") + print(f"parsing LABELS_TO_KEEP failed; setting to empty list") + # an empty list is a good default since we remove reactions if the label is `not in LABELS_TO_KEEP` + LABELS_TO_KEEP = [] +print(f"LABELS_TO_KEEP: '{LABELS_TO_KEEP}'") # Initialize Zulip client client = zulip.Client( @@ -114,9 +116,13 @@ def has_reaction(name: str) -> bool: if match: print(f"matched: '{message}'") + # name: a description of the emoji to be removed + # emoji_name: the emoji name as used on Zulip + # label_name: the name of the corresponding PR label, if present in LABELS_TO_KEEP, we do not remove the reaction + # if there is no corresponding label (e.g. for the "closed-pr" reaction) then this should be an empty string "" + # additional arguments will be passed to the zulip library remove_reaction function def remove_reaction(name: str, emoji_name: str, label_name: str, **kwargs) -> None: - # We only remove the emoji if the corresponding label is not present. - if label_name not in PR_LABELS: + if label_name not in LABELS_TO_KEEP: print(f'Removing {name}') result = client.remove_reaction({ "message_id": message['id'], @@ -145,9 +151,10 @@ def add_reaction(name: str, emoji_name: str) -> None: # We should never remove any "this PR was migrated from a fork" reaction. # Otherwise, remove all previous mutually exclusive emoji reactions (unless - # PR_LABELS contains the corresponding label). + # LABELS_TO_KEEP contains the corresponding label). This is because otherwise this script + # may end up removing reactions that are still relevant. See PR #27570 # Note that the 'merge' and 'closed-pr' reactions do not have a corresponding label, - # so we pass the empty string (which should never be in PR_LABELS) so that they are + # so we pass the empty string (which will never be in LABELS_TO_KEEP) so that they are # always removed. # If the emoji is a custom emoji, add the fields `emoji_code` and `reaction_type` as well. print("Removing previous reactions, if present.")