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.

Author: kim-em

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 []

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"
 }
 
 /--