diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000000000000000000000000000000000000..33ad5147e2f3e8685eb8619e9791d7a881b4a127
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,59 @@
+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
diff --git a/README.md b/README.md
index 9b0df9b3c0c0059c23e54db98e5c453584cc214f..65f322b4e1efbfebaef80a3a81094bdc2f0c85e8 100644
--- a/README.md
+++ b/README.md
@@ -4,216 +4,12 @@ Leon 3.0 [ more detailed information.
+To build Leon you will need JDK, scala, sbt, and some external solver binaries.
+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)
-* 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
+[For change log, see CHANGELOG.md](CHANGELOG.md)
diff --git a/src/sphinx/conf.py b/src/sphinx/conf.py
index 1430aae28de37009668bc4b5f86f80f9a2db2b80..de027efc1654c02de394ab978e07c37987070823 100644
--- a/src/sphinx/conf.py
+++ b/src/sphinx/conf.py
@@ -15,7 +15,7 @@
import sys
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,
# add these directories to sys.path here. If the directory is relative to the
diff --git a/src/sphinx/index.rst b/src/sphinx/index.rst
index c80f95d406be4a03276d8994b5b3334d5cde8b4c..d02cf02930997d013e1710fad8c09500b54d74e4 100644
--- a/src/sphinx/index.rst
+++ b/src/sphinx/index.rst
@@ -19,8 +19,8 @@ Contents:
library
xlang
verification
- isabelle
neon
+ isabelle
limitations
synthesis
repair
diff --git a/src/sphinx/installation.rst b/src/sphinx/installation.rst
index f8de2929d040cf45dfe068eecba15a208d4ae61e..1af4a8eaffb032fce8d512e25556a9ffaae3fb72 100644
--- a/src/sphinx/installation.rst
+++ b/src/sphinx/installation.rst
@@ -3,21 +3,21 @@
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
-much easier to build on Unix-like platforms. 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.
+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 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/)
-
-* Support for at least one SMT solver (See :ref:`smt-solvers`)
+* Support for at least one external solver (See :ref:`smt-solvers`)
+* `Sphinx restructured text tool <http://sphinx-doc.org/>`_ (for building local documentation)
Linux & Mac OS-X
----------------
@@ -41,12 +41,18 @@ 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 <https://git-for-windows.github.io/>`_.
+Get the sources of Leon by cloning the official Leon
+repository. You will need a Git shell for windows, e.g.
+`Git for Windows <https://git-for-windows.github.io/>`_.
.. code-block:: bash
@@ -71,44 +77,148 @@ under Cygwin.
*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/``
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
------------
+External Solvers
+----------------
-Leon relies on SMT solvers to solve the constraints it generates. We currently
-support two major SMT 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
-For Linux users, a native Z3 API is bundled with Leon and should work out of the
-box. For OS-X and Windows users, you will either have to recompile the native
-communication layer yourself or use the SMT-LIB API.
+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 <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
-your architecture.
+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.
-In any case, we recommend that you install both solvers separately and have
-their binaries available in the ``$PATH``.
+After installing sphinx, run ``sbt previewSite``. This will generate the documentation and open a browser.
-Since the default solver uses the native Z3 API, you will have to explicitly
-specify another solver if this native layer is not available to you. Check also
-the ``--solvers`` option in :ref:`cmdlineoptions`.
+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.
-Alternatively, there is a non-SMT solver available. See :ref:`isabelle` for
-details.
+Using Leon in Eclipse
+---------------------
-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 (
-http://sphinx-doc.org/ ), a restructured text toolkit that
-was originally developed to support Python documentation.
+.. code-block:: bash
+
+ $ 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.