From cffbae36678404cbd8ddf64841433ed52540feee Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 11 Jun 2014 21:07:08 -0700
Subject: [PATCH] test(tests/lean/run): add new test group, where we just
 execute Lean (and don't check output)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/shell/CMakeLists.txt | 11 ++++++++++-
 tests/lean/run/t1.lean   |  8 ++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/t1.lean

diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 4e6229019..f3d637096 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -19,7 +19,7 @@ add_test(lean_luahook2 ${CMAKE_CURRENT_BINARY_DIR}/lean -c 100 "${LEAN_SOURCE_DI
 # add_test(lean_lua1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "--lua" "${LEAN_SOURCE_DIR}/../tests/lua/single.lua")
 # add_test(lean_lua2 ${LEAN_SOURCE_DIR}/cmake/redirect.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "-u" "${LEAN_SOURCE_DIR}/../tests/lua/single.lua")
 add_test(lean_unknown_option ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z")
-# add_test(lean_unknown_file1 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
+add_test(lean_unknown_file1 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
 add_test(lean_unknown_file2 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lua")
 
 # # LEAN EXAMPLES
@@ -39,6 +39,15 @@ FOREACH(T ${LEANTESTS})
            COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME})
 ENDFOREACH(T)
 
+# LEAN RUN TESTS
+file(GLOB LEANRUNTESTS "${LEAN_SOURCE_DIR}/../tests/lean/run/*.lean")
+FOREACH(T ${LEANRUNTESTS})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leanruntest_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run"
+           COMMAND "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
+ENDFOREACH(T)
+
 # # LEAN INTERACTIVE TESTS
 # file(GLOB LEANINTERACTIVETESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.lean")
 # FOREACH(T ${LEANINTERACTIVETESTS})
diff --git a/tests/lean/run/t1.lean b/tests/lean/run/t1.lean
new file mode 100644
index 000000000..20e897007
--- /dev/null
+++ b/tests/lean/run/t1.lean
@@ -0,0 +1,8 @@
+print raw ((Bool))
+print raw Bool
+print raw fun (x y : Bool), x x
+print raw fun (x y : Bool) {z : Bool}, x y
+print raw λ [x y : Bool] {z : Bool}, x z
+print raw Pi (x y : Bool) {z : Bool}, x
+print raw ∀ (x y : Bool) {z : Bool}, x
+print raw forall {x y : Bool} w {z : Bool}, x