From 8fce30e7cb027e70cc2b7b9ea0143792776cb2c3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 10 Jun 2025 13:40:45 +1000 Subject: [PATCH] chore: change grind.warning default to false (#8698) This PR turns off the default warning when using `grind`, in preparation for v4.22. I'll removing all the `set_option grind.warning false` in our codebase in a second PR, after an update-stage0. --- src/Lean/Elab/Tactic/Grind.lean | 2 +- src/Lean/Meta/Tactic/Grind/Types.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index 64fa3d46ad..a9f2ef9ed2 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -182,7 +182,7 @@ def evalGrindCore let only := only.isSome let params := if let some params := params then params.getElems else #[] if Grind.grind.warning.get (← getOptions) then - logWarningAt ref "The `grind` tactic is experimental and still under development. Avoid using it in production projects." + logWarningAt ref "The `grind` tactic is new and its behaviour may change in the future. This project has used `set_option grind.warning true` to discourage its use." withMainContext do let result ← grind (← getMainGoal) config only params fallback replaceMainGoal [] diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 6479a84126..820a1d17d1 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -48,9 +48,9 @@ register_builtin_option grind.debug.proofs : Bool := { } register_builtin_option grind.warning : Bool := { - defValue := true + defValue := false group := "debug" - descr := "disable `grind` usage warning" + descr := "generate a warning whenever `grind` is used" } /--