diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh
index 7c9c2ea117..e1b943c580 100755
--- a/script/prepare-llvm-linux.sh
+++ b/script/prepare-llvm-linux.sh
@@ -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=''"
diff --git a/shell.nix b/shell.nix
index 1c7d397242..152d04c653 100644
--- a/shell.nix
+++ b/shell.nix
@@ -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"
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 20736c6539..7702531bc3 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -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")
 
diff --git a/src/Leanc.lean b/src/Leanc.lean
index bd5099f024..4205a45426 100644
--- a/src/Leanc.lean
+++ b/src/Leanc.lean
@@ -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