From 7b7f1d2cac8f6a42a11cc448c65ade9e25bd0aec Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 29 Aug 2019 18:39:47 +0200 Subject: [PATCH] test(tests/bench): add benchmarks as regular ctests with lowered inputs --- src/shell/CMakeLists.txt | 11 ++++ tests/bench/binarytrees.lean.args | 1 + tests/bench/binarytrees.lean.expected.out | 10 ++++ tests/bench/const_fold.lean.args | 1 + tests/bench/const_fold.lean.expected.out | 1 + tests/bench/deriv.lean.args | 1 + tests/bench/deriv.lean.expected.out | 8 +++ tests/bench/qsort.lean.args | 1 + tests/bench/qsort.lean.expected.out | 0 tests/bench/rbmap.lean.args | 1 + tests/bench/rbmap.lean.expected.out | 1 + tests/bench/rbmap_checkpoint.lean.args | 1 + .../bench/rbmap_checkpoint.lean.expected.out | 1 + tests/bench/test_single.sh | 52 +++++++++++++++++++ tests/bench/unionfind.lean.args | 1 + tests/bench/unionfind.lean.expected.out | 1 + .../{rbmap.lean => rbmap_library.lean} | 0 ...ed.out => rbmap_library.lean.expected.out} | 0 18 files changed, 92 insertions(+) create mode 100644 tests/bench/binarytrees.lean.args create mode 100644 tests/bench/binarytrees.lean.expected.out create mode 100644 tests/bench/const_fold.lean.args create mode 100644 tests/bench/const_fold.lean.expected.out create mode 100644 tests/bench/deriv.lean.args create mode 100644 tests/bench/deriv.lean.expected.out create mode 100644 tests/bench/qsort.lean.args create mode 100644 tests/bench/qsort.lean.expected.out create mode 100644 tests/bench/rbmap.lean.args create mode 100644 tests/bench/rbmap.lean.expected.out create mode 100644 tests/bench/rbmap_checkpoint.lean.args create mode 100644 tests/bench/rbmap_checkpoint.lean.expected.out create mode 100755 tests/bench/test_single.sh create mode 100644 tests/bench/unionfind.lean.args create mode 100644 tests/bench/unionfind.lean.expected.out rename tests/compiler/{rbmap.lean => rbmap_library.lean} (100%) rename tests/compiler/{rbmap.lean.expected.out => rbmap_library.lean.expected.out} (100%) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 095bfa8776..275af38518 100644 --- a/src/shell/CMakeLists.txt +++ b/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}) diff --git a/tests/bench/binarytrees.lean.args b/tests/bench/binarytrees.lean.args new file mode 100644 index 0000000000..3c032078a4 --- /dev/null +++ b/tests/bench/binarytrees.lean.args @@ -0,0 +1 @@ +18 diff --git a/tests/bench/binarytrees.lean.expected.out b/tests/bench/binarytrees.lean.expected.out new file mode 100644 index 0000000000..cc400c0b43 --- /dev/null +++ b/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 diff --git a/tests/bench/const_fold.lean.args b/tests/bench/const_fold.lean.args new file mode 100644 index 0000000000..60d3b2f4a4 --- /dev/null +++ b/tests/bench/const_fold.lean.args @@ -0,0 +1 @@ +15 diff --git a/tests/bench/const_fold.lean.expected.out b/tests/bench/const_fold.lean.expected.out new file mode 100644 index 0000000000..2e7aaa7167 --- /dev/null +++ b/tests/bench/const_fold.lean.expected.out @@ -0,0 +1 @@ +93011 93011 diff --git a/tests/bench/deriv.lean.args b/tests/bench/deriv.lean.args new file mode 100644 index 0000000000..45a4fb75db --- /dev/null +++ b/tests/bench/deriv.lean.args @@ -0,0 +1 @@ +8 diff --git a/tests/bench/deriv.lean.expected.out b/tests/bench/deriv.lean.expected.out new file mode 100644 index 0000000000..3896003e22 --- /dev/null +++ b/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 diff --git a/tests/bench/qsort.lean.args b/tests/bench/qsort.lean.args new file mode 100644 index 0000000000..08839f6bb2 --- /dev/null +++ b/tests/bench/qsort.lean.args @@ -0,0 +1 @@ +200 diff --git a/tests/bench/qsort.lean.expected.out b/tests/bench/qsort.lean.expected.out new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/bench/rbmap.lean.args b/tests/bench/rbmap.lean.args new file mode 100644 index 0000000000..749fce669d --- /dev/null +++ b/tests/bench/rbmap.lean.args @@ -0,0 +1 @@ +1000000 diff --git a/tests/bench/rbmap.lean.expected.out b/tests/bench/rbmap.lean.expected.out new file mode 100644 index 0000000000..f7393e847d --- /dev/null +++ b/tests/bench/rbmap.lean.expected.out @@ -0,0 +1 @@ +100000 diff --git a/tests/bench/rbmap_checkpoint.lean.args b/tests/bench/rbmap_checkpoint.lean.args new file mode 100644 index 0000000000..e30f862951 --- /dev/null +++ b/tests/bench/rbmap_checkpoint.lean.args @@ -0,0 +1 @@ +1000000 10 diff --git a/tests/bench/rbmap_checkpoint.lean.expected.out b/tests/bench/rbmap_checkpoint.lean.expected.out new file mode 100644 index 0000000000..b0fe0193b9 --- /dev/null +++ b/tests/bench/rbmap_checkpoint.lean.expected.out @@ -0,0 +1 @@ +100001 100000 diff --git a/tests/bench/test_single.sh b/tests/bench/test_single.sh new file mode 100755 index 0000000000..fa6f0890b9 --- /dev/null +++ b/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 diff --git a/tests/bench/unionfind.lean.args b/tests/bench/unionfind.lean.args new file mode 100644 index 0000000000..67f9d55822 --- /dev/null +++ b/tests/bench/unionfind.lean.args @@ -0,0 +1 @@ +300000 diff --git a/tests/bench/unionfind.lean.expected.out b/tests/bench/unionfind.lean.expected.out new file mode 100644 index 0000000000..47cfc531b3 --- /dev/null +++ b/tests/bench/unionfind.lean.expected.out @@ -0,0 +1 @@ +ok 299000 diff --git a/tests/compiler/rbmap.lean b/tests/compiler/rbmap_library.lean similarity index 100% rename from tests/compiler/rbmap.lean rename to tests/compiler/rbmap_library.lean diff --git a/tests/compiler/rbmap.lean.expected.out b/tests/compiler/rbmap_library.lean.expected.out similarity index 100% rename from tests/compiler/rbmap.lean.expected.out rename to tests/compiler/rbmap_library.lean.expected.out