Skip to content

Latest commit

 

History

History
35 lines (26 loc) · 2.79 KB

Build.md

File metadata and controls

35 lines (26 loc) · 2.79 KB
Raw

Building Theta

Theta uses Java (JDK) 17 with Gradle 7.4 as a build system. Currently, we use OpenJDK 17 (see instructions for Windows and Ubuntu). We are developing Theta on Linux, Windows and MacOS (10.15.7). Currently, floating point types are only fully supported on Linux and MacOS. Windows support is experimental and can cause cryptic exceptions to occur in native code. Theta can be built from the command line, but you can also import it into IntelliJ IDEA. Unfortunately, Eclipse does not support Gradle projects with Kotlin build scripts (yet).

Dependencies

Theta has some external dependencies that may need to be obtained/installed depending on what parts of the framework you are working with.

Z3 SMT Solver: The libraries for the Z3 solver (version 4.5.0) are included in the lib directory, for Windows, Ubuntu (64 bit) and MacOS. However, on Windows, libz3.dll also requires some libraries from the Microsoft Visual C++ Redistributable package that we could not include due to licensing. Install it, or just execute Download-VCredist.ps1, which will download the required libraries. On MacOS, libz3.dylib and libz3java.dylib need to be on DYLD_LIBRARY_PATH. If you have a different OS, you should download the appropriate Z3 binary for version 4.5.0. These libraries should be available on PATH for the executable tools.

Troubleshooting:

  • If Z3 gives an assertion error (unreachable code reached), your Z3 version may not be correct.

MPFR: For floating point support on MacOS, libmpfr_java-1.4.jnilib and libmpfr.dylib (as libmpfr.4.dylib) need to be on DYLD_LIBRARY_PATH. Additionally, libmpfr_java-1.4.jnilib needs to linked as libmpfr_java.jnilib onto both DYLD_LIBRARY_PATH and java.library.path.

GraphViz: Theta can export graphs in dot format and automatically convert them to images. For this, GraphViz has to be installed and dot (or dot.exe on Windows) has to be on the PATH.

Building from the command line

Theta can be built from the command line by simply executing gradlew.bat build (Windows) or ./gradlew build (Linux) from the root of the repository, where build is the name of the task that will compile all projects and run the tests. On Linux make sure you do not use gradle build as it executes your globally installed Gradle tool which might not be the appropriate version.