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

3 files changed, 62 insertions, 12 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b8c9c8f..aa05051 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -4,7 +4,7 @@
 #     (Dockerfile containing: "opam switch set $compiler && eval $(opam env)")
 #   - master (protected branch) => push on GitLab registry and Docker Hub
 #   - other branches (not tags) => push on GitLab registry
-#   - Todo: GitHub PRs => push on GitLab
+#   - GitHub PRs => push on GitLab and report back thanks to @coqbot
 # - test stage (image: mathcomp-dev:$IID_$SLUG_coq-8.6)
 #   - script template foreach project (custom CONTRIB_URL, script)
 #   - jobs foreach project and Coq version (custom COQ_VERSION, CONTRIB_VERSION)
@@ -67,6 +67,9 @@ coq-8.7:
 coq-8.8:
   extends: .opam-build
 
+coq-8.9:
+  extends: .opam-build
+
 coq-dev:
   extends: .opam-build
 
@@ -117,6 +120,7 @@ make-coq-latest:
 # - Add 1 job per Coq version to test, that extends the previous hidden job,
 #   and sets vars COQ_VERSION, CONTRIB_VERSION (compatible Git branch/tag)
 
+# The Four Color Theorem
 .ci-fourcolor:
   extends: .ci
   variables:
@@ -146,3 +150,43 @@ ci-fourcolor-dev:
   extends: .ci-fourcolor
   variables:
     COQ_VERSION: "dev"
+
+# The Odd Order Theorem
+.ci-odd-order:
+  extends: .ci
+  variables:
+    CONTRIB_URL: "https://github.com/math-comp/odd-order.git"
+    CONTRIB_VERSION: master
+  script:
+    - make -j "${NJOBS}"
+    - make install
+
+ci-odd-order-8.7:
+  extends: .ci-odd-order
+  variables:
+    COQ_VERSION: "8.7"
+
+# The Lemma Overloading library
+.ci-lemma-overloading:
+  extends: .ci
+  variables:
+    CONTRIB_URL: "https://github.com/coq-community/lemma-overloading.git"
+    CONTRIB_VERSION: master
+  script:
+    - opam pin add -n -k path coq-lemma-overloading .
+    - opam install -y -v -j "${NJOBS}" coq-lemma-overloading
+
+ci-lemma-overloading-8.8:
+  extends: .ci-lemma-overloading
+  variables:
+    COQ_VERSION: "8.8"
+
+ci-lemma-overloading-8.9:
+  extends: .ci-lemma-overloading
+  variables:
+    COQ_VERSION: "8.9"
+
+ci-lemma-overloading-dev:
+  extends: .ci-lemma-overloading
+  variables:
+    COQ_VERSION: "dev"
diff --git a/INSTALL.md b/INSTALL.md
index 8857dad..3167b1a 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -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
 ```
-
diff --git a/coq-mathcomp-ssreflect.opam b/coq-mathcomp-ssreflect.opam
index 5d31846..a018a3e 100644
--- a/coq-mathcomp-ssreflect.opam
+++ b/coq-mathcomp-ssreflect.opam
@@ -12,7 +12,7 @@ license: "CeCILL-B"
 build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ]
 install: [ make "-C" "mathcomp/ssreflect" "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp'" ]
-depends: [ "coq" { ((>= "8.6" & < "8.9~") | (= "dev"))} ]
+depends: [ "coq" { ((>= "8.6" & < "8.10~") | (= "dev"))} ]
 
 tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
 authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]