Revision as of 15:20, 28 November 2012

CVC4 is a large project with a complicated build system, and it sometimes it a bit non-obvious why it is not doing what you think you want it to. Here is a repository of what can go wrong, what happened and how to mitigate the problem.

Configure Problems

Changing the --prefix option after compiling

If you try to change the ./configure --prefix=... option after having built a copy of CVC4, and then attempt to do make install, you are likely going to see an error like this:

make[6]: Entering directory `/home/taking/ws/cvc4/trunk/builds/x86_64-unknown-linux-gnu/debug/src/parser'
 /bin/mkdir -p '/home/taking/phony_install_targets/cvc4/trunk/lib'
 /bin/bash ../../libtool   --mode=install /usr/bin/install -c   libcvc4parser.la '/home/taking/phony_install_targets/cvc4/trunk/lib'
libtool: install: error: cannot install `libcvc4parser.la' to a directory not ending in /usr/local/lib

What happened is that libtool is not going to install the build library file (libcvc4parser.la) that already has hard links to the previous prefix (/usr/local/lib).

The only supported (and slower) option is to recompile from scratch

 make clean; ./configure ... ; make install

A faster (and more dangerous) option is to touch at least one file in each library to force the build system relink exactly the exported libraries. Run the following from the CVC4 directory and be stunned that it works:

 touch src/smt/smt_engine.h
 touch src/parser/parser.h

Currently, only those two are enough though this may change in the future. Unfortunately, ./configure --prefix=... is not currently smart enough to do this the latter option automatically.

builds Directory

make install to a non-standard prefix

If you are using CVC4 as a library, it is strongly recommended that you use a copy of CVC4 that is installed via make install. If you are building from source, you can make a temporary installation target at configure time. For example, you can use a directory inside of the CVC4 directory

$ cd $CVC4
$ mkdir target
$ ./configure --prefix=target ...
$ make install

You can then link against CVC4 by adding the following to the g++ command line:

• -lcvc4 to link against the CVC4 library
• -L $CVC4/target/lib to add the non standard library directory to the library search path
• -I $CVC4/target/include to add the non-standard include directory to the include search path

To compile the helloworld.cpp example:

 g++ helloword.cpp -o helloworld -lcvc4 -L $CVC4/target/lib/ -I $CVC4/target/include/

As this is a non-standard library directory, you will also need to add it to the linker's library path whenever you run helloworld:

 LD_LIBRARY_PATH="$CVC4/target/lib/" ./helloworld

We do not endorse with as a permanent solution, but it'll get you up and running fast. For more information, on shared libraries [1].

libcvc4 without make install

If you insist on not ever using make install and just using code built using make, it is possible to still use the CVC4 library. (The CVC4 team does not support this.) Oddly this may force you to change which header files you need to include. CVC4's build system is complicated by using a non standard directory structure for building and a desire be a good citizen of /usr/local/include and not pollute it. To support both, a number of files get shuffled around during make install. Part of this is making the include/cvc4 header directory. Includes such as #include <cvc4/cvc4.h> will not be able to find the cvc4 part of the include. You'll need to switch to using includes such as #include "smt/smt_engine.h"

To compile you'll need all of the following arguments to find all of the include files and libraries:

• -L $CVC4/lib
• -I $CVC4/src/
• -I $CVC4/src/include/
• -I $CVC4/builds/src
• -I $CVC4/builds/src/include/

Putting this all together, to get helloworld.cpp working:

$ sed 's:<cvc4/cvc4.h>:"smt/smt_engine.h":' < helloworld.cpp > hello.cpp
$ g++ hello.cpp -o hello -lcvc4 -L /home/taking/ws/cvc4/trunk/builds/lib -I /home/taking/ws/cvc4/trunk/builds/src/include/ -I /home/taking/ws/cvc4/trunk/src/ -I /home/taking/ws/cvc4/trunk/src/include/ -I /home/taking/ws/cvc4/trunk/builds/src
$ LD_LIBRARY_PATH="$CVC4/builds/lib/" ./hello

We do not endorse with as a permanent solution, but it'll get you up and running fast. For more information, on shared libraries [2].