feat: environment linter for definitions containing an underscore (#34519)

This is almost certainly a violation of the naming convention. In the medium-term, this should become a syntax linter: at the moment, there are too many exceptions in mathlib. Making this an environment linter allows auto-generating a list of existing exceptions.

We track the number of violations as a technical debt metric.

Author: grunweg

Mathlib/Tactic/Linter/Style.lean

@@ -12,6 +12,7 @@ public meta import Lean.Server.InfoUtils
 public meta import Mathlib.Tactic.Linter.Header  -- shake: keep
 public import Lean.Parser.Command
 public import Mathlib.Tactic.DeclarationNames
+public import Batteries.Tactic.Lint.Basic
 
 /-!
 ## Style linters
@@ -38,6 +39,10 @@ This file defines the following linters:
 - the `openClassical` linter checks for `open (scoped) Classical` statements which are not
   scoped to a single declaration
 - the `show` linter checks for `show`s that change the goal and should be replaced by `change`
+- the `nameCheck` linter checks for declarations whose names are in non-standard style, such as
+  by containing a double underscore. The `defsWithUnderscore` environment linter checks for
+  definitions whose name contains an underscore: that is also very likely to be a violation of
+  mathlib's naming convention.
 
 All of these linters are enabled in mathlib by default, but disabled globally
 since they enforce conventions which are inherently subjective.
@@ -518,6 +523,51 @@ def doubleUnderscore : Linter where run := withSetOptionIn fun stx => do
 
 initialize addLinter doubleUnderscore
 
+/-- Check `name` is a `Name` containing an underscore that should be linted against
+by the `defsWithUnderscore` linter. Namely, we do not lint
+* names ending in an underscore, or in a namespace ending with an underscore,
+* names containing guillemets `«»` (these tend to be `term<something>` declarations,
+  i.e. internal names for notation, not user-facing commands),
+* names with a component starting with `term` (e.g. `Nat.term_!`)
+* names starting with `Mathlib.Tactic`, `Mathlib.Parser` or containing a `Simps` component
+  (these are probably custom simps projections, i.e. affect how `simps` names its auto-generated
+  lemmas: we usually prefer a generated name `coe_support` over `coeSupport`, which requires a
+  projection named `coe_support`)
+* names that end in `_<number>` or in `_mathlib` (these tend to be autogenerated instance names),
+* library notes.
+-/
+public def isBadNameWithUnderscore (name : Name) : Bool := Id.run do
+  let s := name.toString
+  let declName := name
+  let last := declName.components.getLast?.getD `Default |>.toString
+  if last.endsWith '_' ||
+      s.contains '«' || declName.components.any (·.toString.startsWith "term") ||
+      (`LibraryNote).isPrefixOf declName ||
+      (`Mathlib.Tactic).isPrefixOf declName || (`Mathlib.Parser).isPrefixOf declName ||
+      declName.components.any (· == `Simps) ||
+      last.endsWith "_1" || last.endsWith "_2" || last.endsWith "_mathlib" ||
+      declName.components.any (·.toString.endsWith '_') then
+    return false
+  if declName.toString.contains "_" then return true
+  else return false
+
+open Batteries.Tactic.Lint in
+/-- Linter that checks for definitions whose name contains an underscore:
+such names violate the naming convention. -/
+@[env_linter] public def defsWithUnderscore : Batteries.Tactic.Lint.Linter where
+  noErrorsFound := "no definitions with an underscore in their name found."
+  errorsFound := "FOUND definitions with an underscore in their name."
+  test declName := do
+    unless ((← getEnv).find? declName).get!.isDefinition && !(← isAutoDecl declName) do return none
+    -- We also exclude simprocs: these should be named like normal lemmas.
+    -- check if their type is `Lean.Meta.Simp.Simproc`.
+    if ((← getEnv).find? declName).get!.type.isConstOf `Lean.Meta.Simp.Simproc then return none
+    if isBadNameWithUnderscore declName then
+      return m!"The definition `{declName}` contains an underscore. \
+        This almost surely violates mathlib's naming convention; \
+        use lowerCamelCase or UpperCamelCase instead."
+    else return none
+
 end Style.nameCheck
 
 /-! ### The "openClassical" linter -/

MathlibTest/LintStyle.lean

@@ -447,6 +447,36 @@ info: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20,
 #check "                              \"                \
                                                                   "
 
+/-! Tests for the `nameCheck` linter -/
+section
+
+open Mathlib.Linter.Style.nameCheck
+
+/- Unit tests for the `defsWithUnderscore` linter. -/
+#guard isBadNameWithUnderscore `Foo == false
+#guard isBadNameWithUnderscore `fooBarBaz == false
+#guard isBadNameWithUnderscore `foo_bar == true
+#guard isBadNameWithUnderscore `_fooFoo == true
+#guard isBadNameWithUnderscore `Foo._bar == true
+-- A namespace `Mathlib` in the middle does not silence the linter: we only test for a *prefix*
+-- `Mathlib`, `Mathlib.Parser` or `Mathlib.Tactic`.
+#guard isBadNameWithUnderscore `Nat.Mathlib.foo_bar == true
+#guard isBadNameWithUnderscore `Mathlib.Parser.foo_bar == false
+#guard isBadNameWithUnderscore `Mathlib.Tactic.foo_bar == false
+#guard isBadNameWithUnderscore `AlgebraicGeometry.Scheme.IdealSheafData.Simps.coe_support == false
+
+#guard isBadNameWithUnderscore `Mathlib.Mat._Foo == true
+#guard isBadNameWithUnderscore `Mathlib.foo_ == false
+#guard isBadNameWithUnderscore `«termXYZ» == false
+#guard isBadNameWithUnderscore `ExteriorAlgebra.«term⋀[_]^_» == false
+#guard isBadNameWithUnderscore `Nat.term_! == false
+#guard isBadNameWithUnderscore `Nat.foo_bar2 == true
+#guard isBadNameWithUnderscore `Nat.fooBar_2 == false
+#guard isBadNameWithUnderscore `Nat.foo_bar_2 == false
+#guard isBadNameWithUnderscore `LibraryNote.coercion_into_rings == false
+
+end
+
 /- Tests for the `openClassical` linter -/
 section openClassical