test: mvcgen' with grind should fail when grind fails (#13672)

This PR fixes the semantics of `mvcgen' with grind`: it now logs an
error per VC that `grind` cannot close and throws at the end, instead of
silently leaving the unsolved VC as a residual. The previous
silent-fallback behaviour is preserved as `mvcgen' with (try grind)`,
which `elabPreTac` recognises and routes to the same efficient `.grind`
path with a `silent` flag.

Co-authored-by: Sebastian Graf <sg@lean-fro.org>

tests/bench/mvcgen/sym/lib/VCGen/Context.lean

@@ -29,12 +29,12 @@ public inductive VCGen.PreTac where
   /-- No pre-tactic; VCs are returned as-is. -/
   | none
   /-- Use grind with the given hypothesis simplification methods. -/
-  | grind
+  | grind (silent : Bool := false)
   /-- Use a user-provided tactic syntax. -/
   | tactic (tac : Syntax)
 
 public meta def VCGen.PreTac.isGrind : VCGen.PreTac → Bool
-  | .grind => true
+  | .grind .. => true
   | _ => false
 
 public structure VCGen.Context where
@@ -151,6 +151,8 @@ public structure VCGen.State where
   this to know which user-provided alts have already been consumed (so it doesn't
   warn about them). -/
   inlineHandledInvariants : Std.HashSet Nat := {}
+  /-- Set when a pre-tactic failed on some VC; `elabMVCGen'` throws if true. -/
+  preTacFailed : Bool := false
 
 public abbrev VCGenM := ReaderT VCGen.Context (StateRefT VCGen.State Grind.GrindM)
 

tests/bench/mvcgen/sym/lib/VCGen/Driver.lean

@@ -29,24 +29,26 @@ namespace VCGen
 /--
 Runs the `preTac` on the VC:
 - `.grind`: tries to solve the VC using the accumulated `Grind.Goal` state via `Grind.Goal.grind`.
+  Reports failure via `Lean.logError` unless `silent` is set.
 - `.tactic`: runs the user-provided tactic on the VC, potentially emitting multiple subgoals.
 - `.none`: returns the VC as-is.
 -/
 public meta def PreTac.run : PreTac →  Grind.Goal → VCGenM (List MVarId)
   | .none, goal => return [goal.mvarId]
-  | .grind, goal => do
+  | .grind silent, goal => do
     let savedMCtx ← getMCtx
     match ← goal.grind with
     | .closed => return []
     | .failed .. =>
       setMCtx savedMCtx
+      unless silent do
+        goal.mvarId.withContext do
+          Lean.logError m!"`grind` failed on goal:{indentD (MessageData.ofGoal goal.mvarId)}"
+        modify fun s => { s with preTacFailed := true }
       return [goal.mvarId]
-  | .tactic tac, goal =>
-    try
-      let (gs, _) ← Lean.Elab.runTactic goal.mvarId tac {} {}
-      pure gs
-    catch _ =>
-      pure [goal.mvarId]
+  | .tactic tac, goal => do
+    let (gs, _) ← Lean.Elab.runTactic goal.mvarId tac {} {}
+    pure gs
 
 /--
 Try to elaborate the user's invariant alt for invariant number `n` inline,
@@ -171,6 +173,8 @@ public structure Result where
   avoid spurious "alt does not match any invariant" warnings for inline-consumed
   alts. -/
   inlineHandledInvariants : Std.HashSet Nat := {}
+  /-- True iff some non-silent pre-tactic failed during VC generation. -/
+  preTacFailed : Bool := false
 
 /--
 Generate verification conditions for a goal of the form `P ⊢ₛ wp⟦e⟧ Q s₁ ... sₙ` by repeatedly
@@ -192,6 +196,7 @@ public meta partial def main (goal : MVarId) (ctx : Context) (stepLimit? : Optio
   return {
     invariants := state.invariants,
     vcs,
-    inlineHandledInvariants := state.inlineHandledInvariants }
+    inlineHandledInvariants := state.inlineHandledInvariants,
+    preTacFailed := state.preTacFailed }
 
 end VCGen

tests/bench/mvcgen/sym/lib/VCGen/Frontend.lean

@@ -212,9 +212,15 @@ private meta def elabPreTac (goal : MVarId) (withPreTac : Syntax) : TacticM (VCG
   let mut params ← Grind.mkDefaultParams {}
   if withPreTac.getNumArgs == 0 then return (.none, params)
   let preTac := withPreTac[1]
+  -- Look through `try` so `with (try grind)` still uses the `.grind` path.
+  let (silent, preTac) :=
+    if preTac.getKind == ``Lean.Parser.Tactic.tacticTry_ then
+      (true, preTac[1][0][0][0])
+    else
+      (false, preTac)
   if preTac.getKind == ``Lean.Parser.Tactic.grind then
     params ← elabGrindParams preTac goal
-    return (.grind, params)
+    return (.grind silent, params)
   else
     return (.tactic preTac, params)
 
@@ -321,3 +327,5 @@ public meta def elabMVCGen' : Tactic := fun stx => withMainContext do
     elabInvariants stx[3] result.invariants (suggestInvariant result.vcs)
   let invariants ← result.invariants.filterM (not <$> ·.isAssigned)
   replaceMainGoal (invariants ++ result.vcs).toList
+  if result.preTacFailed then
+    throwError "pre-tactic failed on at least one VC; see errors above"