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
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=`pwd`/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].
Custom CLN Library Installations
Suppose you have CLN make installed to a custom target. I'll assume the full path is in $CLN. (I have only done this once so it might not be minimal.) You are going to have to play with ALL of the following flags when configuring:
- --with-cln
- CLN_CFLAGS="-I$CLN/include/cln/"
- CLN_LIBS="-L$CLN/lib/"
- LD_LIBRARY_PATH : to get configure's gcc instances to be able to use -lcln
- CPPFLAGS="-I$CLN/include/"
- LDFLAGS="-L$CLN/lib/"
- LIBS="-lcln"
Putting this all together:
LD_LIBRARY_PATH="$CLN/lib/" ./configure --with-cln CLN_CFLAGS="-I$CLN/include/cln/" CLN_LIBS="-L$CLN/lib/" CPPFLAGS="-I$CLN/include/" LDFLAGS="-L$CLN/lib/" LIBS="-lcln" ...
Profiling
Google Perftools And Early Exit
Are you getting empty files or no output from google perftools? Make sure to disable early exiting with "--no-early-exit".
$ CPUPROFILE=example.prof ./cvc4 --no-early-exit example.smt unsat PROFILE: interrupts/evictions/bytes = 9/0/1512 $ ls -l example.prof -rw-r--r-- 1 taking taking 8784 Dec 6 17:39 example.prof
If you try to do this without "--no-early-exit", example.prof is empty.
SIGPROF handler is already in use
The configuration options "--enable-profiling" and "--with-google-perftools" are mutually exclusive on some systems. Both require being the handler of SIGPROF on a number of systems. If you see the following error you are likely doing this.
Disabling profiler because SIGPROF handler is already in use.
To confirm this in gdb, catch sigaction. (sigaction comes from the header #include <signal.h></code.>) SIGPROF has an id of 27 on most systems.
google perftools not linking
If libprofiler.so.0 is not showing up in <code>ldd CVC4/builds/bin/cvc4 with --with-google-perftools enabled, you may have a problem like the following: [3]. However, this cannot be applied directly. Something in libtool messes this up. So the following instead:
./configure --with-google-perftools LDFLAGS="-Wl,--no-as-needed /usr/lib/libprofiler.so -Wl,--as-needed" ...
