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