ci: cancel superseded PR runs of Lean Action CI - #908
Open
jessealama wants to merge 2 commits into
Open
jessealama wants to merge 2 commits into
jessealama wants to merge 2 commits into
Conversation
jessealama
requested review from
arademaker,
chenson2018,
fmontesi,
kim-em and
sorrachai
as code owners
September 15, 2026 17:39
Add a concurrency group keyed on workflow and ref. On PR refs a new push cancels the in-flight run. On main and nightly-testing runs queue instead, since report_failures_nightly-testing.yml consumes every completed run.
jessealama
force-pushed
the
ci/lean-action-concurrency
branch
from
September 15, 2026 17:52
c852a2c to
0b107a5
Compare
chenson2018
reviewed
Sep 16, 2026
Comment on lines
+14
to
+15
| group: ${{ github.workflow }}-${{ github.ref }} | ||
| cancel-in-progress: ${{ github.ref != 'refs/heads/main' && github.ref != 'refs/heads/nightly-testing' }} |
Collaborator
There was a problem hiding this comment.
I think this may not behave as expected because of the concurrency queue, which by default allows only one job at a time. There is a setting to expand this, but the docs indicate
Note that
queue: maxcannot be combined withcancel-in-progress: true, because the two options describe conflicting behaviors for handling in-progress runs.
I'm not 100% sure if that also applies to conditional cancel-in-progress, but it seems simplest to follow what Mathlib does: when these conditions apply the id is included in the group name, making them unique.
Contributor
Author
There was a problem hiding this comment.
Ah, good point. I thought that what I had should be safe (and maybe it is), but doing what Mathlib does is just fine.
…rogress This copies what Mathlib does.
jessealama
force-pushed
the
ci/lean-action-concurrency
branch
from
September 16, 2026 15:57
1622106 to
29b08cf
Compare
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds a
concurrencygroup tolean_action_ci.ymlso that new pushes to a PR cancel running steps instead of doing a redundant full build behind it. This saves resources (almost certainly wasted compute and network traffic). It could even reduce the bill theleanproverGitHub org pays for compute. Canceling a redundant run also better reflects development reality: a canceled run shows the branch is busy.(Mathlib does the same thing. GitHub-native concurrency, replacing a third-party approach, was introduced in this PR.)
Runs on
mainandnightly-testingare never canceled.report_failures_nightly-testing.ymlconsumes completed runs viaworkflow_run, so canceling one there would swallow a status report. This also works with the merge queue.docs.ymlis left alone since it only runs on pushes tomain.