feat: control environment linters with Lean.Options

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/Lean.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/AddDecl.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,16 @@ 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
+def snapshotEnvLinterOptions (declName : Name) : CoreM Unit := do
+  let envLinterOpts ← envLinterOptionsRef.get
+  let linterOptions ← getLinterOptions
+  unless envLinterOpts.isEmpty do
+    unless ← isAutoDecl declName do
+      let mut snapshot : NameMap Bool := {}
+      for opt in envLinterOpts do
+        snapshot := snapshot.insert opt.name (getLinterValue opt linterOptions)
+      modifyEnv (envLinterSnapshotExt.addEntry · (declName, snapshot))
 
 private def isNamespaceName : Name → Bool
   | .str .anonymous _ => true
@@ -86,7 +97,7 @@ the public scope if under the module system and if the declaration is not privat
 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 +219,9 @@ where
         return
       catch _ => pure ()
 
+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/AutoDecl.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 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
+
+end Lean

src/Lean/Elab/DeclModifiers.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/MutualDef.lean

@@ -1269,6 +1269,9 @@ where
         guard (!isPrivateName declId.declName || (← ResolveName.backward.privateInPublic.getM)) *>
         some .axiom)
     setEnv async.mainEnv
+    -- Inner `addDecl` from `finishElab` will run on `async.asyncEnv`, where extension modifications
+    -- are not reported back (`reportExts := false`)
+    snapshotEnvLinterOptions declId.declName
 
     -- TODO: parallelize header elaboration as well? Would have to refactor auto implicits catch,
     -- makes `@[simp]` etc harder?

src/Lean/Linter/EnvLinter/Basic.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,19 +49,19 @@ 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
@@ -110,19 +75,24 @@ but it can be selected by `lake builtin-lint --extra`.
 
 Linters are named using their declaration names, without the namespace. These must be distinct.
 -/
-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 (← getEnv)).find? optName then
       Elab.addConstInfo stx declName
       throwError
-        "invalid attribute `builtin_env_linter`, linter `{shortName}` has already been declared"
+        "invalid attribute `builtin_env_linter`, linter `{optName}` has already been declared"
     let isPublic := !isPrivateName decl; let isMeta := isMarkedMeta (← getEnv) decl
     unless isPublic && isMeta do
       throwError "invalid attribute `builtin_env_linter`, \
@@ -133,7 +103,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/Frontend.lean

@@ -32,48 +32,28 @@ 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
+def getEnvLinters : 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
+      let linter ← getEnvLinter optName declName
+      result := result.binInsert (·.optName.lt ·.optName) linter
   pure result
 
+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 +128,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,7 +138,7 @@ 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
@@ -171,10 +151,6 @@ def formatLinterResults
       } 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. -/