Documentation

Mathlib.Tactic.Linter.ValidatePRTitle

Checker for well-formed title and labels #

This script checks if a PR title matches mathlib's commit conventions. 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.

def validateTitle (title : String) :
Array String

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 all error messages for violations found.

Instances For