Revision as of 13:07, 29 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

config.log

If something went wrong when configure, check out builds/config.log for an in-depth error report. This is a good way to spot problems with manual linking configurations. If something goes really wrong and config.log is not in builds, try looking for builds/<arch>/<configuration>/config.log (see #builds Directory). For example,

 builds/x86_64-unknown-linux-gnu/production-cln-profiling/config.log

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

CVC4 does not use the $CVC4/src directory for intermediate object and library file compilation. Instead it compiles everything into the $CVC4/builds directory. Under this directory, you will find that most the files are symbolic links into the same subdirectory.

$ ls -l builds/Makefile
lrwxrwxrwx 1 taking taking 46 Nov 28 14:46 builds/Makefile -> x86_64-unknown-linux-gnu/debug/Makefile.builds
$ ls -l builds/test
lrwxrwxrwx 1 taking taking 35 Nov 28 14:46 builds/test -> x86_64-unknown-linux-gnu/debug/test

Both point into x86_64-unknown-linux-gnu/debug. Roughly speaking there is a directory for each major architecture, x86_64-unknown-linux-gnu and a subdirectory for each significant configuration, debug. CVC4 allows for having multiple architectures and configuration options built in the same builds/ directory. For example, I currently have 3 different significantly different configurations for the x86_64-unknown-linux-gnu architecture.

$ ls builds/x86_64-unknown-linux-gnu/
debug  debug-staticbinary  production-cln-staticbinary

To switch in between these, all you need to do is rerun ./configure. This makes it easy to switch between these three configurations.

This does make it a bit difficult to find things sometimes. Especially when working on the build system itself, and something goes wrong.

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/builds/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 $CVC4/builds/lib -I $CVC4/src/ -I $CVC4/src/include/ -I $CVC4/builds/src/ -I $CVC4/builds/src/include/
$ 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].