Tracking Issue: Linter / Formatter Wishlist

I am compiling a list of things we might like our linter / possible future code formatters / reviewdog to detect/correct/comment on. Feel free to add to this list, or augment items with related issues.

See also: This Zulip thread for Linter requests.

Linters

Style Guide Items

• Variable conventions
• 100 Character line limit
• Header and Imports
  • Presence of copyright header
  • Presence of module docstring
• Structuring Definitions and Theorems
  • : and := and infix operators
    • : and := go before linebreaks.
      • #6761
    • Use spaces on both sides of :, :=
    • Infix operators go before linebreaks and are surrounded by spaces.
  • After stating the theorem, we indent the lines in the subsequent proof by 2 spaces.
    • #7283
  • If the theorem statement requires multiple lines, indent the subsequent lines by 4 spaces.
    • #7283 Partially does this, but should be extended to more than 1 line.
  • the by is placed on the line prior to the first tactic
  • No orphaned parentheses
  • In a class or structure definition, fields are indented 2 spaces
  • and moreover each field should have a docstring.
  • When using a constructor taking several arguments in a definition with each argument on a new line, the arguments line up
  • When providing terms of structures or instances of classes, the where syntax should be used to avoid the need for enclosing braces
• Hypotheses left of colon
• Use a space after binders
• Anonymous functions
  • ↦ preferred to => (only slightly). note: before attempting this, gather consensus if this change is wanted (and worth the churn)
  • λ disallowed in favor of fun
• Calculations
  • calc keyword should be placed on the line prior to the start of the calculation, with the calculation indented.
  • Whichever relations are involved (e.g., = or ≤) should be aligned from one line to the next.
  • The underscores _ used as placeholders for terms indicating the continuation of the calculation should be left-justified.
• Tactic mode
  • When new goals arise as side conditions or steps, they are indented and preceded by a focusing dot · (inserted as .); the dot is not indented.
  • Often t0 <;> t1 is used to execute t0 and then t1 on all new goals. Either write the tactics in one line, or indent the following tactic.
• Make sure the right number of newlines exist between lemmas/sections
• Whitespace and delimiters
  • while $ is a synonym for <|, its use in mathlib is disallowed in favor of <| for consistency as well as because of the symmetry with |>.
• Comments
  • Documentation strings for declarations are delimited with /-- -/.

Items not in the style guide which might nevertheless be nice

• Nonterminal simp (calls to simp that do not close the goal) should be replaced with simp? output.
  • #7496
  • Nonterminal simp at and simp [...] calls should be linted as well.
  • the flexible linter does this: it is disabled by default, since not all errors have a nice fix
• When a namespace is open, ensure it isn't redundantly used on lemma invocations in proofs.
• Similarly, when a notation is available, make sure it is used.
• Look at namespaces / scoped notations that could be opened to shorten parts of the code.
• Use variables declared via variables keyword in the file when possible.
• Check for unnecessary parentheses
• Remove unnecessary/transitively-provided imports (This now exists in the form of Shake)
• Perhaps alphabetize the imports (apparently this changes behavior though, so be careful)
• Replace common ASCII with the corresponding unicode, such as <- to ←.
• Collapse sequences of calls to the same tactic into one call, where possible
  • rw / simp only into one call, when this doesn't affect proof readability.
  • intros
  • subst
• Replace calls to simp/simp only with simp_rw where possible/not too verbose, so that readers can use their cursor to inspect the effect of each step.
• Don't rw with unspecified arguments, this makes the proof harder to read.
• Make sure new lemma names follow the naming conventions (or at least that they don't make obvious mistakes).
• Double declarations of the same variable. i.e. don't use variable {α : Type*} at the top of the file, and then the same declaration again below.
• Use (∀ i, α i) or ((i : X) -> α i) according to whether the α i values are Props
• And even more compute intensive:
  • Make sure simp only calls don't use unnecessary lemmas
  • Generalize typeclasses as much as possible by attempting to replace instance arguments with weaker ones.
• Linter for unneeded by_cases
• Linter for unnecessarily strong TC assumptions
  • Catch cases like "we require AddCommMonoid M, then use only AddZeroClass M.
  • Prior work exists by @alexjbest, in Lean 3
• Similarly, a linter to check that types that do not need to be the same in a theorem definition aren't.
  • Inspired by the lemma fixed in #11205, this problem caught me up for a while, but was a one-character fix.
• Nonempty instance linter.
• A linter that warns you if you are building data using tactics.
• a linter for using Type instead of Type*
• linter for theorem and instance names that are too long
• A "low-level performance optimisation tactic linter", which replaces slower tactics with faster ones.

Formatters

A formatter does not exist yet, but when it does, the above issues should be revisited to see if the formatter can be made to correct issues that the linter would otherwise flag.

(Thanks to Floris, @MohanadAhmed, Sebastien Gouezel for contributing points)

This is a broad wishlist rather than a scoped implementation task. Start by selecting one unchecked linter or formatter item, then read the linked style-guide section and related Zulip thread or issue. Done would require a clearly defined, agreed-upon check or formatter behavior, but no file, entry point, or test is named here.