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)
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 minutesWe now use sbt script to create a leon bash script that runs Leon with
all the appropriate settings:
$ sbt script
$ ./leon --helpNote 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.
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 minutesWe now use sbt script to create a leon bash script that runs leon with
all the appropriate settings:
$ sbt scriptYou 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:
- Copy
unmanaged/common/cafebabe*.jartounmanaged/64/ - Copy
unmanaged/common/vanuatoo*.jartounmanaged/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) or on [his dedicated web page](http://lara.epfl.ch/~mayer/leon/),
Leon typically relies on external (SMT) solvers to solve the constraints it generates.
We currently support two major SMT solvers:
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.
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.
Leon comes with a test suite. Consider running the following commands to invoke different test suites:
$ sbt test $ sbt integration:test $ sbt regression:test
To build this documentation locally, you will need Sphinx ( http://sphinx-doc.org/ ), a restructured text toolkit that was originally developed to support Python documentation.
After installing sphinx, run sbt previewSite. This will generate the documentation and open a browser.
The documentation resides in the src/sphinx/ directory and can also be built without sbt
using the provided Makefile. To do this, in a Linux shell go to the directory src/sphinx/,
type make html, and open in your web browser the generated top-level local HTML file, by default stored in
src/sphinx/_build/html/index.html. Also, you can open the *.rst documentation files in a text editor, since
they are human readable in their source form.
You first need to tell sbt to globally include the Eclipse plugin in its known plugins. To do so type
$ echo "addSbtPlugin(\"com.typesafe.sbteclipse\" % \"sbteclipse-plugin\" % \"2.4.0\")" >> ~/.sbt/0.13/plugins/plugins.sbtIn your Leon home folder, type: `sbt clean compile eclipse`
This should create all the necessary metadata to load Leon as a project in Eclipse.
You should now be able to import the project into your Eclipse workspace. Don't forget to also import dependencies (the bonsai and scalaSmtlib projects, found somewhere in your ~/.sbt directory).
For each run configuration in Eclipse, you have to set the
ECLIPSE_HOME environment variable to point to the home
directory of your Eclipse installation. To do so, go to
Run -> Run Configuration
and then, after picking the configuration you want to run, set the variable in the Environment tab.
If you want to use ScalaTest from within Eclipse, download the ScalaTest plugin. For instructions, see Using ScalaTest with Eclise. Do NOT declare your test packages as nested packages in separate lines, because ScalaTest will not see them for some reason. E.g. don't write
package leon
package test
package myTestPackagebut instead
package leon.test.myTestPackage