From 7e09f9285a27e442134df2e752ff43d4bd2e133a Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Mon, 20 Jul 2020 11:41:21 +0200 Subject: Update installation instructions --- INSTALL.md | 113 ++++++++++++++++++++++++++++++++++--------------------------- 1 file changed, 63 insertions(+), 50 deletions(-) (limited to 'INSTALL.md') diff --git a/INSTALL.md b/INSTALL.md index e4646ae..68de1b4 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -13,27 +13,32 @@ version, see below). You will also need to [install the provers](#installation-of-the-provers) you want to use. -## Requirements -You need to have OCaml version >= 4.09.0 and Coq version 8.9.0. -The easiest way to install these two pieces of software is through opam. +## Installation via opam (recommended) -> **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 -> SMTCoq. In particular this means you want a version of Coq that was compiled -> with OCaml version >= 4.09.0. +### In an existing switch -If you want to use SMTCoq with high performance to check large proof -certificates, you need to use the [version of Coq with native -data-structures](https://github.com/smtcoq/native-coq) instead of -Coq-8.9 (warning: this allows one to use the vernacular commands but not -the tactics). +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 +``` -### Installation via opam (recommended) +### In a new switch -Simply add the coq-extra-dev repo to opam: +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: @@ -41,10 +46,48 @@ and install SMTCoq: 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.9.0. + +> **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 +> SMTCoq. In particular this means you want a version of Coq that was compiled +> with OCaml version >= 4.09.0. -### Installation from the sources, using opam (not recommended) +If you want to use SMTCoq with high performance to check large proof +certificates, you need to use the [version of Coq with native +data-structures](https://github.com/smtcoq/native-coq) instead of +Coq-8.9 (warning: this allows one to use the vernacular commands but not +the tactics). -#### 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,7 +108,7 @@ 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): @@ -73,7 +116,7 @@ Now you can install an OCaml compiler (we recommend 4.09.0): opam switch create ocaml-base-compiler.4.09.0 ``` -#### Install Coq +### Install Coq After OCaml is installed, you can install Coq-8.9.0 through opam. @@ -91,7 +134,7 @@ 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,37 +144,7 @@ make make install ``` - -### 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) +## 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 -- cgit