feat: check PR description begins with "This PR"#40
Open
kim-em wants to merge 2 commits into
Open
Conversation
Adds scripts/pr_description/check_description.sh, a small shell script that reads a PR body and exits non-zero unless the first non-blank line starts with "This PR". The failure message printed on stderr is written so it can be used directly as the body of a sticky PR comment. The companion workflow lives in mathlib4 and will be added separately. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… indentation Address review feedback: - Require a literal space after `This PR` (was a glob, so `This PRs`, `This PR-foo`, `This PR.adds`, `This PR:` and bare `This PR` all spuriously passed). - Skip leading blank lines and HTML comments (single- and multi-line) so a PR template that opens with `<!-- ... -->` doesn't fail the check. - Stop stripping leading whitespace from the first content line so indented markdown code blocks (4-space) don't pass. - Strip a trailing CR so CRLF line endings work. - Tighten the failure message's first line to match the new rule. - Document that the companion workflow should run only on open PRs, so the check doesn't fire on closed/merged bodies that bors may have rewritten. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Contributor
Author
|
It also provides a nice minor generic-AI-slop barrier, as out of the box AIs really like to start PR descriptions with markdown headers... |
Contributor
|
Cross-referencing the (private) Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/180721-mathlib-maintainers/topic/.22This.20PR.22 |
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 PR adds a small
scripts/pr_description/check_description.shscript that fails if a PR body does not begin (after any leading blank lines and whitespace) with the literal phrase "This PR".The motivation is to make sure that pull requests come with at least minimal descriptions, by prompting the author to begin a declarative sentence!
The Lean FRO instituted this CI check some time ago, and everyone has been happy with the resulting improvement in PR description. The FRO found that this format ("This PR") was flexible enough to allow a wide variety of styles, but strict enough to get at least a sentence in every PR. Using declarative sentences with uniform "This PR" beginning also makes it plausible to assemble "release notes", by extracting these first paragraphs, and replacing "This PR" with etc mathlib4#1234 in each.
The check is intentionally minimal: it only requires that the first non-blank line starts with
This PR. The failure message says explicitly that it's nice if the description goes on to discuss the changes, their motivation, and any advice for downstream users, but that the bare minimum is one sentence saying what the PR does.The companion workflow that invokes this script lives in mathlib4 and will follow in a separate PR.
🤖 Prepared with Claude Code