feat: implement "linter sets" that can be turned on as a group (#8106)

This PR adds a `register_linter_set` command for declaring linter sets.
The `getLinterValue` function now checks if the present linter is
contained in a set that has been enabled (using the `set_option` command
or on the command line).

The implementation stores linter set membership in an environment
extension. As a consequence, we need to pass more data to
`getLinterValue`: the argument of ype `Options` has been replaced with a
`LinterOptions`, which you can access by writing `getLinterOptions`
instead of `getOptions`. (The alternative I considered is to modify the
`Options` structure. The current approach seems a bit higher-level and
lower-impact.)

The logic for checking whether a linter should be enabled now goes in
four steps:
1. If the linter has been explicitly en/disabled, return that.
2. If `linter.all` has been explicitly set, return that.
3. If the linter is in any set that has been enabled, return true.
4. Return the default setting for the linter.

Reasoning:
* The linter's explicit setting should take precedence.
* We want to be able to disable all but the explicitly enabled linters
with `linter.all`, so it should take precedence over linter sets.
* We want to progressively enable more linters as they become available,
so the check over sets should be *any*.
* Falling back to the default value last, ensures compatibility with the
current way we define linters.

The public-facing API currently does not allow modifying sets: all
linters have to be added when the set is declared. This way, there is
one place where all the contents of the set are listed.

Linter sets can be declared to contain linters that have not been
declared (yet): this allows declaring linter sets low down in the import
hierarchy when not all the requested linters are defined yet.

---------

Co-authored-by: grunweg <[email protected]>

Author: Vierkantor

src/Lean/Elab/Tactic/Simpa.lean

@@ -24,7 +24,7 @@ namespace Lean.Elab.Tactic.Simpa
 open Lean Parser.Tactic Elab Meta Term Tactic Simp Linter
 
 /-- Gets the value of the `linter.unnecessarySimpa` option. -/
-def getLinterUnnecessarySimpa (o : Options) : Bool :=
+def getLinterUnnecessarySimpa (o : LinterOptions) : Bool :=
   getLinterValue linter.unnecessarySimpa o
 
 deriving instance Repr for UseImplicitLambdaResult
@@ -42,7 +42,7 @@ deriving instance Repr for UseImplicitLambdaResult
     dischargeWrapper.with fun discharge? => do
       let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
           (simplifyTarget := true) (discharge? := discharge?)
-        | if getLinterUnnecessarySimpa (← getOptions) then
+        | if getLinterUnnecessarySimpa (← getLinterOptions) then
             logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'"
           return {}
       g.withContext do
@@ -78,7 +78,7 @@ deriving instance Repr for UseImplicitLambdaResult
             logUnassignedAndAbort (← filterOldMVars (← getMVars e) mvarCounterSaved)
             closeMainGoal `simpa (checkUnassigned := false) h
         | none =>
-          if getLinterUnnecessarySimpa (← getOptions) then
+          if getLinterUnnecessarySimpa (← getLinterOptions) then
             if let .fvar h := e then
               if (← getLCtx).getRoundtrippingUserName? h |>.isSome then
                 logLint linter.unnecessarySimpa (← getRef)

src/Lean/Linter.lean

@@ -12,3 +12,4 @@ import Lean.Linter.UnusedVariables
 import Lean.Linter.MissingDocs
 import Lean.Linter.Omit
 import Lean.Linter.List
+import Lean.Linter.Sets

src/Lean/Linter/Basic.lean

@@ -5,18 +5,68 @@ Authors: Lars König
 -/
 prelude
 import Lean.Data.Options
+import Lean.MonadEnv
 import Lean.Log
 
 namespace Lean.Linter
 
+/-- Linter sets are represented as a map from linter name to set name,
+to make it easy to look up which sets to check for enabling a linter.
+-/
+def LinterSets := NameMap (Array Name)
+  deriving EmptyCollection, Inhabited
+
+/-- Insert a set into a `LinterSets` map.
+
+`entry.1` is the name of the linter set,
+`entry.2` contains the names of the set's linter options.
+-/
+def insertLinterSetEntry (map : LinterSets) (setName : Name) (options : NameSet) : LinterSets :=
+  options.fold (init := map) fun map linterName =>
+    map.insert linterName ((map.findD linterName #[]).push setName)
+
+builtin_initialize linterSetsExt : SimplePersistentEnvExtension (Name × NameSet) LinterSets ← Lean.registerSimplePersistentEnvExtension {
+  addImportedFn := mkStateFromImportedEntries (Function.uncurry <| insertLinterSetEntry ·) {}
+  addEntryFn := (Function.uncurry <| insertLinterSetEntry ·)
+  toArrayFn es := es.toArray
+}
+
+/-- The `LinterOptions` structure is used to determine whether given linters are enabled.
+
+This structure contains all the data required to do so, the `Options` set on the command line
+or by the `set_option` command, and the `LinterSets` that have been declared.
+
+A single structure holding this data is useful since we want `getLinterValue` to be a pure
+function: determinining the `LinterSets` would otherwise require a `MonadEnv` instance.
+-/
+structure LinterOptions where
+  toOptions : Options
+  linterSets : LinterSets
+
+def LinterOptions.get [KVMap.Value α] (o : LinterOptions) := o.toOptions.get (α := α)
+def LinterOptions.get? [KVMap.Value α] (o : LinterOptions) := o.toOptions.get? (α := α)
+
+def _root_.Lean.Options.toLinterOptions [Monad m] [MonadEnv m] (o : Options) : m LinterOptions := do
+  let linterSets := linterSetsExt.getState (← getEnv)
+  return { toOptions := o, linterSets }
+
+/-- Return the set of linter sets that this option is contained in. -/
+def LinterOptions.getSet (o : LinterOptions) (opt : Lean.Option α) : Array Name :=
+  o.linterSets.findD opt.name #[]
+
+def getLinterOptions [Monad m] [MonadOptions m] [MonadEnv m] : m LinterOptions := do
+  (← getOptions).toLinterOptions
+
 register_builtin_option linter.all : Bool := {
   defValue := false
   descr := "enable all linters"
 }
 
-def getLinterAll (o : Options) (defValue := linter.all.defValue) : Bool := o.get linter.all.name defValue
+def getLinterAll (o : LinterOptions) (defValue := linter.all.defValue) : Bool :=
+    o.get linter.all.name defValue
 
-def getLinterValue (opt : Lean.Option Bool) (o : Options) : Bool := o.get opt.name (getLinterAll o opt.defValue)
+def getLinterValue (opt : Lean.Option Bool) (o : LinterOptions) : Bool :=
+  o.get opt.name (getLinterAll o <| (o.getSet opt).any (o.get? · == some true) || opt.defValue)
 
 def logLint [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
     (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit :=
@@ -29,8 +79,11 @@ If `linterOption` is enabled, print a linter warning message at the position det
 Whether a linter option is enabled or not is determined by the following sequence:
 1. If it is set, then the value determines whether or not it is enabled.
 2. Otherwise, if `linter.all` is set, then its value determines whether or not the option is enabled.
-3. Otherwise, the default value determines whether or not it is enabled.
+3. Otherwise, if any of the linter sets containing the option is enabled, it is enabled.
+  (Only enabled linter sets are considered: explicitly disabling a linter set
+  will revert the linters it contains to their default behavior.)
+4. Otherwise, the default value determines whether or not it is enabled.
 -/
-def logLintIf [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
+def logLintIf [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadEnv m]
     (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit := do
-  if getLinterValue linterOption (← getOptions) then logLint linterOption stx msg
+  if getLinterValue linterOption (← getLinterOptions) then logLint linterOption stx msg

src/Lean/Linter/Builtin.lean

@@ -14,11 +14,11 @@ register_builtin_option linter.suspiciousUnexpanderPatterns : Bool := {
   descr := "enable the 'suspicious unexpander patterns' linter"
 }
 
-def getLinterSuspiciousUnexpanderPatterns (o : Options) : Bool := getLinterValue linter.suspiciousUnexpanderPatterns o
+def getLinterSuspiciousUnexpanderPatterns (o : LinterOptions) : Bool := getLinterValue linter.suspiciousUnexpanderPatterns o
 
 def suspiciousUnexpanderPatterns : Linter where
   run cmdStx := do
-    unless getLinterSuspiciousUnexpanderPatterns (← getOptions) do
+    unless getLinterSuspiciousUnexpanderPatterns (← getLinterOptions) do
       return
 
     -- check `[app_unexpander _]` defs defined by pattern matching

src/Lean/Linter/Deprecated.lean

@@ -48,7 +48,7 @@ def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name :=
   (← deprecatedAttr.getParam? env declName).newName?
 
 def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (declName : Name) : m Unit := do
-  if getLinterValue linter.deprecated (← getOptions) then
+  if getLinterValue linter.deprecated (← getLinterOptions) then
     let some attr := deprecatedAttr.getParam? (← getEnv) declName | pure ()
     logWarning <| .tagged ``deprecatedAttr <|
       m!"`{.ofConstName declName true}` has been deprecated" ++ match attr.text? with

src/Lean/Linter/MissingDocs.lean

@@ -19,7 +19,7 @@ register_builtin_option linter.missingDocs : Bool := {
   descr := "enable the 'missing documentation' linter"
 }
 
-def getLinterMissingDocs (o : Options) : Bool := getLinterValue linter.missingDocs o
+def getLinterMissingDocs (o : LinterOptions) : Bool := getLinterValue linter.missingDocs o
 
 
 namespace MissingDocs
@@ -68,7 +68,7 @@ def getHandlers (env : Environment) : NameMap Handler := (missingDocsExt.getStat
 partial def missingDocs : Linter where
   run stx := do
     if let some h := (getHandlers (← getEnv)).find? stx.getKind then
-      h (getLinterMissingDocs (← getOptions)) stx
+      h (getLinterMissingDocs (← getLinterOptions)) stx
 
 builtin_initialize addLinter missingDocs
 

src/Lean/Linter/Sets.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+prelude
+import Lean.Elab.Command
+import Lean.Linter.Basic
+
+namespace Lean.Linter
+
+/-- Add a new linter set that contains the given linters. -/
+def insertLinterSet [MonadEnv m] (setName : Name) (linterNames : NameSet) : m Unit :=
+  modifyEnv (linterSetsExt.addEntry · (setName, linterNames))
+
+/-- `registerSet` wraps `registerOption` by setting relevant values. -/
+def registerSet (setName : Name) (ref : Name := by exact decl_name%) : IO (Lean.Option Bool) := do
+  registerOption setName {
+    declName := ref
+    defValue := false
+    group := "linterSet"
+    descr := ""
+  }
+  return { name := setName, defValue := false }
+
+open Lean.Elab.Command in
+/-- Declare a new linter set by giving the set of options that will be enabled along with the set. -/
+elab doc?:(docComment)? "register_linter_set" name:ident " := " decl:ident* : command => do
+  insertLinterSet name.getId <| decl.foldl (init := ∅) fun names name => names.insert name.getId
+  let initializer ← `($[$doc?]? initialize $name : Lean.Option Bool ← Lean.Linter.registerSet $(quote name.getId))
+  withMacroExpansion (← getRef) initializer <| elabCommand initializer
+
+
+end Lean.Linter

src/Lean/Linter/UnusedVariables.lean

@@ -104,29 +104,29 @@ register_builtin_option linter.unusedVariables.analyzeTactics : Bool := {
 }
 
 /-- Gets the status of `linter.unusedVariables` -/
-def getLinterUnusedVariables (o : Options) : Bool :=
+def getLinterUnusedVariables (o : LinterOptions) : Bool :=
   getLinterValue linter.unusedVariables o
 
 /-- Gets the status of `linter.unusedVariables.funArgs` -/
-def getLinterUnusedVariablesFunArgs (o : Options) : Bool :=
+def getLinterUnusedVariablesFunArgs (o : LinterOptions) : Bool :=
   o.get linter.unusedVariables.funArgs.name (getLinterUnusedVariables o)
 
 /-- Gets the status of `linter.unusedVariables.patternVars` -/
-def getLinterUnusedVariablesPatternVars (o : Options) : Bool :=
+def getLinterUnusedVariablesPatternVars (o : LinterOptions) : Bool :=
   o.get linter.unusedVariables.patternVars.name (getLinterUnusedVariables o)
 
 /-- An `IgnoreFunction` receives:
 
 * a `Syntax.ident` for the unused variable
 * a `Syntax.Stack` with the location of this piece of syntax in the command
-* The `Options` set locally to this syntax
+* The `LinterOptions` set locally to this syntax
 
 and should return `true` to indicate that the lint should be suppressed,
 or `false` to proceed with linting as usual (other `IgnoreFunction`s may still
 say it is ignored). A variable is only linted if it is unused and no
 `IgnoreFunction` returns `true` on this syntax.
 -/
-abbrev IgnoreFunction := Syntax → Syntax.Stack → Options → Bool
+abbrev IgnoreFunction := Syntax → Syntax.Stack → LinterOptions → Bool
 
 /-- Interpret an `IgnoreFunction` from the environment. -/
 unsafe def mkIgnoreFnImpl (constName : Name) : ImportM IgnoreFunction := do
@@ -381,7 +381,8 @@ structure References where
 
 /-- Collect information from the `infoTrees` into `References`.
 See `References` for more information about the return value. -/
-partial def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
+partial def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range)
+    (linterSets : LinterSets) :
     StateRefT References IO Unit := ReaderT.run (r := false) <| go infoTrees none
 where
   go infoTrees ctx? := do
@@ -422,7 +423,7 @@ where
               -- Skip declarations which are outside the command syntax range, like `variable`s
               -- (it would be confusing to lint these), or those which are macro-generated
               if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return true
-              let opts := ci.options
+              let opts : LinterOptions := { toOptions := ci.options, linterSets }
               -- we have to check for the option again here because it can be set locally
               if !getLinterUnusedVariables opts then return true
               let stx := skipDeclIdIfPresent info.stx
@@ -435,7 +436,7 @@ where
                 if let some ref := s.fvarDefs[range]? then
                   { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
                 else
-                  { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
+                  { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts := opts.toOptions, aliases := #[id] } }
             else
               -- Found a direct use, keep track of it
               modify fun s => { s with fvarUses := s.fvarUses.insert id }
@@ -471,7 +472,7 @@ private def hasSorry (stx : Syntax) : Bool :=
 /-- Reports unused variable warnings on each command. Use `linter.unusedVariables` to disable. -/
 def unusedVariables : Linter where
   run cmdStx := do
-    unless getLinterUnusedVariables (← getOptions) do
+    unless getLinterUnusedVariables (← getLinterOptions) do
       return
 
     -- NOTE: `messages` is local to the current command
@@ -488,8 +489,10 @@ def unusedVariables : Linter where
 
     let infoTrees := (← get).infoState.trees.toArray
 
+    let linterSets := linterSetsExt.getState (← getEnv)
+
     -- Run the main collection pass, resulting in `s : References`.
-    let (_, s) ← (collectReferences infoTrees cmdStxRange).run {}
+    let (_, s) ← (collectReferences infoTrees cmdStxRange linterSets).run {}
 
     -- If there are no local defs then there is nothing to do
     if s.fvarDefs.isEmpty then return
@@ -526,7 +529,8 @@ def unusedVariables : Linter where
         | continue
 
       -- If it is blacklisted by an `ignoreFn` then skip it
-      if id'.isIdent && ignoreFns.any (· declStx stack opts) then continue
+      let linterOpts ← opts.toLinterOptions
+      if id'.isIdent && ignoreFns.any (· declStx stack linterOpts) then continue
 
       -- Evaluate ignore functions again on macro expansion outputs
       if ← infoTrees.anyM fun tree => do
@@ -539,7 +543,7 @@ def unusedVariables : Linter where
               (·.getRange?.any (·.includes range))
               (fun stx => stx.isIdent && stx.getRange?.any (· == range))
           then
-            ignoreFns.any (· declStx stack opts)
+            ignoreFns.any (· declStx stack linterOpts)
           else
             false
       then

tests/pkg/linter_set/LinterSet.lean

@@ -0,0 +1,93 @@
+import LinterSet.Def
+
+open Lean Linter
+
+def fooInitially : MetaM Unit := do
+  -- linter.foo1 and linter.foo2 are declared to be false by default
+  assert! !(getLinterValue linter.foo1 (← getLinterOptions))
+  assert! !(getLinterValue linter.foo2 (← getLinterOptions))
+  -- linter.foo_true is declared to be true by default
+  assert! (getLinterValue linter.foo_true (← getLinterOptions))
+  pure ()
+
+#eval fooInitially
+
+set_option linter.set.foo true
+
+def fooSetTrue : MetaM Unit := do
+  -- All linters in the `foo` set should now be true
+  assert! (getLinterValue linter.foo1 (← getLinterOptions))
+  assert! (getLinterValue linter.foo2 (← getLinterOptions))
+  assert! (getLinterValue linter.foo_true (← getLinterOptions))
+  pure ()
+
+#eval fooSetTrue
+
+section OverrideFalse
+
+set_option linter.foo2 false
+
+def overrideFalse : MetaM Unit := do
+  -- The overridden linter should now be false.
+  assert! (getLinterValue linter.foo1 (← getLinterOptions))
+  assert! !(getLinterValue linter.foo2 (← getLinterOptions))
+  assert! (getLinterValue linter.foo_true (← getLinterOptions))
+  pure ()
+
+#eval overrideFalse
+
+end OverrideFalse
+
+section AllFalse
+
+set_option linter.all false
+
+def allSetFalse : MetaM Unit := do
+  -- All linters, including those in the `foo` set, should now be false
+  assert! !(getLinterValue linter.foo1 (← getLinterOptions))
+  assert! !(getLinterValue linter.foo2 (← getLinterOptions))
+  assert! !(getLinterValue linter.foo_true (← getLinterOptions))
+  pure ()
+
+#eval allSetFalse
+
+end AllFalse
+
+set_option linter.set.foo false
+
+def fooSetFalse : MetaM Unit := do
+ -- All linters in the `foo` set should now be back to default.
+  assert! !(getLinterValue linter.foo1 (← getLinterOptions))
+  assert! !(getLinterValue linter.foo2 (← getLinterOptions))
+  assert! (getLinterValue linter.foo_true (← getLinterOptions))
+  pure ()
+
+#eval fooSetFalse
+
+section AllTrue
+
+set_option linter.all true
+
+/-- Running this code will check that all linters in the `foo` set are true.
+
+This docstring is required due to `linter.all` being true(!). -/
+def allSetTrue : MetaM Unit := do
+  -- All linters, including those in the `foo` set, should now be true
+  assert! (getLinterValue linter.foo1 (← getLinterOptions))
+  assert! (getLinterValue linter.foo2 (← getLinterOptions))
+  assert! (getLinterValue linter.foo_true (← getLinterOptions))
+  pure ()
+
+#eval allSetTrue
+
+end AllTrue
+
+/-! Test setting user options from lakefile. -/
+
+open Lean
+
+def barFromLakefile : MetaM Unit := do
+  assert! (getLinterValue linter.bar (← getLinterOptions))
+
+#eval barFromLakefile
+