feat: check PR description begins with "This PR"#40
Draft
kim-em wants to merge 2 commits into
Draft
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>
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
1 participant
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 accompanying failure message is written to stderr and is intended to be reused verbatim as the body of a sticky PR comment.The motivation is to make the first sentence of every PR description usable as a release note. Today many PRs open with
## Summaryor a bare bullet list, which means the first sentence going into release notes is structural noise rather than a description of the change.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