Skip to content

[Merged by Bors] - ci: skip the inputRev check on bump branches and PRs into them - #45382

Closed
bryangingechen wants to merge 1 commit into
leanprover-community:masterfrom
bryangingechen:ci-bump-inputrevs
Closed

bryangingechen wants to merge 1 commit into
leanprover-community:masterfrom
bryangingechen:ci-bump-inputrevs

Conversation

@bryangingechen

@bryangingechen bryangingechen commented Oct 27, 2026 •

Copy link
Copy Markdown
Contributor

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


Note: the base branch has to come from github.base_ref: under pull_request_target, github.ref is now always the default branch. The #45345 run logs REF: refs/heads/master.

`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>
@github-actions

Copy link
Copy Markdown

PR summary e3b58ca9e7

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 e3b58ca9e7
Reference commit 02b1c3bc13

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_template.yml

@github-actions github-actions Bot added the CI Modifies the continuous integration setup or other automation label Oct 27, 2026
@bryangingechen
bryangingechen marked this pull request as ready for review October 27, 2026 19:31

@j-loreaux j-loreaux left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors merge

@mathlib-bors mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Oct 27, 2026
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)
@mathlib-bors mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Oct 27, 2026
@mathlib-bors

mathlib-bors Bot commented Oct 27, 2026

Copy link
Copy Markdown
Contributor

@mathlib-bors mathlib-bors Bot changed the title ci: skip the inputRev check on bump branches and PRs into them [Merged by Bors] - ci: skip the inputRev check on bump branches and PRs into them Oct 27, 2026
@mathlib-bors mathlib-bors Bot closed this Oct 27, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bors-staging This PR is currently being built by bors on the staging branch. CI Modifies the continuous integration setup or other automation ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants