feat: linter attribute improvements

* linters are now checked for redeclaration
* linters are now registered whether or not they are default-enabled
* `@[nolint foo]` checks that `foo` is a linter, and go to definition works
* `@[nolint]` attrs can only be applied in the current module

Std/Lean/NameMapAttribute.lean

@@ -30,9 +30,9 @@ def registerNameMapExtension (α) (name : Name := by exact decl_name%) :
     IO (NameMapExtension α) := do
   registerSimplePersistentEnvExtension {
     name
-    addImportedFn := fun ass => ass.foldl (init := ∅) fun
-                       | names, as => as.foldl (init := names) fun
-                         | names, (a,b) => names.insert a b
+    addImportedFn := fun ass =>
+      ass.foldl (init := ∅) fun names as =>
+        as.foldl (init := names) fun names (a, b) => names.insert a b
     addEntryFn    := fun s n => s.insert n.1 n.2
     toArrayFn     := fun es => es.toArray
   }

Std/Logic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Mario Carneiro
 -/
 import Std.Tactic.Basic
-import Std.Tactic.Lint.Basic
+import Std.Tactic.Lint.Misc
 
 instance {f : α → β} [DecidablePred p] : DecidablePred (p ∘ f) :=
   inferInstanceAs <| DecidablePred fun x => p (f x)

Std/Tactic/Lint/Basic.lean

@@ -18,33 +18,12 @@ framework.  A linter essentially consists of a function
 `(declaration : Name) → MetaM (Option MessageData)`, this function together with some
 metadata is stored in the `Linter` structure. We define two attributes:
 
- * `@[stdLinter]` applies to a declaration of type `Linter` and adds it to the default linter set.
+ * `@[std_linter]` applies to a declaration of type `Linter` and adds it to the default linter set.
 
  * `@[nolint linterName]` omits the tagged declaration from being checked by
    the linter with name `linterName`.
 -/
 
-/-- `@[nolint linterName]` omits the tagged declaration from being checked by
-the linter with name `linterName`. -/
-syntax (name := nolint) "nolint" (ppSpace ident)+ : attr
-
-/-- Defines the user attribute `nolint` for skipping `#lint` -/
-initialize nolintAttr : NameMapExtension (Array Name) ←
-  registerNameMapAttribute {
-    name := `nolint
-    descr := "Do not report this declaration in any of the tests of `#lint`"
-    add := fun _decl stx =>
-      match stx with
-        -- TODO: validate linter names
-        | `(attr|nolint $[$ids]*) => pure $ ids.map (·.getId.eraseMacroScopes)
-        | _ => throwError "unexpected nolint syntax {stx}"
-  }
-
-/-- Returns true if `decl` should be checked
-using `linter`, i.e., if there is no `nolint` attribute. -/
-def shouldBeLinted [Monad m] [MonadEnv m] (linter : Name) (decl : Name) : m Bool :=
-  return !((nolintAttr.find? (← getEnv) decl).getD {}).contains linter
-
 /--
 Returns true if `decl` is an automatically generated declaration.
 
@@ -81,27 +60,72 @@ structure Linter where
 
 /-- A `NamedLinter` is a linter associated to a particular declaration. -/
 structure NamedLinter extends Linter where
+  /-- The name of the named linter. This is just the declaration name without the namespace. -/
+  name : Name
   /-- The linter declaration name -/
   declName : Name
 
-/-- The name of the named linter. This is just the declaration name without the namespace. -/
-def NamedLinter.name (l : NamedLinter) : Name := l.declName.updatePrefix Name.anonymous
-
 /-- Gets a linter by declaration name. -/
-def getLinter (declName : Name) : CoreM NamedLinter := unsafe
-  return { ← evalConstCheck Linter ``Linter declName with declName }
-
-/-- Takes a list of names that resolve to declarations of type `linter`,
-and produces a list of linters. -/
-def getLinters (l : List Name) : CoreM (List NamedLinter) :=
-  l.mapM getLinter
-
-/-- Defines the `std_linter` attribute for adding a linter to the default set. -/
-initialize stdLinterAttr : TagAttribute ←
-  registerTagAttribute
-    (name := `std_linter)
-    (descr := "Use this declaration as a linting test in #lint")
-    (validate := fun name => do
-      let constInfo ← getConstInfo name
-      unless ← (isDefEq constInfo.type (mkConst ``Linter)).run' do
-        throwError "must have type Linter, got {constInfo.type}")
+def getLinter (name declName : Name) : CoreM NamedLinter := unsafe
+  return { ← evalConstCheck Linter ``Linter declName with name, declName }
+
+/-- Defines the `std_linter` extension for adding a linter to the default set. -/
+initialize stdLinterExt :
+    PersistentEnvExtension (Name × Bool) (Name × Bool) (NameMap (Name × Bool)) ←
+  let addEntryFn := fun m (n, b) => m.insert (n.updatePrefix .anonymous) (n, b)
+  registerPersistentEnvExtension {
+    mkInitial := pure {}
+    addImportedFn := fun nss => pure <|
+      nss.foldl (init := {}) fun m ns => ns.foldl (init := m) addEntryFn
+    addEntryFn
+    exportEntriesFn := fun es => es.fold (fun a _ e => a.push e) #[]
+  }
+
+/--
+Defines the `@[std_linter]` attribute for adding a linter to the default set.
+The form `@[std_linter disabled]` will not add the linter to the default set,
+but it will be shown by `#list_linters` and can be selected by the `#lint` command.
+
+Linters are named using their declaration names, without the namespace. These must be distinct.
+-/
+syntax (name := std_linter) "std_linter" &"disabled"? : attr
+
+initialize registerBuiltinAttribute {
+  name := `std_linter
+  descr := "Use this declaration as a linting test in #lint"
+  add   := fun decl stx kind => do
+    let dflt := stx[1].isNone
+    unless kind == .global do throwError "invalid attribute 'std_linter', must be global"
+    let shortName := decl.updatePrefix .anonymous
+    if let some (declName, _) := (stdLinterExt.getState (← getEnv)).find? shortName then
+      Elab.addConstInfo stx declName
+      throwError "invalid attribute 'std_linter', linter '{shortName}' has already been declared"
+    let constInfo ← getConstInfo decl
+    unless ← (isDefEq constInfo.type (mkConst ``Linter)).run' do
+      throwError "must have type Linter, got {constInfo.type}"
+    modifyEnv fun env => stdLinterExt.addEntry env (decl, dflt)
+}
+
+/-- `@[nolint linterName]` omits the tagged declaration from being checked by
+the linter with name `linterName`. -/
+syntax (name := nolint) "nolint" (ppSpace ident)+ : attr
+
+/-- Defines the user attribute `nolint` for skipping `#lint` -/
+initialize nolintAttr : ParametricAttribute (Array Name) ←
+  registerParametricAttribute {
+    name := `nolint
+    descr := "Do not report this declaration in any of the tests of `#lint`"
+    getParam := fun _ => fun
+      | `(attr| nolint $[$ids]*) => ids.mapM fun id => withRef id <| do
+        let shortName := id.getId.eraseMacroScopes
+        let some (declName, _) := (stdLinterExt.getState (← getEnv)).find? shortName
+          | throwError "linter '{shortName}' not found"
+        Elab.addConstInfo id declName
+        pure shortName
+      | _ => Elab.throwUnsupportedSyntax
+  }
+
+/-- Returns true if `decl` should be checked
+using `linter`, i.e., if there is no `nolint` attribute. -/
+def shouldBeLinted [Monad m] [MonadEnv m] (linter : Name) (decl : Name) : m Bool :=
+  return !((nolintAttr.getParam? (← getEnv) decl).getD #[]).contains linter

Std/Tactic/Lint/Frontend.lean

@@ -73,11 +73,16 @@ inductive LintVerbosity
 If `useOnly` is true, it only uses the linters in `extra`.
 Otherwise, it uses all linters in the environment tagged with `@[linter]`.
 If `slow` is false, it only uses the fast default tests. -/
-def getChecks (slow : Bool) (extra : List Name) (useOnly : Bool) : CoreM (List NamedLinter) := do
-  let default ← if useOnly then pure [] else
-    getLinters (stdLinterAttr.getDecls (← getEnv)).toList
-  let default := if slow then default else default.filter (·.isFast)
-  pure $ default ++ (← getLinters extra)
+def getChecks (slow : Bool) (useOnly : Bool) : CoreM (Array NamedLinter) := do
+  let mut result := #[]
+  unless useOnly do
+    for (name, declName, dflt) in stdLinterExt.getState (← getEnv) do
+      if dflt then
+        let linter ← getLinter name declName
+        if slow || linter.isFast then
+          let _ := Inhabited.mk linter
+          result := result.binInsert (·.name.lt ·.name) linter
+  pure result
 
 /--
 Runs all the specified linters on all the specified declarations in parallel,
@@ -212,15 +217,21 @@ elab "#lint"
     | _ => throwUnsupportedSyntax
   let fast := fast.isSome
   let only := only.isSome
-  let extraLinters ← linters.mapM fun id =>
-    withScope ({ · with currNamespace := `Std.Tactic.Lint }) <|
-      resolveGlobalConstNoOverload id
-  let linters ← liftCoreM <| getChecks (slow := !fast) extraLinters.toList only
-  let results ← liftCoreM <| lintCore decls linters.toArray
+  let linters ← liftCoreM do
+    let mut result ← getChecks (slow := !fast) only
+    let linterState := stdLinterExt.getState (← getEnv)
+    for id in linters do
+      let name := id.getId.eraseMacroScopes
+      let some (declName, _) := linterState.find? name | throwErrorAt id "not a linter: {name}"
+      let linter ← getLinter name declName
+      let _ := Inhabited.mk linter
+      result := result.binInsert (·.name.lt ·.name) linter
+    pure result
+  let results ← liftCoreM <| lintCore decls linters
   let failed := results.any (!·.2.isEmpty)
   let mut fmtResults ← liftCoreM <|
     formatLinterResults results decls (groupByFilename := groupByFilename)
-      whereDesc (runSlowLinters := !fast) verbosity linters.length
+      whereDesc (runSlowLinters := !fast) verbosity linters.size
   if failed then
     logError fmtResults
   else if verbosity != LintVerbosity.low then
@@ -229,12 +240,10 @@ elab "#lint"
 open Elab Command in
 /-- The command `#list_linters` prints a list of all available linters. -/
 elab "#list_linters" : command => do
-  let env ← getEnv
-  let ns : Array Name := env.constants.fold (init := #[]) fun ns n ci =>
-    if n.getPrefix == `Std.Tactic.Lint && ci.type == mkConst ``Std.Tactic.Lint.Linter
-      then ns.push n else ns
-  let linters ← ns.mapM fun n => do
-    let b := stdLinterAttr.hasTag (← getEnv) n
-    pure $ toString (n.updatePrefix Name.anonymous) ++ if b then " (*)" else ""
-  logInfo m!"Available linters (linters marked with (*) are in the default lint set):\n{
-    Format.joinSep linters.toList Format.line}"
+  let mut result := #[]
+  for (name, _, dflt) in stdLinterExt.getState (← getEnv) do
+    result := result.binInsert (·.1.lt ·.1) (name, dflt)
+  let mut msg := m!"Available linters (linters marked with (*) are in the default lint set):"
+  for (name, dflt) in result do
+    msg := msg ++ m!"\n{name}{if dflt then " (*)" else ""}"
+  logInfo msg

Std/Tactic/Lint/Misc.lean

@@ -30,7 +30,7 @@ This file defines several small linters.
       | return none
     return m!"The namespace {dup} is duplicated in the name"
 
-/-- A linter object for checking for unused arguments.
+/-- A linter for checking for unused arguments.
 We skip all declarations that contain `sorry` in their value. -/
 @[std_linter] def unusedArguments : Linter where
   noErrorsFound := "No unused arguments."
@@ -55,7 +55,7 @@ We skip all declarations that contain `sorry` in their value. -/
       addMessageContextFull <| .joinSep (← unused.toList.mapM fun (arg, i) =>
           return m!"argument {i+1} {arg} : {← inferType arg}") m!", "
 
-/-- A linter for checking definition doc strings -/
+/-- A linter for checking definition doc strings. -/
 @[std_linter] def docBlame : Linter where
   noErrorsFound := "No definitions are missing documentation."
   errorsFound := "DEFINITIONS ARE MISSING DOCUMENTATION STRINGS:"
@@ -74,8 +74,8 @@ We skip all declarations that contain `sorry` in their value. -/
     let (none) ← findDocString? (← getEnv) declName | return none
     return m!"{kind} missing documentation string"
 
-/-- A linter for checking theorem doc strings -/
-def docBlameThm : Linter where
+/-- A linter for checking theorem doc strings. -/
+@[std_linter disabled] def docBlameThm : Linter where
   noErrorsFound := "No theorems are missing documentation."
   errorsFound := "THEOREMS ARE MISSING DOCUMENTATION STRINGS:"
   test declName := do
@@ -120,9 +120,9 @@ has been used. -/
 /--
 `univParamsGrouped e` computes for each `level` `u` of `e` the parameters that occur in `u`,
 and returns the corresponding set of lists of parameters.
-In pseudo-mathematical form, this returns `{ { p : parameter | p ∈ u } | (u : level) ∈ e }`
-FIXME: We use `Array Name` instead of `HashSet Name`, since `HashSet` does not have an equality instance.
-It will ignore `nm₀.proof_i` declarations.
+In pseudo-mathematical form, this returns `{{p : parameter | p ∈ u} | (u : level) ∈ e}`
+FIXME: We use `Array Name` instead of `HashSet Name`, since `HashSet` does not have an equality
+instance. It will ignore `nm₀.proof_i` declarations.
 -/
 private def univParamsGrouped (e : Expr) (nm₀ : Name) : BaseIO (Lean.HashSet (Array Name)) := do
   let res ← IO.mkRef {}
@@ -204,9 +204,6 @@ with rfl when elaboration results in a different term than the user intended. -/
         return m!"LHS equals RHS syntactically"
       return none
 
-attribute [nolint synTaut] rfl
-
-
 /--
 Return a list of unused have/suffices/let_fun terms in an expression.
 This actually finds all beta-redexes.
@@ -223,7 +220,7 @@ def findUnusedHaves (e : Expr) : MetaM (Array MessageData) := do
   res.get
 
 /-- A linter for checking that declarations don't have unused term mode have statements. We do not
-tag this as `@[stdLlinter]` so that it is not in the default linter set as it is slow and an
+tag this as `@[std_linter]` so that it is not in the default linter set as it is slow and an
 uncommon problem. -/
 @[std_linter] def unusedHavesSuffices : Linter where
   noErrorsFound := "No declarations have unused term mode have statements."
@@ -251,7 +248,7 @@ uncommon problem. -/
 A linter for checking if variables appearing on both sides of an iff are explicit. Ideally, such
 variables should be implicit instead.
 -/
-def explicitVarsOfIff : Linter where
+@[std_linter disabled] def explicitVarsOfIff : Linter where
   noErrorsFound := "No explicit variables on both sides of iff"
   errorsFound := "EXPLICIT VARIABLES ON BOTH SIDES OF IFF"
   test declName := do

scripts/runLinter.lean

@@ -9,7 +9,7 @@ abbrev NoLints := Array (Name × Name)
 /-- Read the given file path and deserialize it as JSON. -/
 def readJsonFile (α) [FromJson α] (path : System.FilePath) : IO α := do
   let _ : MonadExceptOf String IO := ⟨throw ∘ IO.userError, fun x _ => x⟩
-  liftExcept <| fromJson? <|<- liftExcept <| Json.parse <|<- IO.FS.readFile path
+  liftExcept <| fromJson? <|← liftExcept <| Json.parse <|← IO.FS.readFile path
 
 /-- Serialize the given value `a : α` to the file as JSON. -/
 def writeJsonFile [ToJson α] (path : System.FilePath) (a : α) : IO Unit :=
@@ -25,7 +25,7 @@ elab "compile_time_search_path" : term =>
   return toExpr (← searchPathRef.get)
 
 /--
-Usage: `runLinter [--update] [Std.Data.Nat]`
+Usage: `runLinter [--update] [Std.Data.Nat.Basic]`
 
 Runs the linters on all declarations in the given module (or `Std` by default).
 If `--update` is set, the `nolints` file is updated to remove any declarations that no longer need
@@ -41,7 +41,7 @@ unsafe def main (args : List String) : IO Unit := do
       | [] => some `Std
       | [mod] => Syntax.decodeNameLit s!"`{mod}"
       | _ => none
-    | IO.eprintln "Usage: runLinter [--update] [Std.Data.Nat]" *> IO.Process.exit 1
+    | IO.eprintln "Usage: runLinter [--update] [Std.Data.Nat.Basic]" *> IO.Process.exit 1
   let nolintsFile := "scripts/nolints.json"
   let nolints ← readJsonFile NoLints nolintsFile
   searchPathRef.set compile_time_search_path
@@ -50,11 +50,11 @@ unsafe def main (args : List String) : IO Unit := do
     let state := {env}
     Prod.fst <$> (CoreM.toIO · ctx state) do
       let decls ← getDeclsInPackage `Std
-      let linters ← getChecks (slow := true) (extra := []) (useOnly := false)
-      let results ← lintCore decls linters.toArray
+      let linters ← getChecks (slow := true) (useOnly := false)
+      let results ← lintCore decls linters
       if update then
         writeJsonFile (α := NoLints) nolintsFile <|
-          .qsort (lt := fun (a,b) (c,d) => a.lt c || (a == c && b.lt d)) <|
+          .qsort (lt := fun (a, b) (c, d) => a.lt c || (a == c && b.lt d)) <|
           .flatten <| results.map fun (linter, decls) =>
           decls.fold (fun res decl _ => res.push (linter.name, decl)) #[]
       let results := results.map fun (linter, decls) =>
@@ -64,8 +64,8 @@ unsafe def main (args : List String) : IO Unit := do
       if failed then
         let fmtResults ←
           formatLinterResults results decls (groupByFilename := true)
-            "in Std" (runSlowLinters := true) .medium linters.length
+            "in Std" (runSlowLinters := true) .medium linters.size
         IO.print (← fmtResults.toString)
         IO.Process.exit 1
       else
-        IO.print "-- Linting passed."
+        IO.println "-- Linting passed."