aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAssia Mahboubi2018-03-06 14:35:07 +0100
committerGitHub2018-03-06 14:35:07 +0100
commitf26e353970e99ec25c540c92c9722ee4f578391b (patch)
treed76b38798a5030e7dbf5b6dc11d300d37b79fad7
parent6f075b64b936de9ee4fa79ea4dc1d2fb9b9cf2c8 (diff)
parentcc518c0de948f111e3fcb1b766a1a326db9ce955 (diff)
Merge pull request #186 from anton-trunov/add-dev-repo-to-install
[doc] Add instructions for dev version installation via OPAM
-rw-r--r--INSTALL.md32
1 files changed, 19 insertions, 13 deletions
diff --git a/INSTALL.md b/INSTALL.md
index 9752f0f..d9a74fd 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -3,28 +3,33 @@
The library is divided into packages which group together related
files. Each package defines a distribution and compilation unit.
-Packages can be compiled using the traditional `make` utility or
-the more recent `OPAM` one. The released and current dev version are
-also available as opam packages.
+Packages can be compiled using the traditional make utility or
+the more recent OPAM one. The released and current dev versions are
+also available as OPAM packages.
## Compilation and installation of released and current dev version with OPAM
-If you just installed opam you may have to do the following. You may also want
-to read opam user manual first https://opam.ocaml.org/doc/Usage.html
+If you just installed OPAM you may have to do the following. You may also want
+to read [OPAM user manual](https://opam.ocaml.org/doc/Usage.html) first.
```
opam init
eval `opam config env`
```
-Once your opam envionement is configure you can install any math-comp package via
+Once your OPAM environment is configured
+you can install any math-comp package via
```
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin add -n coq -k version 8.7.0
opam install coq -j3
opam install coq-mathcomp-ssreflect.1.6.4 -j3
```
-Replace `ssreflect` here by the package you want, dependencies will be
-installed automatically. You can replace `1.6.4` by `dev` to get the last
-development version. We recommand to pin a particular version of Coq
+Replace `ssreflect` here by the package you want, the dependencies will be
+installed automatically. We recommend pinning a particular version of Coq
(here `8.7.0`).
+To get the latest development version you need to execute the following:
+```
+opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
+opam install coq-mathcomp-ssreflect.dev -j3
+```
## Compilation and installation with make
@@ -34,13 +39,13 @@ The list of Coq versions that are known to work can be obtained with:
```
ls ssreflect/plugin/
```
-Alternatively, if you are familiar with the `OPAM` slang:
+Alternatively, if you are familiar with the OPAM slang:
```
grep depends: ssreflect/opam
```
-If `coqc` is in your `PATH`, then you are good to go. Alternatively you
-can export the `COQBIN` variable to tell make where the `coqc` binary is:
+If `coqc` is in your `PATH`, then you are good to go. Alternatively, you
+can export the `COQBIN` variable to tell `make` where the `coqc` binary is:
```
export COQBIN=/home/gares/COQ/coq/bin/
```
@@ -62,7 +67,7 @@ To install the compiled library, just execute `make install`.
## Compilation and installation of a custom version using OPAM
The instructions assume you are in the `mathcomp` directory
-and that you have `OPAM` installed and configured with the
+and that you have OPAM installed and configured with the
standard Coq repositories.
For each package, pin the `opam` file:
@@ -79,3 +84,4 @@ For example:
```
opam install coq.8.7.0 coq-mathcomp-ssreflect
```
+