Add build for mathcomp/mathcomp-dev:coq-8.10 (#391)

* feat: Add build for mathcomp/mathcomp-dev:coq-8.10

* fix(coq-mathcomp-ssreflect.opam): Bump coq upper bound

* fix(*.opam): Remove "remove" directive

href: coq/opam-coq-archive#703

7 files changed, 38 insertions, 13 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 80772d1..ef0b240 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -93,6 +93,9 @@ coq-8.8:
 coq-8.9:
   extends: .opam-build-once
 
+coq-8.10:
+  extends: .opam-build-once
+
 coq-dev:
   extends: .opam-build
 
@@ -156,6 +159,11 @@ ci-fourcolor-8.9:
   variables:
     COQ_VERSION: "8.9"
 
+ci-fourcolor-8.10:
+  extends: .ci-fourcolor
+  variables:
+    COQ_VERSION: "8.10"
+
 ci-fourcolor-dev:
   extends: .ci-fourcolor
   variables:
@@ -186,6 +194,11 @@ ci-odd-order-8.9:
   variables:
     COQ_VERSION: "8.9"
 
+ci-odd-order-8.10:
+  extends: .ci-odd-order
+  variables:
+    COQ_VERSION: "8.10"
+
 ci-odd-order-dev:
   extends: .ci-odd-order
   variables:
@@ -211,6 +224,11 @@ ci-lemma-overloading-8.9:
   variables:
     COQ_VERSION: "8.9"
 
+ci-lemma-overloading-8.10:
+  extends: .ci-lemma-overloading
+  variables:
+    COQ_VERSION: "8.10"
+
 ci-lemma-overloading-dev:
   extends: .ci-lemma-overloading
   variables:
@@ -241,6 +259,11 @@ ci-bigenough-8.9:
   variables:
     COQ_VERSION: "8.9"
 
+ci-bigenough-8.9:
+  extends: .ci-bigenough
+  variables:
+    COQ_VERSION: "8.10"
+
 ci-bigenough-dev:
   extends: .ci-bigenough
   variables:
@@ -329,6 +352,11 @@ ci-finmap-8.9:
   variables:
     COQ_VERSION: "8.9"
 
+ci-finmap-8.10:
+  extends: .ci-finmap
+  variables:
+    COQ_VERSION: "8.10"
+
 ci-finmap-dev:
   extends: .ci-finmap
   variables:
@@ -380,5 +408,8 @@ mathcomp-dev:coq-8.8:
 mathcomp-dev:coq-8.9:
   extends: .docker-deploy-once
 
+mathcomp-dev:coq-8.10:
+  extends: .docker-deploy-once
+
 mathcomp-dev:coq-dev:
   extends: .docker-deploy
diff --git a/coq-mathcomp-algebra.opam b/coq-mathcomp-algebra.opam
index 6fa40cc..c6c5568 100644
--- a/coq-mathcomp-algebra.opam
+++ b/coq-mathcomp-algebra.opam
@@ -10,10 +10,9 @@ license: "CeCILL-B"
 
 build: [ make "-C" "mathcomp/algebra" "-j" "%{jobs}%" ]
 install: [ make "-C" "mathcomp/algebra" "install" ]
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/algebra'" ]
 depends: [ "coq-mathcomp-fingroup" { = "dev" } ]
 
-tags: [ "keyword:algebra" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
+tags: [ "keyword:algebra" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.algebra" ]
 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 <>" ]
 
 synopsis: "Mathematical Components Library on Algebra"
diff --git a/coq-mathcomp-character.opam b/coq-mathcomp-character.opam
index a5eb54b..4e64b60 100644
--- a/coq-mathcomp-character.opam
+++ b/coq-mathcomp-character.opam
@@ -10,10 +10,9 @@ license: "CeCILL-B"
 
 build: [ make "-C" "mathcomp/character" "-j" "%{jobs}%" ]
 install: [ make "-C" "mathcomp/character" "install" ]
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/character'" ]
 depends: [ "coq-mathcomp-field" { = "dev" } ]
 
-tags: [ "keyword:algebra" "keyword:character" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
+tags: [ "keyword:algebra" "keyword:character" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.character" ]
 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 <>" ]
 
 synopsis: "Mathematical Components Library on character theory"
diff --git a/coq-mathcomp-field.opam b/coq-mathcomp-field.opam
index a72eeb2..bdde3ce 100644
--- a/coq-mathcomp-field.opam
+++ b/coq-mathcomp-field.opam
@@ -10,10 +10,9 @@ license: "CeCILL-B"
 
 build: [ make "-C" "mathcomp/field" "-j" "%{jobs}%" ]
 install: [ make "-C" "mathcomp/field" "install" ]
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/field'" ]
 depends: [ "coq-mathcomp-solvable" { = "dev" } ]
 
-tags: [ "keyword:algebra" "keyword:field" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
+tags: [ "keyword:algebra" "keyword:field" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.field" ]
 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 <>" ]
 
 synopsis: "Mathematical Components Library on Fields"
diff --git a/coq-mathcomp-fingroup.opam b/coq-mathcomp-fingroup.opam
index 2a215d0..3e39c4e 100644
--- a/coq-mathcomp-fingroup.opam
+++ b/coq-mathcomp-fingroup.opam
@@ -10,10 +10,9 @@ license: "CeCILL-B"
 
 build: [ make "-C" "mathcomp/fingroup" "-j" "%{jobs}%" ]
 install: [ make "-C" "mathcomp/fingroup" "install" ]
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/fingroup'" ]
 depends: [ "coq-mathcomp-ssreflect" { = "dev" } ]
 
-tags: [ "keyword:finite groups" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
+tags: [ "keyword:finite groups" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.fingroup" ]
 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 <>" ]
 
 synopsis: "Mathematical Components Library on finite groups"
diff --git a/coq-mathcomp-solvable.opam b/coq-mathcomp-solvable.opam
index 68fcea8..ac561a5 100644
--- a/coq-mathcomp-solvable.opam
+++ b/coq-mathcomp-solvable.opam
@@ -10,10 +10,9 @@ license: "CeCILL-B"
 
 build: [ make "-C" "mathcomp/solvable" "-j" "%{jobs}%" ]
 install: [ make "-C" "mathcomp/solvable"  "install" ]
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/solvable'" ]
 depends: [ "coq-mathcomp-algebra" { = "dev" } ]
 
-tags: [ "keyword:finite groups" "keyword:Feit Thompson theorem" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
+tags: [ "keyword:finite groups" "keyword:Feit Thompson theorem" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.solvable" ]
 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 <>" ]
 
 synopsis: "Mathematical Components Library on finite groups (II)"
diff --git a/coq-mathcomp-ssreflect.opam b/coq-mathcomp-ssreflect.opam
index 8068c6e..28b9e31 100644
--- a/coq-mathcomp-ssreflect.opam
+++ b/coq-mathcomp-ssreflect.opam
@@ -10,10 +10,9 @@ 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.7" & < "8.10~") | (= "dev"))} ]
+depends: [ "coq" { ((>= "8.7" & < "8.11~") | (= "dev"))} ]
 
-tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
+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 <>" ]
 
 synopsis: "Small Scale Reflection"