feat: #grind_lint skip suffix

delete old grind_lint

.

move exception to separate file

note about stage0

src/Init/Grind/Lint.lean

@@ -77,11 +77,16 @@ 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 suffix name₁ …` marks all theorems with the given suffix(es) to be skipped.
+For example, `#grind_lint skip suffix foo` will skip `bar.foo`, `qux.foo`, etc.
+
+Examples:
 ```
 #grind_lint skip Array.range_succ
+#grind_lint skip suffix append
 ```
 -/
-syntax (name := grindLintSkip) "#grind_lint" ppSpace &"skip" ident+ : command
+syntax (name := grindLintSkip) "#grind_lint" ppSpace &"skip" (ppSpace &"suffix")? ident+ : command
 
 end Lean.Grind

src/Lean/Elab/Tactic/Grind.lean

@@ -13,3 +13,4 @@ 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
+public import Lean.Elab.Tactic.Grind.LintExceptions

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

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Elab.Command
 import Init.Grind.Lint
+import Lean.Data.Name
 import Lean.Meta.Tactic.Grind.EMatchTheorem
 import Lean.EnvExtension
 import Lean.Elab.Tactic.Grind.Config
@@ -20,6 +21,12 @@ builtin_initialize skipExt : SimplePersistentEnvExtension Name NameSet ←
     addImportedFn := mkStateFromImportedEntries (·.insert) {}
   }
 
+builtin_initialize skipSuffixExt : SimplePersistentEnvExtension Name NameSet ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := (·.insert)
+    addImportedFn := mkStateFromImportedEntries (·.insert) {}
+  }
+
 builtin_initialize muteExt : SimplePersistentEnvExtension Name NameSet ←
   registerSimplePersistentEnvExtension {
     addEntryFn := (·.insert)
@@ -34,14 +41,23 @@ def checkEMatchTheorem (declName : Name) : CoreM Unit := do
 
 @[builtin_command_elab Lean.Grind.grindLintSkip]
 def elabGrindLintSkip : CommandElab := fun stx => do
-  let `(#grind_lint skip $ids:ident*) := stx | throwUnsupportedSyntax
+  let `(#grind_lint skip $[suffix%$sfx?]? $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
+  if sfx?.isSome then
+    -- Skip by suffix
+    for id in ids do
+      let suffixName := id.getId
+      if skipSuffixExt.getState (← getEnv) |>.contains suffixName then
+        throwError "`{suffixName}` is already in the `#grind_lint` skip suffix set"
+      modifyEnv fun env => skipSuffixExt.addEntry env suffixName
+  else
+    -- Skip by exact name
+    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
@@ -139,13 +155,22 @@ def elabGrindLintInspect : CommandElab := fun stx => liftTermElabM <| withTheRea
         $(⟨stx⟩):command)
       Tactic.TryThis.addSuggestion (header := "Try this to display the actual theorem instances:") stx { suggestion := .tsyntax s }
 
+/-- Check if the last component of `name` ends with the string form of `suff`. -/
+def nameEndsWithSuffix (name suff : Name) : Bool :=
+  match name with
+  | .str _ s => s.endsWith suff.toString
+  | _ => false
+
 def getTheorems (prefixes? : Option (Array Name)) (inModule : Bool) : CoreM (List Name) := do
   let skip := skipExt.getState (← getEnv)
+  let skipSuffixes := skipSuffixExt.getState (← getEnv)
   let origins := (← getEMatchTheorems).getOrigins
   let env ← getEnv
   return origins.filterMap fun origin => Id.run do
     let .decl declName := origin | return none
     if skip.contains declName then return none
+    -- Check if declName's last component ends with any of the skip suffixes
+    if skipSuffixes.any fun suff => nameEndsWithSuffix declName suff then return none
     let some prefixes := prefixes? | return some declName
     if inModule then
       let some modIdx := env.getModuleIdxFor? declName | return none
@@ -189,11 +214,3 @@ def elabGrindLintCheck : CommandElab := fun stx => liftTermElabM <| withTheReade
     Tactic.TryThis.addSuggestion stx { suggestion := .string suggestion }
 
 end Lean.Elab.Tactic.Grind
-
--- We allow these as grind lemmas even though they triggers >20 further instantiations.
--- See tests/lean/run/grind_lint.lean for more details.
-#grind_lint skip BitVec.msb_replicate
-#grind_lint skip BitVec.msb_signExtend
-#grind_lint skip List.replicate_sublist_iff
-#grind_lint skip List.Sublist.append
-#grind_lint skip List.Sublist.middle

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

@@ -0,0 +1,20 @@
+/-
+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
+import Init.Grind.Lint
+import Lean.Elab.Tactic.Grind.Lint
+
+-- We allow these as grind lemmas even though they triggers >20 further instantiations.
+-- See tests/lean/run/grind_lint_*.lean for more details.
+#grind_lint skip BitVec.msb_replicate
+#grind_lint skip BitVec.msb_signExtend
+#grind_lint skip List.replicate_sublist_iff
+#grind_lint skip List.Sublist.append
+#grind_lint skip List.Sublist.middle
+
+-- TODO: restore this after an update-stage0
+-- #grind_lint skip suffix sizeOf_spec

tests/lean/run/grind_lint.lean

@@ -1,43 +0,0 @@
-import Std
-import Lean.Elab.Tactic.Grind.Lint
-
-/-! `BitVec` exceptions -/
-
--- `BitVec.msb_replicate` is reasonable at 25.
-#guard_msgs in
-#grind_lint inspect (min := 30) BitVec.msb_replicate
-
--- `BitVec.msb_signExtend` is reasonable at 22.
-#guard_msgs in
-#grind_lint inspect (min := 25)  BitVec.msb_signExtend
-
-/-! `List` exceptions -/
-
--- TODO: Not sure what to do here, see https://lean-fro.zulipchat.com/#narrow/channel/503415-grind/topic/.60.23grind_lint.60.20command/near/556730710
--- #grind_lint inspect List.getLast?_concat
-#grind_lint skip List.getLast?_concat
-
--- TODO: We should consider changing the grind annotation for `List.getElem?_eq_none`
--- so it only fires if we've already proved the hypothesis holds. (i.e. the new gadget)
--- Other than that, everything looks sane here:
--- #grind_lint inspect List.getLast?_pmap
-#grind_lint skip List.getLast?_pmap
-
--- TODO: `List.Sublist.eq_of_length` should probably only fire when we've already proved the hypotheses.
-
--- `List.replicate_sublist_iff` is reasonable at 30.
-#guard_msgs in
-#grind_lint inspect (min := 30) List.replicate_sublist_iff
-
--- `List.Sublist.append` is reasonable at 25.
-#guard_msgs in
-#grind_lint inspect (min := 25) List.Sublist.append
-
--- `List.Sublist.middle` is reasonable at 25.
-#guard_msgs in
-#grind_lint inspect (min := 25) List.Sublist.middle
-
-/-! Final check of everything: -/
-
-#guard_msgs in
-#grind_lint check (min := 20)

tests/lean/run/grind_lint_1.lean

@@ -71,3 +71,54 @@ info: Try this to display the actual theorem instances:
 
 #guard_msgs in
 #grind_lint check (min := 20) in module Init.Data.Array
+
+/-! Test suffix skipping -/
+
+#grind_lint skip suffix succ
+
+/-- error: `succ` is already in the `#grind_lint` skip suffix set -/
+#guard_msgs in
+#grind_lint skip suffix succ
+
+-- First, let's verify individual theorems ending in succ would normally trigger warnings
+-- This should show that Array.range_succ triggers instantiations
+/--
+info: instantiating `Array.range_succ` triggers 19 additional `grind` theorem instantiations
+---
+info: Try this to display the actual theorem instances:
+  [apply] set_option trace.grind.ematch.instance true in
+  #grind_lint inspect Array.range_succ
+-/
+#guard_msgs in
+#grind_lint inspect Array.range_succ
+
+-- Now verify that theorems ending in `succ` are skipped in check
+-- Note: The suffix skip should apply during check, but inspect bypasses it
+-- Array.range_succ and Array.range'_succ should NOT appear in the output
+/--
+info: instantiating `Array.back?_empty` triggers 17 additional `grind` theorem instantiations
+---
+info: instantiating `Array.back?_mapIdx` triggers 18 additional `grind` theorem instantiations
+---
+info: instantiating `Array.count_empty` triggers 16 additional `grind` theorem instantiations
+---
+info: instantiating `Array.count_singleton` triggers 20 additional `grind` theorem instantiations
+---
+info: instantiating `Array.findIdx_empty` triggers 18 additional `grind` theorem instantiations
+---
+info: instantiating `Array.foldl_empty` triggers 19 additional `grind` theorem instantiations
+---
+info: instantiating `Array.foldr_empty` triggers 19 additional `grind` theorem instantiations
+---
+info: Try this:
+  [apply] #grind_lint check  (min := 15) in Array
+  #grind_lint inspect Array.back?_empty
+  #grind_lint inspect Array.back?_mapIdx
+  #grind_lint inspect Array.count_empty
+  #grind_lint inspect Array.count_singleton
+  #grind_lint inspect Array.findIdx_empty
+  #grind_lint inspect Array.foldl_empty
+  #grind_lint inspect Array.foldr_empty
+-/
+#guard_msgs in
+#grind_lint check (min := 15) in Array

tests/lean/run/grind_lint_array.lean

@@ -1,5 +1,5 @@
 import Std
-import Lean.Elab.Tactic.Grind.Lint
+import Lean.Elab.Tactic.Grind.LintExceptions
 
 /-! Check Array namespace: -/
 

tests/lean/run/grind_lint_bitvec.lean

@@ -1,5 +1,5 @@
 import Std
-import Lean.Elab.Tactic.Grind.Lint
+import Lean.Elab.Tactic.Grind.LintExceptions
 
 /-! `BitVec` exceptions -/
 

tests/lean/run/grind_lint_list.lean

@@ -1,5 +1,5 @@
 import Std
-import Lean.Elab.Tactic.Grind.Lint
+import Lean.Elab.Tactic.Grind.LintExceptions
 
 /-! `List` exceptions -/
 

tests/lean/run/grind_lint_misc.lean

@@ -1,5 +1,5 @@
 import Std
-import Lean.Elab.Tactic.Grind.Lint
+import Lean.Elab.Tactic.Grind.LintExceptions
 
 /-! Check miscellaneous namespaces: -/
 

tests/lean/run/grind_lint_std_hashmap.lean

@@ -1,5 +1,5 @@
 import Std
-import Lean.Elab.Tactic.Grind.Lint
+import Lean.Elab.Tactic.Grind.LintExceptions
 
 /-! Check Std hash/tree map/set namespaces: -/
 

tests/lean/run/grind_lint_std_misc.lean

@@ -1,5 +1,5 @@
 import Std
-import Lean.Elab.Tactic.Grind.Lint
+import Lean.Elab.Tactic.Grind.LintExceptions
 
 /-! Check remaining Std sub-namespaces: -/
 

tests/lean/run/grind_lint_std_treemap.lean

@@ -1,5 +1,5 @@
 import Std
-import Lean.Elab.Tactic.Grind.Lint
+import Lean.Elab.Tactic.Grind.LintExceptions
 
 /-! Check Std tree map/set namespaces: -/