From a99c44b644f0afb1650ef647d41e9ae1f2327686 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Jul 2015 08:08:03 -0700 Subject: [PATCH] fix(CMakeLists.txt): disable problematic tests on Windows Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 2 ++ src/shell/CMakeLists.txt | 10 +++++++--- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e0a2e990e..6db4e2242 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -352,6 +352,7 @@ add_subdirectory(tests/frontends/lean) add_subdirectory(tests/shell) # Include style check +if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows")) include(StyleCheck) file(GLOB_RECURSE LEAN_SOURCES "${LEAN_SOURCE_DIR}" @@ -359,6 +360,7 @@ file(GLOB_RECURSE LEAN_SOURCES "${LEAN_SOURCE_DIR}/[A-Za-z]*.h") add_style_check_target(style "${LEAN_SOURCES}") add_test(NAME style_check COMMAND "${PYTHON_EXECUTABLE}" "${LEAN_SOURCE_DIR}/cmake/Modules/cpplint.py" ${LEAN_SOURCES}) +endif() # Set PROCESSOR_COUNT if(NOT DEFINED PROCESSOR_COUNT) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 62eb1b05d..49ba6c99a 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -52,9 +52,13 @@ add_test(NAME "issue_597" add_test(NAME "issue_616" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" COMMAND bash "./issue_616.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") -add_test(NAME "normalizer_perf" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" - COMMAND bash "./timeout.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "1" "slow1.lean") +if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows")) + # The following test cannot be executed on Windows because of the + # bash script timeout.sh + add_test(NAME "normalizer_perf" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" + COMMAND bash "./timeout.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "1" "slow1.lean") +endif() # LEAN TESTS file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")