feat: disable "experimental" warning for mvcgen (#10638)

This PR disables the "experimental" warning for `mvcgen` by changing its
default.

src/Lean/Elab/Tactic/Do/VCGen.lean

@@ -464,7 +464,7 @@ where
 @[builtin_tactic Lean.Parser.Tactic.mvcgen]
 def elabMVCGen : Tactic := fun stx => withMainContext do
   if mvcgen.warning.get (← getOptions) then
-    logWarningAt stx "The `mvcgen` tactic is experimental and still under development. Avoid using it in production projects."
+    logWarningAt stx "The `mvcgen` tactic is new and its behavior may change in the future. This project has used `set_option mvcgen.warning true` to discourage its use."
   let ctx ← mkSpecContext stx[1] stx[2]
   let fuel := match ctx.config.stepLimit with
     | some n => .limited n

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -18,9 +18,9 @@ open Lean Parser Elab Tactic Meta Do SpecAttr
 builtin_initialize registerTraceClass `Elab.Tactic.Do.vcgen
 
 register_builtin_option mvcgen.warning : Bool := {
-  defValue := true
+  defValue := false
   group    := "debug"
-  descr    := "disable `mvcgen` usage warning"
+  descr    := "enable `mvcgen` usage warning"
 }
 
 inductive Fuel where