Re: [PATCH v2] ci: cancel stale pull request workflow runs

"Harald Nordgren via GitGitGadget" [off-list ref] writes:

From: Harald Nordgren <redacted>

The CI workflow previously grouped all runs by commit hash using
`group: ${{ github.sha }}`.  This meant every push to a pull
request started a separate workflow run, and all workflows
triggered by the same commit shared the same concurrency group.

That's the current status that we normally describe in the present
tense, no?

Signed-off-by: Harald Nordgren <redacted>
---
...
+# For more details about the `concurrency` attribute, see:
 # https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#concurrency
 concurrency:
-  group: ${{ github.sha }}
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.sha }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}

If a user has CI enabled on their own repository, pushes a commit
there, and opens a pull request, wouldn't GitHub Actions trigger
two events for the same commit at the tip of the pushed branch?

Before this change, both events are assigned to the same concurrency
group (the commit object name).  One waits while the other runs, and
the skip-if-redundant logic stops the second one early without
wasting cycles on the same commit.  With this change, the
concurrency groups for these two events are separate.  Would we end
up building and testing the same commit twice in parallel?

I suspect this may not be a problem in practice given how our
contributors use GitHub Actions in our official repositories (either
those owned by gitgitgadget or git).  They push to their own
repositories where CI may not be enabled, so 'push' does not
trigger.  Still, I thought it better to bring this up before the
change gets merged and wastes build cycles.