Repository navigation
[Merged by Bors] - ci: skip the inputRev check on bump branches and PRs into them - #45382
Closed
bryangingechen wants to merge 1 commit into
Closed
bryangingechen wants to merge 1 commit into
bryangingechen wants to merge 1 commit into
Conversation
`bump/*` branches now live in mathlib4 rather than mathlib4-nightly-testing, and PRs into them (e.g. the downstream-lean4 exports) depend on the `nightly-testing` branches of upstream dependencies. Skip the `lake-manifest.json` inputRev validation when the branch, or the PR's base branch, is `bump/*`. The base branch must be read from `github.base_ref`: under `pull_request_target`, `github.ref_name` is the default branch. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
PR summary e3b58ca9e7Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
bryangingechen
marked this pull request as ready for review
October 27, 2026 19:31
mathlib-bors Bot
pushed a commit
that referenced
this pull request
Oct 27, 2026
`bump/*` branches now live in `mathlib4` rather than `mathlib4-nightly-testing`. PRs into them, such as the `downstream-lean4` export in #45345, depend on the `nightly-testing` branches of our dependencies. The "validate lake-manifest.json inputRevs" step in `build_template.yml` runs on these branches and fails them, though it used to be skipped when the branches were in the nightly-testing repo. This PR skips the validation step when either of these starts with `bump/`: - `github.ref_name`: pushes to `bump/*` branches, including the automation's `bump/nightly-*` branches. - `github.base_ref`: PRs into a `bump/*` branch, from any repo. (Note that `head_ref` is not read, so a PR from a branch starting with `bump/` can't get around this.) Not covered: a non-`bump/*` branch pushed to mathlib4 with a PR into a bump branch. Push builds can't see the PR's base, so the check still runs there. (No one should be creating such branches and we have branch protection rules against this.) 🤖 Generated with [Claude Code](https://claude.com/claude-code)
Contributor
|
Pull request successfully merged into master. Build succeeded: |
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
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.
bump/*branches now live inmathlib4rather thanmathlib4-nightly-testing. PRs into them, such as thedownstream-lean4export in #45345, depend on thenightly-testingbranches of our dependencies. The "validate lake-manifest.json inputRevs" step inbuild_template.ymlruns on these branches and fails them, though it used to be skipped when the branches were in the nightly-testing repo.This PR skips the validation step when either of these starts with
bump/:github.ref_name: pushes tobump/*branches, including the automation'sbump/nightly-*branches.github.base_ref: PRs into abump/*branch, from any repo.(Note that
head_refis not read, so a PR from a branch starting withbump/can't get around this.)Not covered: a non-
bump/*branch pushed to mathlib4 with a PR into a bump branch. Push builds can't see the PR's base, so the check still runs there. (No one should be creating such branches and we have branch protection rules against this.)🤖 Generated with Claude Code
Note: the base branch has to come from
github.base_ref: underpull_request_target,github.refis now always the default branch. The #45345 run logsREF: refs/heads/master.