Zulip emoji CI status #17654
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Zulip emoji CI status | |
| on: | |
| workflow_run: | |
| workflows: ["continuous integration", "continuous integration (mathlib forks)"] | |
| types: [requested, completed] | |
| # Limit permissions for GITHUB_TOKEN for the entire workflow | |
| permissions: | |
| contents: read | |
| pull-requests: read | |
| # All other permissions are implicitly 'none' | |
| jobs: | |
| update_ci_emoji: | |
| runs-on: ubuntu-latest | |
| if: github.repository == 'leanprover-community/mathlib4' || | |
| github.repository == 'leanprover-community/mathlib4-nightly-testing' | |
| steps: | |
| - name: Determine PR number | |
| id: pr | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }} | |
| HEAD_REPO_OWNER: ${{ github.event.workflow_run.head_repository.owner.login }} | |
| HEAD_SHA: ${{ github.event.workflow_run.head_sha }} | |
| run: | | |
| # Try to get PR number from the workflow_run event | |
| PR_NUMBER=$(echo '${{ toJSON(github.event.workflow_run.pull_requests) }}' | jq -r '.[0].number // empty') | |
| # For push-triggered CI (non-fork PRs), pull_requests may be empty; | |
| # fall back to looking up the PR by branch name. | |
| # Use owner:branch format to avoid matching the wrong PR when | |
| # multiple forks use the same branch name. | |
| if [ -z "$PR_NUMBER" ]; then | |
| 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) | |
| fi | |
| # If owner-qualified lookup failed, try without owner (for same-repo branches) | |
| if [ -z "$PR_NUMBER" ]; then | |
| 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) | |
| fi | |
| if [ -z "$PR_NUMBER" ]; then | |
| echo "No PR found for branch $HEAD_REPO_OWNER:$HEAD_BRANCH at $HEAD_SHA, skipping" | |
| echo "skip=true" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "Found PR #$PR_NUMBER" | |
| echo "pr_number=$PR_NUMBER" >> "$GITHUB_OUTPUT" | |
| echo "skip=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Determine CI action | |
| id: action | |
| if: steps.pr.outputs.skip != 'true' | |
| run: | | |
| EVENT_ACTION="${{ github.event.action }}" | |
| CONCLUSION="${{ github.event.workflow_run.conclusion }}" | |
| echo "Event action: $EVENT_ACTION, conclusion: $CONCLUSION" | |
| if [ "$EVENT_ACTION" = "requested" ]; then | |
| echo "ci_action=ci-running" >> "$GITHUB_OUTPUT" | |
| elif [ "$EVENT_ACTION" = "completed" ]; then | |
| case "$CONCLUSION" in | |
| success) | |
| echo "ci_action=ci-success" >> "$GITHUB_OUTPUT" | |
| ;; | |
| cancelled) | |
| # Clear the running emoji. A new run may or may not follow | |
| # (manual cancel, branch deleted, etc.), so don't leave stale 🟡. | |
| echo "ci_action=ci-cancelled" >> "$GITHUB_OUTPUT" | |
| ;; | |
| *) | |
| echo "ci_action=ci-failure" >> "$GITHUB_OUTPUT" | |
| ;; | |
| esac | |
| fi | |
| - name: Checkout local actions | |
| if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip' | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| with: | |
| ref: ${{ github.workflow_sha }} | |
| fetch-depth: 1 | |
| sparse-checkout: .github/actions | |
| path: workflow-actions | |
| - name: Checkout mathlib-ci | |
| if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip' | |
| uses: ./workflow-actions/.github/actions/get-mathlib-ci | |
| - name: Set up Python | |
| if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip' | |
| uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0 | |
| with: | |
| python-version: '3.x' | |
| - name: Install dependencies | |
| if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip' | |
| run: | | |
| python -m pip install --upgrade pip | |
| pip install -r "$CI_SCRIPTS_DIR/zulip/requirements.txt" | |
| - name: Update CI emoji | |
| if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip' | |
| env: | |
| ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }} | |
| ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com | |
| ZULIP_SITE: https://leanprover.zulipchat.com | |
| run: | | |
| python "${CI_SCRIPTS_DIR}/zulip/zulip_emoji_reactions.py" "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.action.outputs.ci_action }}" "none" "${{ steps.pr.outputs.pr_number }}" |