From 5ec4b57ba3f79db76c5544b3ee37b917f7f0b58e Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 28 Apr 2020 10:43:48 -0700
Subject: [PATCH] contrib/get-gmp: Rename and update install instructions with
 a warning. (#4407)

---
 INSTALL.md                       | 13 +++++++++++++
 contrib/{get-gmp => get-gmp-dev} | 11 +++++++++++
 contrib/get-win-dependencies     |  2 +-
 3 files changed, 25 insertions(+), 1 deletion(-)
 rename contrib/{get-gmp => get-gmp-dev} (66%)

diff --git a/INSTALL.md b/INSTALL.md
index 9fc2b52c1..b95450dff 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -73,6 +73,19 @@ incorrect behavior (and wrong results) in many builds. This is a known problem
 for MiniSat, and since MiniSat is at the core of CVC4, a problem for CVC4.
 We recommend using a GCC version > 4.5.1.
 
+### Warning: Installing GMP via `contrib/get-gmp-dev`
+
+Do **not** install GMP via the provided script `contrib/get-gmp-dev` unless
+your distribution
+* does not ship with the GMP configuration you need, e.g.,
+  script `contrib/get-win-dependencies` uses `contrib/get-gmp-dev` when
+  cross-compiling GMP for Windows.
+* does not ship with static GMP libraries (e.g., Arch Linux)
+  and you want to build CVC4 statically.
+
+In most of the cases the GMP version installed on your system is the one you
+want and should use.
+
 ## Optional Dependencies
 
 ### SymFPU (Support for the Theory of Floating Point Numbers)
diff --git a/contrib/get-gmp b/contrib/get-gmp-dev
similarity index 66%
rename from contrib/get-gmp
rename to contrib/get-gmp-dev
index 678103cf4..f8a301a89 100755
--- a/contrib/get-gmp
+++ b/contrib/get-gmp-dev
@@ -19,6 +19,17 @@ GMP_DIR="$DEPS_DIR/gmp-$GMPVERSION"
 
 check_dep_dir "$GMP_DIR"
 
+echo =============================================================================
+echo
+echo "This script should only be used if your distribution does not ship with the"
+echo "GMP configuration you need. For example, contrib/get-win-dependencies cross-"
+echo "compiles GMP for Windows. You can also use the script if your distribution"
+echo "does not ship with static GMP libraries (e.g., Arch Linux) and you want to"
+echo "build CVC4 statically."
+echo
+echo "In most of the cases the GMP version installed on your system is the one you"
+echo "want and should use."
+echo
 echo =============================================================================
 echo
 echo "Setting up GMP $GMPVERSION..."
diff --git a/contrib/get-win-dependencies b/contrib/get-win-dependencies
index 1138e3071..02b1e4054 100755
--- a/contrib/get-win-dependencies
+++ b/contrib/get-win-dependencies
@@ -84,7 +84,7 @@ MAKE_CFLAGS="$MAKE_CFLAGS" \
 MAKE_CXXFLAGS="$MAKE_CXXFLAGS" \
 MAKE_LDFLAGS="$MAKE_LDFLAGS" \
 GMPVERSION="$GMPVERSION" \
-  contrib/get-gmp || reporterror
+  contrib/get-gmp-dev || reporterror
 
 echo
 echo =============================================================================
-- 
2.30.2