diff --git a/lakefile.lean b/lakefile.lean index 212047a97ac351..22f2046155ed63 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -120,6 +120,12 @@ lean_exe shake where lean_exe «lint-style» where srcDir := "scripts" +/-- `lake exe check-title-labels` checks if a PR title is correctly formatted, +if the PR has some required area labels (or is not a feature PR) and +if there are no contradictory labels. -/ +lean_exe «check-title-labels» where + srcDir := "scripts" + /-- `lake exe pole` queries the Mathlib speedcenter for build times for the current commit, and then calculates the longest pole diff --git a/scripts/check-title-labels.lean b/scripts/check-title-labels.lean new file mode 100644 index 00000000000000..677100ba244748 --- /dev/null +++ b/scripts/check-title-labels.lean @@ -0,0 +1,152 @@ +/- +Copyright (c) 2024 Michael Rothgang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Rothgang +-/ + +import Cli.Basic +import Batteries.Data.HashMap +import Batteries.Data.String.Matcher + +/-! +# Checker for well-formed title and labels + +This script checks if a PR title matches mathlib's commit conventions, +and if the PR has any contradictory labels. +Not all checks from the commit conventions are implemented: for instance, no effort is made to +verify whether the title or body are written in present imperative tense. +-/ + +/-- Split a string in two, 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 before := s.extract 0 pos + let after := s.extract (s.next pos) s.endPos + (before, after) + +/-- +Check if `title` matches the mathlib conventions for PR titles +(documented at https://leanprover-community.github.io/contribute/commit.html). +Not all checks are implemented: for instance, no effort is made to verify if the title or body +are written in present imperative tense. +Return the number of individual violations found. +-/ +def validate_title (title: String) : IO UInt32 := do + -- The title should be of the form "abbrev: main title" or "abbrev(scope): main title". + if !title.contains ':' then + IO.println "error: the PR title does not contain a colon" + return 1 + let mut numberErrors : UInt32 := 0 + + -- Split 'title' at the first occurrence of ':'. + let (type, 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.containsSubstr " " then + IO.println "error: the PR title contains multiple consecutive spaces; please add just one" + numberErrors := numberErrors + 1 + let main := main.removeLeadingSpaces + if main.front.toLower != main.front then + IO.println "error: the main PR title should be lowercased" + numberErrors := numberErrors + 1 + + -- `type` 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 := (type.splitOn "(").length + let M := (type.splitOn ")").length + let known_types := ["feat", "chore", "perf", "refactor", "style", "fix", "doc", "test"] + if (N, M) == (1, 1) then + if known_types.contains type then + IO.println s!"error: the PR type should be one of {", ".intercalate (known_types.map (s!"\"{·}\""))}" + numberErrors := numberErrors + 1 + else if (N, M) == (2, 2) then + let idx := type.find (· == '(') + let idx2 := type.find (· == ')') + if idx2 < idx then + IO.println s!"error: mismatched parentheses; the PR type should be of the form abbrev(scope)" + numberErrors := numberErrors + 1 + let (scope, type) := splitAtPos type idx + if known_types.contains type then + IO.println s!"error: the PR type should be one of {", ".intercalate (known_types.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 type should be of the form abbrev or abbrev(scope)" + numberErrors := numberErrors + 1 + return numberErrors + + +/-- +Check if a combination of PR labels is considered contradictory. +`labels` contains the names of this PR's labels. +-/ +def has_contradictory_labels (labels : Array String) : Bool := Id.run do + -- Combine common labels. + let substitutions := [ + ("ready-to-merge", "bors"), ("auto-merge-after-CI", "bors"), + ("blocked-by-other-PR", "blocked"), ("blocked-by-core-PR", "blocked"), + ("blocked-by-batt-PR", "blocked"), ("blocked-by-qq-PR", "blocked"), + ] + let mut canonicalise : Std.HashMap String String := .ofList substitutions + let normalised_labels := labels.map fun label ↦ (canonicalise.getD label label) + -- Test for contradictory label combinations. + if normalised_labels.contains "awaiting-review-DONT-USE" then + return true + else if normalised_labels.contains "bors" && + ["awaiting-CI", "awaiting-zulip", "WIP"].any normalised_labels.contains then + return true + else if normalised_labels.contains "awaiting-zulip" && + ["delegated", "awaiting-zulip"].all normalised_labels.contains then + return true + else + return false + + +open Cli in +/-- Implementation of the `check-title-labels` command line program. +The exit code is the number of violations found. -/ +def checkTitleLabelsCLI (args : Parsed) : IO UInt32 := do + let title := (args.positionalArg! "title").value + let labels : Array String := args.variableArgsAs! String + let mut numberErrors := 0 + if !labels.contains "WIP" then + -- We do not complain about WIP PRs. + -- The title should be of the form "abbrev: main title" or "abbrev(scope): main title". + numberErrors := ← validate_title title + -- A feature PR should have a topic label. + if title.startsWith "feat" && !labels.any + (fun s ↦ s.startsWith "t-" || ["CI", "IMO"].contains s) then + IO.println "error: feature PRs should have a 't-something' or the 'CI' label" + numberErrors := numberErrors + 1 + -- Check for contradictory labels. + if has_contradictory_labels labels then + IO.println "error: PR labels are contradictory" + numberErrors := numberErrors + 1 + return numberErrors + + +open Cli in +/-- Setting up command line options and help text for `lake exe check-title-labels`. -/ +def checkTitleLabels : Cmd := `[Cli| + «check-title-labels» VIA checkTitleLabelsCLI; ["0.0.1"] + "Check that a PR title matches the formatting requirements. + If this PR is a feature PR, also verify that it has a topic label, + and that there are no contradictory labels." + + ARGS: + title : String; "this PR's title" + ...labels : Array String; "list of label names of this PR" +] + +/-- The entrypoint to the `lake exe check-title-labels` command. -/ +def main (args : List String) : IO UInt32 := checkTitleLabels.validate args