[Merged by Bors] - fix: do not remove reactions if the corresponding label is still present on the PR

.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 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"

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.")