Skip to content

Building with CMake

Jump to bottom
Michael Rawson edited this page Mar 4, 2024 · 2 revisions

If you don't know CMake, we suggest you take a little time to learn how to use CMake builds and a little about how to write CMake build scripts. Vampire uses a relatively-simple CMake build, so you can read CMakeLists.txt if you like to figure out how it works. Generally you should only need to touch the build system to add new files and un-break builds; ask the team if something isn't working for you.

Build Options

All build options are controlled as additional arguments to CMake. For example, cmake -DEXAMPLE=value .., or you can use a GUI tool if you prefer. Notable options are:

  • Debug build: -DCMAKE_BUILD_TYPE=Debug
  • Target directory: -DCMAKE_INSTALL_PREFIX=/opt/vampire-devel - helpful when compiling z3 to avoid collisions with other installed versions.
  • Static compilation: -DBUILD_SHARED_LIBS=0 This option only prefers static libraries over shared libraries which can lead to a mixed binary. You can check the output of the linking which libraries were not linked in. Please be also aware that Mac OS X does not support completely statically linked libraries (see also Apple's Technical Q&A).
  • "Inter-Procedural Optimisation": -DIPO=ON. This enables potentially-expensive linker options (depending on your system) which may produce a small performance improvement. Probably only useful for competitions.
  • Unit test coverage information: -DCOVERAGE=ON.

Z3

We fix a known version of Z3 via git-submodule. If you don't need Z3, do nothing: CMake will detect this and do the right thing. If you need Z3, first git submodule update --init to pull the correct version of Z3, then build Z3 via its own CMake system into z3/build, which is where Vampire's CMake will find the necessary files. CMake will then detect this build and do the right thing.

Do not commit changes to the toplevel z3 folder unless you mean to change the fixed version of Z3 we build with. If you do want to do this, do it carefully, make sure you know how submodules work, then warn the team after merging so that they can update their submodule builds and look for introduced bugs.

Advanced Z3

  • If you've used Z3 in the past but don't want it for this build, pass -DCMAKE_DISABLE_FIND_PACKAGE_Z3=ON to disable automatically including Z3.
  • If you want to override the Z3 search path, first think carefully about whether you need to do this: Z3 is a fixed submodule for a reason! Then remove CMakeCache.txt if present (the path to Z3 is cached) and pass -DZ3_ROOT=/foo/bar/build/.
  • To make sure CMake found the intended package, pass -DCMAKE_FIND_DEBUG_MODE=ON

Building Z3

Please refer to Z3's CMake documentation. Notable options are:

  • -DZ3_BUILD_LIBZ3_SHARED=0: static library
  • -DCMAKE_INSTALL_PREFIX=/opt/z3-devel: installation path

Building for competitions

TODO how do we build for competitions? E.g. details of build configuration, linking, Spider?

CMake tips'n'tricks

  • Verbose compilation for UNIX Makefiles: if you would like to disable the progress reports and see the commands that are run, call make VERBOSE=1.
Clone this wiki locally