diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 8de5b593d..a0989816a 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -19,3 +19,6 @@ add_test(lean14 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples add_test(lean15 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex15.lean") add_test(lean16 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex16.lean") add_test(lean17 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex17.lean") +add_test(NAME leantests + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" + COMMAND "./test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") diff --git a/tests/lean/ex1.lean b/tests/lean/ex1.lean new file mode 100644 index 000000000..50b374521 --- /dev/null +++ b/tests/lean/ex1.lean @@ -0,0 +1 @@ +Echo "test" diff --git a/tests/lean/ex1.lean.expected.out b/tests/lean/ex1.lean.expected.out new file mode 100644 index 000000000..9daeafb98 --- /dev/null +++ b/tests/lean/ex1.lean.expected.out @@ -0,0 +1 @@ +test diff --git a/tests/lean/test.sh b/tests/lean/test.sh new file mode 100755 index 000000000..55bdc0790 --- /dev/null +++ b/tests/lean/test.sh @@ -0,0 +1,47 @@ +#!/bin/bash +if [ $# -ne 2 -a $# -ne 1 ]; then + echo "Usage: test.sh [lean-executable-path] [yes/no]?" + exit 1 +fi +LEAN=$1 +if [ $# -ne 2 ]; then + INTERACTIVE=no +else + INTERACTIVE=$2 +fi +NUM_ERRORS=0 +for f in `ls *.lean`; do + echo $f + $LEAN $f > $f.produced.out + if test -f $f.expected.out; then + if diff $f.produced.out $f.expected.out; then + echo "-- $f checked" + else + echo "ERROR: file $f.produced.out does not match $f.expected.out" + NUM_ERRORS=$(($NUM_ERRORS+1)) + if [ $INTERACTIVE == "yes" ]; then + meld $f.produced.out $f.expected.out + if diff $f.produced.out $f.expected.out; then + echo "-- mismath was fixed" + fi + fi + fi + else + echo "ERROR: file $f.expected.out does not exist" + NUM_ERRORS=$(($NUM_ERRORS+1)) + if [ $INTERACTIVE == "yes" ]; then + read -p "copy $f.produced.out (y/n)? " + if [ $REPLY == "y" ]; then + cp $f.produced.out $f.expected.out + echo "-- copied $f.produced.out --> $f.expected.out" + fi + fi + fi +done +if [ $NUM_ERRORS -gt 0 ]; then + echo "-- Number of errors: $NUM_ERRORS" + exit 1 +else + echo "-- Passed" + exit 0 +fi