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

This PR re-enables the "experimental" warning for `mvcgen` by changing
its default. The official release has been postponed to justify small
breaking changes in the semantic foundations in the near future.

Author: sgraf812

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

@@ -448,7 +448,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 new and its behavior may change in the future. This project has used `set_option mvcgen.warning true` to discourage its use."
+    logWarningAt stx "The `mvcgen` tactic is experimental and still under development. Avoid using it in production projects."
   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 := false
+  defValue := true
   group    := "debug"
-  descr    := "enable `mvcgen` usage warning"
+  descr    := "disable `mvcgen` usage warning"
 }
 
 inductive Fuel where