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

chore: disable some tests on Windows (#3642)

Browse source 
This is a temporary workaround for a limitation on Windows shared
libraries. We are getting errors of the form:
```
ld.lld: error: too many exported symbols (got 65572, max 65535)
```
This commit is contained in:
Leonardo de Moura 2024-03-09 15:48:41 -08:00 • committed by GitHub
parent 45fccc5906
commit 1d3ef577c2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 25 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/shell/CMakeLists.txt
View file

@ -119,14 +119,18 @@ ENDFOREACH(T)
# LEAN BENCHMARK TESTS
# do not test all .lean files in bench/
file(GLOB LEANBENCHTESTS "${LEAN_SOURCE_DIR}/../tests/bench/*.lean.expected.out")
FOREACH(T_OUT ${LEANBENCHTESTS})
string(REPLACE ".expected.out" "" T ${T_OUT})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leanbenchtest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
ENDFOREACH(T_OUT)
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
message(STATUS "Skipping compiler tests on Windows because of shared library limit on number of exported symbols")
else()
file(GLOB LEANBENCHTESTS "${LEAN_SOURCE_DIR}/../tests/bench/*.lean.expected.out")
FOREACH(T_OUT ${LEANBENCHTESTS})
string(REPLACE ".expected.out" "" T ${T_OUT})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leanbenchtest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
ENDFOREACH(T_OUT)
endif()
file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/plugin/*.lean")
FOREACH(T ${LEANINTERPTESTS})
@ -146,15 +150,19 @@ FOREACH(T ${LEANT0TESTS})
ENDFOREACH(T)
# LEAN PACKAGE TESTS
file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*")
FOREACH(T ${LEANPKGTESTS})
if(IS_DIRECTORY ${T})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leanpkgtest_${T_NAME}"
WORKING_DIRECTORY "${T}"
COMMAND bash -c "${TEST_VARS} ./test.sh")
endif()
ENDFOREACH(T)
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
message(STATUS "Skipping compiler tests on Windows because of shared library limit on number of exported symbols")
else()
file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*")
FOREACH(T ${LEANPKGTESTS})
if(IS_DIRECTORY ${T})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leanpkgtest_${T_NAME}"
WORKING_DIRECTORY "${T}"
COMMAND bash -c "${TEST_VARS} ./test.sh")
endif()
ENDFOREACH(T)
endif()
# LEAN SERVER TESTS
file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/server/*.lean")