chore(tests): use option -t 100000 to speedup tests

This commit is contained in:
Leonardo de Moura 2014-09-10 10:29:55 -07:00
parent 4a4de27a6c
commit e128610711

View file

@ -44,7 +44,7 @@ FOREACH(T ${LEANRUNTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME) GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leanruntest_${T_NAME}" add_test(NAME "leanruntest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run"
COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME})
ENDFOREACH(T) ENDFOREACH(T)
if("${MULTI_THREAD}" MATCHES "ON") if("${MULTI_THREAD}" MATCHES "ON")
@ -54,7 +54,7 @@ FOREACH(T ${LEANITTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME) GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leanittest_${T_NAME}" add_test(NAME "leanittest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive"
COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME})
ENDFOREACH(T) ENDFOREACH(T)
endif() endif()
@ -64,7 +64,7 @@ FOREACH(T ${LEANSLOWTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME) GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leanslowtest_${T_NAME}" add_test(NAME "leanslowtest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow"
COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME})
set_tests_properties("leanslowtest_${T_NAME}" PROPERTIES LABELS "expensive") set_tests_properties("leanslowtest_${T_NAME}" PROPERTIES LABELS "expensive")
ENDFOREACH(T) ENDFOREACH(T)