Skip to content

Commit e12f733

Browse files
grunwegbryangingechen
grunweg
and
bryangingechen
committed
feat: check for PR titles which do not start with "feat" etc. (#29512)
We ignore draft PRs and PRs with the WIP label. The set of checks is intentionally kept small, and could be expanded in the future. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
1 parent be5e7c6 commit e12f733

File tree

7 files changed

+281
-0
lines changed

7 files changed

+281
-0
lines changed

‎.github/workflows/check_pr_titles.yaml‎

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
name: Check PR titles
2+
3+
on:
4+
pull_request_target:
5+
types:
6+
- opened
7+
- edited
8+
9+
# Limit permissions for GITHUB_TOKEN for the entire workflow
10+
permissions:
11+
contents: read
12+
pull-requests: write # Only allow PR comments/labels
13+
# All other permissions are implicitly 'none'
14+
15+
jobs:
16+
check_title:
17+
if: github.repository == 'leanprover-community/mathlib4' && (github.event.action == 'opened' || github.event.changes.title.from)
18+
runs-on: ubuntu-latest
19+
steps:
20+
- name: Checkout
21+
uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
22+
with:
23+
ref: master
24+
- name: Configure Lean
25+
uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0
26+
with:
27+
auto-config: false
28+
use-github-cache: false
29+
use-mathlib-cache: false
30+
31+
- name: check the PR title format
32+
id: pr-title-check
33+
if: github.event.pull_request.draft == false && github.event.pull_request.base == 'master'
34+
env:
35+
TITLE: ${{ github.event.pull_request.title }}
36+
run: |
37+
set -eo pipefail
38+
echo "$TITLE"
39+
label_names=$(echo "${{ toJson(github.event.pull_request.labels) }}" | jq -r '.[].name')
40+
echo "$label_names"
41+
42+
# build command so build lines don't pollute `output` below
43+
lake build check_title_labels
44+
45+
# Capture output and exit code
46+
if output=$(lake exe check_title_labels --labels "$label_names" "$TITLE" 2>&1); then
47+
echo "Check passed"
48+
else
49+
exit_code="$?"
50+
# Escape and set the output for use in subsequent steps
51+
{
52+
echo "errors<<EOF"
53+
echo "$output"
54+
echo "EOF"
55+
} >> "$GITHUB_OUTPUT"
56+
exit "$exit_code"
57+
fi
58+
59+
- name: Add comment to fix PR title
60+
uses: marocchino/sticky-pull-request-comment@773744901bac0e8cbb5a0dc842800d45e9b2b405 # v2.9.4
61+
if: ${{ steps.pr-title-check.outputs.success == 'false'}}
62+
with:
63+
header: 'PR Title Check'
64+
message: |
65+
### 🚨 PR Title Needs Formatting
66+
Please update the title to match our
67+
[commit style conventions](https://leanprover-community.github.io/contribute/commit.html).
68+
69+
Errors from script:
70+
```
71+
${{ steps.pr-title-check.outputs.errors }}
72+
```
73+
74+
<details>
75+
<summary>Details on the required title format</summary>
76+
77+
The title should fit the following format:
78+
```
79+
<kind>(<optional-scope>): <subject>
80+
```
81+
`<kind>` is:
82+
83+
- `feat` (feature)
84+
- `fix` (bug fix)
85+
- `doc` (documentation)
86+
- `style` (formatting, missing semicolons, ...)
87+
- `refactor`
88+
- `test` (when adding missing tests)
89+
- `chore` (maintain)
90+
- `perf` (performance improvement, optimization, ...)
91+
- `ci` (changes to continuous integration, repo automation, ...)
92+
93+
`<optional-scope>` is a name of module or a directory which contains changed modules.
94+
This is not necessary to include, but may be useful if the `<subject>` is insufficient.
95+
The `Mathlib` directory prefix is always omitted.
96+
For instance, it could be
97+
98+
- Data/Nat/Basic
99+
- Algebra/Group/Defs
100+
- Topology/Constructions
101+
102+
`<subject>` has the following constraints:
103+
104+
- do not capitalize the first letter
105+
- no dot(.) at the end
106+
- use imperative, present tense: "change" not "changed" nor "changes"
107+
</details>
108+
109+
- name: Add comment that PR title is fixed
110+
if: ${{ steps.pr-title-check.outputs.success == 'true'}}
111+
uses: marocchino/sticky-pull-request-comment@773744901bac0e8cbb5a0dc842800d45e9b2b405 # v2.9.4
112+
with:
113+
header: 'PR Title Check'
114+
# should do nothing if a 'PR Title Check' comment does not exist
115+
only_update: true
116+
message: |
117+
### ✅ PR Title Formatted Correctly
118+
The title of this PR has been updated to match our
119+
[commit style conventions](https://leanprover-community.github.io/contribute/commit.html).
120+
Thank you!

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6438,6 +6438,7 @@ public import Mathlib.Tactic.Linter.TextBased
64386438
public import Mathlib.Tactic.Linter.UnusedTactic
64396439
public import Mathlib.Tactic.Linter.UnusedTacticExtension
64406440
public import Mathlib.Tactic.Linter.UpstreamableDecl
6441+
public import Mathlib.Tactic.Linter.ValidatePRTitle
64416442
public import Mathlib.Tactic.Measurability
64426443
public import Mathlib.Tactic.Measurability.Init
64436444
public import Mathlib.Tactic.MinImports

‎Mathlib/Tactic.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -176,6 +176,7 @@ public import Mathlib.Tactic.Linter.TextBased
176176
public import Mathlib.Tactic.Linter.UnusedTactic
177177
public import Mathlib.Tactic.Linter.UnusedTacticExtension
178178
public import Mathlib.Tactic.Linter.UpstreamableDecl
179+
public import Mathlib.Tactic.Linter.ValidatePRTitle
179180
public import Mathlib.Tactic.Measurability
180181
public import Mathlib.Tactic.Measurability.Init
181182
public import Mathlib.Tactic.MinImports

‎Mathlib/Tactic/Linter/ValidatePRTitle.lean‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
/-
2+
Copyright (c) 2024 Michael Rothgang. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Michael Rothgang
5+
-/
6+
7+
module
8+
9+
import Mathlib.Init
10+
import Std.Internal.Parsec.String
11+
12+
/-!
13+
# Checker for well-formed title and labels
14+
This script checks if a PR title matches
15+
[mathlib's commit conventions](https://leanprover-community.github.io/contribute/commit.html).
16+
Not all checks from the commit conventions are implemented: for instance, no effort is made to
17+
verify whether the title or body are written in present imperative tense.
18+
-/
19+
20+
open Std.Internal.Parsec String
21+
22+
/-- Basic parser for PR titles: given a title `feat(scope): main title` or `feat: title`,
23+
extracts the `feat` 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+
<*> (
30+
(skipString "(" *> some <$> manyChars (notFollowedBy (skipString "):") *> any)
31+
<* skipString "): ")
32+
<|> (skipString ": " *> pure none)
33+
)
34+
35+
-- Some self-tests for the parser.
36+
/-- info: Except.ok ("feat", some "x") -/
37+
#guard_msgs in
38+
#eval Parser.run prTitle "feat(x): foo"
39+
/-- info: Except.ok ("feat", none) -/
40+
#guard_msgs in
41+
#eval Parser.run prTitle "feat: foo"
42+
/-- info: Except.error "offset 10: expected: ): " -/
43+
#guard_msgs in
44+
#eval Parser.run prTitle "feat(: foo"
45+
/-- info: Except.error "offset 4: expected: : " -/
46+
#guard_msgs in
47+
#eval Parser.run prTitle "feat): foo"
48+
/-- info: Except.error "offset 4: expected: : " -/
49+
#guard_msgs in
50+
#eval Parser.run prTitle "feat)(: foo"
51+
/-- info: Except.error "offset 4: expected: : " -/
52+
#guard_msgs in
53+
#eval Parser.run prTitle "feat)(sdf): foo"
54+
/-- info: Except.ok ("feat", some "sdf") -/
55+
#guard_msgs in
56+
#eval Parser.run prTitle "feat(sdf): foo:"
57+
/-- info: Except.error "offset 4: expected: : " -/
58+
#guard_msgs in
59+
#eval Parser.run prTitle "feat foo"
60+
/-- info: Except.ok ("chore", none) -/
61+
#guard_msgs in
62+
#eval Parser.run prTitle "chore: test"
63+
64+
/--
65+
Check if `title` matches the mathlib conventions for PR titles
66+
(documented at <https://leanprover-community.github.io/contribute/commit.html>).
67+
68+
Not all checks are implemented: for instance, no effort is made to verify if the title or body
69+
are written in present imperative tense.
70+
Return all error messages for violations found.
71+
-/
72+
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,
75+
-- but give some custom errors in some easily detectable cases.
76+
if !title.contains ':' then
77+
return #["error: the PR title does not contain a colon"]
78+
79+
match Parser.run prTitle title with
80+
| Except.error _ =>
81+
return #[s!"error: the PR title should be of the form\n abbrev: main title\nor\n \
82+
abbrev(scope): main title"]
83+
| Except.ok (kind, _scope?) =>
84+
-- Future: also check scope (and the main PR title)
85+
let mut errors := #[]
86+
let knownKinds := ["feat", "chore", "perf", "refactor", "style", "fix", "doc", "test", "ci"]
87+
let mut isFine := false
88+
for k in knownKinds do
89+
isFine := isFine || kind.startsWith k
90+
if isFine == false then
91+
errors := errors.push s!"error: the PR title should be of the form \
92+
\"kind: main title\" or \"kind(scope): main title\"\n
93+
Known PR title kinds are {knownKinds}"
94+
return errors

‎lakefile.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -128,6 +128,11 @@ lean_exe «lint-style» where
128128
-- Executables which import `Lake` must set `-lLake`.
129129
weakLinkArgs := #["-lLake"]
130130

131+
/-- `lake exe check-title-labels` checks if a PR title obeys some basic formatting requirements.
132+
Currently, these checks are quite lenient, but could be made stricter in the future. -/
133+
lean_exe «check_title_labels» where
134+
srcDir := "scripts"
135+
131136
/--
132137
`lake exe pole` queries the Mathlib speedcenter for build times for the current commit,
133138
and then calculates the longest pole

‎scripts/README.md‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,8 @@ to learn about it as well!
9090
- `lint-style.lean`, `lint-style.py`, `print-style-errors.sh`
9191
style linters, written in Python and Lean. Run via `lake exe lint-style`.
9292
Medium-term, the latter two scripts should be rewritten and incorporated in `lint-style.lean`.
93+
- `check-title-labels.lean` verifies that a (non-WIP, non-draft) PR has a well-formed title.
94+
In the future, it may also check that a feature PR has a topic label.
9395
- `lint-bib.sh`
9496
normalize the BibTeX file `docs/references.bib` using `bibtool`.
9597
- `yaml_check.py`, `check-yaml.lean`
@@ -152,6 +154,7 @@ Both of these files should tend to zero over time;
152154
please do not add new entries to these files. PRs removing (the need for) entries are welcome.
153155

154156
**API surrounding CI**
157+
- `check_title_labels.lean` is used to check whether a PR title follows our [commit style conventions](https://leanprover-community.github.io/contribute/commit.html).
155158
- `parse_lake_manifest_changes.py` compares two versions of `lake-manifest.json` to report
156159
dependency changes in Zulip notifications. Used by the `update_dependencies_zulip.yml` workflow
157160
to show which dependencies were updated, added, or removed, with links to GitHub diffs.

‎scripts/check_title_labels.lean‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
/-
2+
Copyright (c) 2024 Michael Rothgang. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Michael Rothgang
5+
-/
6+
7+
import Cli.Basic
8+
import Mathlib.Tactic.Linter.ValidatePRTitle
9+
10+
/-!
11+
# Checker for well-formed title and labels
12+
13+
This script checks if a PR title matches some of
14+
[mathlib's commit conventions](https://leanprover-community.github.io/contribute/commit.html).
15+
Currently, we only verify very basic checks: this could be made stricter in the future.
16+
17+
-/
18+
19+
open Cli in
20+
/-- Implementation of the `check-title-labels` command line program.
21+
The exit code is the number of violations found. -/
22+
def checkTitleLabelsCLI (args : Parsed) : IO UInt32 := do
23+
let title := (args.positionalArg! "title").value
24+
let labels : Array String := args.variableArgsAs! String
25+
-- We not validate titles of WIP PRs.
26+
if labels.contains "WIP" then return 0
27+
28+
let mut numberErrors := 0
29+
-- The title should be of the form "abbrev: main title" or "abbrev(scope): main title".
30+
let titleErrors : Array String := validateTitle title
31+
numberErrors := UInt32.ofNat titleErrors.size
32+
for err in titleErrors do
33+
IO.println err
34+
return min numberErrors 125
35+
36+
open Cli in
37+
/-- Setting up command line options and help text for `lake exe check-title-labels`. -/
38+
def checkTitleLabels : Cmd := `[Cli|
39+
«check-title-labels» VIA checkTitleLabelsCLI; ["0.0.1"]
40+
"Check that a PR title matches the formatting requirements at
41+
<https://leanprover-community.github.io/contribute/commit.html>.
42+
If this PR is a feature PR, also verify that it has a topic label,
43+
and that there are no contradictory labels.
44+
45+
If the inpupt title does not pass validation, output a list of errors."
46+
47+
FLAGS:
48+
"labels" : Array String; "list of label names of this PR\
49+
These are optional; we merely use a WIP label to skip any checks of the PR title"
50+
51+
ARGS:
52+
title : String; "this PR's title"
53+
54+
]
55+
56+
/-- The entrypoint to the `lake exe check-title-labels` command. -/
57+
def main (args : List String) : IO UInt32 := checkTitleLabels.validate args

0 commit comments

Comments
 (0)