fix: do not remove reactions if the corresponding label is still present on the PR (leanprover-community#27570)

Recently the reaction bot on Zulip has been observed to add a reaction and then remove it shortly afterwards (mainly the reactions corresponding to the `ready-to-merge` and `delegated` labels). The mechanism seems to be the following:
- a maintainer writes a comment like "bors merge" (or "bors d+") on a PR that has been `maintainer-merge`'d
- `zulip_emoji_merge_delegate.yaml` and `zulip_emoji_merge_delegate_wf.yaml` react to this comment and:
  - simultaneously adds the "ready-to-merge" and removes the `maintainer-merge` label
  - adds the "merge" emoji reaction on Zulip
- the `zulip_emoji_labelling.yaml` workflow reacts to the `maintainer-merge` label being removed, and clears the "merge" emoji as well. See [this log](https://github.com/leanprover-community/mathlib4/actions/runs/16270158496/job/45935446666#step:5:30) (which removes the "delegated" emoji).

We change the `zulip_emoji_labelling.yaml` workflow so that it passes the current list of labels on the PR to the `zulip_emoji_reactions.py` script, and also change the script so that it only removes a reaction if the corresponding label is NOT present.

cf. https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/merge.2Fdelegate.20emojis.20bot/near/528289834

Author: bryangingechen

.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: ${{ toJSON(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:\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"

scripts/zulip_emoji_reactions.py

@@ -2,12 +2,16 @@
 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 $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.
+# $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]
 ZULIP_EMAIL = sys.argv[2]
@@ -32,6 +36,17 @@
 print(f"ACTION: '{ACTION}'")
 print(f"LABEL_NAME: '{LABEL_NAME}'")
 print(f"PR_NUMBER: '{PR_NUMBER}'")
+try:
+    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 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(
@@ -101,14 +116,22 @@ def has_reaction(name: str) -> bool:
     if match:
         print(f"matched: '{message}'")
 
-        def remove_reaction(name: str, emoji_name: str, **kwargs) -> None:
-            print(f'Removing {name}')
-            result = client.remove_reaction({
-                "message_id": message['id'],
-                "emoji_name": emoji_name,
-                **kwargs
-            })
-            print(f"result: '{result}'")
+        # 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:
+            if label_name not in LABELS_TO_KEEP:
+                print(f'Removing {name}')
+                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({
@@ -122,25 +145,30 @@ 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.
 
-        # Otherwise, remove all previous mutually exclusive emoji reactions.
+        # Otherwise, remove all previous mutually exclusive emoji reactions (unless
+        # 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 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.")
         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.")