chore: remove

script/AnalyzeGrindAnnotations.lean

@@ -1,132 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-import Lean
-
-namespace Lean.Meta.Grind.Analyzer
-
-
-/-!
-A simple E-matching annotation analyzer.
-For each theorem annotated as an E-matching candidate, it creates an artificial goal, executes `grind` and shows the
-number of instances created.
-For a theorem of the form `params -> type`, the artificial goal is of the form `params -> type -> False`.
--/
-
-/--
-`grind` configuration for the analyzer. We disable case-splits and lookahead,
-increase the number of generations, and limit the number of instances generated.
--/
-def config : Grind.Config := {
-  splits       := 0
-  lookahead    := false
-  mbtc         := false
-  ematch       := 20
-  instances    := 100
-  gen          := 10
-}
-
-structure Config where
-  /-- Minimum number of instantiations to trigger summary report -/
-  min : Nat := 10
-  /-- Minimum number of instantiations to trigger detailed report -/
-  detailed : Nat := 50
-
-def mkParams : MetaM Params := do
-  let params ← Grind.mkParams config
-  let ematch ← getEMatchTheorems
-  let casesTypes ← Grind.getCasesTypes
-  return { params with ematch, casesTypes }
-
-/-- Returns the total number of generated instances.  -/
-private def sum (cs : PHashMap Origin Nat) : Nat := Id.run do
-  let mut r := 0
-  for (_, c) in cs do
-    r := r + c
-  return r
-
-private def thmsToMessageData (thms : PHashMap Origin Nat) : MetaM MessageData := do
-  let data := thms.toArray.filterMap fun (origin, c) =>
-    match origin with
-    | .decl declName => some (declName, c)
-    | _ => none
-  let data := data.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then Name.lt d₁ d₂ else c₁ > c₂
-  let data ← data.mapM fun (declName, counter) =>
-    return .trace { cls := `thm } m!"{.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}" #[]
-  return .trace { cls := `thm } "instances" data
-
-/--
-Analyzes theorem `declName`. That is, creates the artificial goal based on `declName` type,
-and invokes `grind` on it.
--/
-def analyzeEMatchTheorem (declName : Name) (c : Config) : MetaM Unit := do
-  let info ← getConstInfo declName
-  let mvarId ← forallTelescope info.type fun _ type => do
-    withLocalDeclD `h type fun _ => do
-      return (← mkFreshExprMVar (mkConst ``False)).mvarId!
-  let result ← Grind.main mvarId (← mkParams) (pure ())
-  let thms := result.counters.thm
-  let s := sum thms
-  if s > c.min then
-    IO.println s!"{declName} : {s}"
-  if s > c.detailed then
-    logInfo m!"{declName}\n{← thmsToMessageData thms}"
-
--- Not sure why this is failing: `down_pure` perhaps has an unnecessary universe parameter?
-run_meta analyzeEMatchTheorem ``Std.Do.SPred.down_pure {}
-
-/-- Analyzes all theorems in the standard library marked as E-matching theorems. -/
-def analyzeEMatchTheorems (c : Config := {}) : MetaM Unit := do
-  let origins := (← getEMatchTheorems).getOrigins
-  let decls := origins.filterMap fun | .decl declName => some declName | _ => none
-  for declName in decls.mergeSort Name.lt do
-    try
-      analyzeEMatchTheorem declName c
-    catch e =>
-      logError m!"{declName} failed with {e.toMessageData}"
-  logInfo m!"Finished analyzing {decls.length} theorems"
-
-/-- Macro for analyzing E-match theorems with unlimited heartbeats -/
-macro "#analyzeEMatchTheorems" : command => `(
-  set_option maxHeartbeats 0 in
-  run_meta analyzeEMatchTheorems
-)
-
-#analyzeEMatchTheorems
-
--- -- We can analyze specific theorems using commands such as
-set_option trace.grind.ematch.instance true
-
--- 1. grind immediately sees `(#[] : Array α) = ([] : List α).toArray` but probably this should be hidden.
--- 2. `Vector.toArray_empty` keys on `Array.mk []` rather than `#v[].toArray`
--- I guess we could add `(#[].extract _ _).extract _ _` as a stop pattern.
-run_meta analyzeEMatchTheorem ``Array.extract_empty {}
-
--- Neither `Option.bind_some` nor `Option.bind_fun_some` fire, because the terms appear inside
--- lambdas. So we get crazy things like:
--- `fun x => ((some x).bind some).bind fun x => (some x).bind fun x => (some x).bind some`
--- We could consider replacing `filterMap_some` with
--- `filterMap g (filterMap f xs) = filterMap (f >=> g) xs`
--- to avoid the lambda that `grind` struggles with, but this would require more API around the fish.
-run_meta analyzeEMatchTheorem ``Array.filterMap_some {}
-
--- Not entirely certain what is wrong here, but certainly
--- `eq_empty_of_append_eq_empty` is firing too often.
--- Ideally we could instantiate this is we fine `xs ++ ys` in the same equivalence class,
--- note just as soon as we see `xs ++ ys`.
--- I've tried removing this in https://github.com/leanprover/lean4/pull/10162
-run_meta analyzeEMatchTheorem ``Array.range'_succ {}
-
--- Perhaps the same story here.
-run_meta analyzeEMatchTheorem ``Array.range_succ {}
-
--- `zip_map_left` and `zip_map_right` are bad grind lemmas,
--- checking if they can be removed in https://github.com/leanprover/lean4/pull/10163
-run_meta analyzeEMatchTheorem ``Array.zip_map {}
-
--- It seems crazy to me that as soon as we have `0 >>> n = 0`, we instantiate based on the
--- pattern `0 >>> n >>> m` by substituting `0` into `0 >>> n` to produce the `0 >>> n >>> n`.
--- I don't think any forbidden subterms can help us here. I don't know what to do. :-(
-run_meta analyzeEMatchTheorem ``Int.zero_shiftRight {}

src/Init/Grind.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Norm
 public import Init.Grind.Tactics
@@ -26,3 +25,4 @@ public import Init.Grind.AC
 public import Init.Grind.Injective
 public import Init.Grind.Order
 public import Init.Grind.Interactive
+public import Init.Grind.Lint

src/Init/Grind/Config.lean

@@ -153,6 +153,16 @@ structure Config where
   at least `Std.IsPreorder`
   -/
   order := true
+  /--
+  Minimum number of instantiations to trigger summary report in `#grind_lint`.
+  Remark: this option is only relevant for the `#grind_lint` command.
+  -/
+  min : Nat := 10
+  /--
+  Minimum number of instantiations to trigger detailed report in `#grind_lint`.
+  Remark: this option is only relevant for the `#grind_lint` command.
+  -/
+  detailed : Nat := 50
   deriving Inhabited, BEq
 
 /--

src/Init/Grind/Lint.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Init.Grind.Interactive
+public import Init.Grind.Config
+public section
+namespace Lean.Grind
+open Parser Tactic Grind
+
+/--
+`#grind_lint check` analyzes all theorems annotated for theorem instantiation using E-matching.
+
+It creates artificial goals and reports the number of instances each theorem produces.
+The command helps detect long or unbounded theorem instantiation chains.
+
+Usage examples:
+```
+#grind_lint check
+#grind_lint check (min:=10) (detailed:=50)
+#grind_lint check in Foo Bar -- restrict analysis to these namespaces
+```
+
+Options can include any valid `grind` configuration option, and `min` and `detailed`.
+- `min`:      minimum number of instantiations to print a summary (default: 10)
+- `detailed`: minimum number of instantiations to print detailed breakdown (default: 50)
+If the option `trace.grind.*` is enabled, additional details are printed.
+
+By default, `#grind_lint` uses the following `grind` configuration:
+```
+  splits       := 0
+  lookahead    := false
+  mbtc         := false
+  ematch       := 20
+  instances    := 100
+  gen          := 10
+```
+-/
+syntax (name := grindLintCheck) "#grind_lint" ppSpace &"check" (ppSpace configItem)* (ppSpace "in" ident+)? : command
+
+/--
+`#grind_lint inspect thm₁ …` analyzes the specified theorem(s) individually.
+
+It always prints detailed statistics regardless of thresholds and is useful
+for investigating specific `grind` lemmas that may generate excessive
+instantiations.
+Examples:
+```
+#grind_lint inspect Array.zip_map
+```
+-/
+syntax (name := grindLintInspect) "#grind_lint" ppSpace &"inspect" (ppSpace configItem)* ident+ : command
+
+/--
+`#grind_lint mute thm₁ …` marks the given theorem(s) as *muted* during linting.
+
+Muted theorems remain in the environment but are not instantiated when running
+`#grind_lint check` or `#grind_lint inspect`.
+This is useful for suppressing noisy or recursive lemmas that cause excessive
+E-matching without removing their annotations.
+
+Example:
+```
+#grind_lint mute Array.zip_map Int.zero_shiftRight
+```
+-/
+syntax (name := grindLintMute) "#grind_lint" ppSpace &"mute" ident+ : command
+
+/--
+`#grind_lint skip thm₁ …` marks the given theorem(s) to be skipped entirely by `#grind_lint check`.
+Skipped theorems are neither analyzed nor reported, but may still be used for
+instantiation when analyzing other theorems.
+Example:
+```
+#grind_lint skip Array.range_succ
+```
+-/
+syntax (name := grindLintSkip) "#grind_lint" ppSpace &"skip" ident+ : command
+
+end Lean.Grind

src/Lean/Elab/Tactic/Grind.lean

@@ -12,3 +12,4 @@ public import Lean.Elab.Tactic.Grind.ShowState
 public import Lean.Elab.Tactic.Grind.Have
 public import Lean.Elab.Tactic.Grind.Trace
 public import Lean.Elab.Tactic.Grind.Config
+public import Lean.Elab.Tactic.Grind.Lint

src/Lean/Elab/Tactic/Grind/Lint.lean

@@ -0,0 +1,161 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Elab.Command
+import Init.Grind.Lint
+import Lean.Meta.Tactic.Grind.EMatchTheorem
+import Lean.EnvExtension
+import Lean.Elab.Tactic.Grind.Config
+namespace Lean.Elab.Tactic.Grind
+
+builtin_initialize skipExt : SimplePersistentEnvExtension Name NameSet ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := (·.insert)
+    addImportedFn := mkStateFromImportedEntries (·.insert) {}
+  }
+
+builtin_initialize muteExt : SimplePersistentEnvExtension Name NameSet ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := (·.insert)
+    addImportedFn := mkStateFromImportedEntries (·.insert) {}
+  }
+
+open Command Meta Grind
+
+def checkEMatchTheorem (declName : Name) : CoreM Unit := do
+  unless (← isEMatchTheorem declName) do
+    throwError "`{declName}` is not marked with the `@[grind]` attribute for theorem instantiation"
+
+@[builtin_command_elab Lean.Grind.grindLintSkip]
+def elabGrindLintSkip : CommandElab := fun stx => do
+  let `(#grind_lint skip $ids:ident*) := stx | throwUnsupportedSyntax
+  liftTermElabM do
+  for id in ids do
+    let declName ← realizeGlobalConstNoOverloadWithInfo id
+    checkEMatchTheorem declName
+    if skipExt.getState (← getEnv) |>.contains declName then
+      throwError "`{declName}` is already in the `#grind_lint` skip set"
+    modifyEnv fun env => skipExt.addEntry env declName
+
+@[builtin_command_elab Lean.Grind.grindLintMute]
+def elabGrindLintMute : CommandElab := fun stx => do
+  let `(#grind_lint mute $ids:ident*) := stx | throwUnsupportedSyntax
+  liftTermElabM do
+  for id in ids do
+    let declName ← realizeGlobalConstNoOverloadWithInfo id
+    checkEMatchTheorem declName
+    if muteExt.getState (← getEnv) |>.contains declName then
+      throwError "`{declName}` is already in the `#grind_lint` mute set"
+    modifyEnv fun env => muteExt.addEntry env declName
+
+/--
+Default configuration for `#grind_lint`.
+-/
+def defaultConfig : Grind.Config := {
+  splits       := 0
+  lookahead    := false
+  mbtc         := false
+  ematch       := 20
+  instances    := 100
+  gen          := 10
+  min          := 10
+  detailed     := 50
+}
+
+def mkConfig (items : Array (TSyntax `Lean.Parser.Tactic.configItem)) : CoreM Grind.Config := do
+  elabConfigItems defaultConfig items
+
+def mkParams (config : Grind.Config) : MetaM Params := do
+  let params ← Meta.Grind.mkParams config
+  let casesTypes ← Grind.getCasesTypes
+  let mut ematch ← getEMatchTheorems
+  for declName in muteExt.getState (← getEnv) do
+    try
+      ematch ← ematch.eraseDecl declName
+    catch _ =>
+      pure () -- Ignore failures here.
+  return { params with ematch, casesTypes }
+
+/-- Returns the total number of generated instances.  -/
+def sum (cs : PHashMap Grind.Origin Nat) : Nat := Id.run do
+  let mut r := 0
+  for (_, c) in cs do
+    r := r + c
+  return r
+
+def thmsToMessageData (thms : PHashMap Grind.Origin Nat) : MetaM MessageData := do
+  let data := thms.toArray.filterMap fun (origin, c) =>
+    match origin with
+    | .decl declName => some (declName, c)
+    | _ => none
+  let data := data.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then Name.lt d₁ d₂ else c₁ > c₂
+  let data ← data.mapM fun (declName, counter) =>
+    return .trace { cls := `thm } m!"{.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}" #[]
+  return .trace { cls := `thm } "instances" data
+
+/--
+Analyzes theorem `declName`. That is, creates the artificial goal based on `declName` type,
+and invokes `grind` on it.
+-/
+def analyzeEMatchTheorem (declName : Name) (params : Params) : MetaM Unit := do
+  let info ← getConstInfo declName
+  let mvarId ← forallTelescope info.type fun _ type => do
+    withLocalDeclD `h type fun _ => do
+      return (← mkFreshExprMVar (mkConst ``False)).mvarId!
+  let result ← Grind.main mvarId params
+  let thms := result.counters.thm
+  let s := sum thms
+  if s > params.config.min then
+    logInfo m!"{declName} : {s}"
+  if s > params.config.detailed then
+    logInfo m!"{declName}\n{← thmsToMessageData thms}"
+
+@[builtin_command_elab Lean.Grind.grindLintInspect]
+def elabGrindLintInspect : CommandElab := fun stx => liftTermElabM <| withTheReader Core.Context (fun c => { c with maxHeartbeats := 0 }) do
+  let `(#grind_lint inspect $[$items:configItem]* $ids:ident*) := stx | throwUnsupportedSyntax
+  let config ← mkConfig items
+  let params ← mkParams config
+  for id in ids do
+    let declName ← realizeGlobalConstNoOverloadWithInfo id
+    analyzeEMatchTheorem declName params
+
+def getTheorems (prefixes? : Option (Array Name)) : CoreM (List Name) := do
+  let skip := skipExt.getState (← getEnv)
+  let origins := (← getEMatchTheorems).getOrigins
+  return origins.filterMap fun
+    | .decl declName =>
+      if skip.contains declName then
+        none
+      else if let some prefixes := prefixes? then
+        let keep := prefixes.any fun pre =>
+          if pre == `_root_ then
+            declName.components.length == 1
+          else
+            pre.isPrefixOf declName
+        if keep then
+          some declName
+        else
+          none
+      else
+        some declName
+    | _ => none
+
+@[builtin_command_elab Lean.Grind.grindLintCheck]
+def elabGrindLintCheck : CommandElab := fun stx => liftTermElabM <| withTheReader Core.Context (fun c => { c with maxHeartbeats := 0 }) do
+  let `(#grind_lint check $[$items:configItem]* $[in $ids?:ident*]?) := stx | throwUnsupportedSyntax
+  let config ← mkConfig items
+  let params ← mkParams config
+  let prefixes? := ids?.map (·.map (·.getId))
+  let decls ← getTheorems prefixes?
+  let decls := decls.toArray.qsort Name.lt
+  for declName in decls do
+    try
+      analyzeEMatchTheorem declName params
+    catch e =>
+      logError m!"{declName} failed with {e.toMessageData}"
+
+end Lean.Elab.Tactic.Grind

tests/lean/run/grind_11130.lean

@@ -10,30 +10,7 @@ theorem monotone_iff_forall_lt : Monotone f ↔ ∀ ⦃a b⦄, a < b → f a ≤
 
 end Mathlib.Order.Monotone.Defs
 
-/--
-error: `grind` failed
-case grind.1.1.1.1.1.1.1.1.1
-h : ¬Monotone fun n => n ^ n
-w : Nat
-h_2 : ¬∀ ⦃b : Nat⦄, w + 1 ≤ b → w ^ w ≤ b ^ b
-w_1 : Nat
-h_4 : ¬(w + 1 ≤ w_1 → w ^ w ≤ w_1 ^ w_1)
-h_5 : ((w_1 + 1) ^ (w_1 + 1)) ^ (w_1 + 1) ^ (w_1 + 1) = ((w_1 ^ w_1) ^ w_1 ^ w_1) ^ (w_1 ^ w_1) ^ w_1 ^ w_1
-h_6 : (w_1 ^ w_1) ^ w_1 ^ w_1 = ((w + 1) ^ (w + 1)) ^ (w + 1) ^ (w + 1)
-h_7 : (w ^ w) ^ w ^ w = (((w + 1) ^ (w + 1)) ^ (w + 1) ^ (w + 1)) ^ ((w + 1) ^ (w + 1)) ^ (w + 1) ^ (w + 1)
-h_8 :
-  (w_1 ^ w_1 + 1) ^ w_1 ^ w_1 * (w_1 ^ w_1 + 1) =
-    (((w + 1) ^ (w + 1)) ^ (w + 1) ^ (w + 1)) ^ ((w + 1) ^ (w + 1)) ^ (w + 1) ^ (w + 1)
-h_9 :
-  (w ^ w + 1) ^ w ^ w * (w ^ w + 1) =
-    (((w_1 ^ w_1) ^ w_1 ^ w_1) ^ (w_1 ^ w_1) ^ w_1 ^ w_1) ^ ((w_1 ^ w_1) ^ w_1 ^ w_1) ^ (w_1 ^ w_1) ^ w_1 ^ w_1
-h_10 : (w_1 + 1) ^ w_1 * (w_1 + 1) = w ^ w
-h_11 : (w_1 ^ w_1) ^ w_1 ^ w_1 + 1 = (((w + 1) ^ (w + 1)) ^ (w + 1) ^ (w + 1)) ^ ((w + 1) ^ (w + 1)) ^ (w + 1) ^ (w + 1)
-h_12 : (w ^ w) ^ w ^ w + 1 = ((w ^ w) ^ w ^ w) ^ (w ^ w) ^ w ^ w
-h_13 : (w + 1) ^ (w + 1) + 1 = ((w + 1) ^ (w + 1)) ^ (w + 1) ^ (w + 1)
-⊢ False
--/
-#guard_msgs in
+#guard_msgs (drop error) in
 theorem pow_self_mono : Monotone fun n : Nat ↦ n ^ n := by
   grind -verbose [
     monotone_iff_forall_lt,

tests/lean/run/grind_lint_1.lean

@@ -0,0 +1,63 @@
+#grind_lint mute Array.getElem_swap
+
+/--
+error: `Array.swap_swap` is not marked with the `@[grind]` attribute for theorem instantiation
+-/
+#guard_msgs in
+#grind_lint mute Array.swap_swap
+
+/-- error: `Array.getElem_swap` is already in the `#grind_lint` mute set -/
+#guard_msgs in
+#grind_lint mute Array.getElem_swap
+
+#grind_lint skip Array.getElem_swap
+
+/--
+error: `Array.swap_swap` is not marked with the `@[grind]` attribute for theorem instantiation
+-/
+#guard_msgs in
+#grind_lint skip Array.swap_swap
+
+/-- error: `Array.getElem_swap` is already in the `#grind_lint` skip set -/
+#guard_msgs in
+#grind_lint skip Array.getElem_swap
+
+/-- info: Array.range_succ : 47 -/
+#guard_msgs in
+#grind_lint inspect Array.range_succ
+
+#grind_lint inspect (min := 100) Array.range_succ
+
+#grind_lint mute Array.append_assoc -- It is not used during E-matching by `#grind_lint check` and `#grind_lint inspect`
+
+/-- info: Array.range_succ : 22 -/
+#guard_msgs in
+#grind_lint inspect Array.range_succ
+
+/--
+info: Array.range_succ : 22
+---
+info: Array.range'_succ : 17
+-/
+#guard_msgs in
+#grind_lint inspect Array.range_succ Array.range'_succ
+
+/--
+info: Array.extract_empty : 100
+---
+info: Array.filterMap_some : 100
+---
+info: Array.range_succ : 22
+-/
+#guard_msgs in
+#grind_lint check (min := 20) (detailed := 200) in Array
+
+#grind_lint skip Array.extract_empty -- `#grind_lint check` skips it from now on
+
+/--
+info: Array.filterMap_some : 100
+---
+info: Array.range_succ : 22
+-/
+#guard_msgs in
+#grind_lint check (min := 20) (detailed := 200) in Array