From 4faeafe30b006b899a338adf6233ff9f943e0c05 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Thu, 23 Apr 2015 12:03:23 +0200
Subject: [PATCH] doc: small fixes in installation mostly
---
doc/index.rst | 1 -
doc/installation.rst | 17 +++++++++++------
doc/r | 1 +
3 files changed, 12 insertions(+), 7 deletions(-)
create mode 100755 doc/r
diff --git a/doc/index.rst b/doc/index.rst
index 2a5bd13d1..2862cb2a4 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -27,6 +27,5 @@ Indices and tables
==================
* :ref:`genindex`
-* :ref:`modindex`
* :ref:`search`
diff --git a/doc/installation.rst b/doc/installation.rst
index 8c5e0df06..39b89cbf2 100644
--- a/doc/installation.rst
+++ b/doc/installation.rst
@@ -13,7 +13,7 @@ Windows.
**Requirements:**
-* 1.7 Java Development Kit. *(Java 8 is not officially supported)*
+* `1.7 Java Development Kit <http://www.oracle.com/technetwork/java/javase/downloads/jdk7-downloads-1880260.html>`_ *(Java 8 is not officially supported)*
* SBT 0.13.X (Available from http://www.scala-sbt.org/)
@@ -63,7 +63,7 @@ all the appropriate settings:
$ sbt script
-You will now need to either port the bash script to Windows, or by running it
+You will now need to either port the bash script to Windows, or to run it
under Cygwin.
.. _smt-solvers:
@@ -72,20 +72,25 @@ SMT Solvers
-----------
Leon relies on SMT solvers to solve the constraints it generates. We currently
-support two major SMT solvers: Z3 and CVC4.
+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.
+
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:
-
+specify another solver if this native layer is not available for you. Check the
+the ``--solvers`` command line option:
-.. code-block:: bash
+::
--solvers=s1,s2 Use solvers s1 and s2
Available:
diff --git a/doc/r b/doc/r
new file mode 100755
index 000000000..d210288c6
--- /dev/null
+++ b/doc/r
@@ -0,0 +1 @@
+make html
--
GitLab