diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2019-09-25 19:00:26 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2019-09-25 19:00:26 +0200 |
| commit | a1cdf710c31d11d5964ac485109188fea42902e5 (patch) | |
| tree | 5efafe78dbaef4cf469b5d0d79dd693a801c489e /INSTALL.md | |
| parent | e07d97931f05bc966b12f30790325ea25a7472f2 (diff) | |
| download | smtcoq-a1cdf710c31d11d5964ac485109188fea42902e5.tar.gz smtcoq-a1cdf710c31d11d5964ac485109188fea42902e5.zip | |
An opam package is back!
Diffstat (limited to 'INSTALL.md')
| -rw-r--r-- | INSTALL.md | 35 |
1 files changed, 18 insertions, 17 deletions
@@ -6,8 +6,9 @@ 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. -For now you have to install it from the sources. (We plan on releasing -an updated opam package soon with the latest additions.) +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. @@ -27,9 +28,21 @@ 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). +``` + + +### 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 with Coq and OCaml opam packages +### Installation from the sources, using opam (not recommended) #### Install opam @@ -90,7 +103,7 @@ make install ``` -### Installation with official Coq 8.9 release +### Installation from the sources, with official Coq 8.9 release (not recommended) 1. Download the last stable version of Coq 8.9: ```bash @@ -119,7 +132,7 @@ make install ``` -### Installation with native-coq +### 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 @@ -152,18 +165,6 @@ make install ``` -### Deprecated: installation via opam (uses Coq-8.5) - -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 of the provers To use SMTCoq, we recommend installing the following two SMT solvers: |