contrib/get-gmp: Rename and update install instructions with a warning. (#4407)

diff --git a/INSTALL.md b/INSTALL.md
index 9fc2b52c1cb0d3a8f49bde02ad6adb8f989c8f8d..b95450dffb569fd882ad2f1d8343daab68e54a0d 100644 (file)
--- 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
deleted file mode 100755 (executable)
index 678103c..0000000
--- a/contrib/get-gmp
+++ /dev/null
@@ -1,35 +0,0 @@
-#!/usr/bin/env bash
-#
-# This script should only be used if your distribution does not ship with the
-# GMP configuration you need. For example, contrib/get-win-dependencies
-# cross-compiles GMP for Windows. You can also use the script if your
-# distribution 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.
-#
-
-source "$(dirname "$0")/get-script-header.sh"
-
-[ -z "${BUILD_TYPE}" ] && BUILD_TYPE="--disable-shared --enable-static"
-[ -n "$HOST" ] && HOST="--host=$HOST"
-[ -z "$GMPVERSION" ] && GMPVERSION=6.1.2
-
-GMP_DIR="$DEPS_DIR/gmp-$GMPVERSION"
-
-check_dep_dir "$GMP_DIR"
-
-echo =============================================================================
-echo
-echo "Setting up GMP $GMPVERSION..."
-echo
-setup_dep "https://gmplib.org/download/gmp/gmp-$GMPVERSION.tar.bz2" "$GMP_DIR"
-cd "$GMP_DIR"
-./configure ${HOST} --prefix="$INSTALL_DIR" --enable-cxx ${BUILD_TYPE}
-make \
-  CFLAGS="${MAKE_CFLAGS}" \
-  CXXFLAGS="${MAKE_CXXFLAGS}" \
-  LDFLAGS="${MAKE_LDFLAGS}" \
-  -j$(nproc)
-make install
-echo

diff --git a/contrib/get-gmp-dev b/contrib/get-gmp-dev
new file mode 100755 (executable)
index 0000000..f8a301a
--- /dev/null
+++ b/contrib/get-gmp-dev
@@ -0,0 +1,46 @@
+#!/usr/bin/env bash
+#
+# This script should only be used if your distribution does not ship with the
+# GMP configuration you need. For example, contrib/get-win-dependencies
+# cross-compiles GMP for Windows. You can also use the script if your
+# distribution 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.
+#
+
+source "$(dirname "$0")/get-script-header.sh"
+
+[ -z "${BUILD_TYPE}" ] && BUILD_TYPE="--disable-shared --enable-static"
+[ -n "$HOST" ] && HOST="--host=$HOST"
+[ -z "$GMPVERSION" ] && GMPVERSION=6.1.2
+
+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..."
+echo
+setup_dep "https://gmplib.org/download/gmp/gmp-$GMPVERSION.tar.bz2" "$GMP_DIR"
+cd "$GMP_DIR"
+./configure ${HOST} --prefix="$INSTALL_DIR" --enable-cxx ${BUILD_TYPE}
+make \
+  CFLAGS="${MAKE_CFLAGS}" \
+  CXXFLAGS="${MAKE_CXXFLAGS}" \
+  LDFLAGS="${MAKE_LDFLAGS}" \
+  -j$(nproc)
+make install
+echo

diff --git a/contrib/get-win-dependencies b/contrib/get-win-dependencies
index 1138e3071556793dfe5172365a9a7fb11958021c..02b1e40547516edffa0669c11486433662a4b571 100755 (executable)
--- 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 =============================================================================