summaryrefslogtreecommitdiff
path: root/INSTALL.md
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2020-04-28 10:43:48 -0700
committerGitHub <noreply@github.com>2020-04-28 10:43:48 -0700
commit5ec4b57ba3f79db76c5544b3ee37b917f7f0b58e (patch)
tree9d7dbdf20ed1a6be0212681b49a87055b946e1eb /INSTALL.md
parent967332f464f3e26d43f05bb9c68a0be788337ef6 (diff)
contrib/get-gmp: Rename and update install instructions with a warning. (#4407)
Diffstat (limited to 'INSTALL.md')
-rw-r--r--INSTALL.md13
1 files changed, 13 insertions, 0 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback