[Merged by Bors] - feat(Analysis/CStarAlgebra/CFC/Order): e * e ≤ e when e is an element of the nonnegative closed unit ball
#17315
Workflow file for this run
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
| # Keeps the Zulip emoji reactions on PR-related messages in sync with each PR's | |
| # actual state (open/closed/merged, labels, CI result). One job, fed by three | |
| # kinds of trigger: | |
| # - schedule: hourly sweep — the self-healing safety net that repairs | |
| # any drift the event triggers miss (dropped webhooks, | |
| # outages, state changes while a run was broken). | |
| # - pull_request_target: label/close/merge/reopen changes, reflected in seconds. | |
| # - workflow_run: CI start/finish, so the CI emoji updates promptly. | |
| # This same workflow serves both leanprover-community/mathlib4 and its | |
| # leanprover-community/mathlib4-nightly-testing mirror (whose adaptation PRs are | |
| # announced in the `nightly-testing-mathlib` Zulip channel); the "Select config" | |
| # step picks the matching config per repo. Everything repo-specific lives in | |
| # those JSON configs; the engine and its docs are in mathlib-ci: | |
| # https://github.com/leanprover-community/mathlib-ci/blob/master/docs/zulip-emoji-reconcile.md | |
| name: Zulip emoji reconcile | |
| on: | |
| schedule: | |
| - cron: "37 * * * *" # hourly, offset to dodge top-of-hour runner load | |
| workflow_dispatch: | |
| inputs: | |
| pr: | |
| description: PR number(s), space-separated; leave empty to sweep recent messages | |
| required: false | |
| default: "" | |
| dry-run: | |
| description: Log planned reaction changes without modifying Zulip | |
| type: boolean | |
| default: false | |
| pull_request_target: # label/close/merge/reopen changes, within seconds | |
| types: [labeled, unlabeled, closed, reopened] | |
| workflow_run: # CI start/finish, so the CI emoji updates promptly | |
| workflows: ["continuous integration", "continuous integration (mathlib forks)"] | |
| types: [requested, completed] | |
| concurrency: | |
| # Serialize runs: the reconciler reads live PR state and then writes reactions, | |
| # so two interleaved runs could re-assert stale state. GitHub keeps only the | |
| # newest queued run per group (earlier pending runs are canceled), which suits a | |
| # level-triggered tool — the last run recomputes everything from live state and | |
| # converges to the final answer. One *shared* group is deliberate: the same PR | |
| # reaches this workflow under different keys (pull_request.number, | |
| # workflow_run.head_sha, nothing on a sweep), so per-PR groups would leave | |
| # exactly those cross-trigger races open. | |
| group: ${{ github.workflow }} | |
| cancel-in-progress: false | |
| permissions: | |
| contents: read | |
| pull-requests: read | |
| jobs: | |
| reconcile: | |
| if: github.repository == 'leanprover-community/mathlib4' || | |
| github.repository == 'leanprover-community/mathlib4-nightly-testing' | |
| runs-on: ubuntu-latest | |
| steps: | |
| # On pull_request_target / workflow_run this checks out the *default* | |
| # branch, so the config (and everything else in this job) is never | |
| # PR-controlled. | |
| - name: Check out reconcile config | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| sparse-checkout: | | |
| .github/zulip-emoji-config.json | |
| .github/zulip-emoji-config-nightly.json | |
| sparse-checkout-cone-mode: false | |
| - name: Select config for this repository | |
| id: cfg | |
| env: | |
| REPO: ${{ github.repository }} | |
| run: | | |
| set -euo pipefail | |
| case "$REPO" in | |
| leanprover-community/mathlib4-nightly-testing) | |
| config=.github/zulip-emoji-config-nightly.json ;; | |
| *) | |
| config=.github/zulip-emoji-config.json ;; | |
| esac | |
| if [ -f "$config" ]; then | |
| echo "config=${config}" >> "$GITHUB_OUTPUT" | |
| echo "present=true" >> "$GITHUB_OUTPUT" | |
| else | |
| # The nightly config reaches mathlib4-nightly-testing only after the | |
| # next master -> nightly-testing sync; until then, no-op rather than | |
| # fail a scheduled run. | |
| echo "::notice::reconcile config ${config} not present yet; skipping." | |
| echo "present=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Determine PR number(s) | |
| id: target | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| EVENT: ${{ github.event_name }} | |
| INPUT_PR: ${{ inputs.pr }} | |
| EVENT_PR: ${{ github.event.pull_request.number }} | |
| HEAD_SHA: ${{ github.event.workflow_run.head_sha }} | |
| run: | | |
| set -euo pipefail | |
| case "$EVENT" in | |
| workflow_dispatch) pr="$INPUT_PR" ;; | |
| pull_request_target) pr="$EVENT_PR" ;; | |
| workflow_run) | |
| # PR(s) at the CI run's head commit (works for fork PRs too). | |
| pr=$(gh api "repos/${GITHUB_REPOSITORY}/commits/${HEAD_SHA}/pulls" \ | |
| --jq 'map(.number) | join(" ")') | |
| ;; | |
| *) pr="" ;; # schedule -> sweep | |
| esac | |
| echo "pr=${pr}" >> "$GITHUB_OUTPUT" | |
| - name: Reconcile | |
| # Emoji reactions are cosmetic: a Zulip or API hiccup must never put a | |
| # red X (or send a failure email) on a contributor's PR or a CI run. So | |
| # the two contributor-facing event triggers swallow failures, matching | |
| # the `continue-on-error` the retired event-driven workflows carried. | |
| # The hourly `schedule` sweep and manual `workflow_dispatch` runs stay | |
| # loud: the sweep is the health signal for the reconciler itself, and a | |
| # manual run is someone actively debugging who wants to see the error. | |
| continue-on-error: ${{ github.event_name == 'pull_request_target' || github.event_name == 'workflow_run' }} | |
| # Skip when no config is present (nightly, pre-sync), and skip only a | |
| # workflow_run whose head commit no longer maps to a PR; schedule and | |
| # PR-less dispatches sweep instead. | |
| if: steps.cfg.outputs.present == 'true' && | |
| (steps.target.outputs.pr != '' || github.event_name == 'schedule' || github.event_name == 'workflow_dispatch') | |
| uses: leanprover-community/mathlib-ci/.github/actions/zulip-emoji-reconcile@5668fbbccf0fecefdfcddf539b8406db197dfc59 | |
| with: | |
| config: ${{ steps.cfg.outputs.config }} | |
| pr: ${{ steps.target.outputs.pr }} | |
| sweep: ${{ !steps.target.outputs.pr }} | |
| dry-run: ${{ inputs.dry-run == true }} | |
| zulip-api-key: ${{ secrets.ZULIP_API_KEY }} | |
| github-token: ${{ github.token }} |