diff options
| author | Assia Mahboubi | 2018-03-06 14:35:07 +0100 |
|---|---|---|
| committer | GitHub | 2018-03-06 14:35:07 +0100 |
| commit | f26e353970e99ec25c540c92c9722ee4f578391b (patch) | |
| tree | d76b38798a5030e7dbf5b6dc11d300d37b79fad7 | |
| parent | 6f075b64b936de9ee4fa79ea4dc1d2fb9b9cf2c8 (diff) | |
| parent | cc518c0de948f111e3fcb1b766a1a326db9ce955 (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.md | 32 |
1 files changed, 19 insertions, 13 deletions
@@ -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 ``` + |
