max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/compiler): ignore some tests for the interpreter

Browse source
This commit is contained in:
Sebastian Ullrich 2019-09-09 18:42:19 +02:00
parent 944de141d3
commit 3d53aaf5a7
3 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/shell/CMakeLists.txt
View file

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

1
tests/compiler/lazylist.lean.no_interpreter Normal file
View file

@ -0,0 +1 @@
[extern] cannot be interpreted

1
tests/compiler/map_big.lean.no_interpreter Normal file
View file

@ -0,0 +1 @@
Too much stack usage for the interpreter