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

fix: actually link against GMP statically

Browse source
This commit is contained in:
Sebastian Ullrich 2021-11-08 17:37:22 +01:00
parent 42ee91bcda
commit 27bc6397a0
3 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -32,8 +32,8 @@ for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/
OPTIONS=()
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 " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -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 --rtlib=compiler-rt -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -Wl,--as-needed -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
# do not set `LEAN_CC` for tests
echo -n " -DLEAN_TEST_VARS=''"

4
src/Leanc.lean
View file

@ -22,9 +22,9 @@ 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 ldflagsInternal := "@LEANC_INTERNAL_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
for arg in args do
match arg with
@ -49,7 +49,7 @@ Beware of the licensing consequences since GMP is LGPL."
cflagsInternal := []
ldflagsInternal := []
cc := rootify cc
let args := cflags ++ cflagsInternal ++ args ++ ldflagsExt ++ ldflags ++ ldflagsInternal ++ ["-Wno-unused-command-line-argument"]
let args := cflags ++ cflagsInternal ++ args ++ ldflagsInternal ++ ldflagsExt ++ ldflags ++ ["-Wno-unused-command-line-argument"]
let args := args.filter (!·.isEmpty) |>.map rootify
if args.contains "-v" then
IO.eprintln s!"{cc} {" ".intercalate args}"

2
src/bin/leanc.in
View file

@ -1,7 +1,7 @@
#!/usr/bin/env bash
# used only for building Lean itself
root=$(dirname $0)
ldflags=("-L$root/lib" "-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@ @LEANC_INTERNAL_LINKER_FLAGS@)
ldflags=(@LEANC_INTERNAL_LINKER_FLAGS@ "-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@)
for arg in "$@"; do
# ccache doesn't like linker flags being passed here
[[ "$arg" = "-c" ]] && ldflags=()