From 8916246be5266d01bc1f27095699d39d8f646cd4 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Tue, 24 Feb 2026 14:10:42 +0100
Subject: [PATCH] test: speed up vcgen_get_throw_set.lean by partially
 evaluating specs (#12670)

This PR speeds up the vcgen_get_throw_set benchmark by a factor of 4 by
partially evaluating specs.
---
 .../bench/mvcgen/sym/vcgen_get_throw_set.lean | 36 ++++++++++++-------
 1 file changed, 23 insertions(+), 13 deletions(-)

diff --git a/tests/bench/mvcgen/sym/vcgen_get_throw_set.lean b/tests/bench/mvcgen/sym/vcgen_get_throw_set.lean
index 52ec487f65..d34958944f 100644
--- a/tests/bench/mvcgen/sym/vcgen_get_throw_set.lean
+++ b/tests/bench/mvcgen/sym/vcgen_get_throw_set.lean
@@ -9,18 +9,35 @@ import Driver
 
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
 
-@[spec]
-theorem Spec.monadLift_ExceptT [Monad m] [WPMonad m ps] {x : m α} :
-    ⦃wp⟦x⟧ (Q.1, Q.2.2)⦄ monadLift (n := ExceptT ε m) x ⦃Q⦄ := by
-  simp [Triple.iff, monadLift, MonadLift.monadLift, MonadLiftT.monadLift, ExceptT.lift, wp]
+set_option mvcgen.warning false
 
-def step (lim : Nat) : ExceptT String (StateM Nat) Unit := do
+abbrev M := ExceptT String <| StateM Nat
+
+-- We partially evaluate a couple of specs for best performance.
+-- If you comment those out, you will see a 4x slowdown.
+
+@[spec high]
+theorem Spec.throw_M {e : String} :
+    ⦃Q.2.1 e⦄ throw (m := M) e ⦃Q⦄ := by
+  mvcgen
+
+@[spec high]
+theorem Spec.set_M {s : Nat} :
+    ⦃fun _ => Q.1 ⟨⟩ s⦄ set (m := M) s ⦃Q⦄ := by
+  mvcgen
+
+@[spec high]
+theorem Spec.get_M :
+    ⦃fun s => Q.1 s s⦄ get (m := M) ⦃Q⦄ := by
+  mvcgen
+
+def step (lim : Nat) : M Unit := do
   let s ← get
   if s > lim then
     throw "s is too large"
   set (s + 1)
 
-def loop (n : Nat) : ExceptT String (StateM Nat) Unit := do
+def loop (n : Nat) : M Unit := do
   match n with
   | 0 => pure ()
   | n+1 => loop n; step n
@@ -30,13 +47,6 @@ def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = 0⌝⦄ loop n ⦃⇓_ s => ⌜s
 set_option maxRecDepth 10000
 set_option maxHeartbeats 10000000
 
-/-
-example : Goal 20 := by
-  simp only [Goal, loop, step]
-  mvcgen'
-  all_goals sorry
--/
-
 #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry)
   [100, 500, 1000]
   -- [1000]