michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(shell): re-activate .lean tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-11 13:56:11 -07:00
parent 1c5d3295cc
commit 05edbe00ad
2 changed files with 8 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/shell/CMakeLists.txt
View file

@ -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")

0
tests/lean/config.lean.expected.out Normal file
View file