From a88f5a56e5dfa418c0708e46d609c6a028f48705 Mon Sep 17 00:00:00 2001 From: damiano Date: Fri, 29 Mar 2024 04:50:16 +0000 Subject: [PATCH] feat: `dupNamespace` as a syntax linter (#11154) An implementation of the `dupNamespace` from `Std` as a syntax linter. The linter emits a warning for declarations that have a repeated, consecutive namespace: * `Nat.Nat.foo` triggers the linter; * `Nat.foo.Nat` does *not* trigger the linter. *Note.* This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose `declId` is present in the source declaration). [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60dupNamespace.60.20linter) The linter found ```lean private theorem Seminorm.Seminorm.isLUB_sSup ... ``` that is skipped by the environment `dupNamespace` linter. --- Mathlib/Tactic/Lint.lean | 65 ++++++++++++++++++++++++++++++++++++++++ test/Lint.lean | 46 ++++++++++++++++++++++++++++ test/Simps.lean | 14 ++++----- 3 files changed, 118 insertions(+), 7 deletions(-) create mode 100644 test/Lint.lean diff --git a/Mathlib/Tactic/Lint.lean b/Mathlib/Tactic/Lint.lean index e2b7035e2c78d0..60b39b640924b0 100644 --- a/Mathlib/Tactic/Lint.lean +++ b/Mathlib/Tactic/Lint.lean @@ -3,6 +3,8 @@ 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 -/ +import Lean.Linter.Util +import Std.Data.Array.Basic import Std.Tactic.Lint /-! @@ -34,3 +36,66 @@ Linter that checks whether a structure should be in Prop. let allProofs ← projs.allM (do isProof <| ← mkConstWithLevelParams <| declName ++ ·) unless allProofs do return none return m!"all fields are propositional but the structure isn't." + +end Std.Tactic.Lint + +/-! +# `dupNamespace` linter + +The `dupNamespace` linter produces a warning when a declaration 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. +-/ + +namespace Mathlib.Linter + +/-- +The `dupNamespace` linter is set on 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_option linter.dupNamespace : Bool := { + defValue := true + descr := "enable the duplicated namespace linter" +} + +namespace DupNamespaceLinter + +open Lean Parser Elab Command Meta + +/-- Gets the value of the `linter.dupNamespace` option. -/ +def getLinterDupNamespace (o : Options) : Bool := Linter.getLinterValue linter.dupNamespace o + +/-- `getIds stx` extracts the `declId` nodes from the `Syntax` `stx`. +If `stx` is an `alias` or an `export`, then it extracts an `ident`, instead of a `declId`. -/ +partial +def getIds : Syntax → Array Syntax + | .node _ `Std.Tactic.Alias.alias args => #[args[2]!] + | .node _ ``Lean.Parser.Command.export args => #[args[3]![0]] + | stx@(.node _ _ args) => + ((args.attach.map fun ⟨a, _⟩ => getIds a).foldl (· ++ ·) #[stx]).filter (·.getKind == ``declId) + | _ => default + +@[inherit_doc linter.dupNamespace] +def dupNamespace : Linter where run := withSetOptionIn fun stx => do + if getLinterDupNamespace (← getOptions) then + match getIds stx with + | #[id] => + let ns := (← getScope).currNamespace + let declName := ns ++ (if id.getKind == ``declId then id[0].getId else id.getId) + let nm := declName.components + let some (dup, _) := nm.zip (nm.tailD []) |>.find? fun (x, y) => x == y + | return + Linter.logLint linter.dupNamespace id + m!"The namespace '{dup}' is duplicated in the declaration '{declName}'" + | _ => return + +initialize addLinter dupNamespace + +end Mathlib.Linter.DupNamespaceLinter diff --git a/test/Lint.lean b/test/Lint.lean new file mode 100644 index 00000000000000..fda11d1abd2f88 --- /dev/null +++ b/test/Lint.lean @@ -0,0 +1,46 @@ +import Mathlib.Tactic.Lint +import Mathlib.Tactic.ToAdditive + +set_option linter.dupNamespace true in +/-- warning: +The namespace 'add' is duplicated in the declaration 'add.add' +[linter.dupNamespace] +-/ +#guard_msgs in +def add.add := True + +namespace Foo +set_option linter.dupNamespace true in +/-- warning: +The namespace 'Foo' is duplicated in the declaration 'Foo.Foo.foo' +[linter.dupNamespace] +-/ +#guard_msgs in +def Foo.foo := True + +-- the `dupNamespace` linter does not notice that `to_additive` created `Foo.add.add`. +#guard_msgs in +@[to_additive] theorem add.mul : True := .intro + +-- However, the declaration `Foo.add.add` is present in the environment. +run_cmd Lean.Elab.Command.liftTermElabM do + let decl := (← Lean.getEnv).find? ``Foo.add.add + guard decl.isSome + +namespace Nat +/-- +warning: +The namespace 'Nat' is duplicated in the declaration 'Foo.Nat.Nat.Nats' [linter.dupNamespace] +-/ +#guard_msgs in +alias Nat.Nats := Nat + +end Nat +end Foo + +namespace add +/-- +warning: The namespace 'add' is duplicated in the declaration 'add.add' [linter.dupNamespace] +-/ +#guard_msgs in +export Nat (add) diff --git a/test/Simps.lean b/test/Simps.lean index 54d791ce9ef78f..5db2db71beaf24 100644 --- a/test/Simps.lean +++ b/test/Simps.lean @@ -123,15 +123,15 @@ example (n : ℕ) : foo.rfl.toFun n = n := by rw [foo.rfl_toFun, id] example (n : ℕ) : foo.rfl.invFun n = n := by rw [foo.rfl_invFun] /- the declarations are `simp` lemmas -/ -@[simps] def foo : ℕ × ℤ := (1, 2) +@[simps] def bar : ℕ × ℤ := (1, 2) -- note: in Lean 4 the first test succeeds without `@[simps]`, however, the remaining tests don't -example : foo.1 = 1 := by simp -example {a : ℕ} {h : 1 = a} : foo.1 = a := by rw [foo_fst, h] -example {a : ℕ} {h : 1 = a} : foo.1 = a := by simp; rw [h] -example {a : ℤ} {h : 2 = a} : foo.2 = a := by simp; rw [h] -example {a : ℕ} {h : 1 = a} : foo.1 = a := by dsimp; rw [h] -- check that dsimp also unfolds -example {a : ℤ} {h : 2 = a} : foo.2 = a := by dsimp; rw [h] +example : bar.1 = 1 := by simp +example {a : ℕ} {h : 1 = a} : bar.1 = a := by rw [bar_fst, h] +example {a : ℕ} {h : 1 = a} : bar.1 = a := by simp; rw [h] +example {a : ℤ} {h : 2 = a} : bar.2 = a := by simp; rw [h] +example {a : ℕ} {h : 1 = a} : bar.1 = a := by dsimp; rw [h] -- check that dsimp also unfolds +example {a : ℤ} {h : 2 = a} : bar.2 = a := by dsimp; rw [h] example {α} (x y : α) (h : x = y) : foo.rfl.toFun x = y := by simp; rw [h] example {α} (x y : α) (h : x = y) : foo.rfl.invFun x = y := by simp; rw [h] -- example {α} (x y : α) (h : x = y) : foo.rfl.toFun = @id α := by { successIfFail {simp}, rfl }