[Merged by Bors] - ci: add commit verification for transient commits #33713

jcommelin · 2026-01-07T13:04:49Z

This PR adds a CI workflow that verifies PRs correctly use transient commits.
This is intended as a stepping stone towards verifying auto-generated commits, see #33707.

What this PR adds:

scripts/verify_commits.sh - Main verification script
.github/workflows/commit_verification.yml - GitHub Actions workflow

Testing locally

The commit at HEAD^^ contains test branch creation scripts. These can be used for testing the functionality of the two shell scripts. To test:

# Checkout the commit with test scripts
git checkout HEAD^^

# Create a test branch based on your current branch (before checkout)
# Save your branch name first:
BASE_BRANCH=$(git rev-parse --abbrev-ref HEAD)
git checkout HEAD^
./scripts/create_test_branch.sh $BASE_BRANCH

# Run verification (should pass)
./scripts/verify_commits.sh $BASE_BRANCH

# Clean up and return
git checkout $BASE_BRANCH && git branch -D ci-x-test-*

Available test scripts:

create_test_branch.sh - Creates a branch with valid transient commits (should pass)
create_test_branch_fail_conflict.sh - Transient commits cause cherry-pick conflicts (should fail)
create_test_branch_fail_transient.sh - Transient commits have net effect (should fail)

🤖 Generated with Claude Code

…ndling - Add show_diff_stat() helper to display file changes on verification failure - Remove spurious `git add -A` in transient verification (cherry-pick stages) - Track untracked files before/after auto-commit command to exclude pre-existing files from tree comparison - Restore state between transient and auto verification phases - Improve error messages with human-readable diff stats 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Allows --json output to be piped directly without log messages corrupting the JSON. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Cherry-pick conflicts indicate that transient commits don't cleanly separate from substantive commits, which means they have side effects. Remove the -X theirs fallback and fail immediately on any conflict. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

github-actions · 2026-01-07T13:05:58Z

PR summary 15f6691e7a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No 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 script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/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).

adomani · 2026-01-07T14:43:56Z

.github/workflows/commit_verification.yml

+name: Commit Verification
+
+on:
+  pull_request:


Suggested change

pull_request:

pull_request_target:

I think that it is ok to leave it as pull_request for testing, but it should probably become pull_request_target before merging.

I'm not sure if pull_request_target is better here. On the one hand it means we won't need to manually approve workflow runs, on the other hand, the workflow will have access to secrets so we need to be more careful about security.

Ok, I'll trust your judgement on this: I only have a superficial understanding of the security implications.

Let's start out with pull_request, I think.

scripts/verify_commits.sh

Co-authored-by: damiano <adomani@gmail.com>

bryangingechen · 2026-01-07T16:52:52Z

.github/workflows/commit_verification.yml

+
+          # Check if any commits have transient prefix
+          HAS_TRANSIENT=$(git log --format="%s" "$BASE_SHA..$HEAD_SHA" | \
+            grep -E "^transient" || true)


Is the prefix transient or transient: (with a colon and space)? Not that it's a particularly common word, but it'd be best to make this check as specific as possible.

Later on, there is

TRANSIENT_PREFIX: "transient"

and it would be good to connect the two: would adding them inside an

env: TRANSIENT_PREFIX="transient"

avoid repetition? (Or "transient: ", or whatever other string we agree on.)

Co-authored-by: damiano <adomani@gmail.com>

adomani · 2026-01-07T19:00:50Z

Thanks!

My view with anything CI-related is that it is easier and quicker to merge-and-test rapidly. In this case, the workflow is a separate one from the main build, so the main concern may be that there will be some CI error, but not much else.

In case @bryangingechen wants to suggest something more, I'll delegate to him!

bors d=bryangingechen

mathlib-bors · 2026-01-07T19:00:52Z

✌️ bryangingechen can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bryangingechen

Thanks! Excited to see how this goes!
bors d+

.github/workflows/commit_verification.yml

scripts/verify_commits.sh

mathlib-bors · 2026-01-07T19:24:07Z

✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

jcommelin

bors r+

This PR adds a CI workflow that verifies PRs correctly use transient commits. This is intended as a stepping stone towards verifying auto-generated commits, see #33707. What this PR adds: - `scripts/verify_commits.sh` - Main verification script - `.github/workflows/commit_verification.yml` - GitHub Actions workflow

mathlib-bors · 2026-01-07T23:36:04Z

Pull request successfully merged into master.

Build succeeded:

jcommelin and others added 9 commits January 7, 2026 08:46

transient: add design for new CI check

2351503

first attempt, thanks Claude

9e8c92e

refactor: rename generate_pr_summary.sh to verify_commits_summary.sh

6ab6a54

🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

fix(verify_commits): send log messages to stderr

e685198

Allows --json output to be piped directly without log messages corrupting the JSON. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

transient: add test branch creation scripts for local testing

0ad706c

transient: remove test scripts and RFC

5825901

remove functionality for verifying auto commits

2a0aac7

github-actions bot added the CI Modifies the continuous integration setup or other automation label Jan 7, 2026

jcommelin added 2 commits January 7, 2026 14:08

document new script in scripts/README.md

bd839ea

try to make the script cope with merge commits

0a931b2

adomani reviewed Jan 7, 2026

View reviewed changes

scripts/verify_commits.sh Outdated Show resolved Hide resolved

adomani reviewed Jan 7, 2026

View reviewed changes

scripts/verify_commits.sh Outdated Show resolved Hide resolved

Apply suggestions from code review

a051603

Co-authored-by: damiano <adomani@gmail.com>

bryangingechen reviewed Jan 7, 2026

View reviewed changes

jcommelin and others added 2 commits January 7, 2026 19:11

Update scripts/verify_commits.sh

5728655

Co-authored-by: damiano <adomani@gmail.com>

TRANSIENT_PREFIX

9005c14

leanprover-community-mathlib4-bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 7, 2026

bryangingechen reviewed Jan 7, 2026

View reviewed changes

.github/workflows/commit_verification.yml Outdated Show resolved Hide resolved

.github/workflows/commit_verification.yml Outdated Show resolved Hide resolved

scripts/verify_commits.sh Outdated Show resolved Hide resolved

Apply suggestions from code review

61cacb8

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

jcommelin commented Jan 7, 2026

View reviewed changes

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jan 7, 2026

mathlib-bors bot changed the title ~~ci: add commit verification for transient commits~~ [Merged by Bors] - ci: add commit verification for transient commits Jan 7, 2026

mathlib-bors bot closed this Jan 7, 2026

[Merged by Bors] - ci: add commit verification for transient commits #33713

[Merged by Bors] - ci: add commit verification for transient commits #33713

Uh oh!

Conversation

jcommelin commented Jan 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Testing locally

Uh oh!

github-actions bot commented Jan 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 15f6691e7a

Import changes for modified files

Declarations diff

Uh oh!

adomani Jan 7, 2026

Choose a reason for hiding this comment

Uh oh!

bryangingechen Jan 7, 2026

Choose a reason for hiding this comment

Uh oh!

adomani Jan 7, 2026

Choose a reason for hiding this comment

Uh oh!

jcommelin Jan 7, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

bryangingechen Jan 7, 2026

Choose a reason for hiding this comment

Uh oh!

adomani Jan 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jcommelin Jan 7, 2026

Choose a reason for hiding this comment

Uh oh!

adomani commented Jan 7, 2026

Uh oh!

mathlib-bors bot commented Jan 7, 2026

Uh oh!

bryangingechen left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Jan 7, 2026

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

jcommelin commented Jan 7, 2026 •

edited

Loading

github-actions bot commented Jan 7, 2026 •

edited

Loading

adomani Jan 7, 2026 •

edited

Loading