* Some documentation about building compatibility and language bindings

* Better errors/warnings when SWIG isn't installed (resolves bug 373)
* Allow compatibility bindings to be built when SWIG isn't available

1 files changed, 77 insertions, 0 deletions

diff --git a/INSTALL b/INSTALL
index 96e9cbd60..e2cceb967 100644
--- a/INSTALL
+++ b/INSTALL
@@ -24,6 +24,10 @@ under doc/ but is not installed by "make install".
 
 Examples/tutorials are not installed with "make install."  See below.
 
+For more information about the build system itself (probably not
+necessary for casual users), see the Appendix at the bottom of this
+file.
+
 *** Build dependences
 
 The following tools and libraries are required to run CVC4. Versions
@@ -78,10 +82,18 @@ Boost project, please visit http://www.boost.org/.
 
 None of these is required, but can improve CVC4 as described below:
 
+  Optional: SWIG 2.0.x (Simplified Wrapper and Interface Generator)
   Optional: CLN v1.3 or newer (Class Library for Numbers)
   Optional: CUDD v2.4.2 or newer (Colorado University Decision Diagram package)
   Optional: GNU Readline library (for an improved interactive experience)
   Optional: The Boost C++ threading library (libboost_thread)
+  Optional: CxxTest unit testing framework
+
+SWIG is necessary to build the Java API (and of course a JDK is
+necessary, too).  SWIG 1.x won't work; you'll need 2.0, and the more
+recent the better.  On Mac, we've seen SWIG segfault when generating
+CVC4 language bindings; version 2.0.8 or higher is recommended to
+avoid this.  See "Language bindings" below for build instructions.
 
 CLN is an alternative multiprecision arithmetic package that can offer
 better performance and memory footprint than GMP.  CLN is covered by
@@ -106,6 +118,13 @@ Boost base library) is needed to run CVC4 in "portfolio"
 (multithreaded) mode.  Check your distribution for a package named
 "libboost-thread-dev" or similar.
 
+CxxTest is necessary to run CVC4's unit tests (included with the
+distribution).  Running these is not really required for users of
+CVC4; "make check" will skip unit tests if CxxTest isn't available,
+and go on to run the extensive system- and regresion-tests in the
+source tree.  However, if you're interested, you can download CxxTest
+at http://cxxtest.com/ .
+
 *** Building with CUDD (optional)
 
 CUDD, if desired, must be installed delicately.  The CVC4 configure
@@ -137,6 +156,47 @@ here:
 The Debian source package "cudd", available from the same repository,
 includes a diff of all changes made to cudd makefiles.
 
+*** Language bindings
+
+There are several options available for using CVC4 from the API.
+
+First, CVC4 offers a complete and flexible API for manipulating
+expressions, maintaining a stack of assertions, and checking
+satisfiability, and related things.  The C++ libraries (libcvc4.so and
+libcvc4parser.so) and required headers are installed normally via a
+"make install".  This API is also available from Java (via CVC4.jar
+and libcvc4jni.so) by configuring with --enable-language-bindings=java.
+You'll also need SWIG 2.0 installed (and you might need to help
+configure find it if you installed it in a nonstandard place with
+--with-swig-dir=/path/to/swig/installation).  You may also need to
+give the configure script the path to your Java headers (in
+particular, jni.h).  You might do so with (for example):
+
+  ./configure --enable-language-bindings=java \
+      JAVA_CPPFLAGS=-I/usr/lib/jvm/java-6-openjdk-amd64/include
+
+There is also a "C++ compatibility API" (#include <cvc4/cvc3_compat.h>
+and link against libcvc4compat.so) that attempts to maintain
+source-level backwards-compatibility with the CVC3 C++ API.  The
+compatibility library is built by default, and
+--enable-language-bindings=java enables the Java compatibility library
+(CVC4compat.jar and libcvc4compatjni.so).
+--enable-language-bindings=c enables the C compatibility library
+(#include <cvc4/bindings/compat/c/c_interface.h> and link against
+libcvc4bindings_c_compat.so), and if you want both C and Java
+bindings, use --enable-language-bindings=c,java.  These compatibility
+language bindings do NOT require SWIG.
+
+The examples/ directory includes some basic examples (the "simple vc"
+and "simple vc compat" family of examples) of all these interfaces.
+
+In principle, since we use SWIG to generate the native Java API, we
+could support other languages as well.  However, using CVC4 from other
+languages is not supported, nor expected to work, at this time.  If
+you're interested in helping to develop, maintain, and test a language
+binding, please contact us via the users' mailing list at
+cvc-users@cs.nyu.edu.
+
 *** Building CVC4 from a repository checkout
 
 The following tools and libraries are additionally required to build
@@ -159,3 +219,20 @@ repository.
 Examples are not built by "make" or "make install".  See
 examples/README for information on what to find in the examples/
 directory, as well as information about building and installing them.
+
+*** Appendix: Build architecture
+
+The build system is generated by automake, libtool, and autoconf.  It
+is somewhat nonstandard, though, which (for one thing) requires that
+GNU Make be used.  If you ./configure in the top-level source
+directory, the objects will actually all appear in
+builds/${arch}/${build_id}.  This is to allow multiple, separate
+builds in the same place (e.g., an assertions-enabled debugging build
+alongside a production build), without changing directories at the
+shell.  The "current" build is maintained, and you can still use
+(e.g.) "make -C src/main" to rebuild objects in just one subdirectory.
+
+You can also create your own build directory inside or outside of the
+source tree and configure from there.  All objects will then be built
+in that directory, and you'll ultimately find the "cvc4" binary in
+src/main/, and the libraries under src/ and src/parser/.