Skip to content

Commit 37fadc0

Browse files
grunwegb-mehta
grunweg
authored and
b-mehta
committed
feat(CI): validate PR titles more strictly (leanprover-community#39680)
- lint extraneous spaces (and any tabs) - check that PR scopes are well-formed - also extract the PR subject, and check that it does not end in a period, and starts in lower-case - linter about strange Unicode characters (anything not allowed by the Unicode linter) Continuation of leanprover-community#34518: this covers the remaining checks of leanprover-community#16303. (This does not check that the subject is in imperative, present tense.)
1 parent c321bf0 commit 37fadc0

2 files changed

Lines changed: 196 additions & 37 deletions

File tree

‎Mathlib/Tactic/Linter/ValidatePRTitle.lean‎

Lines changed: 70 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ Authors: Michael Rothgang
77
module
88

99
import Mathlib.Init
10+
import Mathlib.Tactic.Linter.TextBased.UnicodeLinter
1011
import Std.Internal.Parsec.String
1112

1213
/-!
@@ -20,47 +21,56 @@ verify whether the title or body are written in present imperative tense.
2021
open Std.Internal.Parsec String
2122

2223
/-- Basic parser for PR titles: given a title `kind(scope): main title` or `kind: title`,
23-
extracts the `kind` and `scope` components. In the future, this will be extended to also parse
24-
the main PR title. -/
25-
-- TODO: also parse and return the main PR title
26-
def prTitle : Parser (String × Option String) :=
27-
Prod.mk
28-
<$> (["feat", "chore", "perf", "refactor", "style", "fix", "doc", "test", "ci"].firstM pstring)
29-
<*> (
24+
extracts the `kind`, `scope` and `main title` components. -/
25+
def prTitle : Parser (String × Option String × String) := do
26+
let kind ←
27+
["feat", "chore", "perf", "refactor", "style", "fix", "doc", "test", "ci"].firstM pstring
28+
let scope ← (
3029
(skipString "(" *> some <$> manyChars (notFollowedBy (skipString "):") *> any)
31-
<* skipString "): ")
32-
<|> (skipString ": " *> pure none)
30+
<* skipString "):" <* ws)
31+
<|> (skipString ":" *> ws *> pure none)
3332
)
33+
let mainTitle ← manyChars any
34+
return (kind, scope, mainTitle)
3435

3536
-- Some self-tests for the parser.
36-
/-- info: Except.ok ("feat", some "x") -/
37+
38+
/-- info: Except.ok ("feat", some "x", "") -/
39+
#guard_msgs in
40+
#eval Parser.run prTitle "feat(x):"
41+
/-- info: Except.ok ("feat", some "x", "") -/
42+
#guard_msgs in
43+
#eval Parser.run prTitle "feat(x): "
44+
45+
/-- info: Except.ok ("feat", some "x", "foo") -/
3746
#guard_msgs in
3847
#eval Parser.run prTitle "feat(x): foo"
39-
/-- info: Except.ok ("feat", none) -/
48+
/-- info: Except.ok ("feat", none, "foo") -/
4049
#guard_msgs in
4150
#eval Parser.run prTitle "feat: foo"
42-
/-- info: Except.error "offset 10: expected: ): " -/
51+
/-- info: Except.error "offset 10: expected: ):" -/
4352
#guard_msgs in
4453
#eval Parser.run prTitle "feat(: foo"
45-
/-- info: Except.error "offset 4: expected: : " -/
54+
/-- info: Except.error "offset 4: expected: :" -/
4655
#guard_msgs in
4756
#eval Parser.run prTitle "feat): foo"
48-
/-- info: Except.error "offset 4: expected: : " -/
57+
/-- info: Except.error "offset 4: expected: :" -/
4958
#guard_msgs in
5059
#eval Parser.run prTitle "feat)(: foo"
51-
/-- info: Except.error "offset 4: expected: : " -/
60+
/-- info: Except.error "offset 4: expected: :" -/
5261
#guard_msgs in
5362
#eval Parser.run prTitle "feat)(sdf): foo"
54-
/-- info: Except.ok ("feat", some "sdf") -/
63+
/-- info: Except.ok ("feat", some "sdf", "foo:") -/
5564
#guard_msgs in
5665
#eval Parser.run prTitle "feat(sdf): foo:"
57-
/-- info: Except.error "offset 4: expected: : " -/
66+
/-- info: Except.error "offset 4: expected: :" -/
5867
#guard_msgs in
5968
#eval Parser.run prTitle "feat foo"
60-
/-- info: Except.ok ("chore", none) -/
69+
/-- info: Except.ok ("chore", none, "test") -/
6170
#guard_msgs in
6271
#eval Parser.run prTitle "chore: test"
6372

73+
open Mathlib.Linter.TextBased in
6474
/--
6575
Check if `title` matches the mathlib conventions for PR titles
6676
(documented at <https://leanprover-community.github.io/contribute/commit.html>).
@@ -70,8 +80,8 @@ are written in present imperative tense.
7080
Return all error messages for violations found.
7181
-/
7282
public def validateTitle (title : String) : Array String := Id.run do
73-
-- The title should be of the form "abbrev: main title" or "abbrev(scope): main title".
74-
-- We use the parser above to extract abbrev and scope ignoring the main title,
83+
-- The title should be of the form "abbrev: subject" or "abbrev(scope): subject".
84+
-- We use the parser above to extract abbrev, scope and PR subject,
7585
-- but give some custom errors in some easily detectable cases.
7686
if !title.contains ':' then
7787
return #["error: the PR title does not contain a colon"]
@@ -82,13 +92,47 @@ public def validateTitle (title : String) : Array String := Id.run do
8292
let knownKinds := ["feat", "chore", "perf", "refactor", "style", "fix", "doc", "test", "ci"]
8393
match Parser.run prTitle title.trimAsciiStart.copy with
8494
| Except.error _ =>
85-
return errors.push s!"error: the PR title should be of the form\n kind: main title\n\
86-
or\n kind(scope): main title\nAllowed values for `kind` are {knownKinds}"
87-
| Except.ok (_kind, _scope?) =>
88-
-- Future: also check scope (and the main PR title)
95+
return errors.push s!"error: the PR title should be of the form\n kind: subject\n\
96+
or\n kind(scope): subject\nAllowed values for `kind` are {knownKinds}"
97+
| Except.ok (_kind, scope?, subject) =>
98+
if subject.isEmpty then
99+
errors := errors.push s!"error: the PR title should not be empty"
100+
if let some scope := scope? then
101+
if scope.startsWith "Mathlib/" then
102+
errors := errors.push s!"error: a PR's scope must not start with 'Mathlib/'"
103+
if scope.contains " " then
104+
errors := errors.push s!"error: a PR's scope must not contain spaces"
105+
if scope.contains "\\" then
106+
errors := errors.push
107+
s!"error: a PR's scope must not contain backslashes --- use forward slashes instead"
108+
if scope.endsWith ".lean" then
109+
errors := errors.push s!"error: a PR's scope must not end with '.lean'"
110+
else if scope.contains '.' then
111+
errors := errors.push s!"error: a PR's scope should be a directory, not a module"
112+
-- Future: we could check if `scope` describes a directory that actually exist.
113+
-- Should we allow special syntax such as `Data/*/Basic` or `{Set,Group}Theory`?
114+
115+
-- Titles should be lower-cased (but we allow abbreviations).
116+
if subject.front.toLower != subject.front then
117+
let firstWord := subject.takeWhile (!·.isWhitespace)
118+
if !(firstWord.all (·.isUpper)) then
119+
errors := errors.push "error: the PR subject should be lowercased"
120+
if subject.endsWith "." then
121+
errors := errors.push "error: the PR title should not end with a full stop"
122+
else if subject.endsWith " " then
123+
errors := errors.push "error: the PR title should not end with a space"
89124
if title.contains " " then
90125
errors := errors.push
91126
"error: the PR title contains multiple consecutive spaces; please add just one"
92-
if title.endsWith "." then
93-
errors := errors.push "error: the PR title should not end with a full stop"
127+
if title.contains "\t" then
128+
errors := errors.push
129+
"error: the PR title contains a tab; please use single spaces instead"
130+
-- Check for unicode characters which are not allowed: we don't want direction-changing
131+
-- characters, invisible spaces or so (for example). We re-use the code in the Unicode linter.
132+
let badChars := title.chars.filter (fun c ↦ !UnicodeLinter.isAllowedCharacter c && c != '\t')
133+
if !badChars.isEmpty then
134+
let err := ", ".intercalate <| badChars.map
135+
(fun c ↦ s!"'{c}' ({UnicodeLinter.Char.printCodepointHex c}).")|>.toList
136+
errors := errors.push s!"error: the PR contains {badChars.length} Unicode characters \
137+
which are not allowed: {err}"
94138
return errors

‎MathlibTest/ValidatePRTitle.lean‎

Lines changed: 126 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -18,37 +18,128 @@ elab "#check_title " title:str : command => do
1818
#guard_msgs in
1919
#check_title "feat(Algebra): my short PR title"
2020

21+
/-- info: Message: 'error: the PR title does not contain a colon' -/
22+
#guard_msgs in
23+
#check_title ""
24+
2125
/-- info: Message: 'error: the PR title does not contain a colon' -/
2226
#guard_msgs in
2327
#check_title "my short PR title"
2428

29+
section kind
30+
2531
/--
2632
info: Message: 'error: the PR title should be of the form
27-
kind: main title
33+
kind: subject
2834
or
29-
kind(scope): main title
35+
kind(scope): subject
3036
Allowed values for `kind` are [feat, chore, perf, refactor, style, fix, doc, test, ci]'
3137
-/
3238
#guard_msgs in
3339
#check_title "fsdfs: bad title"
3440

41+
/--
42+
info: Message: 'error: the PR title should be of the form
43+
kind: subject
44+
or
45+
kind(scope): subject
46+
Allowed values for `kind` are [feat, chore, perf, refactor, style, fix, doc, test, ci]'
47+
-/
48+
#guard_msgs in
49+
#check_title "feat(test) :(confusing) bad title"
50+
51+
/--
52+
info: Message: 'error: the PR title should be of the form
53+
kind: subject
54+
or
55+
kind(scope): subject
56+
Allowed values for `kind` are [feat, chore, perf, refactor, style, fix, doc, test, ci]'
57+
-/
58+
#guard_msgs in
59+
#check_title "feat(test) : bad title"
60+
61+
end kind
62+
63+
/-- info: Message: 'error: the PR title should not be empty' -/
64+
#guard_msgs in
65+
#check_title "feat:"
66+
67+
/-- info: Message: 'error: the PR title should not be empty' -/
68+
#guard_msgs in
69+
#check_title "feat: "
70+
71+
/--
72+
info: Message: 'error: the PR title starts with a space'
73+
---
74+
info: Message: 'error: the PR title contains multiple consecutive spaces; please add just one'
75+
-/
76+
#guard_msgs in
77+
#check_title " feat: some PR title"
78+
79+
section scope
80+
81+
/-- info: Message: 'error: a PR's scope must not start with 'Mathlib/'' -/
82+
#guard_msgs in
83+
#check_title "feat(Mathlib/Algebra): title"
84+
85+
/-- info: Message: 'error: a PR's scope must not end with '.lean'' -/
86+
#guard_msgs in
87+
#check_title "feat(Algebra.lean): title"
88+
89+
/-- info: Message: 'error: a PR's scope should be a directory, not a module' -/
90+
#guard_msgs in
91+
#check_title "feat(Algebra.Topology): title"
92+
93+
/-- info: Message: 'error: a PR's scope must not contain spaces' -/
94+
#guard_msgs in
95+
#check_title "feat(Algebra Topology): title"
96+
97+
/--
98+
info: Message: 'error: a PR's scope must not contain backslashes --- use forward slashes instead'
99+
-/
100+
#guard_msgs in
101+
#check_title "feat(Algebra\\Too): title"
102+
103+
#guard_msgs in
104+
#check_title "feat(Algebra/Too): title"
105+
106+
end scope
107+
108+
section subject
109+
35110
/-- info: Message: 'error: the PR title should not end with a full stop' -/
36111
#guard_msgs in
37112
#check_title "feat: bad title."
38113

39-
-- Enable if/when we decide to enforce lower-cased titles.
40-
-- /-- info: Message: 'error: the main PR title should be lowercased' -/
41-
-- #guard_msgs in
42-
-- #check_title "feat: My Bad Title"
43-
44-
-- Acronyms are valid PR titles, in any case.
114+
/-- info: Message: 'error: the PR subject should be lowercased' -/
115+
#guard_msgs in
116+
#check_title "feat: My Bad Title"
117+
-- Starting with an acronym is fine, however.
45118
#guard_msgs in
46119
#check_title "feat: RPC acronyms are fine"
47120

121+
-- This PR title is arguably not very bad (Lindelöf is a proper name),
122+
-- a better fix is to start with a verb (which you should do anyway.)
123+
/-- info: Message: 'error: the PR subject should be lowercased' -/
124+
#guard_msgs in
125+
#check_title "feat: Lindelöf spaces something something"
126+
127+
#guard_msgs in
128+
#check_title "feat: add lemmas about Lindelöf spaces"
129+
130+
-- Tabs in PR titles are banned.
131+
/-- info: Message: 'error: the PR title contains a tab; please use single spaces instead' -/
132+
#guard_msgs in
133+
#check_title "feat: PR title with a \t tab"
134+
135+
/-- info: Message: 'error: the PR title contains a tab; please use single spaces instead' -/
136+
#guard_msgs in
137+
#check_title "feat(\t): RPC acronyms are fine"
138+
48139
/--
49-
info: Message: 'error: the PR title contains multiple consecutive spaces; please add just one'
50-
---
51140
info: Message: 'error: the PR title should not end with a full stop'
141+
---
142+
info: Message: 'error: the PR title contains multiple consecutive spaces; please add just one'
52143
-/
53144
#guard_msgs in
54145
#check_title "chore: bad Title."
@@ -65,6 +156,30 @@ info: Message: 'error: the PR title should not end with a full stop'
65156
#guard_msgs in
66157
#check_title "feat(test) (confusing) bad title"
67158

68-
-- TODO: should this error?
159+
-- TODO: should this give a better error?
160+
/-- info: Message: 'error: a PR's scope must not contain spaces' -/
69161
#guard_msgs in
70162
#check_title "feat(confusing) (forbidden): title"
163+
164+
#guard_msgs in
165+
#check_title "feat: umlauts such as Lindelöf spaces are allowed"
166+
167+
/--
168+
info: Message: 'error: the PR contains 2 Unicode characters which are not allowed: '' (U+206b)., '' (U+206c).'
169+
-/
170+
#guard_msgs in
171+
#check_title "feat: title with \u206B non-allowed unicode\u206C"
172+
173+
end subject
174+
175+
/--
176+
info: Message: 'error: a PR's scope must not start with 'Mathlib/''
177+
---
178+
info: Message: 'error: a PR's scope must not end with '.lean''
179+
---
180+
info: Message: 'error: the PR title should not end with a full stop'
181+
---
182+
info: Message: 'error: the PR title contains multiple consecutive spaces; please add just one'
183+
-/
184+
#guard_msgs in
185+
#check_title "feat(Mathlib/Algebra.lean): title."

0 commit comments

Comments
 (0)