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

fix: robust linking of cyclically dependent libraries

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-13 18:20:21 +01:00
parent b0e8183663
commit fe03e70a8a
2 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/CMakeLists.txt
View file

@ -311,6 +311,14 @@ find_package(PythonInterp)
include_directories(${CMAKE_BINARY_DIR}/include)
# libleancpp and the stdlib libraries are cyclically dependent. This works by default on macOS, which also doesn't like
# the linker flags necessary on other platforms.
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
set(LEANC_STATIC_LINKER_FLAGS "-lleancpp" "-lInit" "-lStd" "-lLean")
else()
set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group" "-lleancpp" "-lInit" "-lStd" "-lLean" "-Wl,--end-group")
endif()
if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -fPIC")
endif()

4
src/bin/leanc.in
View file

@ -16,9 +16,7 @@ bindir=$(dirname $0)
cflags=("-I$bindir/../include")
ldflags=("-L$bindir/../lib/lean" "-lgmp" @LEANC_EXTRA_FLAGS@)
# static linker flags
# NOTE: libleancpp and libInit are cyclically dependent
ldflags_ext=("-lleancpp" "-lInit" "-lStd" "-lLean" "-lleancpp" "-lInit" "-lStd" "-lLean" "-lStd")
ldflags_ext=(@LEANC_STATIC_LINKER_FLAGS@)
for arg in "$@"; do
# passed -shared ~> switch to shared linker flags
[[ $arg == "-shared" ]] && ldflags_ext=(@LEANC_SHARED_LINKER_FLAGS@)