From d919bac222bf134ed4146230cc3a4956107b9053 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Tue, 26 May 2026 14:28:08 +0000 Subject: [PATCH 1/3] feat: add builtin linter sets and make `linter.extra` a linter set --- src/Lean/Linter/Extra.lean | 15 ++++++ src/Lean/Linter/Extra/DupNamespace.lean | 4 +- .../Linter/Extra/UnnecessarySeqFocus.lean | 4 +- src/Lean/Linter/Extra/UnreachableTactic.lean | 4 +- .../Linter/Extra/UnusedDecidableInType.lean | 4 +- src/Lean/Linter/Init.lean | 49 ++++++++++++++++--- src/Lean/Linter/Sets.lean | 1 - src/Lean/Linter/UnusedVariables.lean | 2 +- 8 files changed, 67 insertions(+), 16 deletions(-) diff --git a/src/Lean/Linter/Extra.lean b/src/Lean/Linter/Extra.lean index 11224aec7fb5..7d805bc1cb7d 100644 --- a/src/Lean/Linter/Extra.lean +++ b/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 diff --git a/src/Lean/Linter/Extra/DupNamespace.lean b/src/Lean/Linter/Extra/DupNamespace.lean index b8a188854570..fbc2461aa710 100644 --- a/src/Lean/Linter/Extra/DupNamespace.lean +++ b/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 diff --git a/src/Lean/Linter/Extra/UnnecessarySeqFocus.lean b/src/Lean/Linter/Extra/UnnecessarySeqFocus.lean index 0a5570252f95..d7c2270249af 100644 --- a/src/Lean/Linter/Extra/UnnecessarySeqFocus.lean +++ b/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 diff --git a/src/Lean/Linter/Extra/UnreachableTactic.lean b/src/Lean/Linter/Extra/UnreachableTactic.lean index d5043e7a9f9e..1e5ae0f63770 100644 --- a/src/Lean/Linter/Extra/UnreachableTactic.lean +++ b/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 diff --git a/src/Lean/Linter/Extra/UnusedDecidableInType.lean b/src/Lean/Linter/Extra/UnusedDecidableInType.lean index bba0cbdd9058..c10c8bdccaf1 100644 --- a/src/Lean/Linter/Extra/UnusedDecidableInType.lean +++ b/src/Lean/Linter/Extra/UnusedDecidableInType.lean @@ -286,7 +286,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 @@ -300,7 +300,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"} \ diff --git a/src/Lean/Linter/Init.lean b/src/Lean/Linter/Init.lean index 6be4352426ca..1659b48a0c85 100644 --- a/src/Lean/Linter/Init.lean +++ b/src/Lean/Linter/Init.lean @@ -28,11 +28,48 @@ 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)) + +private def foldBuiltinsInto (init : LinterSets) : IO LinterSets := do + let mut s := init + for (n, ms) in (← builtinLinterSetsRef.get) do + s := insertLinterSetEntry s n ms + return s + +builtin_initialize linterSetsExt : + PersistentEnvExtension (Name × NameSet) (Name × NameSet) LinterSetsState ← + registerPersistentEnvExtension { + mkInitial := return { merged := (← foldBuiltinsInto {}), localEntries := #[] } + addImportedFn := fun ess => do + let mut s ← foldBuiltinsInto {} + for es in ess do for (n, ms) in es do + s := insertLinterSetEntry s n ms + return { merged := s, 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 +87,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. -/ diff --git a/src/Lean/Linter/Sets.lean b/src/Lean/Linter/Sets.lean index 114b698ef851..7aa9590d52ea 100644 --- a/src/Lean/Linter/Sets.lean +++ b/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 diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index 23aec7b92b2d..1d3e75b39abe 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/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 {} From 0dc8cea71eb81a56ac38173b259828966ca06651 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Tue, 26 May 2026 15:04:38 +0000 Subject: [PATCH 2/3] chore: refactor `linterSetsExt` --- src/Lean/Linter/Init.lean | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/src/Lean/Linter/Init.lean b/src/Lean/Linter/Init.lean index 1659b48a0c85..fa25e69fade6 100644 --- a/src/Lean/Linter/Init.lean +++ b/src/Lean/Linter/Init.lean @@ -51,21 +51,19 @@ use `register_builtin_linter_set` rather than calling this directly. -/ def addBuiltinLinterSet (setName : Name) (linterNames : NameSet) : IO Unit := do builtinLinterSetsRef.modify (·.push (setName, linterNames)) -private def foldBuiltinsInto (init : LinterSets) : IO LinterSets := do - let mut s := init - for (n, ms) in (← builtinLinterSetsRef.get) do - s := insertLinterSetEntry s n ms - return s - builtin_initialize linterSetsExt : PersistentEnvExtension (Name × NameSet) (Name × NameSet) LinterSetsState ← registerPersistentEnvExtension { - mkInitial := return { merged := (← foldBuiltinsInto {}), localEntries := #[] } + mkInitial := do + let merged := (← builtinLinterSetsRef.get).foldl (init := {}) fun s (n, ms) => + insertLinterSetEntry s n ms + return { merged, localEntries := #[] } addImportedFn := fun ess => do - let mut s ← foldBuiltinsInto {} - for es in ess do for (n, ms) in es do - s := insertLinterSetEntry s n ms - return { merged := s, localEntries := #[] } + 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 From 26512dfd4059f7ffd9c8b3a113ebb8307e2d7b4c Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Wed, 27 May 2026 16:17:04 +0000 Subject: [PATCH 3/3] chore: fix test --- src/Lean/Linter/Init.lean | 18 ------------------ tests/lake/tests/builtin-lint/Linters.lean | 2 +- 2 files changed, 1 insertion(+), 19 deletions(-) diff --git a/src/Lean/Linter/Init.lean b/src/Lean/Linter/Init.lean index ca83adb17a51..88cdb207e98e 100644 --- a/src/Lean/Linter/Init.lean +++ b/src/Lean/Linter/Init.lean @@ -109,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 @@ -153,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 diff --git a/tests/lake/tests/builtin-lint/Linters.lean b/tests/lake/tests/builtin-lint/Linters.lean index 13e58ccb76b4..c967d12e7f50 100644 --- a/tests/lake/tests/builtin-lint/Linters.lean +++ b/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"