[Merged by Bors] - fix(CI): prevent empty grep pattern from matching all lean-pr-testing branches #33546
Conversation
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
… branches When no PRs are found between old and new nightlies, the `prs.txt` file is empty. An empty pattern file causes `grep -f prs.txt` to match ALL lines, which incorrectly selects every `lean-pr-testing-*` branch for merging. This caused a catastrophic failure on 2026-01-04 where the workflow attempted to merge 600+ old adaptation branches into nightly-testing, breaking the build. The fix checks if PRS is empty and exits early, setting branches_exist=false. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
PR summary 6f1904fdccImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
github-actions
bot
added
the
CI
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jan 4, 2026
Reverts the following branches that were incorrectly merged due to a bug in discover-lean-pr-testing.yml where an empty prs.txt caused grep to match ALL lean-pr-testing branches: - lean-pr-testing-2714 (from Oct 2023!) - lean-pr-testing-11455 - lean-pr-testing-11163 - lean-pr-testing-10231 - lean-pr-testing-10178 - lean-pr-testing-10059 These PRs are not in nightly-2026-01-04, so their adaptations should not be merged. The bug fix is in: leanprover-community#33546 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
adomani
reviewed
Jan 4, 2026
Collaborator
adomani
left a comment
adomani
left a comment
There was a problem hiding this comment.
Looks reasonable: let's see how it works!
bors merge
leanprover-community-mathlib4-bot
added
the
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jan 4, 2026
… branches (#33546) When no PRs are found between old and new nightlies, the `prs.txt` file is empty. An empty pattern file causes `grep -f prs.txt` to match ALL lines, which incorrectly selects every `lean-pr-testing-*` branch for merging. This caused a catastrophic failure on 2026-01-04 where the workflow attempted to merge 600+ old adaptation branches into nightly-testing, including branches for PRs that aren't even in the nightly (like lean-pr-testing-10387 from September 2025, and lean-pr-testing-2714 from October 2023!). The fix checks if PRS is empty and exits early, setting `branches_exist=false`. See workflow run: https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/20690417192 🤖 Generated with [Claude Code](https://claude.com/claude-code)
Contributor
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
kim-em
added a commit
to kim-em/mathlib4
that referenced
this pull request
Jan 6, 2026
… branches (leanprover-community#33546) When no PRs are found between old and new nightlies, the `prs.txt` file is empty. An empty pattern file causes `grep -f prs.txt` to match ALL lines, which incorrectly selects every `lean-pr-testing-*` branch for merging. This caused a catastrophic failure on 2026-01-04 where the workflow attempted to merge 600+ old adaptation branches into nightly-testing, including branches for PRs that aren't even in the nightly (like lean-pr-testing-10387 from September 2025, and lean-pr-testing-2714 from October 2023!). The fix checks if PRS is empty and exits early, setting `branches_exist=false`. See workflow run: https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/20690417192 🤖 Generated with [Claude Code](https://claude.com/claude-code)
goliath-klein
pushed a commit
to PrParadoxy/mathlib4
that referenced
this pull request
Jan 24, 2026
… branches (leanprover-community#33546) When no PRs are found between old and new nightlies, the `prs.txt` file is empty. An empty pattern file causes `grep -f prs.txt` to match ALL lines, which incorrectly selects every `lean-pr-testing-*` branch for merging. This caused a catastrophic failure on 2026-01-04 where the workflow attempted to merge 600+ old adaptation branches into nightly-testing, including branches for PRs that aren't even in the nightly (like lean-pr-testing-10387 from September 2025, and lean-pr-testing-2714 from October 2023!). The fix checks if PRS is empty and exits early, setting `branches_exist=false`. See workflow run: https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/20690417192 🤖 Generated with [Claude Code](https://claude.com/claude-code)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
When no PRs are found between old and new nightlies, the
prs.txtfile is empty. An empty pattern file causesgrep -f prs.txtto match ALL lines, which incorrectly selects everylean-pr-testing-*branch for merging.This caused a catastrophic failure on 2026-01-04 where the workflow attempted to merge 600+ old adaptation branches into nightly-testing, including branches for PRs that aren't even in the nightly (like lean-pr-testing-10387 from September 2025, and lean-pr-testing-2714 from October 2023!).
The fix checks if PRS is empty and exits early, setting
branches_exist=false.See workflow run: https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/20690417192
🤖 Generated with Claude Code