From 3d53aaf5a77e402374909c320c45d1dbde8e8830 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 9 Sep 2019 18:42:19 +0200 Subject: [PATCH] chore(tests/compiler): ignore some tests for the interpreter --- src/shell/CMakeLists.txt | 10 ++++++---- tests/compiler/lazylist.lean.no_interpreter | 1 + tests/compiler/map_big.lean.no_interpreter | 1 + 3 files changed, 8 insertions(+), 4 deletions(-) create mode 100644 tests/compiler/lazylist.lean.no_interpreter create mode 100644 tests/compiler/map_big.lean.no_interpreter diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index c398805692..9fdd6ee293 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -179,10 +179,12 @@ ENDFOREACH(T) # LEAN INTERPRETER TESTS file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean") FOREACH(T ${LEANINTERPTESTS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leaninterptest_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler" - COMMAND bash "./test_single_interpret.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) + if(NOT EXISTS "${T}.no_interpreter") + GET_FILENAME_COMPONENT(T_NAME ${T} NAME) + add_test(NAME "leaninterptest_${T_NAME}" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler" + COMMAND bash "./test_single_interpret.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) + endif() ENDFOREACH(T) # LEAN BENCHMARK TESTS diff --git a/tests/compiler/lazylist.lean.no_interpreter b/tests/compiler/lazylist.lean.no_interpreter new file mode 100644 index 0000000000..c826867c8f --- /dev/null +++ b/tests/compiler/lazylist.lean.no_interpreter @@ -0,0 +1 @@ +[extern] cannot be interpreted \ No newline at end of file diff --git a/tests/compiler/map_big.lean.no_interpreter b/tests/compiler/map_big.lean.no_interpreter new file mode 100644 index 0000000000..1476ad79bd --- /dev/null +++ b/tests/compiler/map_big.lean.no_interpreter @@ -0,0 +1 @@ +Too much stack usage for the interpreter \ No newline at end of file