Fix regressions in regress1 after #4613. (#4616)

[cvc5.git] / INSTALL.md

diff --git a/INSTALL.md b/INSTALL.md
index 55bd4aef519b3e46f7b3aa293f040ece23d33286..b95450dffb569fd882ad2f1d8343daab68e54a0d 100644 (file)
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -1,4 +1,4 @@
-CVC4 prerelease version 1.7.
+CVC4 prerelease version 1.8.
 ============================
 
 ## Building CVC4
@@ -12,7 +12,7 @@ CVC4 prerelease version 1.7.
     make install     # to install into the prefix specified above
 
 All binaries are built into `<build_dir>/bin`, the CVC4 library is built into
-`<build_dir>/src`.
+`<build_dir>/lib`.
 
 ## Supported Operating Systems
 
@@ -23,6 +23,21 @@ On macOS, we recommend using Homebrew (https://brew.sh/) to install the
 dependencies.  We also have a Homebrew Tap available at
 https://github.com/CVC4/homebrew-cvc4 .
 
+### Cross-compiling for Windows
+
+Cross-compiling CVC4 with Mingw-w64 can be done as follows:
+
+```
+  HOST=x86_64-w64-mingw32 ./contrib/get-win-dependencies
+  ./configure --win64 --static <configure options...>
+
+  cd <build_dir>   # default is ./build
+  make             # use -jN for parallel build with N threads
+```
+
+The built binary `cvc4.exe` is located in `<build_dir>/bin` and the CVC4 library
+can be found in `<build_dir>/lib`.
+
 ## Build dependencies
 
 The following tools and libraries are required to build and run CVC4.  
@@ -34,6 +49,7 @@ compatible.
 - [CMake >= 3.1](https://cmake.org)
 - [GNU Bash](https://www.gnu.org/software/bash/)
 - [Python >= 2.7](https://www.python.org)
+  + module [toml](https://pypi.org/project/toml/)
 - [GMP v4.2 (GNU Multi-Precision arithmetic library)](https://gmplib.org)
 - [libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library)](http://www.antlr3.org/)
 - [Java >= 1.6](https://www.java.com)
@@ -57,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)
@@ -94,7 +123,7 @@ Configure CVC4 with `configure.sh --lfsc` to build with this dependency.
 ### SWIG >= 3.0.x (Simplified Wrapper and Interface Generator)
 
 SWIG 3.0.x (and a JDK) is necessary to build the Java API.
-See [Language Bindings](language-bindings) below for build instructions.
+See [Language Bindings](#language-bindings) below for build instructions.
 
 ### CLN >= v1.3 (Class Library for Numbers)
 
@@ -187,17 +216,7 @@ binding, please contact one of the project leaders.
 
 ## Building the Examples
 
-The examples provided in directory `examples` are not built by default.
-
-    make examples                      # build all examples
-    make runexamples                   # build and run all examples
-    make <example>                     # build examples/<subdir>/<example>.<ext>
-    ctest example/<subdir>/<example>   # run test example/<subdir>/<example>
-
-All examples binaries are built into `<build_dir>/bin/examples`.
-
-See `examples/README` for more detailed information on what to find in the
-`examples` directory.
+See `examples/README.md` for instructions on how to build and run the examples.
 
 ## Testing CVC4
 
@@ -222,24 +241,6 @@ We have 4 categories of tests:
 - **unit tests** in directory `test/unit`
   (label: **unit**)
 
-### Testing Examples
-
-For building instructions, see [Building the Examples](building-the-examples).
-
-We use prefix `example/` + `<subdir>/` + `<example>` (for `<example>` in
-`example/<subdir>/`) as test target name.  
-
-    make bitvectors                       # build example/api/bitvectors.cpp
-    ctest -R bitvectors                   # run all tests that match '*bitvectors*'
-                                          # > runs example/api/bitvectors
-                                          # >      example/api/bitvectors_and_arrays
-                                          # >      ...
-    ctest -R bitvectors$                  # run all tests that match '*bitvectors'
-                                          # > runs example/api/bitvectors
-    ctest -R example/api/bitvectors$      # run all tests that match '*example/api/bitvectors'
-                                          # > runs example/api/bitvectors
-
-
 ### Testing System Tests
 
 The system tests are not built by default.