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

feat: link external dependencies statically again

Browse source
This commit is contained in:
Sebastian Ullrich 2021-10-28 12:01:47 +02:00
parent 5bbc160f4b
commit b236273780
4 changed files with 15 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
script/prepare-llvm-linux.sh
View file

@ -28,14 +28,15 @@ $CP $GLIBC/lib/crt* llvm/lib/
$CP $GLIBC/lib/crt* stage1/lib/
# runtime
(cd llvm; $CP --parents lib/clang/*/lib/*/{*crt{begin,end}.o,libclang_rt.builtins*} ../stage1)
$CP llvm/lib/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.* stage1/lib/
$CP llvm/lib/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a stage1/lib/
# glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)!
$CP $GLIBC/lib/lib{c_nonshared,gcc_s}* stage1/lib/glibc
$CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc
for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
OPTIONS=()
echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++ -DLEAN_USE_LIBCXX=ON"
echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
# allow C++ code to include /usr since it needs quite a few more headers
echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm --stdlib=libc++ -I/usr/include -I/usr/include/x86_64-linux-gnu'"
echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -I ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -fuse-ld=ROOT/bin/ld.lld'"
echo -n " -DLEAN_TEST_VARS='LD_LIBRARY_PATH=$PWD/stage1/lib:\${LD_LIBRARY_PATH:-}'"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a --rtlib=compiler-rt -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
# do not set `LEAN_CC` for tests
echo -n " -DLEAN_TEST_VARS=''"

2
shell.nix
View file

@ -13,7 +13,7 @@ in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null }:
hardeningDisable = [ "all" ];
# more convenient `ctest` output
CTEST_OUTPUT_ON_FAILURE = 1;
GMP = pkgs.gmp;
GMP = pkgs.gmp.override { withStatic = true; };
GLIBC = pkgs.glibc;
shellHook = ''
export LEAN_SRC_PATH="$PWD/src"

13
src/CMakeLists.txt
View file

@ -277,14 +277,15 @@ else()
set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lStd -lleanrt -Wl,--end-group")
endif()
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin" OR "${LEAN_USE_LIBCXX}")
set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lc++")
set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lc++")
else()
set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lstdc++")
set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lstdc++")
set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
set(LEAN_CXX_STDLIB "-lc++")
endif()
set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} ${LEAN_CXX_STDLIB}")
set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} ${LEAN_CXX_STDLIB}")
set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lm")
set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lm")

2
src/Leanc.lean
View file

@ -22,7 +22,7 @@ Beware of the licensing consequences since GMP is LGPL."
-- We assume that the CMake variables do not contain escaped spaces
let cflags := ["-I", (root / "include").toString] ++ "@LEANC_EXTRA_FLAGS@".trim.splitOn
let mut cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn
let mut ldflags := ["-L", (root / "lib").toString, "-L", (root / "lib" / "lean").toString, (← IO.getEnv "LEANC_GMP").getD "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn
let mut ldflags := ["-L", (root / "lib" / "lean").toString, "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn
let mut ldflagsExt := "@LEANC_STATIC_LINKER_FLAGS@".trim.splitOn
let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn