From 2ba4c55a8498ac495129feeca1ee6dbc9165a8db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Wed, 29 Apr 2026 13:50:40 +0100 Subject: [PATCH] feat: upstream `dupNamespace` environment linter (#13538) This PR upstreams `dupNamespace` linter from batteries to work with new core environment linting framework, as a "clippy" linter - i.e. one that is not enabled by default. Stacked on top of #13513. --------- Co-authored-by: Mac Malone Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com> --- src/Lean/Linter/EnvLinter/Builtin.lean | 12 ++++++++++++ tests/elab/env_linter.lean | 4 ++-- tests/lake/tests/builtin-lint/ClippyViolations.lean | 4 ++++ .../tests/builtin-lint/input/ClippyViolations.lean | 4 ++++ tests/lake/tests/builtin-lint/test.sh | 12 ++++++++++++ 5 files changed, 34 insertions(+), 2 deletions(-) diff --git a/src/Lean/Linter/EnvLinter/Builtin.lean b/src/Lean/Linter/EnvLinter/Builtin.lean index 565599d449..068149b298 100644 --- a/src/Lean/Linter/EnvLinter/Builtin.lean +++ b/src/Lean/Linter/EnvLinter/Builtin.lean @@ -97,6 +97,18 @@ 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 clippy] 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 diff --git a/tests/elab/env_linter.lean b/tests/elab/env_linter.lean index 36589659b1..0c5b5202de 100644 --- a/tests/elab/env_linter.lean +++ b/tests/elab/env_linter.lean @@ -140,7 +140,7 @@ def testGetChecksClippy : CoreM (Array Name) := do let checks ← getChecks (scope := .clippy) (runOnly := none) return checks.map (·.name) -/-- info: #[`dummyClippyLinter] -/ +/-- info: #[`dummyClippyLinter, `dupNamespace] -/ #guard_msgs in #eval testGetChecksClippy @@ -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, `dummyClippyLinter] -/ +/-- info: #[`checkUnivs, `defLemma, `dummyBadName, `dummyClippyLinter, `dupNamespace] -/ #guard_msgs in #eval testGetChecksAll diff --git a/tests/lake/tests/builtin-lint/ClippyViolations.lean b/tests/lake/tests/builtin-lint/ClippyViolations.lean index b4e9c015e7..0a9438bc5a 100644 --- a/tests/lake/tests/builtin-lint/ClippyViolations.lean +++ b/tests/lake/tests/builtin-lint/ClippyViolations.lean @@ -2,3 +2,7 @@ import Linters -- This name ends with 'Clippy' — the dummyClippy linter should flag it. def badNameClippy : Nat := 1 + +-- The component `Dup` appears consecutively in this declaration's name — +-- the builtin clippy `dupNamespace` env linter should flag it. +def Dup.Dup.violation : Nat := 2 diff --git a/tests/lake/tests/builtin-lint/input/ClippyViolations.lean b/tests/lake/tests/builtin-lint/input/ClippyViolations.lean index b4e9c015e7..0a9438bc5a 100644 --- a/tests/lake/tests/builtin-lint/input/ClippyViolations.lean +++ b/tests/lake/tests/builtin-lint/input/ClippyViolations.lean @@ -2,3 +2,7 @@ import Linters -- This name ends with 'Clippy' — the dummyClippy linter should flag it. def badNameClippy : Nat := 1 + +-- The component `Dup` appears consecutively in this declaration's name — +-- the builtin clippy `dupNamespace` env linter should flag it. +def Dup.Dup.violation : Nat := 2 diff --git a/tests/lake/tests/builtin-lint/test.sh b/tests/lake/tests/builtin-lint/test.sh index 0fd16aab37..3c25949692 100755 --- a/tests/lake/tests/builtin-lint/test.sh +++ b/tests/lake/tests/builtin-lint/test.sh @@ -85,6 +85,8 @@ test_run lint --builtin-only Clean lake_out lint --builtin-only ClippyViolations || true no_match_pat 'badNameClippy' produced.out no_match_pat 'clippy text linter saw a declaration' produced.out +# Builtin clippy env linter `dupNamespace` is non-default, so it stays silent. +no_match_pat 'Dup.Dup.violation' produced.out # --clippy should run only non-default (clippy) linters, including the clippy # text linter which tags its warnings with `linter.clippy`. @@ -92,6 +94,9 @@ lake_out lint --clippy ClippyViolations || true match_pat 'badNameClippy' produced.out match_pat "declaration name ends with 'Clippy'" produced.out match_pat 'clippy text linter saw a declaration' produced.out +# Builtin `dupNamespace` env linter fires under --clippy. +match_pat 'Dup.Dup.violation' produced.out +match_pat "namespace .*Dup.* is duplicated" produced.out # --clippy should not run default linters no_match_pat 'shouldBeTheorem' produced.out @@ -108,6 +113,13 @@ no_match_pat 'missing doc string' produced.out lake_out lint --lint-all ClippyViolations || true match_pat 'badNameClippy' produced.out match_pat 'clippy text linter saw a declaration' produced.out +match_pat 'Dup.Dup.violation' produced.out + +# --lint-only dupNamespace runs only the builtin clippy `dupNamespace` env linter. +lake_out lint --lint-only dupNamespace ClippyViolations || true +match_pat 'Dup.Dup.violation' produced.out +no_match_pat 'badNameClippy' produced.out +no_match_pat 'shouldBeTheorem' produced.out # Multiple --lint-only flags accumulate: both named linters should run lake_out lint --lint-only defLemma --lint-only checkUnivs || true