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

feat: leanmake: print out compile flags in analogy to pkg-config/llvm-config

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-19 12:26:20 +02:00 • committed by Leonardo de Moura
parent 7b2bcbe683
commit 573a128096
2 changed files with 12 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/CMakeLists.txt
View file

@ -554,7 +554,7 @@ add_custom_target(update-stage0
DEPENDS Init
WORKING_DIRECTORY "${LIB_SOURCE_DIR}/..")
configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc")
configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc" @ONLY)
install(FILES "${CMAKE_BINARY_DIR}/bin/leanc"
DESTINATION bin
PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)

14
src/bin/leanc.in
View file

@ -8,14 +8,22 @@
#
# Interesting options:
# * `-U LEAN_MULTI_THREAD` can be used to optimize programs not making use of multi-threading
# * `-print-cflags`: print C compiler flags necessary for building against the Lean runtime and abort
# * `-print-ldlags`: print C compiler flags necessary for statically linking against the Lean library and abort
set -e
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
linker_flags="-lleancpp -lInit -lleancpp -lInit"
ldflags_ext=("-lleancpp" "-lInit" "-lleancpp" "-lInit")
for arg in "$@"; do
[[ $arg == "-shared" ]] && linker_flags="@LEANC_SHARED_LINKER_FLAGS@"
# passed -shared ~> switch to shared linker flags
[[ $arg == "-shared" ]] && ldflags_ext=(@LEANC_SHARED_LINKER_FLAGS@)
[[ $arg == "-print-cflags" ]] && echo "${cflags[@]} ${cflags_ext[@]}" && exit
[[ $arg == "-print-ldflags" ]] && echo "${ldflags_ext[@]} ${ldflags[@]}" && exit
done
# Check C++ compiler
@ -27,4 +35,4 @@ done
[ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!"
# Note the `-x c` for treating all input as C code
@CMAKE_CXX_COMPILER_LAUNCHER@ $LEAN_CXX -D LEAN_MULTI_THREAD "-I$bindir/../include" -x c "$@" -x none "-L$bindir/../lib/lean" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
@CMAKE_CXX_COMPILER_LAUNCHER@ $LEAN_CXX -D LEAN_MULTI_THREAD "${cflags[@]}" -x c "$@" -x none "${ldflags_ext[@]}" "${ldflags[@]}" -Wno-unused-command-line-argument