From 4f7c5f4dcacb1879683e847faa07caeda5f54526 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 20 Nov 2025 06:45:31 +0100 Subject: [PATCH] feat: `#grind_lint skip suffix` delete old grind_lint . move exception to separate file note about stage0 --- src/Init/Grind/Lint.lean | 9 +++- src/Lean/Elab/Tactic/Grind.lean | 1 + src/Lean/Elab/Tactic/Grind/Lint.lean | 47 +++++++++++------ .../Elab/Tactic/Grind/LintExceptions.lean | 20 ++++++++ tests/lean/run/grind_lint.lean | 43 ---------------- tests/lean/run/grind_lint_1.lean | 51 +++++++++++++++++++ tests/lean/run/grind_lint_array.lean | 2 +- tests/lean/run/grind_lint_bitvec.lean | 2 +- tests/lean/run/grind_lint_list.lean | 2 +- tests/lean/run/grind_lint_misc.lean | 2 +- tests/lean/run/grind_lint_std_hashmap.lean | 2 +- tests/lean/run/grind_lint_std_misc.lean | 2 +- tests/lean/run/grind_lint_std_treemap.lean | 2 +- 13 files changed, 118 insertions(+), 67 deletions(-) create mode 100644 src/Lean/Elab/Tactic/Grind/LintExceptions.lean delete mode 100644 tests/lean/run/grind_lint.lean diff --git a/src/Init/Grind/Lint.lean b/src/Init/Grind/Lint.lean index 150a45113f..4aa847bf82 100644 --- a/src/Init/Grind/Lint.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index c4fc1dc669..e15ca2fab8 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Grind/Lint.lean b/src/Lean/Elab/Tactic/Grind/Lint.lean index 5858bad56f..d1d361d5d0 100644 --- a/src/Lean/Elab/Tactic/Grind/Lint.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Grind/LintExceptions.lean b/src/Lean/Elab/Tactic/Grind/LintExceptions.lean new file mode 100644 index 0000000000..52372c84a6 --- /dev/null +++ b/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 diff --git a/tests/lean/run/grind_lint.lean b/tests/lean/run/grind_lint.lean deleted file mode 100644 index 9d5eb51110..0000000000 --- a/tests/lean/run/grind_lint.lean +++ /dev/null @@ -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) diff --git a/tests/lean/run/grind_lint_1.lean b/tests/lean/run/grind_lint_1.lean index b2d97b05ca..465f172cf8 100644 --- a/tests/lean/run/grind_lint_1.lean +++ b/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 diff --git a/tests/lean/run/grind_lint_array.lean b/tests/lean/run/grind_lint_array.lean index c62a6a7e4c..0a76f93709 100644 --- a/tests/lean/run/grind_lint_array.lean +++ b/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: -/ diff --git a/tests/lean/run/grind_lint_bitvec.lean b/tests/lean/run/grind_lint_bitvec.lean index 09f7bba9d7..c676176e50 100644 --- a/tests/lean/run/grind_lint_bitvec.lean +++ b/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 -/ diff --git a/tests/lean/run/grind_lint_list.lean b/tests/lean/run/grind_lint_list.lean index 453929ded5..549c747d02 100644 --- a/tests/lean/run/grind_lint_list.lean +++ b/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 -/ diff --git a/tests/lean/run/grind_lint_misc.lean b/tests/lean/run/grind_lint_misc.lean index a48d4dbde4..c00003010d 100644 --- a/tests/lean/run/grind_lint_misc.lean +++ b/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: -/ diff --git a/tests/lean/run/grind_lint_std_hashmap.lean b/tests/lean/run/grind_lint_std_hashmap.lean index e822103088..3d6c409c23 100644 --- a/tests/lean/run/grind_lint_std_hashmap.lean +++ b/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: -/ diff --git a/tests/lean/run/grind_lint_std_misc.lean b/tests/lean/run/grind_lint_std_misc.lean index 5b998f6b37..2f38716963 100644 --- a/tests/lean/run/grind_lint_std_misc.lean +++ b/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: -/ diff --git a/tests/lean/run/grind_lint_std_treemap.lean b/tests/lean/run/grind_lint_std_treemap.lean index 285d212eb9..974a546fdd 100644 --- a/tests/lean/run/grind_lint_std_treemap.lean +++ b/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: -/