From 5c4328261edace427e7cad73fdca288f6d73b87d Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 18 Oct 2019 11:34:05 +0200 Subject: 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 --- .gitlab-ci.yml | 31 +++++++++++++++++++++++++++++++ coq-mathcomp-algebra.opam | 3 +-- coq-mathcomp-character.opam | 3 +-- coq-mathcomp-field.opam | 3 +-- coq-mathcomp-fingroup.opam | 3 +-- coq-mathcomp-solvable.opam | 3 +-- coq-mathcomp-ssreflect.opam | 5 ++--- 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" -- cgit v1.2.3