Skip to content
Snippets Groups Projects
Commit c21623d6 authored by Viktor Kuncak's avatar Viktor Kuncak
Browse files

Lars in doc contribs. Moved README instructions to doc and CHANGELOG.md

parent 0831d796
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
CHANGELOG.md 0 → 100644
+ 59
− 0
View file @ c21623d6
Change Log
----------
#### v?.?
Among the changes are (see the commits for details):
* Leon can now do program repair, thanks to Etienne and Manos
* Isabelle proof assistant can now be used as a solver, thanks to Lars Hupel
* A DSL for writing equational proofs in Leon, thanks to Sandro Stucki and Marco Antognini
* Leon now uses the improved SMT-LIB library, thanks to the continuous work of Regis Blanc
* New case studies, including a little robot case study thanks to Etienne
* Improved termination checker of Nicolas Voirol with additions from Samuel Gruetter
* Many additions to Leon's library, including the state monad
* Numerous refactorings and bug fixes thanks to relentless work of Manos
* Add --watch option to automatically re-run Leon after file modifications, thanks to Etienne
#### v3.0
*Released 17.02.2015*
* Int is now treated as BitVector(32)
* Introduce BigInt for natural numbers
#### v2.4
*Released 10.02.2015*
* Implement support for higher-order functions
#### v2.3
*Released 03.03.2014*
* Accept multiple files with multiple modules/classes. Support class
definitions with methods.
* Introduce the Leon library with common generic datastructures, List and
Option for now.
* Add PortfolioSolver which tries a list of solvers (--solvers) in parallel.
* Add EnumerationSolver which uses Vanuatoo to guess models.
* Add documentation and sbt support for development under Eclipse,
#### v2.2
*Released 04.02.2014*
* Generics for functions and ADTs
* Use instantiation-time mixing for timeout sovlers
* Improve unrolling solvers to use incremental solvers
#### v2.1
*Released 10.01.2014*
* Reworked TreeOps API
* Tracing evaluators
* Support for range positions
* Support choose() in evaluators
* Flatten functions in results of synthesis
* Improved pretty printers with context information
#### v2.0
* First release
README.md
+ 7
− 211
View file @ c21623d6
...@@ -4,216 +4,12 @@ Leon 3.0 [![Build Status](http://laraquad4.epfl.ch:9000/epfl-lara/leon/status/ma ...@@ -4,216 +4,12 @@ Leon 3.0 [![Build Status](http://laraquad4.epfl.ch:9000/epfl-lara/leon/status/ma
Getting Started Getting Started
--------------- ---------------
This section gives a very quick overview of how to build and use Leon; refer to To build Leon you will need JDK, scala, sbt, and some external solver binaries.
the following sections if you wish (or need) more detailed information. On Linux, it should already work out of the box.
To build it, you will need, the following: To get started, see the documentation chapters, such as
* [Getting Started](src/sphinx/gettingstarted.rst)
* [Installation](src/sphinx/installation.rst)
* [Introduction to Leon](src/sphinx/intro.rst)
* Java Runtime Environment, from Oracle, e.g. Version 7 Update 5 (to run sbt and scala) [For change log, see CHANGELOG.md](CHANGELOG.md)
* Scala, from Typesafe, e.g. version 2.11.5
* sbt, at least version 0.13.1 (to build Leon)
* a recent GLIBC3 or later, works with e.g. _apt-get_ (for Z3)
* GNU Multiprecision library, e.g. gmp3, works with e.g. _apt-get_ (for Z3)
The following can be obtained from the web, but for convenience they are contained in the
repository and are actually automatically handled by the default build configuration:
* ScalaZ3 hosted on [GitHub](https://github.com/psuter/ScalaZ3/)
* The [libz3 library](http://z3.codeplex.com/) from microsoft
To build, type this:
$ sbt clean
$ sbt package # takes a while
$ sbt script
Then you can try e.g.
$ ./leon ./testcases/verification/datastructures/RedBlackTree.scala
and get something like this:
<pre>
┌──────────────────────┐
╔═╡ Verification Summary ╞════════════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ add postcondition 82:15 valid Z3-f 0.061 ║
║ add precond. (call ins(x, t)) 81:15 valid Z3-f 0.004 ║
║ add precond. (call makeBlack(ins(x, t))) 81:5 valid Z3-f 0.017 ║
║ balance match exhaustiveness 90:5 valid Z3-f 0.006 ║
║ balance postcondition 101:15 valid Z3-f 0.060 ║
║ blackBalanced match exhaustiveness 45:43 valid Z3-f 0.003 ║
║ blackHeight match exhaustiveness 50:40 valid Z3-f 0.004 ║
║ buggyAdd postcondition 87:15 invalid Z3-f 1.306 ║
║ buggyAdd precond. (call ins(x, t)) 86:5 invalid Z3-f 0.027 ║
║ buggyBalance match exhaustiveness 104:5 invalid Z3-f 0.007 ║
║ buggyBalance postcondition 115:15 invalid Z3-f 0.029 ║
║ content match exhaustiveness 17:37 valid Z3-f 0.083 ║
║ flip match exhaustiveness 117:31 valid Z3-f 0.004 ║
║ ins match exhaustiveness 59:5 valid Z3-f 0.004 ║
║ ins postcondition 66:15 valid Z3-f 1.385 ║
║ ins precond. (call ins(x, t.left)) 62:37 valid Z3-f 0.011 ║
║ ins precond. (call ins(x, t.right)) 64:40 valid Z3-f 0.012 ║
║ makeBlack postcondition 77:14 valid Z3-f 0.013 ║
║ redDescHaveBlackChildren match exhaustiveness 40:53 valid Z3-f 0.004 ║
║ redNodesHaveBlackChildren match exhaustiveness 34:54 valid Z3-f 0.004 ║
║ size match exhaustiveness 22:33 valid Z3-f 0.004 ║
║ size postcondition 25:15 valid Z3-f 0.048 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 22 valid: 18 invalid: 4 unknown 0 3.096 ║
╚═════════════════════════════════════════════════════════════════════════════════════════════════╝
</pre>
Building 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
much easier to build on Unix-like plattforms. Not to say it is impossible to
build on Windows. But some scripts used to run and test the system are shell
script and you will need to manually port them to Windows if you wish to use
Windows.
First you need a Java Runtime Environment. The most recent version should work.
Simply follow the standard installation process (e.g. _apt-get_) for your system.
Next, you need the [Simple Build Tool](http://www.scala-sbt.org/) (sbt)
which seems to be (as of today) the standard way to build Scala program. Again
you should follow the installation procedure. You can also find information
about sbt [here](http://typesafe.com/platform/tools/scala/sbt). Sbt is quite a complex
tool, so I would suggest looking at the getting started guide on the wiki page.
However, if you just want to quickly build Leon and never look back, then the
information provided here should be sufficient.
(This section is outdated for linux, but can be useful to adapt on Windows/Mac)
Now you will have to build the [ScalaZ3 project](https://github.com/psuter/ScalaZ3/).
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 [here](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.
Finally you can build Leon. Start ```sbt``` from a terminal to get an interactive
sbt session. Then type:
> clean
This will make sure the build is clean, then:
> package
This will compile everything and create jar files. This could take a long time.
Finally you need to generate a running script with the command:
> script
This will generate the leon script that can be used to run leon from command line
with correct arguments and classpath. This script you should not need to re-generate
another time, if you modify some code you just need to run ```compile``` again. If anything
goes wrong, you should carefully read the error message and try to fix it. You can
refer to the troubleshooting section of this manual.
Note that Leon is organised as a structure of two projects, with one main (or
root) project and 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. The subproject is in _'library'_ and contains required code to make
Leon input programs valid Scala programs. The point of having this library
sub-project, is that you can use the generated jar for the library sub-project
on its own and you should be able to compile Leon testcases with the standard
Scala compiler.
Now we can make sure that the build went fine. Leon comes with a test suite.
Use ```sbt test``` to run all the tests.
Using Leon in Eclipse
---------------------
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.sbt
In 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](http://help.eclipse.org/juno/index.jsp?topic=%2Forg.eclipse.platform.doc.user%2Ftasks%2Ftasks-importproject.htm) 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 [here](http://www.scalatest.org/user_guide/using_scalatest_with_eclipse).
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
<pre>
package leon
package test
package myTestPackage
</pre>
but instead
<pre>
package leon.test.myTestPackage
</pre>
Changelog
---------
#### v?.?
* Add --watch option to automatically re-run Leon after file modifications.
#### v3.0
*Released 17.02.2015*
* Int is now treated as BitVector(32)
* Introduce BigInt for natural numbers
#### v2.4
*Released 10.02.2015*
* Implement support for higher-order functions
#### v2.3
*Released 03.03.2014*
* Accept multiple files with multiple modules/classes. Support class
definitions with methods.
* Introduce the Leon library with common generic datastructures, List and
Option for now.
* Add PortfolioSolver which tries a list of solvers (--solvers) in parallel.
* Add EnumerationSolver which uses Vanuatoo to guess models.
* Add documentation and sbt support for development under Eclipse,
#### v2.2
*Released 04.02.2014*
* Generics for functions and ADTs
* Use instantiation-time mixing for timeout sovlers
* Improve unrolling solvers to use incremental solvers
#### v2.1
*Released 10.01.2014*
* Reworked TreeOps API
* Tracing evaluators
* Support for range positions
* Support choose() in evaluators
* Flatten functions in results of synthesis
* Improved pretty printers with context information
#### v2.0
* First release
src/sphinx/conf.py
+ 1
− 1
View file @ c21623d6
...@@ -15,7 +15,7 @@ ...@@ -15,7 +15,7 @@
import sys import sys
import os import os
docauthorlist = u'M. Antognini, R. Blanc, S. Gruetter, E. Kneuss, M. Koukoutos, V. Kuncak, S. Stucki, P. Suter' docauthorlist = u'M. Antognini, R. Blanc, S. Gruetter, L. Hupel, E. Kneuss, M. Koukoutos, V. Kuncak, S. Stucki, P. Suter'
# If extensions (or modules to document with autodoc) are in another directory, # If extensions (or modules to document with autodoc) are in another directory,
# add these directories to sys.path here. If the directory is relative to the # add these directories to sys.path here. If the directory is relative to the
......
src/sphinx/index.rst
+ 1
− 1
View file @ c21623d6
...@@ -19,8 +19,8 @@ Contents: ...@@ -19,8 +19,8 @@ Contents:
library library
xlang xlang
verification verification
isabelle
neon neon
isabelle
limitations limitations
synthesis synthesis
repair repair
......
src/sphinx/installation.rst
+ 145
− 35
View file @ c21623d6
...@@ -3,21 +3,21 @@ ...@@ -3,21 +3,21 @@
Installing Leon Installing Leon
=============== ===============
Leon requires quite a few dependencies, and you will need to make sure Leon requires quite a few dependencies, and you will need to
everything is correctly set up before being able to build it. Leon is probably make sure everything is correctly set up before being able
much easier to build on Unix-like platforms. Not to say it is impossible to to build it. Leon is probably easiest to build on Linux-like
build on Windows. But some scripts used to run and test the system are shell platforms, but read on regarding other platforms.
script and you will need to manually port them to Windows if you wish to use
Windows.
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:** **Requirements:**
* `Java SE Development Kit 7 <http://www.oracle.com/technetwork/java/javase/downloads/jdk7-downloads-1880260.html>`_ * `Java SE Development Kit 8 <http://www.oracle.com/technetwork/java/javase/downloads/jdk8-downloads-2133151.html>`_ or `Java SE Development Kit 7 <http://www.oracle.com/technetwork/java/javase/downloads/jdk7-downloads-1880260.html>`_ for your platform
* SBT 0.13.x (Available from http://www.scala-sbt.org/) * SBT 0.13.x (Available from http://www.scala-sbt.org/)
* Support for at least one external solver (See :ref:`smt-solvers`)
* Support for at least one SMT solver (See :ref:`smt-solvers`) * `Sphinx restructured text tool <http://sphinx-doc.org/>`_ (for building local documentation)
Linux & Mac OS-X Linux & Mac OS-X
---------------- ----------------
...@@ -41,12 +41,18 @@ all the appropriate settings: ...@@ -41,12 +41,18 @@ all the appropriate settings:
$ sbt script $ sbt script
$ ./leon --help $ ./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 Windows
------- -------
Get the sources of Leon by cloning the official Leon repository. You will need Get the sources of Leon by cloning the official Leon
a Git shell for windows, e.g. `Git for Windows <https://git-for-windows.github.io/>`_. repository. You will need a Git shell for windows, e.g.
`Git for Windows <https://git-for-windows.github.io/>`_.
.. code-block:: bash .. code-block:: bash
...@@ -71,44 +77,148 @@ under Cygwin. ...@@ -71,44 +77,148 @@ under Cygwin.
*Missing jars* *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: 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/`` 1. Copy ``unmanaged/common/cafebabe*.jar`` to ``unmanaged/64/``
2. Copy ``unmanaged/common/vanuatoo*.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
.. _smt-solvers: .. _smt-solvers:
SMT Solvers External Solvers
----------- ----------------
Leon relies on SMT solvers to solve the constraints it generates. We currently Leon typically relies on external (SMT) solvers to solve the constraints it generates.
support two major SMT solvers:
We currently support two major SMT solvers:
* CVC4, http://cvc4.cs.nyu.edu/web/ * CVC4, http://cvc4.cs.nyu.edu/web/
* Z3, https://github.com/Z3Prover/z3 * Z3, https://github.com/Z3Prover/z3
For Linux users, a native Z3 API is bundled with Leon and should work out of the Solver binaries that you install should match your operating
box. For OS-X and Windows users, you will either have to recompile the native system and your architecture. We recommend that you install
communication layer yourself or use the SMT-LIB API. 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 <https://github.com/psuter/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
-------------
Leon comes with a test suite. Consider running the following commands to
invoke different test suites:
$ sbt test
$ sbt integration:test
$ sbt regression:test
Building Leon Documentation
---------------------------
Solver binaries that you install should match your operating system and To build this documentation locally, you will need Sphinx (
your architecture. http://sphinx-doc.org/ ), a restructured text toolkit that
was originally developed to support Python documentation.
In any case, we recommend that you install both solvers separately and have After installing sphinx, run ``sbt previewSite``. This will generate the documentation and open a browser.
their binaries available in the ``$PATH``.
Since the default solver uses the native Z3 API, you will have to explicitly The documentation resides in the ``src/sphinx/`` directory and can also be built without ``sbt``
specify another solver if this native layer is not available to you. Check also using the provided ``Makefile``. To do this, in a Linux shell go to the directory ``src/sphinx/``,
the ``--solvers`` option in :ref:`cmdlineoptions`. 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.
Alternatively, there is a non-SMT solver available. See :ref:`isabelle` for Using Leon in Eclipse
details. ---------------------
Building Documentation You first need to tell sbt to globally include the Eclipse plugin in its known plugins.
---------------------- To do so type
To build this documentation locally, you will need Sphinx ( .. code-block:: bash
http://sphinx-doc.org/ ), a restructured text toolkit that
was originally developed to support Python documentation. $ echo "addSbtPlugin(\"com.typesafe.sbteclipse\" % \"sbteclipse-plugin\" % \"2.4.0\")" >> ~/.sbt/0.13/plugins/plugins.sbt
In 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 <http://help.eclipse.org/juno/index.jsp?topic=%2Forg.eclipse.platform.doc.user%2Ftasks%2Ftasks-importproject.htm>`_ 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 <http://www.scalatest.org/user_guide/using_scalatest_with_eclipse>`_.
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
.. code-block:: scala
package leon
package test
package myTestPackage
but instead
.. code-block:: scala
package leon.test.myTestPackage
After installing sphinx, run ``sbt previewSite``. This will generate the documentation and open a browser.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment