Merge pull request #688 from pi8027/coq-8.13

[CI/CD] support Coq 8.13

2 files changed, 54 insertions, 14 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1bb8aca..4b0d207 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -98,10 +98,8 @@ coq-8.11:
 coq-8.12:
   extends: .opam-build-once
 
-# to uncomment when 8.13+alpha available
-# coq-8.13:
-#   # to be replaced with .opam-build-once when 8.13.0 available
-#   extends: .opam-build
+coq-8.13:
+  extends: .opam-build-once
 
 coq-dev:
   extends: .opam-build
@@ -149,11 +147,10 @@ test-coq-dev:
   variables:
     COQ_VERSION: "dev"
 
-# test-coq-8.13:
-#   # to be replaced with .test-once (to disable this nightly build) when 8.13.0 is released
-#   extends: .test
-#   variables:
-#     COQ_VERSION: "8.13"
+test-coq-8.13:
+  extends: .test-once
+  variables:
+    COQ_VERSION: "8.13"
 
 test-coq-8.12:
   extends: .test-once
@@ -229,6 +226,11 @@ ci-fourcolor-8.12:
   variables:
     COQ_VERSION: "8.12"
 
+ci-fourcolor-8.13:
+  extends: .ci-fourcolor
+  variables:
+    COQ_VERSION: "8.13"
+
 ci-fourcolor-dev:
   extends: .ci-fourcolor
   variables:
@@ -259,6 +261,11 @@ ci-odd-order-8.12:
   variables:
     COQ_VERSION: "8.12"
 
+ci-odd-order-8.13:
+  extends: .ci-odd-order
+  variables:
+    COQ_VERSION: "8.13"
+
 ci-odd-order-dev:
   extends: .ci-odd-order
   variables:
@@ -289,6 +296,11 @@ ci-lemma-overloading-8.12:
   variables:
     COQ_VERSION: "8.12"
 
+ci-lemma-overloading-8.13:
+  extends: .ci-lemma-overloading
+  variables:
+    COQ_VERSION: "8.13"
+
 ci-lemma-overloading-dev:
   extends: .ci-lemma-overloading
   variables:
@@ -319,6 +331,11 @@ ci-bigenough-8.12:
   variables:
     COQ_VERSION: "8.12"
 
+ci-bigenough-8.13:
+  extends: .ci-bigenough
+  variables:
+    COQ_VERSION: "8.13"
+
 ci-bigenough-dev:
   extends: .ci-bigenough
   variables:
@@ -350,6 +367,11 @@ ci-real-closed-8.12:
   variables:
     COQ_VERSION: "8.12"
 
+ci-real-closed-8.13:
+  extends: .ci-real-closed
+  variables:
+    COQ_VERSION: "8.13"
+
 ci-real-closed-dev:
   extends: .ci-real-closed
   variables:
@@ -381,6 +403,11 @@ ci-finmap-8.12:
   variables:
     COQ_VERSION: "8.12"
 
+ci-finmap-8.13:
+  extends: .ci-finmap
+  variables:
+    COQ_VERSION: "8.13"
+
 ci-finmap-dev:
   extends: .ci-finmap
   variables:
@@ -412,6 +439,11 @@ ci-multinomials-8.12:
   variables:
     COQ_VERSION: "8.12"
 
+ci-multinomials-8.13:
+  extends: .ci-multinomials
+  variables:
+    COQ_VERSION: "8.13"
+
 ci-multinomials-dev:
   extends: .ci-multinomials
   variables:
@@ -438,6 +470,11 @@ ci-analysis-8.12:
   variables:
     COQ_VERSION: "8.12"
 
+ci-analysis-8.13:
+  extends: .ci-analysis
+  variables:
+    COQ_VERSION: "8.13"
+
 ci-analysis-dev:
   extends: .ci-analysis
   variables:
@@ -463,6 +500,11 @@ ci-fcsl-pcm-8.12:
   variables:
     COQ_VERSION: "8.12"
 
+ci-fcsl-pcm-8.13:
+  extends: .ci-fcsl-pcm
+  variables:
+    COQ_VERSION: "8.13"
+
 ci-fcsl-pcm-dev:
   extends: .ci-fcsl-pcm
   variables:
@@ -519,10 +561,8 @@ mathcomp-dev_coq-8.11:
 mathcomp-dev_coq-8.12:
   extends: .docker-deploy-once
 
-# to uncomment when 8.13+alpha available
-# mathcomp-dev_coq-8.13:
-#   # to be replaced with .docker-deploy-once when 8.13.0 available
-#   extends: .docker-deploy
+mathcomp-dev_coq-8.13:
+  extends: .docker-deploy-once
 
 mathcomp-dev_coq-dev:
   extends: .docker-deploy
diff --git a/coq-mathcomp-ssreflect.opam b/coq-mathcomp-ssreflect.opam
index 4f3f6c3..b34b7c7 100644
--- a/coq-mathcomp-ssreflect.opam
+++ b/coq-mathcomp-ssreflect.opam
@@ -9,7 +9,7 @@ license: "CECILL-B"
 
 build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ]
 install: [ make "-C" "mathcomp/ssreflect" "install" ]
-depends: [ "coq" { ((>= "8.10" & < "8.13~") | (= "dev"))} ]
+depends: [ "coq" { ((>= "8.10" & < "8.14~") | (= "dev"))} ]
 
 tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.ssreflect" ]
 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 <>" ]