chore(CI): combine nightly bump and pr-testing merge workflows#1655
Merged
chore(CI): combine nightly bump and pr-testing merge workflows#1655
Conversation
This combines `nightly_bump_toolchain.yml` and `discover-lean-pr-testing.yml` into a single `nightly_bump_and_merge.yml` workflow. Previously, when the toolchain was bumped: 1. The bump workflow pushed → CI ran (potentially failing) 2. This triggered the discover workflow which merged adaptations → CI ran again This caused spurious CI failure notifications for the intermediate state (bumped toolchain without the adaptations). Now both operations happen in a single workflow: 1. Bump the toolchain (commit locally) 2. Find and merge any relevant lean-pr-testing branches 3. Push everything at once → single CI run The merge script is also updated to not push (the workflow handles the push). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
github-actions
bot
added
the
awaiting-review
This was referenced Feb 4, 2026
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Feb 10, 2026
This combines `nightly_bump_toolchain.yml` and `discover-lean-pr-testing.yml` into a single `nightly_bump_and_merge.yml` workflow. Previously, when the toolchain was bumped: 1. The bump workflow pushed → CI ran (potentially failing) 2. This triggered the discover workflow which merged adaptations → CI ran again This caused spurious CI failure notifications for the intermediate state (bumped toolchain without the adaptations). Now both operations happen in a single workflow: 1. Bump the toolchain (commit locally, don't push yet) 2. Find and merge any relevant lean-pr-testing branches 3. Push everything at once → single CI run The merge script is also updated to not push (the workflow handles the push). ## Related - Companion PR for batteries: leanprover-community/batteries#1655 - #34821 will need to update the workflow list for `mathlib-nightly-testing` app once this is merged 🤖 Prepared with Claude Code
fgdorais
reviewed
Feb 11, 2026
| # Report successful merges | ||
| if [ -n "$SUCCESSFUL_MERGES" ]; then | ||
| MESSAGE+=$'### ✅ Successfully merged branches into Batteries' \'nightly-testing\':\n\n' | ||
| MESSAGE+=$'### Successfully merged branches into Batteries'\'' \'nightly-testing\':\n\n' |
Collaborator
There was a problem hiding this comment.
Shouldn't this be:
Suggested change
| MESSAGE+=$'### Successfully merged branches into Batteries'\'' \'nightly-testing\':\n\n' | |
| MESSAGE+=$'### Successfully merged branches into Batteries\' \'nightly-testing\':\n\n' |
Some more examples below.
Comment on lines
+65
to
+66
| echo "RELEASE_TAG=$RELEASE_TAG" >> "${GITHUB_ENV}" | ||
| echo "new=$RELEASE_TAG" >> "$GITHUB_OUTPUT" |
Collaborator
There was a problem hiding this comment.
Inconsistent use: ${GITHUB_ENV} vs $GITHUB_OUTPUT. There a some other cases. Both work and are commonly used, so this doesn't matter much.
michaellee94
pushed a commit
to michaellee94/mathlib4
that referenced
this pull request
Feb 15, 2026
…rover-community#34827) This combines `nightly_bump_toolchain.yml` and `discover-lean-pr-testing.yml` into a single `nightly_bump_and_merge.yml` workflow. Previously, when the toolchain was bumped: 1. The bump workflow pushed → CI ran (potentially failing) 2. This triggered the discover workflow which merged adaptations → CI ran again This caused spurious CI failure notifications for the intermediate state (bumped toolchain without the adaptations). Now both operations happen in a single workflow: 1. Bump the toolchain (commit locally, don't push yet) 2. Find and merge any relevant lean-pr-testing branches 3. Push everything at once → single CI run The merge script is also updated to not push (the workflow handles the push). ## Related - Companion PR for batteries: leanprover-community/batteries#1655 - leanprover-community#34821 will need to update the workflow list for `mathlib-nightly-testing` app once this is merged 🤖 Prepared with Claude Code
rao107
pushed a commit
to rao107/mathlib4
that referenced
this pull request
Feb 18, 2026
…rover-community#34827) This combines `nightly_bump_toolchain.yml` and `discover-lean-pr-testing.yml` into a single `nightly_bump_and_merge.yml` workflow. Previously, when the toolchain was bumped: 1. The bump workflow pushed → CI ran (potentially failing) 2. This triggered the discover workflow which merged adaptations → CI ran again This caused spurious CI failure notifications for the intermediate state (bumped toolchain without the adaptations). Now both operations happen in a single workflow: 1. Bump the toolchain (commit locally, don't push yet) 2. Find and merge any relevant lean-pr-testing branches 3. Push everything at once → single CI run The merge script is also updated to not push (the workflow handles the push). ## Related - Companion PR for batteries: leanprover-community/batteries#1655 - leanprover-community#34821 will need to update the workflow list for `mathlib-nightly-testing` app once this is merged 🤖 Prepared with Claude Code
mathlib-merge-conflicts
bot
added
the
merge-conflict
Maldooor
pushed a commit
to Maldooor/mathlib4
that referenced
this pull request
Feb 25, 2026
…rover-community#34827) This combines `nightly_bump_toolchain.yml` and `discover-lean-pr-testing.yml` into a single `nightly_bump_and_merge.yml` workflow. Previously, when the toolchain was bumped: 1. The bump workflow pushed → CI ran (potentially failing) 2. This triggered the discover workflow which merged adaptations → CI ran again This caused spurious CI failure notifications for the intermediate state (bumped toolchain without the adaptations). Now both operations happen in a single workflow: 1. Bump the toolchain (commit locally, don't push yet) 2. Find and merge any relevant lean-pr-testing branches 3. Push everything at once → single CI run The merge script is also updated to not push (the workflow handles the push). ## Related - Companion PR for batteries: leanprover-community/batteries#1655 - leanprover-community#34821 will need to update the workflow list for `mathlib-nightly-testing` app once this is merged 🤖 Prepared with Claude Code
pfaffelh
pushed a commit
to pfaffelh/mathlib4
that referenced
this pull request
Mar 2, 2026
…rover-community#34827) This combines `nightly_bump_toolchain.yml` and `discover-lean-pr-testing.yml` into a single `nightly_bump_and_merge.yml` workflow. Previously, when the toolchain was bumped: 1. The bump workflow pushed → CI ran (potentially failing) 2. This triggered the discover workflow which merged adaptations → CI ran again This caused spurious CI failure notifications for the intermediate state (bumped toolchain without the adaptations). Now both operations happen in a single workflow: 1. Bump the toolchain (commit locally, don't push yet) 2. Find and merge any relevant lean-pr-testing branches 3. Push everything at once → single CI run The merge script is also updated to not push (the workflow handles the push). ## Related - Companion PR for batteries: leanprover-community/batteries#1655 - leanprover-community#34821 will need to update the workflow list for `mathlib-nightly-testing` app once this is merged 🤖 Prepared with Claude Code
…e-workflows # Conflicts: # .github/workflows/nightly_bump_toolchain.yml
Fix $'...' quoting so \n and \' are properly interpreted as escape sequences, and use consistent $GITHUB_ENV style without braces. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 3, 2026
mathlib-merge-conflicts
bot
removed
the
merge-conflict
fgdorais
approved these changes
Mar 4, 2026
github-actions
bot
removed
the
awaiting-review
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.
This combines
nightly_bump_toolchain.ymlanddiscover-lean-pr-testing.ymlinto a single
nightly_bump_and_merge.ymlworkflow.Previously, when the toolchain was bumped:
This caused spurious CI failure notifications for the intermediate state
(bumped toolchain without the adaptations).
Now both operations happen in a single workflow:
The merge script is also updated to not push (the workflow handles the push).
Related
🤖 Prepared with Claude Code