feat: add linter.extra.dupNamespace.consecutiveOnly option to dupNamespace linter

src/Lean/Linter/Extra/DupNamespace.lean

@@ -20,19 +20,23 @@ 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.
+contains the same namespace more than once.
 
-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).
+By default, only consecutive duplication is reported: `Nat.Nat.foo` and `One.two.two` trigger a
+warning, while `Nat.One.Nat` does not. Setting `linter.extra.dupNamespace.consecutiveOnly` to
+`false` also reports non-consecutive duplication, so that `Nat.One.Nat` triggers a warning as well.
 -/
+
 register_builtin_option linter.extra.dupNamespace : Bool := {
   defValue := false
   descr := "enable the duplicated namespace linter"
 }
 
+register_builtin_option linter.extra.dupNamespace.consecutiveOnly : Bool := {
+  defValue := true
+  descr := "only warn on consecutive duplicated namespaces"
+}
+
 namespace DupNamespaceLinter
 
 open Lean Parser Elab Command Meta Linter
@@ -78,10 +82,24 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ 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.logLintIf linter.extra.dupNamespace id
-        m!"The namespace '{dup}' is duplicated in the declaration '{declName}'"
+      let duplicated :=
+        if (← getBoolOption `linter.extra.dupNamespace.consecutiveOnly (defValue := true)) then
+          -- Only check consecutive components
+          nm.zip (nm.tailD []) |>.filterMap fun (x, y) ↦ if x == y then some x else none
+        else
+          -- Collect distinct components which appear more than once.
+          List.eraseDups <| nm.filter (fun comp ↦ nm.count comp > 1)
+      match duplicated with
+      | [] => continue
+      | [ns] =>
+        Linter.logLint linter.extra.dupNamespace id
+          m!"The namespace `{ns}` is duplicated in the declaration \
+          `{.ofConstName (fullNames := true) declName}`."
+      | _ =>
+        let ns := MessageData.andList (duplicated.map (m!"`{·}`"))
+        Linter.logLint linter.extra.dupNamespace id
+          m!"The namespaces {ns} are duplicated in the declaration \
+          `{.ofConstName (fullNames := true) declName}`."
 
 end DupNamespaceLinter
 

tests/elab/dupNamespace.lean

@@ -0,0 +1,39 @@
+set_option linter.extra.dupNamespace true
+
+/--
+warning: The namespace `Foo` is duplicated in the declaration `Foo.Foo`.
+
+Note: This linter can be disabled with `set_option linter.extra.dupNamespace false`
+-/
+#guard_msgs in
+theorem Foo.Foo : True := trivial
+
+theorem Foo.Bar.Foo : True := trivial
+
+/--
+warning: The namespaces `Bar` and `Foo` are duplicated in the declaration `Bar.Bar.Foo.Foo`.
+
+Note: This linter can be disabled with `set_option linter.extra.dupNamespace false`
+-/
+#guard_msgs in
+theorem Bar.Bar.Foo.Foo : True := trivial
+
+section
+set_option linter.extra.dupNamespace.consecutiveOnly false
+
+/--
+warning: The namespace `Bar` is duplicated in the declaration `Bar.Foo.Bar`.
+
+Note: This linter can be disabled with `set_option linter.extra.dupNamespace false`
+-/
+#guard_msgs in
+theorem Bar.Foo.Bar : True := trivial
+
+/--
+warning: The namespaces `Bar` and `Foo` are duplicated in the declaration `Bar.Foo.Bar.Foo`.
+
+Note: This linter can be disabled with `set_option linter.extra.dupNamespace false`
+-/
+#guard_msgs in
+theorem Bar.Foo.Bar.Foo : True := trivial
+end