Skip to content

ci(build_fork.yml): supersede fork CI runs by PR head sha instead of arrival order - #43955

Open
bryangingechen wants to merge 2 commits into
leanprover-community:masterfrom
bryangingechen:bgc-replace-concurrency-with-head-check
Open

bryangingechen wants to merge 2 commits into
leanprover-community:masterfrom
bryangingechen:bgc-replace-concurrency-with-head-check

Conversation

@bryangingechen

@bryangingechen bryangingechen commented Sep 19, 2026

Copy link
Copy Markdown
Contributor

This PR addresses a race condition reported at #mathlib4 > [pre-commit.ci lite] cancelling CI. We replace build_fork.yml's concurrency block with a guard job that picks the surviving fork run by comparing against the PR's live head sha, rather than by the order GitHub created the runs in.

Details of the race When two pushes to a PR occur in quick succession, sometimes the CI for the HEAD commit is triggered before CI for the previous commit starts, causing `cancel-in-progress` to cancel CI for the HEAD commit, causing the CI to get stuck until a manual re-trigger or another push. Example: on #43646, the run for commit `d046ac32` (committed 22:42:59) was created at 22:43:03 and [cancelled](https://github.com/leanprover-community/mathlib4/actions/runs/34538806707) one second later by the run for `a201b6db` (committed 22:41:49), which then [reported the PR's status](https://github.com/leanprover-community/mathlib4/actions/runs/34538807811) for a 70-second-stale commit.

The new guard job skips the build when its sha is no longer the PR head, and otherwise cancels the branch's other in-flight runs. The guard fails open: an API error or a failure of guard itself builds anyway so a mistake costs a duplicate build rather than a PR with no CI. Never dispatching stale builds saves roughly what superseded runs now cost by living ~30s longer, so this should be roughly neutral with respect to runner usage.

Two companion changes:

  • A run skipped by the guard still concludes success, and decls-diff.yml read success as "there is an import-graph artifact to diff", so it now checks for the artifact instead.
  • build_fork.yml stops passing concurrency_group to build_template.yml, which would otherwise log a group that no longer exists; the input in build_template.yml also becomes optional.

🤖 Generated with Claude Code

bryangingechen and others added 2 commits September 15, 2026 00:53
`build_fork.yml`'s `guard` skips the build for a superseded commit, and a run
whose only executed job succeeded still concludes `success` — which
`decls-diff.yml` read as evidence that an `import-graph` artifact existed to
diff. Check for the artifact instead, in a cheap job ahead of the full-history
checkout.

Also on the guard itself: build rather than skip CI when `guard` fails, so the
job boundary fails open the way the step already does; cap `guard` at five
minutes; and stop passing `concurrency_group`, which would otherwise log a
group that no longer exists.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@bryangingechen bryangingechen added CI Modifies the continuous integration setup or other automation LLM-generated PRs with substantial input from LLMs - review accordingly labels Sep 19, 2026
@github-actions

Copy link
Copy Markdown

PR summary 669cd1679a

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.


No changes to strong technical debt.
No changes to weak technical debt.

Current commit 669cd1679a
Reference commit 55a449c5f2

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

  • .github/workflows/build_fork.yml
  • .github/workflows/build_template.yml
  • .github/workflows/decls-diff.yml

@bryangingechen
bryangingechen marked this pull request as ready for review September 19, 2026 02:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

CI Modifies the continuous integration setup or other automation LLM-generated PRs with substantial input from LLMs - review accordingly

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant