Skip to content

feat(Tactic/Linter/ValidatePRTitle): do not check the capitalisation of the commit subject #43136

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
joneugster wants to merge 2 commits into
base: master
Choose a base branch
from
Open

feat(Tactic/Linter/ValidatePRTitle): do not check the capitalisation of the commit subject #43136

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e80da89
fix: disable pr title check for capitalisation
joneugster Aug 26, 2026
fe7618e
drop tests
joneugster Aug 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 3 additions & 11 deletions Mathlib/Tactic/Linter/ValidatePRTitle.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -119,17 +119,9 @@ public def validateTitle (title : String) : Array String := Id.run do
-- Future: we could check if `scope` describes a directory that actually exist.
-- Should we allow special syntax such as `Data/*/Basic` or `{Set,Group}Theory`?

-- Titles should be lower-cased (but we allow abbreviations, or a `s` or `'ed` suffix).
if subject.front.toLower != subject.front then
let firstWord := subject.takeWhile (!·.isWhitespace)
let suffixes := ["'s", "s", "'ed"]
let mut withoutSuffix := firstWord
for suff in suffixes do
if firstWord.endsWith suff then
withoutSuffix := firstWord.dropSuffix suff
break
if !(isAbbreviation withoutSuffix) then
errors := errors.push s!"error: the PR subject `{subject}` should be lowercased"
-- note: we do not check capitalisation as the subject might start with abbreviations or
-- proper nouns.

if subject.endsWith "." then
errors := errors.push "error: the PR title should not end with a full stop"
else if subject.endsWith " " then
Expand Down
40 changes: 0 additions & 40 deletions MathlibTest/ValidatePRTitle.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,38 +114,6 @@ section subject
#guard_msgs in
#check_title "feat: bad title."

/-- info: Message: 'error: the PR subject `My Bad Title` should be lowercased' -/
#guard_msgs in
#check_title "feat: My Bad Title"
-- Starting with an acronym is fine, however.
#guard_msgs in
#check_title "feat: RPC acronyms are fine"
#guard_msgs in #check_title "feat: `ℕ` is countable"
-- We also allow a `s`, `'s` or `'ed` suffix, as manual heuristic.
#guard_msgs in #check_title "feat: RPCs are yellow"
#guard_msgs in #check_title "chore: LLMs require adjusting our policies"
#guard_msgs in #check_title "chore: PR'ed lemmas"
#guard_msgs in #check_title "feat(CI): PR's to be deleted"
#guard_msgs in #check_title "chore: FCP'ed decisions should be listed separately"
-- We only remove at most one suffix.
/-- info: Message: 'error: the PR subject `PR'ed's lemmas` should be lowercased' -/
#guard_msgs in #check_title "chore: PR'ed's lemmas"
/-- info: Message: 'error: the PR subject `PRs's something` should be lowercased' -/
#guard_msgs in #check_title "chore: PRs's something"
-- This is not quite an abbreviation (and a grammar error).
/--
info: Message: 'error: the PR subject `FCPed decisions should be listed separately` should be lowercased'
-/
#guard_msgs in #check_title "chore: FCPed decisions should be listed separately"

-- This PR title is arguably not very bad (Lindelöf is a proper name),
-- a better fix is to start with a verb (which you should do anyway.)
/--
info: Message: 'error: the PR subject `Lindelöf spaces something something` should be lowercased'
-/
#guard_msgs in
#check_title "feat: Lindelöf spaces something something"

#guard_msgs in
#check_title "feat: add lemmas about Lindelöf spaces"

Expand Down Expand Up @@ -215,13 +183,5 @@ info: Message: 'error: the PR title contains multiple consecutive spaces; please
#guard_msgs in
#check_title "feat(ModuleForm): 2e is less than 6"

/-- info: Message: 'error: the PR subject `W3c` should be lowercased' -/
#guard_msgs in
#check_title "feat(ModuleForm): W3c"

#guard_msgs in
#check_title "feat(ModuleForm): W3C"

/-- info: Message: 'error: the PR subject `A new lemma` should be lowercased' -/
#guard_msgs in
#check_title "feat(ModuleForm): A new lemma"
Loading