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

chore: link leanshared using leanc after all

Browse source
This commit is contained in:
Sebastian Ullrich 2021-08-18 09:30:59 +02:00
parent 40f41a1f14
commit 88f3de7a44
3 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
nix/bootstrap.nix
View file

@ -85,8 +85,8 @@ rec {
stdlibLinkFlags = "-L${gmp}/lib -L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean";
leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; } ''
mkdir $out
c++ -fPIC -shared ${lib.optionalString stdenv.isLinux "-Bsymbolic-functions"} \
${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/* -Wl,-force_load,${Std.staticLib}/* -Wl,-force_load,${Lean.staticLib}/* -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a -Wl,-force_load,${leancpp}/lib/libleanrt_initial-exec.a"
LEAN_CXX=${stdenv.cc}/bin/c++ ${lean-bin-tools-unwrapped}/bin/leanc -x none -shared ${lib.optionalString stdenv.isLinux "-Bsymbolic-functions"} \
${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/* -Wl,-force_load,${Std.staticLib}/* -Wl,-force_load,${Lean.staticLib}/* -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a"
else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive"} ${stdlibLinkFlags} \
-o $out/libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}
'';

4
src/bin/leanc.in
View file

@ -23,8 +23,8 @@ args=("$@")
for arg in "$@"; do
# passed -shared ~> switch to shared linker flags
[[ $arg == "-shared" ]] && ldflags_ext=(@LEANC_SHARED_LINKER_FLAGS@) && args=("-x" "c" "$@" "-x" "none")
# linking against libleanshared explicitly ~> do not link against static stdlib
[[ $arg == "-lleanshared" ]] && ldflags_ext=()
# linking against libleanshared explicitly (or linking libleanshared itself) ~> do not link against static stdlib
[[ $arg == "-lleanshared" || $arg == *libleanshared.* ]] && ldflags_ext=()
# Note the `-x c` for treating all input as C code
[[ $arg == "-c" ]] && ldflags=() && ldflags_ext=() && args=("-x" "c" "$@" "-x" "none")
[[ $arg == "--print-cflags" ]] && echo "${cflags[@]}" && exit

3
src/stdlib.make.in
View file

@ -33,8 +33,7 @@ Lean: Init Std
leanshared: Init Std Lean
@mkdir -p "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}" || true
# can't use leanc here since it would try to link against leanshared
${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} -shared -o "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}" ${LEANSHARED_LINKER_FLAGS} -lgmp ${LEANC_EXTRA_FLAGS} -L${LIB}/lean
"${LEAN_BIN}/leanc" -x none -shared -o "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}" ${LEANSHARED_LINKER_FLAGS} ${LEANC_OPTS}
Leanpkg: Init Std Lean leanshared
+"${LEAN_BIN}/leanmake" bin PKG=Leanpkg BIN_NAME=leanpkg${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE}'