diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index c54c7f7759..29cbbffc89 100755 --- a/script/prepare-llvm-linux.sh +++ b/script/prepare-llvm-linux.sh @@ -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=''" diff --git a/src/Leanc.lean b/src/Leanc.lean index 0986e70a91..ac4753942f 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -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}" diff --git a/src/bin/leanc.in b/src/bin/leanc.in index cc7a6158b3..5cb9a1633d 100755 --- a/src/bin/leanc.in +++ b/src/bin/leanc.in @@ -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=()