test(tests/bench): add benchmarks as regular ctests with lowered inputs

src/shell/CMakeLists.txt

@@ -176,6 +176,17 @@ FOREACH(T ${LEANCOMPTESTS})
            COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
 ENDFOREACH(T)
 
+# LEAN BENCHMARK TESTS
+# do not test all .lean files in bench/
+file(GLOB LEANBENCHTESTS "${LEAN_SOURCE_DIR}/../tests/bench/*.lean.expected.out")
+FOREACH(T_OUT ${LEANBENCHTESTS})
+  string(REPLACE ".expected.out" "" T ${T_OUT})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leanbenchtest_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench"
+           COMMAND bash "./test_single.sh" ${T_NAME})
+ENDFOREACH(T_OUT)
+
 # LEANPKG TESTS
 # file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/lean/leanpkg/*.sh")
 # FOREACH(T ${LEANPKGTESTS})

tests/bench/binarytrees.lean.args

@@ -0,0 +1 @@
+18

tests/bench/binarytrees.lean.expected.out

@@ -0,0 +1,10 @@
+stretch tree of depth 19	 check: 1048575
+262144	 trees of depth 4	 check: 8126464
+65536	 trees of depth 6	 check: 8323072
+16384	 trees of depth 8	 check: 8372224
+4096	 trees of depth 10	 check: 8384512
+1024	 trees of depth 12	 check: 8387584
+256	 trees of depth 14	 check: 8388352
+64	 trees of depth 16	 check: 8388544
+16	 trees of depth 18	 check: 8388592
+long lived tree of depth 18	 check: 524287

tests/bench/const_fold.lean.args

@@ -0,0 +1 @@
+15

tests/bench/const_fold.lean.expected.out

@@ -0,0 +1 @@
+93011 93011

tests/bench/deriv.lean.args

@@ -0,0 +1 @@
+8

tests/bench/deriv.lean.expected.out

@@ -0,0 +1,8 @@
+1 count: 6
+2 count: 22
+3 count: 90
+4 count: 420
+5 count: 2202
+6 count: 12886
+7 count: 83648
+8 count: 598592

tests/bench/qsort.lean.args

@@ -0,0 +1 @@
+200

tests/bench/rbmap.lean.args

@@ -0,0 +1 @@
+1000000

tests/bench/rbmap.lean.expected.out

@@ -0,0 +1 @@
+100000

tests/bench/rbmap_checkpoint.lean.args

@@ -0,0 +1 @@
+1000000 10

tests/bench/rbmap_checkpoint.lean.expected.out

@@ -0,0 +1 @@
+100001 100000

tests/bench/test_single.sh

@@ -0,0 +1,52 @@
+#!/usr/bin/env bash
+if [ $# -ne 2 -a $# -ne 1 ]; then
+    echo "Usage: test_single.sh [file] [yes/no]?"
+    exit 1
+fi
+ulimit -s 8192
+if [ $# -ne 3 ]; then
+    INTERACTIVE=no
+else
+    INTERACTIVE=$2
+fi
+ff="$1"
+
+DIFF=diff
+if diff --color --help >/dev/null 2>&1; then
+  DIFF="diff --color";
+fi
+
+./compile.sh "$ff" || exit 1
+
+[ -f "$ff.args" ] && args=$(cat "$ff.args")
+"./$ff.out" $args > "$ff.produced.out"
+if [ $? -ne 0 ]; then
+   echo "Failed to execute $ff.out"
+   exit 1
+fi
+
+if test -f "$ff.expected.out"; then
+    if $DIFF -u --ignore-all-space -I "executing external script" "$ff.expected.out" "$ff.produced.out"; then
+        echo "-- checked"
+        exit 0
+    else
+        echo "ERROR: file $ff.produced.out does not match $ff.expected.out"
+        if [ $INTERACTIVE == "yes" ]; then
+            meld "$ff.produced.out" "$ff.expected.out"
+            if diff -I "executing external script" "$ff.expected.out" "$ff.produced.out"; then
+                echo "-- mismatch was fixed"
+            fi
+        fi
+        exit 1
+    fi
+else
+    echo "ERROR: file $ff.expected.out does not exist"
+    if [ $INTERACTIVE == "yes" ]; then
+        read -p "copy $ff.produced.out (y/n)? "
+        if [ $REPLY == "y" ]; then
+            cp -- "$ff.produced.out" "$ff.expected.out"
+            echo "-- copied $ff.produced.out --> $ff.expected.out"
+        fi
+    fi
+    exit 1
+fi

tests/bench/unionfind.lean.args

@@ -0,0 +1 @@
+300000

tests/bench/unionfind.lean.expected.out

@@ -0,0 +1 @@
+ok 299000