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.

Equations

• One or more equations did not get rendered due to their size.