Skip to content

ci: self-heal nightly-testing-green after a history rewrite#40586

Open
kim-em wants to merge 1 commit into
masterfrom
ci-nightly-testing-green-selfheal
Open

ci: self-heal nightly-testing-green after a history rewrite#40586
kim-em wants to merge 1 commit into
masterfrom
ci-nightly-testing-green-selfheal

Conversation

@kim-em

@kim-em kim-em commented Jun 14, 2026

Copy link
Copy Markdown
Contributor

This PR makes the nightly-testing-green update in nightly_detect_failure.yml recover from a history rewrite instead of freezing. The branch is advanced with a plain fast-forward push, which is rejected once nightly-testing history diverges from its tip (for example a toolchain reset to an rc). #38847 dropped the original git push --force and deferred recovery to a daily force-push job that does not exist, so the branch stuck on v4.31.0-rc1 for weeks until it was force-pushed by hand.

Fast-forward when possible, and otherwise force-push to recover, but only when the tested commit is strictly newer than the current tip by committer date, so an out-of-order CI completion can never roll the branch backwards. nightly-testing-daily keeps its fast-forward-or-skip behavior, and the stale comment referencing the nonexistent force-push job is corrected.

🤖 Prepared with Claude Code

@github-actions

github-actions Bot commented Jun 14, 2026

Copy link
Copy Markdown

PR summary 9b1c62f014

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)

Lean-aware diff — post-build, computed from the Lean environment (commit 9b1c62f).

  • +0 new declarations
  • −0 removed declarations

No declaration differences.


No changes to strong technical debt.

No changes to weak technical debt.

Current commit 9b1c62f014
Reference commit 9e7b1c1166

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.sh 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/nightly_detect_failure.yml

@github-actions github-actions Bot added the CI Modifies the continuous integration setup or other automation label Jun 14, 2026
@kim-em kim-em force-pushed the ci-nightly-testing-green-selfheal branch from fc66f95 to ef3d526 Compare June 14, 2026 06:32
The `nightly-testing-green` branch is advanced with a plain fast-forward push,
which is rejected as non-fast-forward once `nightly-testing` history is rewritten
(e.g. a toolchain reset to an rc). #38847 dropped the old `--force` and deferred
recovery to a daily force-push job that never existed, so the branch stuck on
v4.31.0-rc1 for weeks until it was force-pushed by hand. Force-push to recover,
but only when the tested commit is at least as new as the current tip (by
committer date), so an out-of-order CI completion still cannot roll it backwards.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@kim-em kim-em force-pushed the ci-nightly-testing-green-selfheal branch from ef3d526 to 9b1c62f Compare June 14, 2026 06:40
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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant