ci: explain the expected format of bad PR titles better (leanprover-community#36523)

If a PR kind was not recognised, explain which ones are expected.

This also clarifies the check's logic: this error was supposed to be emitted already, but wasn't (due to a last-minute refactoring of the linter). Remove the old code path was never run (and is run now).

Author: grunweg

Mathlib/Tactic/Linter/ValidatePRTitle.lean

@@ -19,8 +19,8 @@ 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 `feat(scope): main title` or `feat: title`,
-extracts the `feat` and `scope` components. In the future, this will be extended to also parse
+/-- 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) :=
@@ -79,20 +79,13 @@ public def validateTitle (title : String) : Array String := Id.run do
   if title.startsWith " " then
     errors := #["error: the PR title starts with a space"]
 
+  let knownKinds := ["feat", "chore", "perf", "refactor", "style", "fix", "doc", "test", "ci"]
   match Parser.run prTitle title.trimAsciiStart.copy with
   | Except.error _ =>
-    return errors.push s!"error: the PR title should be of the form\n  abbrev: main title\n\
-      or\n  abbrev(scope): main title"
-  | Except.ok (kind, _scope?) =>
+    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)
-    let knownKinds := ["feat", "chore", "perf", "refactor", "style", "fix", "doc", "test", "ci"]
-    let mut isFine := false
-    for k in knownKinds do
-      isFine := isFine || kind.startsWith k
-    if isFine == false then
-      errors := errors.push s!"error: the PR title should be of the form \
-        \"kind: main title\" or \"kind(scope): main title\"\n
-        Known PR title kinds are {knownKinds}"
     if title.contains "  " then
       errors := errors.push
         "error: the PR title contains multiple consecutive spaces; please add just one"

MathlibTest/ValidatePRTitle.lean

@@ -24,9 +24,10 @@ elab "#check_title " title:str : command => do
 
 /--
 info: Message: 'error: the PR title should be of the form
-  abbrev: main title
+  kind: main title
 or
-  abbrev(scope): main title'
+  kind(scope): main title
+Allowed values for `kind` are [feat, chore, perf, refactor, style, fix, doc, test, ci]'
 -/
 #guard_msgs in
 #check_title "fsdfs: bad title"