422920f643
This PR adds an experimental tactic `mvcgen'` that will soon replace `mvcgen`. It has been reimplemented from the ground up using the new `SymM`-based framework for efficient symbolic evaluation and can outperform `mvcgen` by a factor of >100x for some synthetic benchmarks. `mvcgen'` aspires to be feature-complete with `mvcgen`. Known exceptions currently are join point sharing, introduction of local specs and smaller bugs. The implementation of `mvgen'` used to live in the benchmark suite for rapid prototyping; this commit merely moves it into the Lean toolchain. Doing so results in an build time instruction count increase in seemingly unrelated tests such as `elab/delayed_assign//instructions`; the reason is that the builtin elaborator attribute now pulls in substantially more import code on startup. --------- Co-authored-by: Sebastian Graf <sg@lean-fro.org>
18 lines
460 B
Text
18 lines
460 B
Text
/-
|
|
Copyright (c) 2026 Lean FRO LLC. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Sebastian Graf
|
|
-/
|
|
import Cases.MatchIota
|
|
import Driver
|
|
|
|
set_option mvcgen.warning false
|
|
|
|
open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
|
|
open MatchIota
|
|
|
|
set_option maxRecDepth 10000
|
|
set_option maxHeartbeats 10000000
|
|
|
|
#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry)
|
|
[50, 100, 150]
|