From 689b3aa8d747fa9575c36746d67f83b1f7caeaa7 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 1 Oct 2025 16:10:40 +0200 Subject: [PATCH] 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 | 2 +- src/Lean/Elab/Tactic/Do/VCGen/Basic.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean index 0410b6b3bb..dc12594dc7 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean index 031f9be542..5a5cbc954d 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean +++ b/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