diff --git a/Mathlib/Tactic/Linter/ValidatePRTitle.lean b/Mathlib/Tactic/Linter/ValidatePRTitle.lean index 1fb45d557e4a16..478e2e9bf94488 100644 --- a/Mathlib/Tactic/Linter/ValidatePRTitle.lean +++ b/Mathlib/Tactic/Linter/ValidatePRTitle.lean @@ -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 diff --git a/MathlibTest/ValidatePRTitle.lean b/MathlibTest/ValidatePRTitle.lean index d7b20b55b20290..c20980f5058734 100644 --- a/MathlibTest/ValidatePRTitle.lean +++ b/MathlibTest/ValidatePRTitle.lean @@ -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" @@ -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"