diff --git a/src/sphinx/isabelle.rst b/src/sphinx/isabelle.rst index c48fa16ebfe37d1ddce0400c56ffdea99fb2ba29..a375ccb4302926d839b2b8015b7af09d34b866cf 100644 --- a/src/sphinx/isabelle.rst +++ b/src/sphinx/isabelle.rst @@ -28,20 +28,10 @@ verification. Installation ------------ -You can obtain a copy of Isabelle for your operating system at `its website -<https://isabelle.in.tum.de/>`_, then follow the `installation instructions -<https://isabelle.in.tum.de/installation.html>`_. The installation path needs -to be passed to Leon via the ``--isabelle:base`` command line option. (The path -will end in ``Isabelle2015``. Depending on your operating system, this folder -might be some levels into the installation tree.) - -On Linux, you can skip this step. Leon is able to download and install Isabelle -itself. During the first start, you just need to pass the command line option -``--isabelle:download=true``. You may specify ``--isabelle:base``, but don't -have to. - -Additionally, you need to instruct Git to fetch all the referenced repositories -via ``git submodule update --init --recursive``. +You don't have to obtain a copy of Isabelle. Leon is able to download and +install Isabelle itself. The installation happens in the appropriate folder for +your operating system, e.g. ``%APPDATA%`` under Windows or ``$HOME/.local`` +under Linux. Basic usage diff --git a/src/sphinx/options.rst b/src/sphinx/options.rst index a5be01e35269e12864cd6716947727209497b337..38f18d0aef81eea7dd1006c92fda59f170b3f25e 100644 --- a/src/sphinx/options.rst +++ b/src/sphinx/options.rst @@ -313,27 +313,6 @@ CVC4 Solver Isabelle ******** -* ``--isabelle:base=<path>`` - - Specify the installation directory of Isabelle. In Isabelle-parlance, this is - called ``$ISABELLE_HOME``. It will have the form ``/path/to/Isabelle2015``. - When no Isabelle installation can be found there, the system suggests to - enable the ``download`` option. - -* ``--isabelle:build`` - - Flag to indicate that during the start-up of Leon, Isabelle should - automatically build all required library sources. This is on by default, and - should usually be left on. Building only happens when some dependencies - changed and subsequent runs of Leon don't rebuild the library. However, even - if nothing is build, it still requires the system a couple of seconds to - figure that out. - -* ``--isabelle:download`` - - If necessary, perform a full system bootstrap by downloading and unpacking a - copy of Isabelle. Off by default. Only supported under Linux. - * ``--isabelle:dump=<path>`` Makes the system write theory files containing the translated definitions