diff --git a/src/Leanc.lean b/src/Leanc.lean index ac4753942f..86609af40d 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -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 diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 85f33616e8..ffcb0a178c 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -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")