Skip to content

Setting up the Environment

Jump to bottom
Kassing edited this page May 4, 2026 · 3 revisions

Initial Setup

This guide describes how to set up the AProVE development environment in Eclipse or in IntelliJ. Please follow the steps carefully to ensure a working configuration.

  1. Clone or fork the repository Contributors should work on a fork of the repository and stage a pull request after implementing new features. Clone the fork into a folder aprove-open-source.
mkdir aprove_project/
cd aprove_project/
git clone git@github.com:<fork-name>/aprove-open-source.git
cd aprove-open-source/

  1. Install Required Dependencies

    Depending on what you want to work on in AProVE you need different additional tools installed. In the following, you can find a list of all external tools that AProVE might call. If you start working on AProVE and have no idea what you need to install: Just install the satisfiability checkers and ignore the rest.

    Satisfiability checkers (Termination, Complexity)

    For (non)termination proofs you also need the satisfiability checkers Z3, Yices, and MiniSat:

    • Z3: Please visit https://github.com/Z3Prover/z3/releases to download Z3 (version >= 4.4.0). For Linux please download the source code, then compile and install it as described in the README file. In addition, you have to pass the option --java to scripts/mk_make.py to build Z3's java bindings. Alternatively, you can download pre-compiled binaries from https://github.com/Z3Prover/z3/releases. To do so, you have to select ''Planned'' in the section ''OTHER DOWNLOADS'' on the right. Afterwards, please make sure to add the Z3 sub-directory containing the executable z3 to your path environment as described below. Furthermore, the folder containing the file libz3java.so has to be added to the environment variable LD_LIBRARY_PATH. This works similar to setting the path environment (see below).

    • Yices 1: AProVE still runs only with Yices 1 (e.g., Yices 1.0.40 released December 4, 2013), but not Yices 2. Please download Yices 1 from https://yices.csl.sri.com/old/download-yices1.html. After extracting the files, please make sure to add the yices bin sub-directory (/home/username/yices-1.0.40/bin/) to your path environment as described below. Moreover, please make sure that this sub-directory appears before any other directory (e.g., /usr/local/bin) that would contain another Yices binary.

    • MiniSat To run AProVE, you need to install MiniSat version 2 or higher: Linux On Debian and Ubuntu it suffices to install the minisat2 package. For other systems: Make sure that make and the developer version of zlib are installed on your sytem. Download http://minisat.se/downloads/minisat2-070721.zip and unzip it. Inside the minisat/simp directory, run make rs (this depends on glibc-static, install if not present on your system). Rename the resulting file minisat_static to minisat and add its directory to your path environment as described below.

    Graphviz (GUI)

    If you need to visualize graphs, please also download and install the Graphviz tools (containing dot) from http://www.graphviz.org/. For Debian and Ubuntu it suffices to install the graphviz package.

    CeTA (Certification)

    In order to invoke CeTA from the GUI one needs to install CeTA (version >= 2.22). It is available at http://cl-informatik.uibk.ac.at/software/ceta/, where both precompiled binaries and the sources are available. To compile CeTA you additionally need to install the Glasgow Haskell Compiler, which is included in the Haskell Platform. After installing CeTA, please make sure that ceta is accessible, by adjusting your path environment as described below.

    KoAT (Complexity)

    To be able to prove upper bounds on the complexity of Integer Term Rewrite Systems from the GUI, one needs to install the tool KoAT. Moreover, KoAT is used by some complexity analysis techniques for classical Term Rewriting. Please checkout KoAT from github. Install KoAT according to the supplied instructions. Rename the resulting executable to koat and add its directory to your path environment as described below.

    LoAT (Complexity)

    To be able to prove lower bounds on the complexity of Integer Term Rewrite Systems from the GUI, one needs to install the tool LoAT. The recommended way to install LoAT is to download the pre-compiled binary for Linux/x64. Alternatively, checkout LoAT from github. Install LoAT according to the supplied instructions. In any case, rename the resulting executable to loat and add its directory to your path environment as described below.

    CoFloCo (Complexity)

    Some complexity analysis techniques for Term Rewriting require CoFloCo. Please follow the installation instructions from the CoFloCo website.

    Clang (C-Program Analysis)

    To be able to analyze C Programs, one needs to install Clang 2.9. To do so, please download and install the suitable precompiled binary of Clang 2.9, which is available here. Newer version of Clang up to and including Clang 3.5 should also work, but we cannot guarantee this.

Using Eclipse

  1. Download and Install the newest version of Eclipse here

  2. Import the Eclipse Project and set the correct Java Version

    1. Navigate to: File → Import → General → Existing Projects into Workspace

    2. Select the aprove_project/ directory

    3. Import all detected projects

    AProVE is currently developed with Java 25. You can set the Java version in the preferences of each Project. Right-click the project then Properties > Java Compiler > Compiler Compliance Level and set it to 25.

  3. Import the Eclipse Preferences

    1. Navigate to: File → Import → General → Preferences

    2. Select the file: aprove_project/aprove-open-source/eclipsePreferences/preferences.epf

    This file contains settings for the Java Code Formatter as well as custom compiler errors and warnings.

  4. Run ant target initialSetup

    Make sure you have the right ant version installed for your JDK.

    cd aprove_project/aprove-open-source/
ant -f build-aprove.xml initialSetup

    You can also do this from eclipse by setting up the correct Ant-file. To do this, go to the properties for the aprove project, choose the tab "Builders" and create an "Ant Builder", for which you configure the possible targets.

  5. Wait for Eclipse to build the Workspace

    You might need to refresh the project.

    Eclipse can build your workspace automatically. For this, make sure to check the menu entry Project > Build Automatically. However, since AProVE is a big project, you might want to disable this. In this case, you have to trigger the Eclipse build manually via Project > Build All. Using the automatic build is more convenient (better IDE support) as long as you can tolerate being interrupted by the automatic build occasionally.

  6. Using the Automatic Build without being interrupted by it very frequently

    If the box in Menu > Project > Build Automatically is checked, the Eclipse provides a much better editing support. However, if not configured correctly, then the automatic build can really get in the way, because it frequently interrupts the user for several minutes to rebuild the whole project. This might have several reasons, but is not the intended way how it should work.

    For me, the available RAM for Eclipse was set too low, so Eclipse could not keep the whole project into memory at once. The problem was solved by increasing the available RAM. This can be configured in the eclipse.ini file. I set -Xms1024m for the minimum size and -Xmx4096m for the maximum size.

    Another helpful option is to enable Window > Preferences > General > Startup and Shutdown > Refresh workspace on startup. This causes Eclipse to refresh its workspace when it is started, which often causes a rebuild of the project. If this option is disabled you might run into the situation that you start Eclipse and do something else while it start. But then, when you actually start working with Eclipse and make the first changes it notices that it needs to refresh its workspace and causes a rebuild, effectively interrupting you again from starting to work with the code. I strongly suggest checking this box, so that Eclipse is ready to go when you are.

  7. Configure run

    You need to configure how aprove should be run. A list of all command line flags can be found here in the 'AProVE Command-Line Version' section. For configuration go to 'Run --> Open Run Dialog... --> Java Application --> New and use aprove.Main as main class.

    An example of a run configuration that gives the WST output, a plain proof output, and uses a timer of 60 seconds on an examples named #4.16.ari located in the examples/TRS_Standard folder would be:

    -m wst -p plain -t 60 examples/TRS_Standard/#4.16.ari

Using IntelliJ

  1. Download and install the newest version of Eclipse

    This is needed because the build process depends on some Eclipse libraries.

  2. Install the Ant plugin from the marketplace in IntelliJ

  3. Start IntelliJ and open the approve-open-source directory

  4. If necessary, locate the Eclipse's installation directory upon prompt (e.g. /usr/lib/eclipse)

  5. Import the Ant build script

    Navigate to View -> Tool Windows -> Ant and press the +-button and select the file approve-open-source/build-aprove.xml.

  6. Configure the SDKs

    Navigate to File -> Project Structure and further Platform Settings -> SDKs, press the +-button and add both the SDK 25 as well as SDK 8. Then navigate to Project Settings -> Project and select 25 as your SDK and your language level. Make sure your language level is lower or equal to your SDK version. Do the same under Project Settings -> Modules.

  7. Increase the maximum heap size of the build process

    Navigate to Settings -> Build, Execution, Deployment -> Compiler and set the shared heap size to e.g. 4069.

  8. Run ant target initialSetup

    Open the Ant tool window and double-click the respective item.

  9. Configure run

    In toolbar on the top, select the configurations dropdown menu and press Edit configurations.... Then, add a new Application configuration and set aprove.Main as the Main class. Then configure the program arguments as required, for example -m wst -p plain -t 60 examples/TRS_Standard/#4.16.ari.

Fixing the Eclipse Build

  1. Disable automatic build in: Menu > Project > Build Automatically
  2. Clean all projects: Menu > Project > Clean (enable Clean all projects, disable Start a build immediately) > Clean
  3. Run ant scripts:
    1. In the aprove_project/aprove-open-source/ directory: run ant -f build-aprove.xml cleanAll initialSetup
  4. Refresh all projects: In the Project Explorer right click each project > select Refresh
  5. Enable automatic build in: Menu > Project > Build Automatically
  6. Wait for the build to finish (see bottom right corner in the status bar, this might take a few minutes)

Still Problems?

  1. Try to to the steps above again and read everything very carefully!

  2. Try compiling in the console:

    $ cd ~/workspace/aprove
$ ant

  3. Eclipse sometimes messes up its builds (rarely happens). Then, e.g. some perfectly valid imports are not resolved by Eclipse any more. In such a case, it can be helpful to

    • refresh the project (click on the project root in the package explorer and press F5)
    • clean the project via Menu Project -> Clean...

  4. If you see an error like "declared package does not match expected package", then you may need to set the source folder in your project properties: Project properties -> Java Build Path -> Source -> set to aprove-open-source/src

  5. Another issue that may come up is Eclipse crashing with an OutOfMemoryException. To prevent this, invoke Eclipse as follows:

    eclipse -vmargs -Xms512m -Xmx512m -XX:PermSize=128m -XX:MaxPermSize=128m

  6. Using Eclipse on 32 bit machines?

    Memory options to be passed to eclipse: -Xmx<number>m where is a suitably high number, bigger than 128 (recommended: 256 or more, you had better have enough RAM). This is necessary for Eclipse to be able to compile the continuously growing AProVE project (more than 4000 classes surely lead to one heck of a dependency graph).

  7. Final Option: Ask a fellow AProVE developer like Jan-Christoph Kassing (Kassing@cs.rwth-aachen.de)

Clone this wiki locally