installation.rst

Installing Leon

Leon requires quite a few dependencies, and you will need to make sure everything is correctly set up before being able to build it. Leon is probably easiest to build on Linux-like platforms, but read on regarding other platforms.

Due to its nature, this documentation section may not always be up to date; we welcome pull requests with carefully written and tested improvements to the information below.

Requirements:

• Java SE Development Kit 8 or Java SE Development Kit 7 for your platform
• SBT 0.13.x (Available from http://www.scala-sbt.org/)
• Support for at least one external solver (See :ref:`smt-solvers`)
• Sphinx restructured text tool (for building local documentation)

Linux & Mac OS-X

Get the sources of Leon by cloning the official Leon repository:

$ git clone https://github.com/epfl-lara/leon.git
Cloning into 'leon'...
// ...
$ cd leon
$ sbt clean compile
// takes about 3 minutes

We now use sbt script to create a leon bash script that runs Leon with all the appropriate settings:

$ sbt script
$ ./leon --help

Note that Leon is organized as a structure of several projects, with a main (or root) project and at least one sub-project. From a user point of view, this should most of the time be transparent and the build command should take care of everything.

Windows

Get the sources of Leon by cloning the official Leon repository. You will need a Git shell for windows, e.g. Git for Windows.

$ git clone https://github.com/epfl-lara/leon.git
Cloning into 'leon'...
// ...
$ cd leon
$ sbt clean compile
// takes about 3 minutes

We now use sbt script to create a leon bash script that runs leon with all the appropriate settings:

$ sbt script

You will now need to either port the bash script to Windows, or to run it under Cygwin.

Known issues

Missing jars

If running leon produces errors because it could not find some cafebabe*.jar or vanuatoo*.jar, it is probably because symlinks have not been resolved. If your architecture is x64, do the following:

1. Copy unmanaged/common/cafebabe*.jar to unmanaged/64/
2. Copy unmanaged/common/vanuatoo*.jar to unmanaged/64/

You may be able to obtain additional tips on getting Leon to work on Windows from Mikael Mayer, http://people.epfl.ch/mikael.mayer

External Solvers

Leon typically relies on external (SMT) solvers to solve the constraints it generates.

We currently support two major SMT solvers:

• CVC4, http://cvc4.cs.nyu.edu/web/
• Z3, https://github.com/Z3Prover/z3

Solver binaries that you install should match your operating system and your architecture. We recommend that you install these solvers as a binary and have their binaries available in the $PATH. Once they are installed, you can instruct Leon to use a given sequence of solvers. The more solvers you have installed, the more successful Leon might get, because solver capabilities are incomparable.

In addition to these external binaries, a native Z3 API for Linux is bundled with Leon and should work out of the box (although having an external Z3 binary is a good idea in any case). For other platforms you will have to recompile the native Z3 communication layer yourself; see the section below.

As of now the default solver is the native Z3 API, you will have to explicitly specify another solver if this native layer is not available to you, e.g., by giving the option --solvers=smt-cvc4 to use CVC4. Check the --solvers option in :ref:`cmdlineoptions`.

In addition to SMT solvers, it is possible to automatically invoke the Isabelle proof assistant on the proof obligations that Leon generates. See :ref:`isabelle` for details.

Building ScalaZ3 and Z3 API

The main reason for using the Z3 API is that it is currently faster when there are many calls to the solver, as in the case of synthesis and repair.

To build the ScalaZ3 on Linux, you should follow the instructions given in the ScalaZ3 project. The ScalaZ3 is a Scala wrapper on the Z3 native library from Microsoft. It is used in Leon to make native call to Z3. The generated .jar from ScalaZ3 will be dependent on your own z3 native library, which you can obtain from http://z3.codeplex.com/ . However, the ScalaZ3 repository comes with 32 and 64 bits version for Linux and you should probably use those ones to make sure the version is compatible. You can install the Z3 native library in some standard system library path such as /usr/lib. You need to install the scalaz3.jar file in the "unmanaged" directory. The build system is configured to use any jar file in the "unmanaged" directory. Finally be aware that the Z3 library will come with its own set of dependencies, in particular you will need to have GMP. You will probably have to fight with a few errors before everything can finally work together.

An analogous process has been reported to be relatively straightforward on OS-X and also possible on Windows.

Running Tests