feat(CI): validate more aspects of PR titles

Mathlib/Tactic/Linter/ValidatePRTitle.lean

@@ -20,23 +20,31 @@ verify whether the title or body are written in present imperative tense.
 open Std.Internal.Parsec String
 
 /-- Basic parser for PR titles: given a title `kind(scope): main title` or `kind: title`,
-extracts the `kind` and `scope` components. In the future, this will be extended to also parse
-the main PR title. -/
--- TODO: also parse and return the main PR title
-def prTitle : Parser (String × Option String) :=
-  Prod.mk
-    <$> (["feat", "chore", "perf", "refactor", "style", "fix", "doc", "test", "ci"].firstM pstring)
-    <*> (
+extracts the `kind`, `scope` and `main title` components. -/
+def prTitle : Parser (String × Option String × String) := do
+  let kind ←
+    ["feat", "chore", "perf", "refactor", "style", "fix", "doc", "test", "ci"].firstM pstring
+  let scope ← (
       (skipString "(" *> some <$> manyChars (notFollowedBy (skipString "):") *> any)
         <* skipString "): ")
       <|> (skipString ": " *> pure none)
     )
+  let mainTitle ← many1Chars any
+  return (kind, scope, mainTitle)
 
 -- Some self-tests for the parser.
-/-- info: Except.ok ("feat", some "x") -/
+
+/-- info: Except.error "offset 6: expected: ): " -/
+#guard_msgs in
+#eval Parser.run prTitle "feat(x):"
+/-- info: Except.error "offset 9: unexpected end of input" -/
+#guard_msgs in
+#eval Parser.run prTitle "feat(x): "
+
+/-- info: Except.ok ("feat", some "x", "foo") -/
 #guard_msgs in
 #eval Parser.run prTitle "feat(x): foo"
-/-- info: Except.ok ("feat", none) -/
+/-- info: Except.ok ("feat", none, "foo") -/
 #guard_msgs in
 #eval Parser.run prTitle "feat: foo"
 /-- info: Except.error "offset 10: expected: ): " -/
@@ -51,13 +59,13 @@ def prTitle : Parser (String × Option String) :=
 /-- info: Except.error "offset 4: expected: : " -/
 #guard_msgs in
 #eval Parser.run prTitle "feat)(sdf): foo"
-/-- info: Except.ok ("feat", some "sdf") -/
+/-- info: Except.ok ("feat", some "sdf", "foo:") -/
 #guard_msgs in
 #eval Parser.run prTitle "feat(sdf): foo:"
 /-- info: Except.error "offset 4: expected: : " -/
 #guard_msgs in
 #eval Parser.run prTitle "feat foo"
-/-- info: Except.ok ("chore", none) -/
+/-- info: Except.ok ("chore", none, "test") -/
 #guard_msgs in
 #eval Parser.run prTitle "chore: test"
 
@@ -84,11 +92,24 @@ public def validateTitle (title : String) : Array String := Id.run do
   | Except.error _ =>
     return errors.push s!"error: the PR title should be of the form\n  kind: main title\n\
       or\n  kind(scope): main title\nAllowed values for `kind` are {knownKinds}"
-  | Except.ok (_kind, _scope?) =>
-    -- Future: also check scope (and the main PR title)
+  | Except.ok (_kind, scope?, mainTitle) =>
+    if let some scope := scope? then
+      if scope.startsWith "Mathlib/" then
+        errors := errors.push s!"error: the PR scope must not start with 'Mathlib/'"
+      if scope.endsWith ".lean" then
+        errors := errors.push s!"error: a PR's scope must not end with '.lean'"
+      -- Disabling this for now, to reduce warning fatigue. Might enable this in the future.
+      -- if scope.contains '.' then
+      --  errors := errors.push s!"error: a PR's scope should be a directory, not a module"
+      -- Future: we could check if `scope` describes a directory that actually exist.
+    -- Titles should be lower-cased: we don't enforce this for now.
+    if mainTitle.front.toLower != mainTitle.front then
+      errors := errors.push "error: the main PR title should be lowercased"
+    if mainTitle.endsWith "." then
+      errors := errors.push "error: the PR title should not end with a full stop"
     if title.contains "  " then
       errors := errors.push
         "error: the PR title contains multiple consecutive spaces; please add just one"
-    if title.endsWith "." then
-      errors := errors.push "error: the PR title should not end with a full stop"
+    -- Future: add more checks!
+
     return errors

MathlibTest/ValidatePRTitle.lean

@@ -18,6 +18,10 @@ elab "#check_title " title:str : command => do
 #guard_msgs in
 #check_title "feat(Algebra): my short PR title"
 
+/-- info: Message: 'error: the PR title does not contain a colon' -/
+#guard_msgs in
+#check_title ""
+
 /-- info: Message: 'error: the PR title does not contain a colon' -/
 #guard_msgs in
 #check_title "my short PR title"
@@ -32,23 +36,45 @@ Allowed values for `kind` are [feat, chore, perf, refactor, style, fix, doc, tes
 #guard_msgs in
 #check_title "fsdfs: bad title"
 
+-- TODO: can these error messages be more informative?
+/--
+info: Message: 'error: the PR title should be of the form
+  kind: main title
+or
+  kind(scope): main title
+Allowed values for `kind` are [feat, chore, perf, refactor, style, fix, doc, test, ci]'
+-/
+#guard_msgs in
+#check_title "feat:"
+
+/--
+info: Message: 'error: the PR title should be of the form
+  kind: main title
+or
+  kind(scope): main title
+Allowed values for `kind` are [feat, chore, perf, refactor, style, fix, doc, test, ci]'
+-/
+#guard_msgs in
+#check_title "feat: "
+
 /-- info: Message: 'error: the PR title should not end with a full stop' -/
 #guard_msgs in
 #check_title "feat: bad title."
 
--- Enable if/when we decide to enforce lower-cased titles.
--- /-- info: Message: 'error: the main PR title should be lowercased' -/
--- #guard_msgs in
--- #check_title "feat: My Bad Title"
+/-- info: Message: 'error: the main PR title should be lowercased' -/
+#guard_msgs in
+#check_title "feat: My Bad Title"
 
 -- Acronyms are valid PR titles, in any case.
+-- TODO: fix this false positive!
+/-- info: Message: 'error: the main PR title should be lowercased' -/
 #guard_msgs in
 #check_title "feat: RPC acronyms are fine"
 
 /--
-info: Message: 'error: the PR title contains multiple consecutive spaces; please add just one'
----
 info: Message: 'error: the PR title should not end with a full stop'
+---
+info: Message: 'error: the PR title contains multiple consecutive spaces; please add just one'
 -/
 #guard_msgs in
 #check_title "chore: bad   Title."