Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11

1 files changed, 102 insertions, 89 deletions

diff --git a/INSTALL.md b/INSTALL.md
index 89b3e8a..7e41cd8 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -6,17 +6,75 @@ SMTCoq is designed to work on computers equipped with a POSIX (Unix or a
 clone) operating system. It is known to work under GNU/Linux (i386 and
 amd64) and Mac OS X.
 
-<!-- The simplest way is to install it using opam. You can also install it -->
-<!-- from the sources (this is mandatory if you want to use the native -->
-<!-- version, see below). -->
+The simplest way is to install it using opam. You can also install it
+from the sources (this is mandatory if you want to use the native
+version, see below).
 
 You will also need to [install the provers](#installation-of-the-provers)
 you want to use.
 
-## Requirements
+
+## Installation via opam (recommended)
+
+### In an existing switch
+
+You need to have OCaml version >= 4.09.0 and Coq version 8.11.*.
+
+Simply add the coq-extra-dev repo to opam:
+```bash
+opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
+```
+and install SMTCoq:
+```bash
+opam install coq-smtcoq
+```
+
+### In a new switch
+
+Create a switch with the last version of OCaml:
+```bash
+opam switch create ocaml-base-compiler.4.10.0
+eval $(opam env)
+```
+add the Coq repos to opam:
+```bash
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
+```
+and install SMTCoq:
+```bash
+opam install coq-smtcoq
+```
+
+### If you are new to opam
+
+We recommended to install the required packages from
+[opam](https://opam.ocaml.org). Once you have installed opam on your system you
+should issue the following command:
+
+```bash
+opam init
+```
+
+which will initialize the opam installation and prompt for modifying the shell
+init file.
+
+Once opam is installed you should still issue
+
+```bash
+eval `opam config env`
+```
+
+(this is not necessary if you start another session in your shell).
+
+Then follow the instructions of the previous section.
+
+
+## Installation from the sources, using opam (not recommended)
+
+### Requirements
 
 You need to have OCaml version >= 4.09.0 and Coq version 8.11.*.
-The easiest way to install these two pieces of software is through opam.
 
 > **Warning**: The version of Coq that you plan to use must have been compiled
 > with the same version of OCaml that you are going to use to compile
@@ -29,22 +87,7 @@ data-structures](https://github.com/smtcoq/native-coq) instead of
 Coq-8.11 (warning: this allows one to use the vernacular commands but not
 the tactics).
 
-
-<!-- ### Installation via opam (recommended) -->
-
-<!-- Simply add the coq-extra-dev repo to opam: -->
-<!-- ```bash -->
-<!-- opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -->
-<!-- ``` -->
-<!-- and install SMTCoq: -->
-<!-- ```bash -->
-<!-- opam install coq-smtcoq -->
-<!-- ``` -->
-
-
-### Installation from the sources, using opam <!-- (not recommended) -->
-
-#### Install opam
+### Install opam
 
 We recommended to install the required packages from
 [opam](https://opam.ocaml.org). Once you have installed opam on your system you
@@ -65,33 +108,33 @@ eval `opam config env`
 
 (this is not necessary if you start another session in your shell).
 
-#### Install OCaml
+### Install OCaml
 
-Now you can install an OCaml compiler (we recommend 4.09.0):
+Now you can install an OCaml compiler (we recommend 4.10.0):
 
 ```bash
-opam switch create ocaml-base-compiler.4.09.0
+opam switch create ocaml-base-compiler.4.10.0
 ```
 
-#### Install Coq
+### Install Coq
 
-After OCaml is installed, you can install Coq-8.11.0 through opam.
+After OCaml is installed, you can install Coq-8.11.2 through opam.
 
 ```bash
-opam install coq.8.11.0
+opam install coq.8.11.2
 ```
 
 If you also want to install CoqIDE at the same time you can do
 
 ```bash
-opam install coq.8.11.0 coqide.8.11.0
+opam install coq.8.11.2 coqide.8.11.2
 ```
 
 but you might need to install some extra packages and libraries for your system
 (such as GTK2, gtksourceview2, etc.).
 
 
-#### Install SMTCoq
+### Install SMTCoq
 
 Compile and install SMTCoq by using the following commands in the src directory.
 
@@ -101,67 +144,37 @@ make
 make install
 ```
 
+## Installation with native-coq (not recommended except for high performances)
+
+> **Warning**: this installation procedure is recommended only to use
+> the vernacular commands efficiently (in particular, to check very
+> large proof certificates). It does not allow one to use the tactics.
+
+1. Download the git version of Coq with native compilation:
+```bash
+git clone https://github.com/smtcoq/native-coq.git
+```
+   and compile it by following the instructions available in the
+   repository. We recommand that you do not install it, but only compile
+   it in local:
+```bash
+./configure -local
+make
+```
 
-<!-- ### Installation from the sources, with official Coq 8.9 release (not recommended) -->
-
-<!-- 1. Download the last stable version of Coq 8.9: -->
-<!-- ```bash -->
-<!-- wget https://github.com/coq/coq/archive/V8.9.0.tar.gz -->
-<!-- ``` -->
-<!--    and compile it by following the instructions available in the -->
-<!--    repository (make sure you use OCaml 4.09.0 for that). We recommand -->
-<!--    that you do not install it, but only compile it in local: -->
-<!-- ```bash -->
-<!-- ./configure -local -->
-<!-- make -->
-<!-- ``` -->
-
-<!-- 2. Set an environment variable COQBIN to the directory where Coq's -->
-<!--    binaries are; for instance: -->
-<!-- ```bash -->
-<!-- export COQBIN=/home/jdoe/coq-8.9.0/bin/ -->
-<!-- ``` -->
-<!--    (the final slash is mandatory). -->
-
-<!-- 3. Compile and install SMTCoq by using the following commands in the src directory. -->
-<!-- ``` -->
-<!-- ./configure.sh -->
-<!-- make -->
-<!-- make install -->
-<!-- ``` -->
-
-
-<!-- ### Installation with native-coq (not recommended except for high performances) -->
-
-<!-- > **Warning**: this installation procedure is recommended only to use -->
-<!-- > the vernacular commands efficiently (in particular, to check very -->
-<!-- > large proof certificates). It does not allow one to use the tactics. -->
-
-<!-- 1. Download the git version of Coq with native compilation: -->
-<!-- ```bash -->
-<!-- git clone https://github.com/smtcoq/native-coq.git -->
-<!-- ``` -->
-<!--    and compile it by following the instructions available in the -->
-<!--    repository. We recommand that you do not install it, but only compile -->
-<!--    it in local: -->
-<!-- ```bash -->
-<!-- ./configure -local -->
-<!-- make -->
-<!-- ``` -->
-
-<!-- 2. Set an environment variable COQBIN to the directory where Coq's -->
-<!--    binaries are; for instance: -->
-<!-- ```bash -->
-<!-- export COQBIN=/home/jdoe/native-coq/bin/ -->
-<!-- ``` -->
-<!--    (the final slash is mandatory). -->
-
-<!-- 3. Compile and install SMTCoq by using the following commands in the src directory. -->
-<!-- ``` -->
-<!-- ./configure.sh -native -->
-<!-- make -->
-<!-- make install -->
-<!-- ``` -->
+2. Set an environment variable COQBIN to the directory where Coq's
+   binaries are; for instance:
+```bash
+export COQBIN=/home/jdoe/native-coq/bin/
+```
+   (the final slash is mandatory).
+
+3. Compile and install SMTCoq by using the following commands in the src directory.
+```
+./configure.sh -native
+make
+make install
+```
 
 
 ## Installation of the provers