diff options
| author | Erik Martin-Dorel | 2019-01-29 13:29:38 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-01-29 13:29:38 +0100 |
| commit | e5ff94165ab722bfb77d4437a58d49aacc81683d (patch) | |
| tree | 085d71f53ff53dc81ef4892957b4fae5fa3b2333 /INSTALL.md | |
| parent | 6a8472fd6b9a9a31514d71c2628e2f7cfc341eaa (diff) | |
Add more libraries to CI & Update local opam doc (#272)
* Update INSTALL.md for installing mathcomp as local opam packages
This patch documents the change 1046da99d22462d6aeb23dd12043c2537f47abf1
that was required by the GitLab CI setup to be able to rely on opam 2.0.
Close #251
* Propose to bump the required version of coq in coq-mathcomp-ssreflect.opam
so the CI could use the Docker image coqorg/coq:8.9 (which is already available
albeit it currently is a synonymous of coqorg/coq:8.9-beta1 with the opam repos
coq-released + coq-core-dev + coq-extra-dev)
* [ci] Add math-comp/odd-order and coq-community/lemma-overloading jobs
Related: math-comp/math-comp#245 and math-comp/math-comp#256
Diffstat (limited to 'INSTALL.md')
| -rw-r--r-- | INSTALL.md | 26 |
1 files changed, 16 insertions, 10 deletions
@@ -12,7 +12,7 @@ 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` +eval $(opam config env) ``` Once your OPAM environment is configured you can install any math-comp package via @@ -38,7 +38,7 @@ If you want to install the library in a dedicated environment current OPAM setup you can run the following commands: ``` opam init --root=$PWD/MC -eval `opam config env --root=$PWD/MC` +eval $(opam config env --root=$PWD/MC`) ``` After that the installations instructions above apply. @@ -73,22 +73,28 @@ 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 -standard Coq repositories. +The instructions assume you are in the parent directory (that contains +this file `INSTALL.md`) and that you have OPAM installed and +configured with the standard Coq repositories. -For each package, pin the `opam` file: +First, we recommend pinning a particular version of Coq +(here `8.8.0`): ``` -opam pin -n add ssreflect +opam pin add -n coq -k version 8.8.0 +``` + +Then for each math-comp package, pin the `opam` file: ``` +opam pin add -n -k path coq-mathcomp-ssreflect . +``` + This can be achieved in one go as follows: ``` -for P in */opam; do opam pin -n add ${P%%/opam}; done +for P in *.opam; do opam pin add -n -k path ${P%.opam} .; done ``` Then you can use `opam install` to compile and install any package. For example: ``` -opam install coq.8.8.0 coq-mathcomp-ssreflect +opam install coq-mathcomp-character -j3 ``` - |