diff --git a/src/Lean/Elab/Tactic/Grind/Param.lean b/src/Lean/Elab/Tactic/Grind/Param.lean index c502c5d15536..784cd0bc4303 100644 --- a/src/Lean/Elab/Tactic/Grind/Param.lean +++ b/src/Lean/Elab/Tactic/Grind/Param.lean @@ -96,6 +96,7 @@ def processParam (params : Grind.Params) throwErrorAt id "redundant parameter `{id}`, `grind` uses local hypotheses automatically" else throw err + Linter.checkDeprecated declName let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer match kind with | .ematch .user => @@ -221,6 +222,7 @@ public def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.T if incremental then throwErrorAt p "invalid `-` occurrence, it can only used at the `grind` tactic entry point" let declName ← realizeGlobalConstNoOverloadWithInfo id + Linter.checkDeprecated declName if let some declName ← Grind.isCasesAttrCandidate? declName false then Grind.ensureNotBuiltinCases declName params := { params with casesTypes := (← params.casesTypes.eraseDecl declName) } diff --git a/tests/lean/run/grindDeprecated.lean b/tests/lean/run/grindDeprecated.lean new file mode 100644 index 000000000000..194acaac1955 --- /dev/null +++ b/tests/lean/run/grindDeprecated.lean @@ -0,0 +1,27 @@ +/-! +Test that `grind` flags deprecated theorems. +See https://github.com/leanprover/lean4/issues/11582 +-/ +set_option backward.grind.inferPattern true -- Use old pattern inference (no suggestions) +set_option linter.deprecated true -- Enable the deprecated linter (test framework disables all linters) + +def foo : Nat := 0 + +@[deprecated "use foo_eq_zero' instead" (since := "2025-01-01")] +theorem foo_eq_zero : foo = 0 := rfl + +/-- warning: `foo_eq_zero` has been deprecated: use foo_eq_zero' instead -/ +#guard_msgs in +example : foo = foo := by grind [foo_eq_zero] + +-- Also test the `-` syntax for erasing theorems +@[grind] +theorem bar_eq_zero : foo = 0 := rfl + +-- This theorem is deprecated AND marked with @[grind], so we can erase it +@[deprecated bar_eq_zero (since := "2025-01-01"), grind] +theorem bar_eq_zero' : foo = 0 := rfl + +/-- warning: `bar_eq_zero'` has been deprecated: Use `bar_eq_zero` instead -/ +#guard_msgs in +example : foo = foo := by grind [- bar_eq_zero']