test: add two benchmarks for mvcgen in the style of SymM (#12163)
This PR adds two benchmarks for mvcgen in the style of Leo's SymM benchmarks. While performance on add_sub_cancel_StateM.lean is in the same order of magnitude as the corresponding MetaM benchmark, add_if_sub_StateM.lean is far slower. Measurements for add_sub_cancel: ``` goal_10: 245.576221 ms, kernel: 134.134182 ms goal_20: 613.945320 ms, kernel: 115.453811 ms goal_30: 1074.053596 ms, kernel: 179.076070 ms goal_40: 1680.678302 ms, kernel: 252.066677 ms goal_50: 2457.209584 ms, kernel: 293.974096 ms goal_60: 3271.773330 ms, kernel: 368.394386 ms goal_70: 3981.247921 ms, kernel: 434.297822 ms goal_80: 5077.300540 ms, kernel: 507.047772 ms goal_90: 6486.990060 ms, kernel: 556.952095 ms goal_100: 7791.399986 ms, kernel: 623.605163 ms ``` Measurements for add_if_sub: ``` goal_2: 89.762349 ms, kernel: 43.320205 ms goal_3: 190.655546 ms, kernel: 38.888499 ms goal_4: 434.461936 ms, kernel: 75.234581 ms goal_5: 1110.295284 ms, kernel: 161.698707 ms goal_6: 3241.383031 ms, kernel: 326.137173 ms goal_7: 11675.609970 ms, kernel: 684.907188 ms ``` Much room for improvement.
This commit is contained in:
Sebastian Graf
GitHub
parent
0bcac0d46c
commit
b44c7e161c
2 changed files with 181 additions and 0 deletions
82
tests/bench/mvcgen/add_if_sub_StateM.lean
Normal file
82
tests/bench/mvcgen/add_if_sub_StateM.lean
Normal file
|
|
@ -0,0 +1,82 @@
|
|||
import Lean
|
||||
import Std.Tactic.Do
|
||||
|
||||
open Std.Do
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
/-!
|
||||
Same benchmark as `shallow_add_sub_cancel` but using `mvcgen`.
|
||||
-/
|
||||
|
||||
def step (v : Nat) : StateM Nat Unit := do
|
||||
let s ← get
|
||||
set (v + s)
|
||||
let s' ← get
|
||||
if s' = s then
|
||||
set (s' - v)
|
||||
|
||||
def loop (n : Nat) : StateM Nat Unit := do
|
||||
match n with
|
||||
| 0 => pure ()
|
||||
| n+1 => step n; loop n
|
||||
|
||||
def Goal (n : Nat) : Prop := ∀ s₁, ⦃fun s => ⌜s = s₁⌝⦄ loop n ⦃⇓_ s₂ => ⌜s₂ > s₁⌝⦄
|
||||
|
||||
open Lean Meta Elab
|
||||
|
||||
/-- Helper function for executing a tactic `k` for solving `Goal n`. -/
|
||||
def driver (n : Nat) (check := true) (k : MVarId → MetaM Unit) : MetaM Unit := do
|
||||
let some goal ← unfoldDefinition? (mkApp (mkConst ``Goal) (mkNatLit n)) | throwError "UNFOLD FAILED!"
|
||||
let mvar ← mkFreshExprMVar goal
|
||||
let startTime ← IO.monoNanosNow
|
||||
k mvar.mvarId!
|
||||
let endTime ← IO.monoNanosNow
|
||||
let ms := (endTime - startTime).toFloat / 1000000.0
|
||||
if check then
|
||||
let startTime ← IO.monoNanosNow
|
||||
checkWithKernel (← instantiateExprMVars mvar)
|
||||
let endTime ← IO.monoNanosNow
|
||||
let kernelMs := (endTime - startTime).toFloat / 1000000.0
|
||||
IO.println s!"goal_{n}: {ms} ms, kernel: {kernelMs} ms"
|
||||
else
|
||||
IO.println s!"goal_{n}: {ms} ms"
|
||||
|
||||
/-!
|
||||
`MetaM` Solution
|
||||
-/
|
||||
|
||||
/-
|
||||
A tactic for solving goal `Goal n`
|
||||
-/
|
||||
macro "solve" : tactic => `(tactic| {
|
||||
intro s₁
|
||||
mvcgen -trivial [loop, step]
|
||||
with grind
|
||||
})
|
||||
|
||||
/--
|
||||
Solves a goal of the form `Goal n` using the `solve` tactic.
|
||||
-/
|
||||
def solveUsingMeta (n : Nat) (check := true) : MetaM Unit := do
|
||||
driver n check fun mvarId => do
|
||||
let ([], _) ← runTactic mvarId (← `(tactic| solve)).raw {} {} | throwError "FAILED!"
|
||||
|
||||
def runBenchUsingMeta : MetaM Unit := do
|
||||
IO.println "=== Symbolic Simulation Tests ==="
|
||||
IO.println ""
|
||||
for n in [2:6] do
|
||||
solveUsingMeta n
|
||||
|
||||
set_option maxRecDepth 10000
|
||||
set_option maxHeartbeats 10000000
|
||||
/--
|
||||
info: === Symbolic Simulation Tests ===
|
||||
|
||||
goal_2: 99.023526 ms, kernel: 20.580785 ms
|
||||
goal_3: 188.955486 ms, kernel: 37.464098 ms
|
||||
goal_4: 436.369632 ms, kernel: 74.872961 ms
|
||||
goal_5: 1071.272357 ms, kernel: 148.864428 ms
|
||||
-/
|
||||
#guard_msgs in
|
||||
#eval runBenchUsingMeta
|
||||
99
tests/bench/mvcgen/add_sub_cancel_StateM.lean
Normal file
99
tests/bench/mvcgen/add_sub_cancel_StateM.lean
Normal file
|
|
@ -0,0 +1,99 @@
|
|||
import Lean
|
||||
import Std.Tactic.Do
|
||||
|
||||
open Std.Do
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
/-!
|
||||
Same benchmark as `shallow_add_sub_cancel` but using `mvcgen`.
|
||||
-/
|
||||
|
||||
def step (v : Nat) : StateM Nat Unit := do
|
||||
let s ← get
|
||||
set (s + v)
|
||||
let s ← get
|
||||
set (s - v)
|
||||
|
||||
def loop (n : Nat) : StateM Nat Unit := do
|
||||
match n with
|
||||
| 0 => pure ()
|
||||
| n+1 => step n; loop n
|
||||
|
||||
def Goal (n : Nat) : Prop := ∀ post, ⦃post⦄ loop n ⦃⇓_ => post⦄
|
||||
|
||||
open Lean Meta Elab
|
||||
|
||||
/-- Helper function for executing a tactic `k` for solving `Goal n`. -/
|
||||
def driver (n : Nat) (check := true) (k : MVarId → MetaM Unit) : MetaM Unit := do
|
||||
let some goal ← unfoldDefinition? (mkApp (mkConst ``Goal) (mkNatLit n)) | throwError "UNFOLD FAILED!"
|
||||
let mvar ← mkFreshExprMVar goal
|
||||
let startTime ← IO.monoNanosNow
|
||||
k mvar.mvarId!
|
||||
let endTime ← IO.monoNanosNow
|
||||
let ms := (endTime - startTime).toFloat / 1000000.0
|
||||
if check then
|
||||
let startTime ← IO.monoNanosNow
|
||||
checkWithKernel (← instantiateExprMVars mvar)
|
||||
let endTime ← IO.monoNanosNow
|
||||
let kernelMs := (endTime - startTime).toFloat / 1000000.0
|
||||
IO.println s!"goal_{n}: {ms} ms, kernel: {kernelMs} ms"
|
||||
else
|
||||
IO.println s!"goal_{n}: {ms} ms"
|
||||
|
||||
/-!
|
||||
`MetaM` Solution
|
||||
-/
|
||||
|
||||
/-
|
||||
A tactic for solving goal `Goal n`
|
||||
-/
|
||||
macro "solve" : tactic => `(tactic| {
|
||||
intro post
|
||||
mvcgen -trivial [loop, step]
|
||||
with grind
|
||||
})
|
||||
|
||||
/--
|
||||
Solves a goal of the form `Goal n` using the `solve` tactic.
|
||||
-/
|
||||
def solveUsingMeta (n : Nat) (check := true) : MetaM Unit := do
|
||||
driver n check fun mvarId => do
|
||||
let ([], _) ← runTactic mvarId (← `(tactic| solve)).raw {} {} | throwError "FAILED!"
|
||||
|
||||
def runBenchUsingMeta (sizes : List Nat) : MetaM Unit := do
|
||||
IO.println "=== Symbolic Simulation Tests ==="
|
||||
IO.println ""
|
||||
for n in sizes do
|
||||
solveUsingMeta n
|
||||
|
||||
set_option maxRecDepth 10000
|
||||
set_option maxHeartbeats 10000000
|
||||
/-
|
||||
info: === Symbolic Simulation Tests ===
|
||||
|
||||
goal_10: 245.576221 ms, kernel: 134.134182 ms
|
||||
goal_20: 613.945320 ms, kernel: 115.453811 ms
|
||||
goal_30: 1074.053596 ms, kernel: 179.076070 ms
|
||||
goal_40: 1680.678302 ms, kernel: 252.066677 ms
|
||||
goal_50: 2457.209584 ms, kernel: 293.974096 ms
|
||||
goal_60: 3271.773330 ms, kernel: 368.394386 ms
|
||||
goal_70: 3981.247921 ms, kernel: 434.297822 ms
|
||||
goal_80: 5077.300540 ms, kernel: 507.047772 ms
|
||||
goal_90: 6486.990060 ms, kernel: 556.952095 ms
|
||||
goal_100: 7791.399986 ms, kernel: 623.605163 ms
|
||||
-/
|
||||
#guard_msgs in
|
||||
#eval runBenchUsingMeta [10, 20, 30, 40, 50, 60, 70, 80, 90, 100]
|
||||
|
||||
/-
|
||||
#eval runBenchUsingMeta [30]
|
||||
|
||||
example : Goal 10 := by
|
||||
intro post
|
||||
set_option trace.Elab.Tactic.Do.spec true in
|
||||
mvcgen -trivial [loop, step]
|
||||
|
||||
simp [*]
|
||||
-- with grind
|
||||
-/
|
||||
Loading…
Add table
Reference in a new issue