From aaacae6a23a947daa348265988a036be8cace5c0 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Thu, 2 Jul 2026 13:02:22 +0000 Subject: [PATCH 1/3] feat: add `linter.extra.dupNamespace.consecutiveOnly` option to `dupNamespace linter` --- src/Lean/Linter/Extra/DupNamespace.lean | 29 +++++++++++++++--- tests/elab/dupNamespace.lean | 39 +++++++++++++++++++++++++ 2 files changed, 64 insertions(+), 4 deletions(-) create mode 100644 tests/elab/dupNamespace.lean diff --git a/src/Lean/Linter/Extra/DupNamespace.lean b/src/Lean/Linter/Extra/DupNamespace.lean index fbc2461aa710..43ab4e5b7799 100644 --- a/src/Lean/Linter/Extra/DupNamespace.lean +++ b/src/Lean/Linter/Extra/DupNamespace.lean @@ -33,6 +33,12 @@ register_builtin_option linter.extra.dupNamespace : Bool := { 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 +84,25 @@ 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 options ← getOptions + 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}`." + | dup => + 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 diff --git a/tests/elab/dupNamespace.lean b/tests/elab/dupNamespace.lean new file mode 100644 index 000000000000..f3537b372137 --- /dev/null +++ b/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 From 0fbfad15138755a5aad1f9dd169acc4956e88855 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Thu, 2 Jul 2026 13:09:42 +0000 Subject: [PATCH 2/3] chore: minor refactopr and fix docstring --- src/Lean/Linter/Extra/DupNamespace.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Lean/Linter/Extra/DupNamespace.lean b/src/Lean/Linter/Extra/DupNamespace.lean index 43ab4e5b7799..c7f0127ed91b 100644 --- a/src/Lean/Linter/Extra/DupNamespace.lean +++ b/src/Lean/Linter/Extra/DupNamespace.lean @@ -20,14 +20,17 @@ 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. +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. *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" @@ -38,7 +41,6 @@ register_builtin_option linter.extra.dupNamespace.consecutiveOnly : Bool := { descr := "only warn on consecutive duplicated namespaces" } - namespace DupNamespaceLinter open Lean Parser Elab Command Meta Linter @@ -84,7 +86,6 @@ 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 options ← getOptions let duplicated := if (← getBoolOption `linter.extra.dupNamespace.consecutiveOnly (defValue := true)) then -- Only check consecutive components @@ -98,7 +99,7 @@ def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do Linter.logLint linter.extra.dupNamespace id m!"The namespace `{ns}` is duplicated in the declaration \ `{.ofConstName (fullNames := true) declName}`." - | dup => + | _ => let ns := MessageData.andList (duplicated.map (m!"`{·}`")) Linter.logLint linter.extra.dupNamespace id m!"The namespaces {ns} are duplicated in the declaration \ From 3df446e2e44decb84a26ded4e5bcbf0af7bb4a43 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Thu, 2 Jul 2026 16:24:49 +0000 Subject: [PATCH 3/3] chore: fix docstring --- src/Lean/Linter/Extra/DupNamespace.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/Lean/Linter/Extra/DupNamespace.lean b/src/Lean/Linter/Extra/DupNamespace.lean index c7f0127ed91b..62db5ba263ac 100644 --- a/src/Lean/Linter/Extra/DupNamespace.lean +++ b/src/Lean/Linter/Extra/DupNamespace.lean @@ -25,10 +25,6 @@ contains the same namespace more than once. 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. - -*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 := {