feat: add builtin linter sets and make linter.extra a builtin linter set

src/Lean/Linter/Extra.lean

@@ -10,3 +10,18 @@ public import Lean.Linter.Extra.DupNamespace
 public import Lean.Linter.Extra.UnnecessarySeqFocus
 public import Lean.Linter.Extra.UnreachableTactic
 public import Lean.Linter.Extra.UnusedDecidableInType
+
+namespace Lean.Linter
+
+/-- Record the four extra linters as members of the `linter.extra` set, so that they pick up the
+set-membership fallback in `getLinterValue`. The `linter.extra` option itself is registered as a
+builtin option in `Lean.Linter.Init`. -/
+builtin_initialize
+  addBuiltinLinterSet `linter.extra <|
+    NameSet.empty
+      |>.insert `linter.extra.dupNamespace
+      |>.insert `linter.extra.unnecessarySeqFocus
+      |>.insert `linter.extra.unreachableTactic
+      |>.insert `linter.extra.unusedDecidableInType
+
+end Lean.Linter

src/Lean/Linter/Extra/DupNamespace.lean

@@ -70,7 +70,7 @@ def getAliasSyntax {m} [Monad m] [MonadResolveName m] (stx : Syntax) : m (Array
 
 @[inherit_doc linter.extra.dupNamespace]
 def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do
-  if getLinterValueExtra linter.extra.dupNamespace (← getLinterOptions) then
+  if getLinterValue linter.extra.dupNamespace (← getLinterOptions) then
     let mut aliases := #[]
     if let some exp := stx.find? (·.isOfKind `Lean.Parser.Command.export) then
       aliases ← getAliasSyntax exp
@@ -80,7 +80,7 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do
       let nm := declName.components
       let some (dup, _) := nm.zip (nm.tailD []) |>.find? fun (x, y) ↦ x == y
         | continue
-      Linter.logLintIfExtra linter.extra.dupNamespace id
+      Linter.logLintIf linter.extra.dupNamespace id
         m!"The namespace '{dup}' is duplicated in the declaration '{declName}'"
 
 end DupNamespaceLinter

src/Lean/Linter/Extra/UnnecessarySeqFocus.lean

@@ -165,7 +165,7 @@ end
 
 @[inherit_doc Lean.Linter.Extra.linter.extra.unnecessarySeqFocus]
 def unnecessarySeqFocusLinter : Linter where run := withSetOptionIn fun stx => do
-  unless getLinterValueExtra linter.extra.unnecessarySeqFocus (← getLinterOptions)
+  unless getLinterValue linter.extra.unnecessarySeqFocus (← getLinterOptions)
       && (← getInfoState).enabled do
     return
   if (← get).messages.hasErrors then
@@ -182,7 +182,7 @@ def unnecessarySeqFocusLinter : Linter where run := withSetOptionIn fun stx => d
   let mut last : Lean.Syntax.Range := ⟨0, 0⟩
   for (r, stx) in let _ := @lexOrd; let _ := @ltOfOrd.{0}; unused.qsort (key ·.1 < key ·.1) do
     if last.start ≤ r.start && r.stop ≤ last.stop then continue
-    logLintIfExtra linter.extra.unnecessarySeqFocus stx
+    logLintIf linter.extra.unnecessarySeqFocus stx
       "Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice"
     last := r
 

src/Lean/Linter/Extra/UnreachableTactic.lean

@@ -96,7 +96,7 @@ end
 
 @[inherit_doc linter.extra.unreachableTactic]
 def unreachableTacticLinter : Linter where run := withSetOptionIn fun stx => do
-  unless getLinterValueExtra linter.extra.unreachableTactic (← getLinterOptions)
+  unless getLinterValue linter.extra.unreachableTactic (← getLinterOptions)
     && (← getInfoState).enabled do
     return
   if (← get).messages.hasErrors then
@@ -117,7 +117,7 @@ def unreachableTacticLinter : Linter where run := withSetOptionIn fun stx => do
   let mut last : Lean.Syntax.Range := ⟨0, 0⟩
   for (r, stx) in let _ := @lexOrd; let _ := @ltOfOrd.{0}; unreachable.qsort (key ·.1 < key ·.1) do
     if last.start ≤ r.start && r.stop ≤ last.stop then continue
-    logLintIfExtra linter.extra.unreachableTactic stx "this tactic is never executed"
+    logLintIf linter.extra.unreachableTactic stx "this tactic is never executed"
     last := r
 
 builtin_initialize addLinter unreachableTacticLinter

src/Lean/Linter/Extra/UnusedDecidableInType.lean

@@ -275,7 +275,7 @@ private def isDecidableVariant (type : Expr) : Bool :=
 
 @[inherit_doc linter.extra.unusedDecidableInType]
 def unusedDecidableInTypeLinter : Linter where run := withSetOptionIn fun _ => do
-  unless getLinterValueExtra linter.extra.unusedDecidableInType (← getLinterOptions)
+  unless getLinterValue linter.extra.unusedDecidableInType (← getLinterOptions)
       && (← getInfoState).enabled do
     return
   if (← get).messages.hasErrors then
@@ -289,7 +289,7 @@ def unusedDecidableInTypeLinter : Linter where run := withSetOptionIn fun _ => d
         && thm.type.hasInstanceBinderOf isDecidableVariant
     unless thms.isEmpty do liftTermElabM do for thm in thms do
       onUnusedInstancesWhere thm isDecidableVariant fun unusedParams => do
-        logLintIfExtra linter.extra.unusedDecidableInType (← getRef) m!"\
+        logLintIf linter.extra.unusedDecidableInType (← getRef) m!"\
           {unusedInstancesMsg thm.name unusedParams}\n\n\
           Consider removing \
           {if unusedParams.size = 1 then "this hypothesis" else "these hypotheses"} \

src/Lean/Linter/Init.lean

@@ -28,11 +28,46 @@ def insertLinterSetEntry (map : LinterSets) (setName : Name) (options : NameSet)
   options.foldl (init := map) fun map linterName =>
     map.insert linterName ((map.getD 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
-}
+/-- State of `linterSetsExt`.
+
+`merged` is the queryable union of all sources (builtins folded in at env creation,
+imported entries from oleans, and locally added entries). `localEntries` tracks entries
+added in the current module so they can be exported into the olean.
+-/
+structure LinterSetsState where
+  merged : LinterSets := {}
+  localEntries : Array (Name × NameSet) := #[]
+  deriving Inhabited
+
+/-- Builtin linter sets registered from `builtin_initialize` blocks in core code.
+
+Entries here are folded into every `LinterSetsState` produced by `linterSetsExt`, so they
+participate in `getLinterValue` like any user-declared set.
+-/
+builtin_initialize builtinLinterSetsRef : IO.Ref (Array (Name × NameSet)) ← IO.mkRef #[]
+
+/-- Register a builtin linter set entry. Only valid during initialization;
+use `register_builtin_linter_set` rather than calling this directly. -/
+def addBuiltinLinterSet (setName : Name) (linterNames : NameSet) : IO Unit := do
+  builtinLinterSetsRef.modify (·.push (setName, linterNames))
+
+builtin_initialize linterSetsExt :
+    PersistentEnvExtension (Name × NameSet) (Name × NameSet) LinterSetsState ←
+  registerPersistentEnvExtension {
+    mkInitial := do
+      let merged := (← builtinLinterSetsRef.get).foldl (init := {}) fun s (n, ms) =>
+        insertLinterSetEntry s n ms
+      return { merged, localEntries := #[] }
+    addImportedFn := fun ess => do
+      let s := (← builtinLinterSetsRef.get).foldl (init := {}) fun s (n, ms) =>
+        insertLinterSetEntry s n ms
+      let merged := ess.foldl (init := s) fun s es =>
+        es.foldl (init := s) fun s (n, ms) => insertLinterSetEntry s n ms
+      return { merged, localEntries := #[] }
+    addEntryFn := fun st (n, ms) =>
+      { merged := insertLinterSetEntry st.merged n ms, localEntries := st.localEntries.push (n, ms) }
+    exportEntriesFn := fun st => st.localEntries
+  }
 
 /-- The `LinterOptions` structure is used to determine whether given linters are enabled.
 
@@ -50,7 +85,7 @@ 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)
+  let linterSets := (linterSetsExt.getState (← getEnv)).merged
   return { toOptions := o, linterSets }
 
 /-- Return the set of linter sets that this option is contained in. -/
@@ -74,18 +109,9 @@ register_builtin_option linter.extra : Bool := {
 def getLinterAll (o : LinterOptions) (defValue := linter.all.defValue) : Bool :=
     o.get linter.all.name defValue
 
-def getLinterExtra (o : LinterOptions) (defValue := linter.extra.defValue) : Bool :=
-  o.get linter.extra.name 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)
 
-/--
-Like `getLinterValue`, but the cross-linter fallback is `linter.extra` instead of `linter.all`.
--/
-def getLinterValueExtra (opt : Lean.Option Bool) (o : LinterOptions) : Bool :=
-  o.get opt.name (getLinterExtra o opt.defValue)
-
 /--
 Tag attached by `logLint` to every linter warning so consumers
 (e.g. `Lean.Linter.recordLints`) can distinguish linter-produced messages
@@ -118,12 +144,3 @@ Whether a linter option is enabled or not is determined by the following sequenc
 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 (← getLinterOptions) then logLint linterOption stx msg
-
-/--
-Like `logLintIf`, but uses `getLinterValueExtra` to gate emission on the extra fallback.
-Use for extra linters: emits the warning iff `linterOption` is on under the extra
-selection rules described on `getLinterValueExtra`.
--/
-def logLintIfExtra [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadEnv m]
-    (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit := do
-  if getLinterValueExtra linterOption (← getLinterOptions) then logLint linterOption stx msg

src/Lean/Linter/Sets.lean

@@ -36,5 +36,4 @@ elab doc?:(docComment)? "register_linter_set" name:ident " := " decl:ident* : co
   let initializer ← `($[$doc?]? meta initialize $name : Lean.Option Bool ← Lean.Linter.registerSet $(quote name.getId))
   withMacroExpansion (← getRef) initializer <| elabCommand initializer
 
-
 end Lean.Linter

src/Lean/Linter/UnusedVariables.lean

@@ -494,7 +494,7 @@ def unusedVariables : Linter where
 
     let infoTrees := (← get).infoState.trees.toArray
 
-    let linterSets := linterSetsExt.getState (← getEnv)
+    let linterSets := (linterSetsExt.getState (← getEnv)).merged
 
     -- Run the main collection pass, resulting in `s : References`.
     let (_, s) ← (collectReferences infoTrees cmdStxRange linterSets).run {}

tests/lake/tests/builtin-lint/Linters.lean

@@ -16,7 +16,7 @@ open Lean Meta Lean.Linter Lean.Elab.Command
 -- `logLint`, which is how `lake lint --extra` identifies extra-scope entries.
 def dummyExtraTextLinter : Linter where
   run cmdStx := do
-    unless getLinterExtra (← getLinterOptions) do return
+    unless getLinterValue linter.extra (← getLinterOptions) do return
     unless cmdStx.getKind == ``Lean.Parser.Command.declaration do return
     logLint linter.extra cmdStx m!"extra text linter saw a declaration"