From 05edbe00ad15cf88f045459a606154fde962bdf1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Jun 2014 13:56:11 -0700 Subject: [PATCH] chore(shell): re-activate .lean tests Signed-off-by: Leonardo de Moura --- src/shell/CMakeLists.txt | 26 ++++++++------------------ tests/lean/config.lean.expected.out | 0 2 files changed, 8 insertions(+), 18 deletions(-) create mode 100644 tests/lean/config.lean.expected.out diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 9109dca9c..4e6229019 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -30,24 +30,14 @@ add_test(lean_unknown_file2 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_C # COMMAND ${CMAKE_CURRENT_BINARY_DIR}/lean ${T}) # ENDFOREACH(T) -# # LEAN TESTS -# 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" ${T_NAME}) -# ENDFOREACH(T) - -# # LEAN PP TESTS -# # For making sure that Lean can parse the output produced by its pretty printer -# file(GLOB LEANPPTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") -# FOREACH(T ${LEANPPTESTS}) -# GET_FILENAME_COMPONENT(T_NAME ${T} NAME) -# add_test(NAME "leanpptest_${T_NAME}" -# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" -# COMMAND "./test_single_pp.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T}) -# ENDFOREACH(T) +# LEAN TESTS +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 100000" ${T_NAME}) +ENDFOREACH(T) # # LEAN INTERACTIVE TESTS # file(GLOB LEANINTERACTIVETESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.lean") diff --git a/tests/lean/config.lean.expected.out b/tests/lean/config.lean.expected.out new file mode 100644 index 000000000..e69de29bb