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>
30 lines
770 B
Text
30 lines
770 B
Text
import Lake
|
|
open System Lake DSL
|
|
|
|
package mvcgen_bench where
|
|
precompileModules := true
|
|
|
|
lean_lib Baseline where
|
|
srcDir := "lib"
|
|
|
|
lean_lib Driver where
|
|
srcDir := "lib"
|
|
|
|
lean_lib Cases where
|
|
srcDir := "cases"
|
|
|
|
@[default_target]
|
|
lean_lib VCGenBench where
|
|
roots := #[`vcgen_add_sub_cancel, `vcgen_add_sub_cancel_deep, `vcgen_add_sub_cancel_simp,
|
|
`vcgen_get_throw_set, `vcgen_get_throw_set_grind, `vcgen_pure_precond,
|
|
`vcgen_reader_state, `vcgen_match_split]
|
|
moreLeanArgs := #["--tstack=102400"] -- 100 MB in KB
|
|
|
|
@[default_target]
|
|
lean_lib BaselineBench where
|
|
roots := #[`baseline_add_sub_cancel]
|
|
moreLeanArgs := #["--tstack=102400"] -- 100 MB in KB
|
|
|
|
@[test_driver]
|
|
lean_lib VCGenTest where
|
|
roots := #[`test_vcgen, `test_do_logic]
|