From 94b3de0130925fb4c3dcab892203789d24889d5e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 29 Aug 2019 18:38:39 +0200
Subject: [PATCH] chore(tests/bench): parameterize all benchmarks

---
 tests/bench/Makefile              |  4 ++++
 tests/bench/const_fold.lean       | 15 +++++++++------
 tests/bench/deriv.lean            | 13 ++++++++-----
 tests/bench/speedcenter.exec.yaml |  4 ++--
 4 files changed, 23 insertions(+), 13 deletions(-)

diff --git a/tests/bench/Makefile b/tests/bench/Makefile
index 1f6535f0f4..8fb84e623c 100644
--- a/tests/bench/Makefile
+++ b/tests/bench/Makefile
@@ -103,6 +103,10 @@ bench/frontend.%.bench: BENCH_PARAMS = --new-frontend frontend_test.lean
 
 bench/binarytrees.%.bench: BENCH_PARAMS = 21
 
+bench/deriv.%.bench: BENCH_PARAMS = 10
+
+bench/const_fold.%.bench: BENCH_PARAMS = 23
+
 bench/qsort.%.bench: BENCH_PARAMS = 400
 
 bench/rbmap.%.bench: BENCH_PARAMS = 2000000
diff --git a/tests/bench/const_fold.lean b/tests/bench/const_fold.lean
index acd06b6599..e52f037a04 100644
--- a/tests/bench/const_fold.lean
+++ b/tests/bench/const_fold.lean
@@ -65,9 +65,12 @@ def eval : Expr → Nat
 | Add l r   => eval l + eval r
 | Mul l r   => eval l * eval r
 
-def main : IO UInt32 :=
-let e  := (mkExpr 23 1);
-let v₁ := eval e;
-let v₂ := eval (constFolding (reassoc e));
-IO.println (toString v₁ ++ " " ++ toString v₂) *>
-pure 0
+unsafe def main : List String → IO UInt32
+| [s] => do
+  let n := s.toNat;
+  let e  := (mkExpr n 1);
+  let v₁ := eval e;
+  let v₂ := eval (constFolding (reassoc e));
+  IO.println (toString v₁ ++ " " ++ toString v₂);
+  pure 0
+| _ => pure 1
diff --git a/tests/bench/deriv.lean b/tests/bench/deriv.lean
index ad5877b348..e8a2bc6e01 100644
--- a/tests/bench/deriv.lean
+++ b/tests/bench/deriv.lean
@@ -89,8 +89,11 @@ do
   IO.println (toString (i+1) ++ " count: " ++ (toString $ count d));
   pure d
 
-def main (xs : List String) : IO UInt32 :=
-do let x := Var "x";
-   let f := pow x x;
-   nest deriv 10 f;
-   pure 0
+unsafe def main : List String → IO UInt32
+| [s] => do
+  let n := s.toNat;
+  let x := Var "x";
+  let f := pow x x;
+  nest deriv n f;
+  pure 0
+| _ => pure 1
diff --git a/tests/bench/speedcenter.exec.yaml b/tests/bench/speedcenter.exec.yaml
index cc237512e6..3621fa3be1 100644
--- a/tests/bench/speedcenter.exec.yaml
+++ b/tests/bench/speedcenter.exec.yaml
@@ -48,13 +48,13 @@
     <<: *time
     cmd: ./deriv.lean.out
   build_config:
-    cmd: ./compile.sh deriv.lean
+    cmd: ./compile.sh deriv.lean 10
 - attributes:
     description: const_fold
     tags: [fast, suite]
   run_config:
     <<: *time
-    cmd: bash -c "ulimit -s unlimited && ./const_fold.lean.out"
+    cmd: bash -c "ulimit -s unlimited && ./const_fold.lean.out 23"
   build_config:
     cmd: ./compile.sh const_fold.lean
 - attributes: