From 76559870c8a81a9e3ba3f1242e60ff8e5f53c03a Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 22 Mar 2019 22:17:54 +0100
Subject: Detail: Print a more legible description for the cloned external
 libraries

---
 .gitlab-ci.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index d326aae..3177724 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -112,6 +112,7 @@ coq-dev:
     - git clone -b "${CONTRIB_VERSION}" --depth 1 "${CONTRIB_URL}" /home/coq/ci
     - cd /home/coq/ci
     - git rev-parse --verify HEAD
+    - git describe --all --long --abbrev=40 --always --dirty
   except:
     - tags
     - merge_requests
-- 
cgit v1.2.3


From c11764ca767ce6c306fef3892a78f0114e5e818c Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 22 Mar 2019 03:39:46 +0100
Subject: [ci] Add tests with more libraries

- coq-mathcomp-odd-order.dev + coq.dev
- coq-mathcomp-bigenough.dev, coq-{8.7, 8.8, 8.9, dev}
- coq-mathcomp-finmap.dev, coq-{8.7, 8.8, 8.9, dev}

The configs below are commented-out as the upstream repos' opam is not
yet marked as compatible with mathcomp.dev (and Travis CI doesn't test
it with mathcomp-dev images)

 # - coq-mathcomp-real-closed.dev, coq-{8.7, 8.8, 8.9, dev}
 # - coq-mathcomp-analysis.dev, coq-{8.8, 8.9, dev}

Close math-comp/math-comp#245
---
 .gitlab-ci.yml | 123 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 123 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3177724..3eae6fa 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -163,6 +163,11 @@ ci-odd-order-8.7:
   variables:
     COQ_VERSION: "8.7"
 
+ci-odd-order-dev:
+  extends: .ci-odd-order
+  variables:
+    COQ_VERSION: "dev"
+
 # The Lemma Overloading library
 .ci-lemma-overloading:
   extends: .ci
@@ -188,6 +193,124 @@ ci-lemma-overloading-dev:
   variables:
     COQ_VERSION: "dev"
 
+# The bigenough library (will be later subsumed by near)
+.ci-bigenough:
+  extends: .ci
+  variables:
+    CONTRIB_URL: "https://github.com/math-comp/bigenough.git"
+    CONTRIB_VERSION: master
+  script:
+    - opam pin add -n -k path coq-mathcomp-bigenough .
+    - opam install -y -v -j "${NJOBS}" coq-mathcomp-bigenough
+
+ci-bigenough-8.7:
+  extends: .ci-bigenough
+  variables:
+    COQ_VERSION: "8.7"
+
+ci-bigenough-8.8:
+  extends: .ci-bigenough
+  variables:
+    COQ_VERSION: "8.8"
+
+ci-bigenough-8.9:
+  extends: .ci-bigenough
+  variables:
+    COQ_VERSION: "8.9"
+
+ci-bigenough-dev:
+  extends: .ci-bigenough
+  variables:
+    COQ_VERSION: "dev"
+
+# # The real-closed library
+# .ci-real-closed:
+#   extends: .ci
+#   variables:
+#     CONTRIB_URL: "https://github.com/math-comp/real-closed.git"
+#     CONTRIB_VERSION: master
+#   script:
+#     - opam pin add -n -k path coq-mathcomp-real-closed .
+#     - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-real-closed
+#     - opam install -y -v -j "${NJOBS}" coq-mathcomp-real-closed
+# 
+# ci-real-closed-8.7:
+#   extends: .ci-real-closed
+#   variables:
+#     COQ_VERSION: "8.7"
+# 
+# ci-real-closed-8.8:
+#   extends: .ci-real-closed
+#   variables:
+#     COQ_VERSION: "8.8"
+# 
+# ci-real-closed-8.9:
+#   extends: .ci-real-closed
+#   variables:
+#     COQ_VERSION: "8.9"
+# 
+# ci-real-closed-dev:
+#   extends: .ci-real-closed
+#   variables:
+#     COQ_VERSION: "dev"
+# 
+# # The analysis library
+# .ci-analysis:
+#   extends: .ci
+#   variables:
+#     CONTRIB_URL: "https://github.com/math-comp/analysis.git"
+#     CONTRIB_VERSION: master
+#   script:
+#     - opam pin add -n -k path coq-mathcomp-analysis .
+#     - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-analysis
+#     - opam install -y -v -j "${NJOBS}" coq-mathcomp-analysis
+# 
+# ci-analysis-8.8:
+#   extends: .ci-analysis
+#   variables:
+#     COQ_VERSION: "8.8"
+# 
+# ci-analysis-8.9:
+#   extends: .ci-analysis
+#   variables:
+#     COQ_VERSION: "8.9"
+# 
+# ci-analysis-dev:
+#   extends: .ci-analysis
+#   variables:
+#     COQ_VERSION: "dev"
+
+# The finmap library
+.ci-finmap:
+  extends: .ci
+  variables:
+    CONTRIB_URL: "https://github.com/math-comp/finmap.git"
+    CONTRIB_VERSION: master
+  script:
+    - opam pin add -n -k path coq-mathcomp-finmap .
+    - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-finmap
+    - opam install -y -v -j "${NJOBS}" coq-mathcomp-finmap
+
+ci-finmap-8.7:
+  extends: .ci-finmap
+  variables:
+    COQ_VERSION: "8.7"
+
+ci-finmap-8.8:
+  extends: .ci-finmap
+  variables:
+    COQ_VERSION: "8.8"
+
+ci-finmap-8.9:
+  extends: .ci-finmap
+  variables:
+    COQ_VERSION: "8.9"
+
+ci-finmap-dev:
+  extends: .ci-finmap
+  variables:
+    COQ_VERSION: "dev"
+
 ################
 ### deploy stage
 ################
-- 
cgit v1.2.3