Skip to content

Commit 738faa5

Browse files
kim-emkim-em
committed
feat(ci): add CI status emoji reactions to Zulip messages (leanprover-community#35230)
This PR extends the emojibot to show CI build status on Zulip messages that mention a PR: - 🟡 CI running - ✅ CI passed - ❌ CI failed These are independent of the existing PR status emojis (merged, delegated, awaiting-author, etc.) and can coexist with them. The new `zulip_emoji_ci_status.yaml` workflow triggers on `workflow_run` events from both CI workflows. Cancelled runs are ignored (a new run will follow shortly). 🤖 Prepared with Claude Code
1 parent 265f65e commit 738faa5

2 files changed

Lines changed: 124 additions & 0 deletions

File tree

‎.github/workflows/zulip_emoji_ci_status.yaml‎

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
name: Zulip emoji CI status
2+
3+
on:
4+
workflow_run:
5+
workflows: ["continuous integration", "continuous integration (mathlib forks)"]
6+
types: [requested, completed]
7+
8+
# Limit permissions for GITHUB_TOKEN for the entire workflow
9+
permissions:
10+
contents: read
11+
pull-requests: read
12+
# All other permissions are implicitly 'none'
13+
14+
jobs:
15+
update_ci_emoji:
16+
runs-on: ubuntu-latest
17+
if: github.repository == 'leanprover-community/mathlib4'
18+
steps:
19+
- name: Determine PR number
20+
id: pr
21+
env:
22+
GH_TOKEN: ${{ github.token }}
23+
HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }}
24+
HEAD_REPO_OWNER: ${{ github.event.workflow_run.head_repository.owner.login }}
25+
HEAD_SHA: ${{ github.event.workflow_run.head_sha }}
26+
run: |
27+
# Try to get PR number from the workflow_run event
28+
PR_NUMBER=$(echo '${{ toJSON(github.event.workflow_run.pull_requests) }}' | jq -r '.[0].number // empty')
29+
# For push-triggered CI (non-fork PRs), pull_requests may be empty;
30+
# fall back to looking up the PR by branch name.
31+
# Use owner:branch format to avoid matching the wrong PR when
32+
# multiple forks use the same branch name.
33+
if [ -z "$PR_NUMBER" ]; then
34+
PR_NUMBER=$(gh pr list --repo "${{ github.repository }}" --head "$HEAD_REPO_OWNER:$HEAD_BRANCH" --state open --json number,headRefOid --jq ".[] | select(.headRefOid == \"$HEAD_SHA\") | .number" 2>/dev/null || true)
35+
fi
36+
# If owner-qualified lookup failed, try without owner (for same-repo branches)
37+
if [ -z "$PR_NUMBER" ]; then
38+
PR_NUMBER=$(gh pr list --repo "${{ github.repository }}" --head "$HEAD_BRANCH" --state open --json number,headRefOid --jq ".[] | select(.headRefOid == \"$HEAD_SHA\") | .number" 2>/dev/null || true)
39+
fi
40+
if [ -z "$PR_NUMBER" ]; then
41+
echo "No PR found for branch $HEAD_REPO_OWNER:$HEAD_BRANCH at $HEAD_SHA, skipping"
42+
echo "skip=true" >> "$GITHUB_OUTPUT"
43+
else
44+
echo "Found PR #$PR_NUMBER"
45+
echo "pr_number=$PR_NUMBER" >> "$GITHUB_OUTPUT"
46+
echo "skip=false" >> "$GITHUB_OUTPUT"
47+
fi
48+
49+
- name: Determine CI action
50+
id: action
51+
if: steps.pr.outputs.skip != 'true'
52+
run: |
53+
EVENT_ACTION="${{ github.event.action }}"
54+
CONCLUSION="${{ github.event.workflow_run.conclusion }}"
55+
echo "Event action: $EVENT_ACTION, conclusion: $CONCLUSION"
56+
if [ "$EVENT_ACTION" = "requested" ]; then
57+
echo "ci_action=ci-running" >> "$GITHUB_OUTPUT"
58+
elif [ "$EVENT_ACTION" = "completed" ]; then
59+
case "$CONCLUSION" in
60+
success)
61+
echo "ci_action=ci-success" >> "$GITHUB_OUTPUT"
62+
;;
63+
cancelled)
64+
# Clear the running emoji. A new run may or may not follow
65+
# (manual cancel, branch deleted, etc.), so don't leave stale 🟡.
66+
echo "ci_action=ci-cancelled" >> "$GITHUB_OUTPUT"
67+
;;
68+
*)
69+
echo "ci_action=ci-failure" >> "$GITHUB_OUTPUT"
70+
;;
71+
esac
72+
fi
73+
74+
- name: Checkout mathlib repository
75+
if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
76+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
77+
with:
78+
ref: master
79+
sparse-checkout: |
80+
scripts/zulip_emoji_reactions.py
81+
82+
- name: Set up Python
83+
if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
84+
uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
85+
with:
86+
python-version: '3.x'
87+
88+
- name: Install dependencies
89+
if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
90+
run: |
91+
python -m pip install --upgrade pip
92+
pip install zulip
93+
94+
- name: Update CI emoji
95+
if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
96+
env:
97+
ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
98+
ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
99+
ZULIP_SITE: https://leanprover.zulipchat.com
100+
run: |
101+
python scripts/zulip_emoji_reactions.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.action.outputs.ci_action }}" "none" "${{ steps.pr.outputs.pr_number }}"

‎scripts/zulip_emoji_reactions.py‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,8 @@
2727
# command), it is 'ready-to-merge' or 'delegated'. On a bors merge-, bors r- or bors d- command,
2828
# it is 'remove-label'. (This particular value is not used in this script.)
2929
# Note that `bors d-` is *not* a bors command, so only has an effect on mathlib's PR labels.
30+
# - if CI status changed, it is 'ci-running', 'ci-success', 'ci-failure', or 'ci-cancelled'
31+
# (see .github/workflows/zulip_emoji_ci_status.yaml)
3032
ACTION = sys.argv[4]
3133
# Name of the label that was applied or removed
3234
# (if applicable; is 'none' if a PR was closed, reopened or merged)
@@ -110,6 +112,9 @@ def has_reaction(name: str) -> bool:
110112
has_awaiting_author = has_reaction('writing')
111113
has_maintainer_merge = has_reaction('hammer')
112114
has_closed = has_reaction('closed-pr')
115+
has_ci_running = has_reaction('yellow')
116+
has_ci_success = has_reaction('check')
117+
has_ci_failure = has_reaction('cross_mark')
113118
first_in_thread = hashPR.search(message['subject']) and message['display_recipient'] == 'PR reviews' and message['subject'] not in first_by_subject
114119
first_by_subject[message['subject']] = message['id']
115120
match = urlPR.search(content) or first_in_thread
@@ -139,6 +144,24 @@ def add_reaction(name: str, emoji_name: str) -> None:
139144
"emoji_name": emoji_name
140145
})
141146

147+
# CI status emojis are mutually exclusive with each other
148+
# but independent of PR status emojis.
149+
if ACTION.startswith('ci-'):
150+
if has_ci_running:
151+
remove_reaction('ci-running', 'yellow', '')
152+
if has_ci_success:
153+
remove_reaction('ci-success', 'check', '')
154+
if has_ci_failure:
155+
remove_reaction('ci-failure', 'cross_mark', '')
156+
match ACTION:
157+
case 'ci-running':
158+
add_reaction('ci-running', 'yellow')
159+
case 'ci-success':
160+
add_reaction('ci-success', 'check')
161+
case 'ci-failure':
162+
add_reaction('ci-failure', 'cross_mark')
163+
continue
164+
142165
# The maintainer merge label is different from the others, as it is not mutually exclusive
143166
# with them: just add or remove it manually and leave the other emojis alone.
144167
if LABEL_NAME == "maintainer-merge" and message['display_recipient'] != 'mathlib reviewers':

0 commit comments

Comments
 (0)