Build Problems
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.
Contents
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
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</cdoe>. Roughly speaking there is a directory for each major architecture, <code>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].