aboutsummaryrefslogtreecommitdiffstats
path: root/INSTALL.md
diff options
context:
space:
mode:
Diffstat (limited to 'INSTALL.md')
-rw-r--r--INSTALL.md65
1 files changed, 60 insertions, 5 deletions
diff --git a/INSTALL.md b/INSTALL.md
index 3a16700..0c2808d 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -13,7 +13,7 @@ You will also need to [install the provers](#installation-of-the-provers)
you want to use.
-## Installation via opam (recommended)
+## Installation of version 2.0 via opam (recommended)
### In an existing switch
@@ -21,6 +21,61 @@ You need to have OCaml version >= 4.09 and Coq >= 8.11.
Simply add the coq-extra-dev repo to opam:
```bash
+opam repo add coq-released https://coq.inria.fr/opam/released
+```
+and install SMTCoq:
+```bash
+opam install coq-smtcoq
+```
+
+### In a new switch
+
+Create a switch:
+```bash
+opam switch create ocaml-base-compiler.4.09.0
+eval $(opam env)
+```
+add the Coq repos to opam:
+```bash
+opam repo add coq-released https://coq.inria.fr/opam/released
+```
+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 of the development version via opam
+
+### In an existing switch
+
+You need to have OCaml version >= 4.09 and Coq 8.13.
+
+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:
@@ -73,7 +128,7 @@ Then follow the instructions of the previous section.
### Requirements
-You need to have OCaml version >= 4.11.1 and Coq version 8.12.*.
+You need to have OCaml version >= 4.11.1 and Coq version 8.13.*.
> **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
@@ -111,16 +166,16 @@ opam switch create ocaml-base-compiler.4.11.1
### Install Coq
-After OCaml is installed, you can install Coq-8.12.1 through opam.
+After OCaml is installed, you can install Coq-8.13.2 through opam.
```bash
-opam install coq.8.12.1
+opam install coq.8.13.2
```
If you also want to install CoqIDE at the same time you can do
```bash
-opam install coq.8.12.1 coqide.8.12.1
+opam install coq.8.13.2 coqide.8.13.2
```
but you might need to install some extra packages and libraries for your system