Revamp and improve algorithm.

scripts/check-title-labels.lean

@@ -11,6 +11,13 @@ import Batteries.Data.HashMap
 # Main docstring: TODO!
 -/
 
+-- Split a string at a given position. Assumes `pos` is valid.
+-- FIXME: this should be added to batteries, as a version of "splitOn"
+def splitAtPos (s : String) (pos : String.Pos) : String × String :=
+  let kind := s.extract 0 pos
+  let main := s.extract (s.next pos) s.endPos
+  (kind, main)
+
 /--
 Check if `title` matches the mathlib conventions for PR titles.
 Return the number of individual violations found.
@@ -22,40 +29,51 @@ def validate_title(title: String) : IO UInt32 := do
     return 1
   let mut numberErrors : UInt32 := 0
 
-  let idx := title.find (· == ':')
   -- Split 'title' at the first occurrence of ':'.
-  -- XXX: is there better API for this, say in batteries?
-  let kind := title.extract 0 idx
-  let main := title.extract (title.next idx) title.endPos
+  let (kind, main) := splitAtPos title (title.find (· == ':'))
   if main.endsWith "." then
     IO.println "error: the PR title should not end with a full stop"
     numberErrors := numberErrors + 1
   if main.front != ' ' then
     IO.println "error: the PR should have the form 'abbrev: main title', with a space"
     numberErrors := numberErrors + 1
+  else if main.startsWith "  " then
+    IO.println "error: the PR title contains multiple consecutive spaces; please add just one"
+    numberErrors := numberErrors + 1
   let main := main.removeLeadingSpaces
-  -- FIXME: let main := main.dropPrefix " " from batteries would be better!
   if main.front.toLower != main.front then
     IO.println "error: the main PR title should be lowercased"
     numberErrors := numberErrors + 1
 
+  -- kind should be of the form abbrev or abbrev(scope), where `scope` is of the form
+  -- `Algebra/Basic`, without a leading `Mathlib` or a trailing `.lean`
   let N := (kind.splitOn "(").length
   let M := (kind.splitOn ")").length
   let known_kinds := ["feat", "chore", "perf", "refactor", "style", "fix", "doc"]
-  if N > 2 || M > 2 then
-    IO.println "error: the PR kind should be of the form abbrev or abbrev(scope)"
-    numberErrors := numberErrors + 1
-  else if (N == 2 && M == 1) || (N == 1 && M == 2) then
-    IO.println "error: the PR kind should be of the form abbrev or abbrev(scope)"
-    numberErrors := numberErrors + 1
-  else if (N == 2) && (M == 2) then
-    numberErrors := 0
-    -- TODO: split kind and scope; then validate kind and scope
-  else
-    -- N == M == 1, i.e. no scope in parentheses
+  if (N, M) == (1, 1) then
+    if !known_kinds.contains kind then
+      IO.println s!"error: the PR kind should be one of {", ".intercalate (known_kinds.map (s!"\"{·}\""))}"
+      numberErrors := numberErrors + 1
+  else if (N, M) == (2, 2) then
+    let idx := kind.find (· == '(')
+    let idx2 := kind.find (· == ')')
+    if idx2 < idx then
+      IO.println s!"error: mismatched parentheses; the PR kind should be of the form abbrev(scope)"
+      numberErrors := numberErrors + 1
+    let (scope, kind) := splitAtPos kind idx
     if !known_kinds.contains kind then
       IO.println s!"error: the PR kind should be one of {", ".intercalate (known_kinds.map (s!"\"{·}\""))}"
       numberErrors := numberErrors + 1
+    if scope.startsWith "Mathlib/" then
+      IO.println s!"error: the PR scope must not start with 'Mathlib/'"
+      numberErrors := numberErrors + 1
+    if scope.endsWith ".lean" then
+      IO.println s!"error: a PR's scope must not end with '.lean'"
+      numberErrors := numberErrors + 1
+    -- Future: we could further validate the scope, that this is a valid module or directory
+  else
+    IO.println "error: the PR kind should be of the form abbrev or abbrev(scope)"
+    numberErrors := numberErrors + 1
   return numberErrors