refactor: turn dupNamespace into a Lean.Linter

src/Lean/Linter/EnvLinter/Builtin.lean

@@ -97,18 +97,6 @@ a higher universe level than `α`. -/
     if bad.isEmpty then return none
     return m!"universes {bad} only occur together."
 
-/-- A linter for checking whether a declaration has a namespace twice consecutively in its name. -/
-@[builtin_env_linter extra] def dupNamespace : EnvLinter where
-  noErrorsFound := "No declarations have a duplicate namespace."
-  errorsFound := "DUPLICATED NAMESPACES IN NAME:"
-  test declName := do
-    if ← isAutoDecl declName then return none
-    if ← isImplicitReducible declName then return none
-    let nm := declName.components
-    let some (dup, _) := nm.zip nm.tail! |>.find? fun (x, y) => x == y
-      | return none
-    return m!"The namespace {dup} is duplicated in the name"
-
 end Lean.Linter.EnvLinter
 
 end

src/Lean/Linter/Extra.lean

@@ -6,5 +6,6 @@ Authors: Wojciech Różowski
 module
 
 prelude
+public import Lean.Linter.Extra.DupNamespace
 public import Lean.Linter.Extra.UnnecessarySeqFocus
 public import Lean.Linter.Extra.UnreachableTactic

src/Lean/Linter/Extra/DupNamespace.lean

@@ -0,0 +1,90 @@
+/-
+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) 2023 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+module
+
+prelude
+public import Lean.Elab.Command
+public import Lean.Linter.Basic
+
+public section
+
+namespace Lean.Linter.Extra
+open Lean Parser Elab Command Meta Linter
+
+/--
+The `dupNamespace` linter is set off by default.  Lean emits a warning on any declaration that
+contains the same namespace at least twice consecutively.
+
+For instance, `Nat.Nat.foo` and `One.two.two` trigger a warning, while `Nat.One.Nat` does not.
+
+*Note.*
+This linter will not detect duplication in namespaces of autogenerated declarations
+(other than the one whose `declId` is present in the source declaration).
+-/
+register_builtin_option linter.extra.dupNamespace : Bool := {
+  defValue := false
+  descr := "enable the duplicated namespace linter"
+}
+
+namespace DupNamespaceLinter
+
+open Lean Parser Elab Command Meta Linter
+
+/--
+If `pos` is a `String.Pos`, then `getNamesFrom pos` returns the array of identifiers
+for the names of the declarations whose syntax begins in position at least `pos`.
+-/
+def getNamesFrom {m} [Monad m] [MonadEnv m] [MonadFileMap m] (pos : String.Pos.Raw) :
+    m (Array Syntax) := do
+  -- declarations from parallelism branches should not be interesting here, so use `local`
+  let drs := declRangeExt.toPersistentEnvExtension.getState (asyncMode := .local) (← getEnv)
+  let fm ← getFileMap
+  let mut nms := #[]
+  for (nm, rgs) in drs do
+    if pos ≤ fm.ofPosition rgs.range.pos then
+      let ofPos1 := fm.ofPosition rgs.selectionRange.pos
+      let ofPos2 := fm.ofPosition rgs.selectionRange.endPos
+      nms := nms.push (mkIdentFrom (.ofRange ⟨ofPos1, ofPos2⟩) nm)
+  return nms
+
+/--
+If `stx` is a syntax node for an `export` statement, then `getAliasSyntax stx` returns the array of
+identifiers with the "exported" names.
+-/
+def getAliasSyntax {m} [Monad m] [MonadResolveName m] (stx : Syntax) : m (Array Syntax) := do
+  let mut aliases := #[]
+  if let `(export $_ ($ids*)) := stx then
+    let currNamespace ← getCurrNamespace
+    for idStx in ids do
+      let id := idStx.getId
+      aliases := aliases.push
+        (mkIdentFrom (.ofRange (idStx.raw.getRange?.getD default)) (currNamespace ++ id))
+  return aliases
+
+@[inherit_doc linter.extra.dupNamespace]
+def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do
+  if getLinterValueExtra linter.extra.dupNamespace (← getLinterOptions) then
+    let mut aliases := #[]
+    if let some exp := stx.find? (·.isOfKind `Lean.Parser.Command.export) then
+      aliases ← getAliasSyntax exp
+    for id in (← getNamesFrom (stx.getPos?.getD default)) ++ aliases do
+      let declName := id.getId
+      if declName.hasMacroScopes || isPrivateName declName then continue
+      let nm := declName.components
+      let some (dup, _) := nm.zip (nm.tailD []) |>.find? fun (x, y) ↦ x == y
+        | continue
+      Linter.logLintIfExtra linter.extra.dupNamespace id
+        m!"The namespace '{dup}' is duplicated in the declaration '{declName}'"
+
+end DupNamespaceLinter
+
+builtin_initialize addLinter DupNamespaceLinter.dupNamespace
+
+end Lean.Linter.Extra

tests/elab/env_linter.lean

@@ -140,7 +140,7 @@ def testGetChecksExtra : CoreM (Array Name) := do
   let checks ← getChecks (scope := .extra) (runOnly := none)
   return checks.map (·.name)
 
-/-- info: #[`checkUnivs, `defLemma, `dummyBadName, `dummyExtraLinter, `dupNamespace] -/
+/-- info: #[`checkUnivs, `defLemma, `dummyBadName, `dummyExtraLinter] -/
 #guard_msgs in
 #eval testGetChecksExtra
 
@@ -149,7 +149,7 @@ def testGetChecksAll : CoreM (Array Name) := do
   let checks ← getChecks (scope := .all) (runOnly := none)
   return checks.map (·.name)
 
-/-- info: #[`checkUnivs, `defLemma, `dummyBadName, `dummyExtraLinter, `dupNamespace] -/
+/-- info: #[`checkUnivs, `defLemma, `dummyBadName, `dummyExtraLinter] -/
 #guard_msgs in
 #eval testGetChecksAll
 

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

@@ -10,7 +10,7 @@ example : True := by
   skip <;> skip
   trivial
 -- The component `Dup` appears consecutively in this declaration's name —
--- the builtin extra `dupNamespace` env linter should flag it.
+-- the builtin extra `dupNamespace` text linter should flag it.
 def Dup.Dup.violation : Nat := 2
 
 -- This uses `def` for a Prop — the default `defLemma` linter should flag this

tests/lake/tests/builtin-lint/test.sh

@@ -87,7 +87,7 @@ no_match_pat 'badNameExtra' produced.out
 no_match_pat 'extra text linter saw a declaration' produced.out
 # Builtin extra text linter `unnecessarySeqFocus` is non-default, so silent.
 no_match_pat 'tac1 <;> tac2' produced.out
-# Builtin extra env linter `dupNamespace` is non-default, so it stays silent.
+# Builtin extra text linter `dupNamespace` is non-default, so it stays silent.
 no_match_pat 'Dup.Dup.violation' produced.out
 # Builtin extra text linter `unreachableTactic` is non-default, so silent.
 no_match_pat 'this tactic is never executed' produced.out
@@ -104,7 +104,7 @@ match_pat 'extra text linter saw a declaration' produced.out
 # tag `linter.extra.unnecessarySeqFocus` is matched by the `linter.extra`
 # prefix filter.
 match_pat 'tac1 <;> tac2' produced.out
-# Builtin `dupNamespace` env linter fires under --extra.
+# Builtin `dupNamespace` extra text linter fires under --extra.
 match_pat 'Dup.Dup.violation' produced.out
 match_pat "namespace .*Dup.* is duplicated" produced.out
 # Builtin `unreachableTactic` extra text linter fires under --extra.
@@ -134,7 +134,7 @@ match_pat 'tac1 <;> tac2' produced.out
 no_match_pat 'badNameExtra' produced.out
 no_match_pat 'Dup.Dup.violation' produced.out
 
-# --lint-only dupNamespace runs only the builtin extra `dupNamespace` env linter.
+# --lint-only dupNamespace runs only the builtin extra `dupNamespace` text linter.
 lake_out lint --lint-only dupNamespace ExtraViolations || true
 match_pat 'Dup.Dup.violation' produced.out
 no_match_pat 'badNameExtra' produced.out