From 28f2686bf6a0f33c3b9f35cc8bc2af55aab220ad Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 21 Apr 2015 17:16:40 +0200
Subject: [PATCH] Some improvements to installation docs
---
doc/gettingstarted.rst | 16 ++-----
doc/index.rst | 1 +
doc/installation.rst | 96 +++++++++++++++++++++++++++++++++++++++---
3 files changed, 95 insertions(+), 18 deletions(-)
diff --git a/doc/gettingstarted.rst b/doc/gettingstarted.rst
index bd3810a64..34809d337 100644
--- a/doc/gettingstarted.rst
+++ b/doc/gettingstarted.rst
@@ -9,23 +9,13 @@ detailed information on how to setup Leon on your system.
To build Leon, you will need, the following:
-* 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
+* a 1.7 Java Development Kit, from Oracle (to run sbt and scala)
+* sbt, at least version 0.13.X (to build Leon)
To build, type this::
$ sbt clean
- $ sbt package # takes a while
+ $ sbt compile # takes about 3 minutes
$ sbt script
Then you can try e.g::
diff --git a/doc/index.rst b/doc/index.rst
index 2d8042646..2a5bd13d1 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -29,3 +29,4 @@ Indices and tables
* :ref:`genindex`
* :ref:`modindex`
* :ref:`search`
+
diff --git a/doc/installation.rst b/doc/installation.rst
index 4ba56f416..ae204708b 100644
--- a/doc/installation.rst
+++ b/doc/installation.rst
@@ -1,13 +1,99 @@
Installing Leon
===============
-Detailed instruction on building and installing Leon on various platform.
+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.
-Linux
------
-Mac OS-X
---------
+**Requirements:**
+
+* 1.7 Java Development Kit. *(Java 8 is not officially supported)*
+
+* SBT 0.13.X (Available from http://www.scala-sbt.org/)
+
+* Support for at least one SMT solver (See :ref:`smt-solvers`)
+
+Linux & Mac OS-X
+----------------
+
+Get the sources of Leon by cloning the official Leon repository:
+
+.. code-block:: bash
+
+ $ 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:
+
+.. code-block:: bash
+
+ $ sbt script
+ $ ./leon --help
+
Windows
-------
+
+Get the sources of Leon by cloning the official Leon repository (You will need a git shell for windows e.g. https://msysgit.github.io/):
+
+.. code-block:: bash
+
+ $ 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:
+
+.. code-block:: bash
+
+ $ sbt script
+
+You will now need to either port the bash script to Windows, or by running it
+under Cygwin.
+
+.. _smt-solvers:
+
+SMT Solvers
+-----------
+
+Leon relies on SMT solvers to solve the constraints it generates. We currently
+support two major SMT solvers: Z3 and CVC4.
+
+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.
+
+In any case, we recommend that you install both solvers separately and have
+their binaries available in the ``$PATH``.
+
+Since the default solver uses the native Z3 API, you will have to explicitly
+specify another solver if this native layer is not available for you:
+
+
+.. code-block:: bash
+
+ --solvers=s1,s2 Use solvers s1 and s2
+ Available:
+ enum : Enumeration-based counter-example-finder
+ fairz3 : Native Z3 with z3-templates for unfolding (default)
+ smt-cvc4 : CVC4 through SMT-LIB
+ smt-cvc4-cex : CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only
+ smt-cvc4-proof : CVC4 through SMT-LIB, in-solver inductive reasonning, for proofs only
+ smt-z3 : Z3 through SMT-LIB
+ smt-z3-q : Z3 through SMT-LIB, with quantified encoding
+ unrollz3 : Native Z3 with leon-templates for unfolding
+
+
--
GitLab