diff --git a/src/bin/leanc.in b/src/bin/leanc.in
index 446c65addd..3b238a7a1f 100755
--- a/src/bin/leanc.in
+++ b/src/bin/leanc.in
@@ -10,12 +10,14 @@
 # * `-U LEAN_MULTI_THREAD` can be used to optimize programs not making use of multi-threading
 # * `-print-cflags`: print C compiler flags necessary for building against the Lean runtime and abort
 # * `-print-ldlags`: print C compiler flags necessary for statically linking against the Lean library and abort
+# * Set the `LEANC_GMP` environment variable to a path to `libgmp.a` (or `-l:libgmp.a` on Linux) to link GMP statically.
+#   Beware of the licensing consequences since GMP is LGPL.
 
 set -e
 bindir=$(dirname $0)
 
 cflags=("-I$bindir/../include")
-ldflags=("-L$bindir/../lib/lean" "-lgmp" @LEANC_EXTRA_FLAGS@)
+ldflags=("-L$bindir/../lib/lean" "${LEANC_GMP:--lgmp}" @LEANC_EXTRA_FLAGS@)
 ldflags_ext=(@LEANC_STATIC_LINKER_FLAGS@)
 for arg in "$@"; do
     # passed -shared ~> switch to shared linker flags
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 185e2c5e0a..fb497e06e0 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -3,6 +3,9 @@ SHELL := /usr/bin/env bash -euo pipefail
 # any absolute path to the stdlib breaks the Makefile
 LEAN_PATH=
 
+# link GMP statically if STATIC=ON
+LEANC_GMP="${GMP_LIBRARIES}"
+
 # LEAN_OPTS: don't use native code (except for primitives) since it is from the previous stage
 # MORE_DEPS: rebuild the stdlib whenever the compiler has changed
 LEANMAKE_OPTS=\