chore: further tweaks for the title checks around capitalisation (leanprover-community#40179)

Also allow a few selected suffixes to abbreviations. And make the error messages about suffixes more detailed.

Author: grunweg

Mathlib/Tactic/Linter/ValidatePRTitle.lean

@@ -119,11 +119,17 @@ 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).
+    -- 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)
-      if !isAbbreviation firstWord then
-        errors := errors.push "error: the PR subject should be lowercased"
+      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"
     if subject.endsWith "." then
       errors := errors.push "error: the PR title should not end with a full stop"
     else if subject.endsWith " " then

MathlibTest/ValidatePRTitle.lean

@@ -114,16 +114,35 @@ section subject
 #guard_msgs in
 #check_title "feat: bad title."
 
-/-- info: Message: 'error: the PR subject should be lowercased' -/
+/-- 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 should be lowercased' -/
+/--
+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"
 
@@ -196,13 +215,13 @@ 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 should be lowercased' -/
+/-- 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 should be lowercased' -/
+/-- info: Message: 'error: the PR subject `A new lemma` should be lowercased' -/
 #guard_msgs in
 #check_title "feat(ModuleForm): A new lemma"