From 88bf0276e458d157fb215a19ccf1428717579959 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 17 Jan 2025 09:26:50 +1100 Subject: [PATCH 1/3] feat: do not report Lean internals via exact? and rw? --- src/Lean/Meta/Tactic/LibrarySearch.lean | 7 +++++-- src/Lean/Meta/Tactic/Rewrites.lean | 7 ++++--- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/Lean/Meta/Tactic/LibrarySearch.lean b/src/Lean/Meta/Tactic/LibrarySearch.lean index 493bc1a29e30..d433df48e33e 100644 --- a/src/Lean/Meta/Tactic/LibrarySearch.lean +++ b/src/Lean/Meta/Tactic/LibrarySearch.lean @@ -71,12 +71,15 @@ open LazyDiscrTree (InitEntry findMatches) private def addImport (name : Name) (constInfo : ConstantInfo) : MetaM (Array (InitEntry (Name × DeclMod))) := + -- Don't report lemmas from `Lean.*` or `*.Tactic.*` to users. + let nc := name.components + if nc.head? = `Lean ∨ `Tactic ∈ nc then return #[] else forallTelescope constInfo.type fun _ type => do let e ← InitEntry.fromExpr type (name, DeclMod.none) let a := #[e] if e.key == .const ``Iff 2 then - let a := a.push (←e.mkSubEntry 0 (name, DeclMod.mp)) - let a := a.push (←e.mkSubEntry 1 (name, DeclMod.mpr)) + let a := a.push (← e.mkSubEntry 0 (name, DeclMod.mp)) + let a := a.push (← e.mkSubEntry 1 (name, DeclMod.mpr)) pure a else pure a diff --git a/src/Lean/Meta/Tactic/Rewrites.lean b/src/Lean/Meta/Tactic/Rewrites.lean index 4786735dc475..dfc1fa575850 100644 --- a/src/Lean/Meta/Tactic/Rewrites.lean +++ b/src/Lean/Meta/Tactic/Rewrites.lean @@ -44,11 +44,12 @@ private def addImport (name : Name) (constInfo : ConstantInfo) : if constInfo.isUnsafe then return #[] if !allowCompletion (←getEnv) name then return #[] -- We now remove some injectivity lemmas which are not useful to rewrite by. - if name matches .str _ "injEq" then return #[] - if name matches .str _ "sizeOf_spec" then return #[] match name with - | .str _ n => if n.endsWith "_inj" ∨ n.endsWith "_inj'" then return #[] + | .str _ n => if n = "injEq" ∨ n = "sizeOf_spec" ∨ n.endsWith "_inj" ∨ n.endsWith "_inj'" then return #[] | _ => pure () + -- Don't report lemmas from `Lean.*` or `*.Tactic.*` to users. + let nc := name.components + if nc.head? = `Lean ∨ `Tactic ∈ nc then return #[] withNewMCtxDepth do withReducible do forallTelescopeReducing constInfo.type fun _ type => do match type.getAppFnArgs with From a42885426d0f5473d25fbbd878db1b1ec204951b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 17 Jan 2025 09:33:29 +1100 Subject: [PATCH 2/3] test --- tests/lean/librarySearch.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tests/lean/librarySearch.lean b/tests/lean/librarySearch.lean index 41e274b50dc2..0ce93640d504 100644 --- a/tests/lean/librarySearch.lean +++ b/tests/lean/librarySearch.lean @@ -275,3 +275,9 @@ error: apply? didn't find any relevant lemmas -/ #guard_msgs in example {α : Sort u} (x y : α) : Eq x y := by apply? + +-- If this lemmas is added later to the library, please update this `#guard_msgs`. +-- The point of this test is to ensure that `Lean.Grind.not_eq_prop` is not reported to users. +/-- error: `exact?` could not close the goal. Try `apply?` to see partial suggestions. -/ +#guard_msgs in +example (p q : Prop) : (¬ p = q) = (p = ¬ q) := by exact? From 0f2ad69104e2a10cc8985e949880a25ffdd73e50 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 17 Jan 2025 10:08:52 +1100 Subject: [PATCH 3/3] factor out test --- src/Lean/Data/Name.lean | 5 +++++ src/Lean/Meta/Tactic/LibrarySearch.lean | 5 ++--- src/Lean/Meta/Tactic/Rewrites.lean | 5 ++--- 3 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean index 8e7bed47e4bf..a7f93da5ec1a 100644 --- a/src/Lean/Data/Name.lean +++ b/src/Lean/Data/Name.lean @@ -184,6 +184,11 @@ def anyS (n : Name) (f : String → Bool) : Bool := | .num p _ => p.anyS f | _ => false +/-- Return true if the name is in a namespace associated to metaprogramming.-/ +def isMetaprogramming (n : Name) : Bool := + let components := n.components + components.head? == `Lean || (components.any fun n => n == `Tactic || n == `Linter) + end Name end Lean diff --git a/src/Lean/Meta/Tactic/LibrarySearch.lean b/src/Lean/Meta/Tactic/LibrarySearch.lean index d433df48e33e..95544d6b2c30 100644 --- a/src/Lean/Meta/Tactic/LibrarySearch.lean +++ b/src/Lean/Meta/Tactic/LibrarySearch.lean @@ -71,9 +71,8 @@ open LazyDiscrTree (InitEntry findMatches) private def addImport (name : Name) (constInfo : ConstantInfo) : MetaM (Array (InitEntry (Name × DeclMod))) := - -- Don't report lemmas from `Lean.*` or `*.Tactic.*` to users. - let nc := name.components - if nc.head? = `Lean ∨ `Tactic ∈ nc then return #[] else + -- Don't report lemmas from metaprogramming namespaces. + if name.isMetaprogramming then return #[] else forallTelescope constInfo.type fun _ type => do let e ← InitEntry.fromExpr type (name, DeclMod.none) let a := #[e] diff --git a/src/Lean/Meta/Tactic/Rewrites.lean b/src/Lean/Meta/Tactic/Rewrites.lean index dfc1fa575850..8a543104039f 100644 --- a/src/Lean/Meta/Tactic/Rewrites.lean +++ b/src/Lean/Meta/Tactic/Rewrites.lean @@ -47,9 +47,8 @@ private def addImport (name : Name) (constInfo : ConstantInfo) : match name with | .str _ n => if n = "injEq" ∨ n = "sizeOf_spec" ∨ n.endsWith "_inj" ∨ n.endsWith "_inj'" then return #[] | _ => pure () - -- Don't report lemmas from `Lean.*` or `*.Tactic.*` to users. - let nc := name.components - if nc.head? = `Lean ∨ `Tactic ∈ nc then return #[] + -- Don't report lemmas from metaprogramming namespaces. + if name.isMetaprogramming then return #[] withNewMCtxDepth do withReducible do forallTelescopeReducing constInfo.type fun _ type => do match type.getAppFnArgs with