From c32a57e5806476ed6bac4c9cf1bb11cea2b02ea2 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Thu, 9 Oct 2025 08:31:18 +0200 Subject: [PATCH] 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. --- 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 9881eae2a8..2a175654b9 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean index 83782aad54..8dfbb325a5 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 := false + defValue := true group := "debug" - descr := "enable `mvcgen` usage warning" + descr := "disable `mvcgen` usage warning" } inductive Fuel where