feat: generic linter, absorbing cdot linter and attribute [instance] in linter

Mathlib.lean

@@ -3664,6 +3664,7 @@ import Mathlib.Tactic.ByContra
 import Mathlib.Tactic.CC.Addition
 import Mathlib.Tactic.CC.Datatypes
 import Mathlib.Tactic.CC.Lemmas
+import Mathlib.Tactic.CDotLinter
 import Mathlib.Tactic.CancelDenoms
 import Mathlib.Tactic.CancelDenoms.Core
 import Mathlib.Tactic.Cases

Mathlib/Tactic.lean

@@ -13,6 +13,7 @@ import Mathlib.Tactic.ByContra
 import Mathlib.Tactic.CC.Addition
 import Mathlib.Tactic.CC.Datatypes
 import Mathlib.Tactic.CC.Lemmas
+import Mathlib.Tactic.CDotLinter
 import Mathlib.Tactic.CancelDenoms
 import Mathlib.Tactic.CancelDenoms.Core
 import Mathlib.Tactic.Cases

Mathlib/Tactic/Basic.lean

@@ -9,6 +9,7 @@ import Mathlib.Tactic.PPWithUniv
 import Mathlib.Tactic.ExtendDoc
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.TypeStar
+import Mathlib.Tactic.CDotLinter
 
 set_option autoImplicit true
 

Mathlib/Tactic/CDotLinter.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2024 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+import Lean.Elab.Command
+import Lean.Linter.Util
+
+/-!
+#  The "generic" linter
+
+The "generic" linter takes as input a function
+`unwanted : Syntax → Array Syntax` that returns the syntax nodes of an input syntax that
+should be flagged.
+
+
+TODO:
+* Add `blackout? : Syntax → Bool` to prevent further inspection by the linter?
+* Add `context? : InfoTree → Bool` for further effects combining `unwanted` and `blackout?` and
+  possibly doing some further filtering?
+
+See  #11890 for an example of how this may be extended.
+-/
+
+open Lean Elab
+
+namespace Mathlib.Linter
+
+/-- The "generic" linter emits a warning on "generic" syntax. -/
+register_option linter.generic : Bool := {
+  defValue := true
+  descr := "enable the generic linter"
+}
+
+namespace generic
+
+/-- find `cdot` syntax. -/
+partial
+def findDot : Syntax → (Array Syntax)
+  | stx@(.node _ k args) =>
+    let dargs := (args.map findDot).flatten
+    if k == ``Lean.Parser.Term.cdot then dargs.push stx else dargs
+  |_ => default
+
+/-- is the actual symbol `·`? -/
+def isCDot? : Syntax → Bool
+  | .node _ _ #[.atom _ v] => v == "·"
+  | _ => false
+
+/-- the main unwanted syntax: a `cdot` that is not a `·`. -/
+def unwanted.cDot (stx : Syntax) : Array Syntax :=
+  (findDot stx).filter (!isCDot? ·)
+
+end generic
+
+end Mathlib.Linter
+
+namespace Mathlib.Linter.generic
+
+/-- Gets the value of the `linter.generic` option. -/
+def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.generic o
+
+/-- The main implementation of the terminal refine linter. -/
+def terminalRefineLinter (contains? : Syntax → Array Syntax) : Linter where
+  run := withSetOptionIn fun stx => do
+    unless getLinterHash (← getOptions) do
+      return
+    if (← MonadState.get).messages.hasErrors then
+      return
+    let _ ← (contains? stx).mapM fun s =>
+      Linter.logLint linter.generic s m!"here"
+
+initialize addLinter (terminalRefineLinter unwanted.cDot)

scripts/noshake.json

@@ -280,7 +280,7 @@
   ["Mathlib.Tactic.CategoryTheory.MonoidalComp"],
   "Mathlib.Tactic.CC.Addition":
   ["Mathlib.Logic.Basic", "Mathlib.Tactic.CC.Lemmas"],
-  "Mathlib.Tactic.Basic": ["Batteries"],
+  "Mathlib.Tactic.Basic": ["Batteries", "Mathlib.Tactic.CDotLinter"],
   "Mathlib.Tactic.Attr.Register": ["Lean.Meta.Tactic.Simp.SimpTheorems"],
   "Mathlib.Tactic.ArithMult": ["Mathlib.Tactic.ArithMult.Init"],
   "Mathlib.RingTheory.PolynomialAlgebra": ["Mathlib.Data.Matrix.DMatrix"],