Fix CI double-build race by keying concurrency on commit SHA

[mkarlesky]

Summary

Investigated why the existing push-vs-PR CI dedup mechanism
(check-duplicate-push, PR #1246) works inconsistently — "most instances
produce double builds, some skip the branch-push build."

Root cause: check-duplicate-push is a one-shot, point-in-time poll. On
a push event it queries gh pr list --head <branch> --state open once,
near the start of the run, and decides then and there whether to skip.
Push and PR-creation are independent, asynchronously-fired GitHub events
with no ordering guarantee between them. In the ordinary "push a branch,
then separately open a PR from it" flow — the dominant real-world case —
the poll almost always runs before the PR exists, finds nothing, and lets
the full run proceed to completion. The later pull_request-triggered run
then duplicates it, with no way to detect or cancel the redundant push run
(the concurrency: block was deliberately keyed by event_name
specifically so push and PR runs for the same commit couldn't cancel each
other — itself a fix for an earlier bug, commit bf878a97, where
branch-only concurrency grouping let a new commit's push run wrongly cancel
an older commit's still-running PR check). Outright skips of the push
run only happen in the narrower case where the PR already existed before
the push (e.g. a follow-up commit to an already-open PR).

Fix

Key the concurrency group on the commit SHA instead of branch+event, and
remove the custom polling job entirely:

concurrency:
  group: ci-${{ github.event.pull_request.head.sha || github.sha }}
  cancel-in-progress: true

github.event.pull_request.head.sha is the PR branch's real head commit on
a pull_request event; github.sha is the pushed commit on a push
event. For the identical commit, both resolve to the same group key — so a
push run and a later pull_request run for that commit now land in the
same concurrency group, and GitHub's own cancel-in-progress cancels
whichever started first the instant the second one starts. This is
event-driven, not a fixed-point-in-time guess, so it correctly handles a PR
being opened while the push run's multi-job matrix (several minutes) is
still in flight — not just the first few seconds after push. Keying on the
commit rather than the branch avoids reintroducing bf878a97's bug, since
a different commit on the same branch gets its own group.

Residual gap: if the push run fully completes before the PR is ever
opened, there's nothing left to cancel and it still runs twice for that
commit — a much narrower window than today's near-universal race.

Alternatives considered (not adopted)

• Retry/poll with backoff in the existing push-side check: narrows but
  doesn't eliminate the race, and adds latency to every push run.
• Narrow the push: trigger to protected branches only, relying on
  pull_request alone for feature branches: would eliminate the problem
  for the common case, but is a workflow philosophy change (no CI feedback
  on a bare push to a new feature branch until a PR exists), not a plumbing
  fix — kept as a separate, independent option if wanted later.
• PR-side "was this SHA already built via push?" reuse check: not racy
  in that direction (a PR can only reference an already-pushed commit), and
  would close the residual gap above, but adds custom-script complexity for
  a narrow edge case — flagged for later if the residual gap proves to
  matter in practice.

Verification

This PR is itself a live test of the fix (push already happened; opening
this PR now exercises the exact "push, then promptly open a PR" scenario
the old mechanism handled worst). actionlint confirms no new issues
introduced. Full verification plan (see plan file) also covers a follow-up
commit to this open PR and a fresh-branch/immediate-PR test.

🤖 Generated with Claude Code