summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--INSTALL.md13
-rwxr-xr-xcontrib/get-gmp-dev (renamed from contrib/get-gmp)11
-rwxr-xr-xcontrib/get-win-dependencies2
3 files changed, 25 insertions, 1 deletions
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
index 678103cf4..f8a301a89 100755
--- a/contrib/get-gmp
+++ b/contrib/get-gmp-dev
@@ -21,6 +21,17 @@ 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"
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 =============================================================================
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback