From 20756c382cab7b978677568e20a984115a7614ea Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Mon, 18 Nov 2013 18:02:12 -0500
Subject: [PATCH] test(*): split leantests, leanslowtests, leanluatests,
 leanluadocs into singletons

---
 doc/lua/test_single.sh       | 18 ++++++++++++++++
 src/shell/CMakeLists.txt     | 24 ++++++++++++++++------
 src/shell/lua/CMakeLists.txt | 23 +++++++++++++++------
 tests/lean/test_single.sh    | 40 ++++++++++++++++++++++++++++++++++++
 tests/lua/test_single.sh     | 16 +++++++++++++++
 5 files changed, 109 insertions(+), 12 deletions(-)
 create mode 100755 doc/lua/test_single.sh
 create mode 100755 tests/lean/test_single.sh
 create mode 100755 tests/lua/test_single.sh

diff --git a/doc/lua/test_single.sh b/doc/lua/test_single.sh
new file mode 100755
index 000000000..aa0261e4e
--- /dev/null
+++ b/doc/lua/test_single.sh
@@ -0,0 +1,18 @@
+#!/bin/sh
+# Test is all examples in the .md files are working
+if [ $# -ne 2 ]; then
+    echo "Usage: test.sh [leanlua-executable-path] [file]"
+    exit 1
+fi
+ulimit -s unlimited
+LEANLUA=$1
+f=$2
+echo "-- testing $f"
+awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/{ in_block = 0; print "" } /```lua/{ in_block = 1; print "" }' $f > $f.lua
+if $LEANLUA $f.lua > $f.produced.out; then
+    echo "-- worked"
+    exit 0
+else
+    echo "ERROR executing $f.lua, produced output is at $f.produced.out"
+    exit 1
+fi
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 016a6b96a..c053b43dc 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -6,9 +6,21 @@ add_test(example1 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../exampl
 add_test(example2 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex2.lean")
 add_test(example3 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex3.lean")
 add_test(example1_stdin ${CMAKE_CURRENT_BINARY_DIR}/lean < "${LEAN_SOURCE_DIR}/../examples/lean/ex1.lean")
-add_test(NAME leantests
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
-         COMMAND "./test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
-add_test(NAME leanslowtests
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow"
-         COMMAND "../test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
+
+# LEANTESTS
+file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
+FOREACH(T ${LEANTESTS})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leantest_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
+           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
+ENDFOREACH(T)
+
+# LEANSLOWTESTS
+file(GLOB LEANSLOWTESTS "${LEAN_SOURCE_DIR}/../tests/lean/slow/*.lean")
+FOREACH(T ${LEANSLOWTESTS})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leanslowtest_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow"
+           COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
+ENDFOREACH(T)
diff --git a/src/shell/lua/CMakeLists.txt b/src/shell/lua/CMakeLists.txt
index a0e25680c..04b98649c 100644
--- a/src/shell/lua/CMakeLists.txt
+++ b/src/shell/lua/CMakeLists.txt
@@ -1,12 +1,23 @@
 add_executable(leanlua leanlua.cpp)
 target_link_libraries(leanlua ${EXTRA_LIBS})
-add_test(NAME leanluatests
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua"
-         COMMAND "./test.sh" "${CMAKE_CURRENT_BINARY_DIR}/leanlua")
 
-add_test(NAME leanluadocs
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lua"
-         COMMAND "./test.sh" "${CMAKE_CURRENT_BINARY_DIR}/leanlua")
+# LEANLUATESTS
+file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua")
+FOREACH(T ${LEANLUATESTS})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leanluatest_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua"
+           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/leanlua" ${T})
+ENDFOREACH(T)
+
+# LEANLUADOCS
+file(GLOB LEANLUADOCS "${LEAN_SOURCE_DIR}/../doc/lua/*.lua")
+FOREACH(T ${LEANLUADOCS})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leanluadoc_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lua"
+           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/leanlua" ${T})
+ENDFOREACH(T)
 
 if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux"))
   if (NOT (${CMAKE_CXX_COMPILER} MATCHES "clang"))
diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh
new file mode 100755
index 000000000..21b0fb4a5
--- /dev/null
+++ b/tests/lean/test_single.sh
@@ -0,0 +1,40 @@
+#!/bin/bash
+if [ $# -ne 3 -a $# -ne 2 ]; then
+    echo "Usage: test.sh [lean-executable-path] [file] [yes/no]?"
+    exit 1
+fi
+ulimit -s unlimited
+LEAN=$1
+if [ $# -ne 3 ]; then
+    INTERACTIVE=no
+else
+    INTERACTIVE=$3
+fi
+f=$2
+echo "-- testing $f"
+$LEAN config.lean $f > $f.produced.out
+if test -f $f.expected.out; then
+    if diff $f.produced.out $f.expected.out; then
+        echo "-- checked"
+        exit 0
+    else
+        echo "ERROR: file $f.produced.out does not match $f.expected.out"
+        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
+        exit 1
+    fi
+else
+    echo "ERROR: file $f.expected.out does not exist"
+    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
+    exit 1
+fi
diff --git a/tests/lua/test_single.sh b/tests/lua/test_single.sh
new file mode 100755
index 000000000..fe46e3ae7
--- /dev/null
+++ b/tests/lua/test_single.sh
@@ -0,0 +1,16 @@
+#!/bin/bash
+if [ $# -ne 2 ]; then
+    echo "Usage: test.sh [leanlua-executable-path] [file]"
+    exit 1
+fi
+ulimit -s unlimited
+LEANLUA=$1
+f=$2
+echo "-- testing $f"
+if $LEANLUA util.lua $f > $f.produced.out; then
+    echo "-- worked"
+    exit 0
+else
+    echo "ERROR executing $f, produced output is at $f.produced.out"
+    exit 1
+fi