feat: control environment linters with Lean.Option (#13893)

This PR makes environment linters (the declaration-level checks run by
`lake lint --builtin-lint`) controlled by `Lean.Option`s, just like
ordinary linters. Each environment linter is tied to a boolean option,
so you enable or disable it per declaration with `set_option linter.X
false in ...` and across a lint run with the new `lake lint
--linters=linter.X,-linter.Y` flag. Using `--lint-only` with the same
syntax will only collect information from the specified linters and will
not run the default on linters. The previous `lake lint` flags
`--extra`, `--lint-all`, and the `builtin_nolint` attribute, are removed
in favour of this option-based control.

Whether a linter applies to a declaration is decided by the value of its
controlling option at the time that declaration was elaborated.
`Lean.addDecl` snapshots the resolved value of every registered
environment-linter option for each new declaration (also from
`Elab.MutualDef`, where the inner `addDecl` runs on an async
environment) and stores it in an environment extension that `lake
builtin-lint` reads. The `@[builtin_env_linter linter.X]` attribute now
takes the controlling option name, and the registry maps option name to
linter declaration. `--linters` is translated into `weak` option
overrides applied to the lint build. `isAutoDecl` moves to a new
`Lean.AutoDecl` module so `Lean.addDecl` can use it.

Builds on #13852 (builtin linter sets); `linter.extra` becomes a linter
set whose members are the existing extra linters.

@claude was used to update the help string in Lake CLI, readapt the
tests (that were then manually cleaned) and to write this PR
description.

Author: wkrozowski

src/Init.lean

@@ -48,4 +48,3 @@ public import Init.BinderNameHint
 public import Init.Task
 public import Init.MethodSpecsSimp
 public import Init.LawfulBEqTactics
-public import Init.Linter

src/Init/Linter.lean

@@ -37,6 +37,7 @@ public import Lean.Log
 public import Lean.Linter
 public import Lean.SubExpr
 public import Lean.LabelAttribute
+public import Lean.AutoDecl
 public import Lean.AddDecl
 public import Lean.Replay
 public import Lean.PrivateName

src/Lean.lean

@@ -9,6 +9,8 @@ prelude
 public import Lean.Meta.Sorry
 public import Lean.Util.CollectAxioms
 public import Lean.OriginalConstKind
+public import Lean.AutoDecl
+import Lean.Linter.Init
 import Lean.Compiler.MetaAttr
 import all Lean.OriginalConstKind  -- for accessing `privateConstKindsExt`
 
@@ -28,7 +30,19 @@ private def Environment.addDeclAux (env : Environment) (opts : Options) (decl :
     (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment :=
   env.addDeclCore (Core.getMaxHeartbeats opts).toUSize decl cancelTk? (!debug.skipKernelTC.get opts)
 
-
+open Linter in
+/--
+Saves the state of `Lean.Option`s associated with environment linters into `envLinterSnapshotExt`
+-/
+def snapshotEnvLinterOptions (declName : Name) : CoreM Unit := do
+  let envLinterOpts ← envLinterOptionsRef.get
+  unless envLinterOpts.isEmpty do
+    let linterOptions ← getLinterOptions
+    unless ← isAutoDeclOrPrivate_Internal declName do
+      let mut snapshot : NameMap Bool := {}
+      for opt in envLinterOpts do
+        snapshot := snapshot.insert opt.name (getLinterValue opt linterOptions)
+      modifyEnv (envLinterSnapshotExt.insert · declName snapshot)
 
 private def isNamespaceName : Name → Bool
   | .str .anonymous _ => true
@@ -80,13 +94,7 @@ def warnIfUsesSorry (decl : Declaration) : CoreM Unit := do
 builtin_initialize
   registerTraceClass `addDecl
 
-/--
-Adds the given declaration to the environment's private scope, deriving a suitable presentation in
-the public scope if under the module system and if the declaration is not private. If `forceExpose`
-is true, exposes the declaration body, i.e. preserves the full representation in the public scope,
-independently of `Environment.isExporting` and even for theorems.
--/
-def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit :=
+private def addDeclCore (decl : Declaration) (forceExpose : Bool) : CoreM Unit :=
   withTraceNode `addDecl (fun _ => return m!"adding declarations {decl.getNames}") do
   -- register namespaces for newly added constants; this used to be done by the kernel itself
   -- but that is incompatible with moving it to a separate task
@@ -208,6 +216,15 @@ where
         return
       catch _ => pure ()
 
+/--
+Adds the given declaration to the environment's private scope, deriving a suitable presentation in
+the public scope if under the module system and if the declaration is not private. If `forceExpose`
+is true, exposes the declaration body, i.e. preserves the full representation in the public scope,
+independently of `Environment.isExporting` and even for theorems.
+-/
+def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit := do
+  addDeclCore decl forceExpose
+  discard <| decl.getTopLevelNames.mapM snapshotEnvLinterOptions
 
 def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true)
     (markMeta : Bool := false) : CoreM Unit := do

src/Lean/AddDecl.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
+-/
+
+module
+
+prelude
+public import Lean.Structure
+public import Lean.CoreM
+
+public section
+
+namespace Lean
+/--
+Returns true if `decl` is an automatically generated declaration.
+
+Also returns true if `decl` is an internal name or created during macro
+expansion.
+-/
+def isAutoDeclOrPrivate_Internal (decl : Name) : CoreM Bool := do
+  if decl.hasMacroScopes then return true
+  if decl.isInternal then return true
+  let env ← getEnv
+  if isReservedName env decl then return true
+  if let Name.str n s := decl then
+    if (← isAutoDeclOrPrivate_Internal n) then return true
+    if s.startsWith "proof_"
+        || s.startsWith "match_"
+        || s.startsWith "unsafe_"
+        || s.startsWith "grind_"
+    then return true
+    if env.isConstructor n && s ∈ ["injEq", "inj", "sizeOf_spec", "elim", "noConfusion"] then
+      return true
+    if let ConstantInfo.inductInfo _ := env.find? n then
+      if s.startsWith "brecOn_" || s.startsWith "below_" then return true
+      if s ∈ [casesOnSuffix, recOnSuffix, brecOnSuffix, belowSuffix,
+          "ndrec", "ndrecOn", "noConfusionType", "noConfusion", "ofNat", "toCtorIdx", "ctorIdx",
+          "ctorElim", "ctorElimType"] then
+        return true
+      if let some _ := isSubobjectField? env n (.mkSimple s) then
+        return true
+    -- Coinductive/inductive lattice-theoretic predicates:
+    if let ConstantInfo.inductInfo _ := env.find? (Name.str n "_functor") then
+      if s == "functor_unfold" || s == casesOnSuffix || s == "mutual" then return true
+      if env.isConstructor (Name.str (Name.str n "_functor") s) then return true
+  pure false
+
+end Lean

src/Lean/AutoDecl.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Lean.DocString.Add
 public import Lean.Linter.Init
-import Lean.Linter.EnvLinter.Nolint
 meta import Lean.Parser.Command
 
 public section

src/Lean/Elab/DeclModifiers.lean

@@ -10,10 +10,8 @@ Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
 module
 
 prelude
-public import Lean.Structure
 public import Lean.Elab.InfoTree.Main
-import Lean.ExtraModUses
-public import Lean.Linter.EnvLinter.Nolint
+public import Lean.AutoDecl
 
 public section
 
@@ -36,39 +34,6 @@ metadata is stored in the `EnvLinter` structure. We define two attributes:
    the linter with name `linterName`.
 -/
 
-/--
-Returns true if `decl` is an automatically generated declaration.
-
-Also returns true if `decl` is an internal name or created during macro
-expansion.
--/
-def isAutoDecl (decl : Name) : CoreM Bool := do
-  if decl.hasMacroScopes then return true
-  if decl.isInternal then return true
-  let env ← getEnv
-  if isReservedName env decl then return true
-  if let Name.str n s := decl then
-    if (← isAutoDecl n) then return true
-    if s.startsWith "proof_"
-        || s.startsWith "match_"
-        || s.startsWith "unsafe_"
-        || s.startsWith "grind_"
-    then return true
-    if env.isConstructor n && s ∈ ["injEq", "inj", "sizeOf_spec", "elim", "noConfusion"] then
-      return true
-    if let ConstantInfo.inductInfo _ := env.find? n then
-      if s.startsWith "brecOn_" || s.startsWith "below_" then return true
-      if s ∈ [casesOnSuffix, recOnSuffix, brecOnSuffix, belowSuffix,
-          "ndrec", "ndrecOn", "noConfusionType", "noConfusion", "ofNat", "toCtorIdx", "ctorIdx",
-          "ctorElim", "ctorElimType"] then
-        return true
-      if let some _ := isSubobjectField? env n (.mkSimple s) then
-        return true
-    -- Coinductive/inductive lattice-theoretic predicates:
-    if let ConstantInfo.inductInfo _ := env.find? (Name.str n "_functor") then
-      if s == "functor_unfold" || s == casesOnSuffix || s == "mutual" then return true
-      if env.isConstructor (Name.str (Name.str n "_functor") s) then return true
-  pure false
 
 /-- An environment linting test for the `lake builtin-lint` command. -/
 structure EnvLinter where
@@ -84,46 +49,50 @@ structure EnvLinter where
 
 /-- A `NamedEnvLinter` is an environment linter associated to a particular declaration. -/
 structure NamedEnvLinter extends EnvLinter where
-  /-- The name of the named linter. This is just the declaration name without the namespace. -/
-  name : Name
+  /-- The option name associated to the linter. -/
+  optName : Name
   /-- The linter declaration name -/
   declName : Name
 
-/-- Gets an environment linter by declaration name. -/
-def getEnvLinter (name declName : Name) : CoreM NamedEnvLinter := unsafe
-  return { ← evalConstCheck EnvLinter ``EnvLinter declName with name, declName }
+/-- Gets an environment linter by option name. -/
+def getEnvLinter (optName declName : Name) : CoreM NamedEnvLinter := unsafe
+  return { ← evalConstCheck EnvLinter ``EnvLinter declName with optName, declName }
 
 /-- Defines the `envLinterExt` extension for adding an environment linter to the default set. -/
 builtin_initialize envLinterExt :
-    SimplePersistentEnvExtension (Name × Bool) (NameMap (Name × Bool)) ←
-  let addEntryFn := fun m (n, b) => m.insert (n.updatePrefix .anonymous) (n, b)
+    SimplePersistentEnvExtension (Name × Name) (NameMap Name) ←
+  let addEntryFn := fun m (optName, declName) => m.insert optName declName
   registerSimplePersistentEnvExtension {
     addImportedFn := fun nss =>
       nss.foldl (init := {}) fun m ns => ns.foldl (init := m) addEntryFn
     addEntryFn
   }
 
 /--
-Defines the `@[builtin_env_linter]` attribute for adding a linter to the default set.
-The form `@[builtin_env_linter extra]` will not add the linter to the default set,
-but it can be selected by `lake builtin-lint --extra`.
-
-Linters are named using their declaration names, without the namespace. These must be distinct.
+Defines the `builtin_env_linter` attribute for registering an environment linter.
+Each environment linter needs to have a registered Boolean-value `Lean.Option` that will be
+associated with it by providing the option name in the attribute, i.e.
+`@[builtin_env_linter linter.envLinter.myLinter]`.
 -/
-syntax (name := builtin_env_linter) "builtin_env_linter" &" extra"? : attr
+syntax (name := builtin_env_linter) "builtin_env_linter " ident : attr
 
 builtin_initialize registerBuiltinAttribute {
   name := `builtin_env_linter
   descr := "Use this declaration as a linting test in `lake builtin-lint`"
   add   := fun decl stx kind => do
-    let dflt := stx[1].isNone
     unless kind == .global do throwError "invalid attribute `builtin_env_linter`, must be global"
-    let shortName := decl.updatePrefix .anonymous
-    if let some (declName, _) := (envLinterExt.getState (← getEnv)).find? shortName then
+    let optName ← match stx with
+    | `(attr| builtin_env_linter $id:ident) => pure id.getId
+    | _ => throwError "invalid `builtin_env_linter` syntax: expected an option name argument"
+    let env ← getEnv
+    unless env.contains optName do
+      throwError "invalid attribute `builtin_env_linter`, no constant named `{optName}`; \
+        did you forget `register_builtin_option {optName} : Bool := ...`?"
+    if let some declName := (envLinterExt.getState env).find? optName then
       Elab.addConstInfo stx declName
       throwError
-        "invalid attribute `builtin_env_linter`, linter `{shortName}` has already been declared"
-    let isPublic := !isPrivateName decl; let isMeta := isMarkedMeta (← getEnv) decl
+        "invalid attribute `builtin_env_linter`, linter `{optName}` has already been declared"
+    let isPublic := !isPrivateName decl; let isMeta := isMarkedMeta env decl
     unless isPublic && isMeta do
       throwError "invalid attribute `builtin_env_linter`, \
         declaration `{.ofConstName decl}` must be marked as `public` and `meta`\
@@ -133,7 +102,7 @@ builtin_initialize registerBuiltinAttribute {
     unless ← (isDefEq constInfo.type (mkConst ``EnvLinter)).run' do
       throwError "`{.ofConstName decl}` must have type `{.ofConstName ``EnvLinter}`, got \
         `{constInfo.type}`"
-    modifyEnv fun env => envLinterExt.addEntry env (decl, dflt)
+    modifyEnv fun env => envLinterExt.addEntry env (optName, decl)
 }
 
 end Lean.Linter.EnvLinter

src/Lean/Linter/EnvLinter/Basic.lean

@@ -11,6 +11,7 @@ module
 
 prelude
 public import Lean.Linter.EnvLinter.Basic
+public import Lean.Linter.Init
 import Lean.DeclarationRange
 import Lean.Util.Path
 import Lean.CoreM
@@ -32,48 +33,36 @@ inductive LintVerbosity
   | high
   deriving Inhabited, DecidableEq, Repr
 
-/-- Which set of linters to run. -/
-inductive LintScope
-  /-- Run only default linters. -/
-  | default
-  /-- Run default linters together with the non-default (extra) linters. -/
-  | extra
-  /-- Run all linters (default + extra). -/
-  | all
-  deriving Inhabited, DecidableEq, Repr
-
-/-- `getChecks` produces a list of linters to run.
-
-If `runOnly` is populated, only those named linters are run (regardless of `scope`).
-Otherwise, linter selection depends on `scope`:
-- `default`: only linters with `isDefault = true`
-- `extra`: linters with `isDefault = true` together with linters with `isDefault = false`
-- `all`: all linters -/
-def getChecks (scope : LintScope := .default) (runOnly : Option (List Name) := none) :
-    CoreM (Array NamedEnvLinter) := do
+/--
+Getter for the registered environment linters. The result is sorted by the linter option name.
+-/
+def getEnvLinters (opts? : Option LinterOptions := none) : CoreM (Array NamedEnvLinter) := do
   let mut result := #[]
-  for (name, declName, isDefault) in envLinterExt.getState (← getEnv) do
-    let shouldRun := match runOnly with
-      | some only => only.contains name
-      | none => match scope with
-        | .default => isDefault
-        | .extra => true
-        | .all => true
-    if shouldRun then
-      let linter ← getEnvLinter name declName
-      result := result.binInsert (·.name.lt ·.name) linter
+  for (optName, declName) in envLinterExt.getState (← getEnv) do
+      if opts?.all (isLinterEnabledByOptions optName) then
+        let linter ← getEnvLinter optName declName
+        result := result.binInsert (·.optName.lt ·.optName) linter
   pure result
 
+/--
+Queries the `envLinterSnapshotExt` to see if a given environment linter is enabled for the given
+declaration.
+-/
+def isLinterEnabledFor (env : Environment) (linter : NamedEnvLinter) (decl : Name) : Bool :=
+  match getEnvLinterSnapshotEntry? env decl linter.optName with
+  | some b => b
+  | none => false
 
 /--
 Runs all the specified linters on all the specified declarations in parallel,
 producing a list of results.
 -/
 def lintCore (decls : Array Name) (linters : Array NamedEnvLinter) :
     CoreM (Array (NamedEnvLinter × Std.HashMap Name MessageData)) := do
+  let env ← getEnv
   let tasks : Array (NamedEnvLinter × Array (Name × Task (Except Exception <| Option MessageData))) ←
     linters.mapM fun linter => do
-      let decls ← decls.filterM (shouldBeLinted linter.name)
+      let decls := decls.filter (isLinterEnabledFor env linter ·)
       (linter, ·) <$> decls.mapM fun decl => (decl, ·) <$> do
         let act : MetaM (Option MessageData) := do
           linter.test decl
@@ -148,7 +137,7 @@ def formatLinterResults
     (results : Array (NamedEnvLinter × Std.HashMap Name MessageData))
     (decls : Array Name)
     (groupByFilename : Bool)
-    (whereDesc : String) (scope : LintScope := .default)
+    (whereDesc : String)
     (verbose : LintVerbosity) (numLinters : Nat) (useErrorFormat : Bool := false) :
     CoreM MessageData := do
   let formattedResults ← results.filterMapM fun (linter, results) => do
@@ -158,23 +147,19 @@ def formatLinterResults
           groupedByFilename results (useErrorFormat := useErrorFormat)
         else
           printWarnings results
-      pure $ some m!"/- The `{linter.name}` linter reports:\n{linter.errorsFound} -/\n{warnings}\n"
+      pure $ some m!"/- The `{linter.optName}` linter reports:\n{linter.errorsFound} -/\n{warnings}\n"
     else if verbose = LintVerbosity.high then
       pure $ some m!"/- OK: {linter.noErrorsFound} -/"
     else
       pure none
   let mut s := MessageData.joinSep formattedResults.toList Format.line
-  let numAutoDecls := (← decls.filterM isAutoDecl).size
+  let numAutoDecls := (← decls.filterM isAutoDeclOrPrivate_Internal).size
   let failed := results.map (·.2.size) |>.foldl (·+·) 0
   unless verbose matches LintVerbosity.low do
     s := m!"-- Found {failed} error{if failed == 1 then "" else "s"
       } in {decls.size - numAutoDecls} declarations (plus {
       numAutoDecls} automatically generated ones) {whereDesc
       } with {numLinters} linters\n\n{s}"
-  match scope with
-  | .default => s := m!"{s}-- (non-default linters skipped)\n"
-  | .extra => pure ()
-  | .all => pure ()
   pure s
 
 /-- Get the list of declarations in the current module. -/