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

chore: fix foreign test on macOS, again

Browse source
This commit is contained in:
Sebastian Ullrich 2021-11-09 17:34:00 +01:00
parent 6ca944f453
commit 09d549aecd
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Leanc.lean
View file

@ -23,7 +23,7 @@ Beware of the licensing consequences since GMP is LGPL."
let cflags := ["-I", (root / "include").toString] ++ "@LEANC_EXTRA_FLAGS@".trim.splitOn
let mut cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn
let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn
let mut ldflags := ["-L", (root / "lib" / "lean").toString, "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn
let mut ldflags := ["-L", (root / "lib" / "lean").toString, (← IO.getEnv "LEANC_GMP").getD "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn
let mut ldflagsExt := "@LEANC_STATIC_LINKER_FLAGS@".trim.splitOn
for arg in args do

3
src/shell/CMakeLists.txt
View file

@ -81,7 +81,8 @@ ENDFOREACH(T)
add_test(NAME leancomptest_foreign
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler/foreign"
COMMAND bash -c "${LEAN_BIN}/leanmake --always-make CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'")
# LEANC_OPTS is necessary for macOS c++ to find its headers, GMP will be removed soon
COMMAND bash -c "LEANC_GMP=${GMP_LIBRARIES} ${LEAN_BIN}/leanmake --always-make CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'")
add_test(NAME leancomptest_doc_example
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler"
COMMAND bash -c "export ${TEST_VARS}; leanmake --always-make bin && ./build/bin/test hello world")