From 1046da99d22462d6aeb23dd12043c2537f47abf1 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 20 Dec 2018 17:36:24 +0100 Subject: Move-and-rename opam files to the root folder * (Update make's path accordingly) * This patch is required for opam 2.0 pinning * As a result, these *.opam files are now similar to the opam files in https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-mathcomp-*/coq-mathcomp-*.dev/ --- coq-mathcomp-algebra.opam | 17 +++++++++++++++++ coq-mathcomp-character.opam | 17 +++++++++++++++++ coq-mathcomp-field.opam | 17 +++++++++++++++++ coq-mathcomp-fingroup.opam | 17 +++++++++++++++++ coq-mathcomp-solvable.opam | 17 +++++++++++++++++ coq-mathcomp-ssreflect.opam | 17 +++++++++++++++++ mathcomp/algebra/opam | 17 ----------------- mathcomp/character/opam | 17 ----------------- mathcomp/field/opam | 17 ----------------- mathcomp/fingroup/opam | 17 ----------------- mathcomp/solvable/opam | 17 ----------------- mathcomp/ssreflect/opam | 17 ----------------- 12 files changed, 102 insertions(+), 102 deletions(-) create mode 100644 coq-mathcomp-algebra.opam create mode 100644 coq-mathcomp-character.opam create mode 100644 coq-mathcomp-field.opam create mode 100644 coq-mathcomp-fingroup.opam create mode 100644 coq-mathcomp-solvable.opam create mode 100644 coq-mathcomp-ssreflect.opam delete mode 100644 mathcomp/algebra/opam delete mode 100644 mathcomp/character/opam delete mode 100644 mathcomp/field/opam delete mode 100644 mathcomp/fingroup/opam delete mode 100644 mathcomp/solvable/opam delete mode 100644 mathcomp/ssreflect/opam diff --git a/coq-mathcomp-algebra.opam b/coq-mathcomp-algebra.opam new file mode 100644 index 0000000..b466385 --- /dev/null +++ b/coq-mathcomp-algebra.opam @@ -0,0 +1,17 @@ +opam-version: "1.2" +name: "coq-mathcomp-algebra" +version: "dev" +maintainer: "Mathematical Components " + +homepage: "https://math-comp.github.io/math-comp/" +bug-reports: "Mathematical Components " +dev-repo: "https://github.com/math-comp/math-comp.git" +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" ] +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 <>" ] diff --git a/coq-mathcomp-character.opam b/coq-mathcomp-character.opam new file mode 100644 index 0000000..684e450 --- /dev/null +++ b/coq-mathcomp-character.opam @@ -0,0 +1,17 @@ +opam-version: "1.2" +name: "coq-mathcomp-character" +version: "dev" +maintainer: "Mathematical Components " + +homepage: "https://math-comp.github.io/math-comp/" +bug-reports: "Mathematical Components " +dev-repo: "https://github.com/math-comp/math-comp.git" +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" ] +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 <>" ] diff --git a/coq-mathcomp-field.opam b/coq-mathcomp-field.opam new file mode 100644 index 0000000..5c31290 --- /dev/null +++ b/coq-mathcomp-field.opam @@ -0,0 +1,17 @@ +opam-version: "1.2" +name: "coq-mathcomp-field" +version: "dev" +maintainer: "Mathematical Components " + +homepage: "https://math-comp.github.io/math-comp/" +bug-reports: "Mathematical Components " +dev-repo: "https://github.com/math-comp/math-comp.git" +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" ] +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 <>" ] diff --git a/coq-mathcomp-fingroup.opam b/coq-mathcomp-fingroup.opam new file mode 100644 index 0000000..2c741b7 --- /dev/null +++ b/coq-mathcomp-fingroup.opam @@ -0,0 +1,17 @@ +opam-version: "1.2" +name: "coq-mathcomp-fingroup" +version: "dev" +maintainer: "Mathematical Components " + +homepage: "https://math-comp.github.io/math-comp/" +bug-reports: "Mathematical Components " +dev-repo: "https://github.com/math-comp/math-comp.git" +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" ] +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 <>" ] diff --git a/coq-mathcomp-solvable.opam b/coq-mathcomp-solvable.opam new file mode 100644 index 0000000..736d5bc --- /dev/null +++ b/coq-mathcomp-solvable.opam @@ -0,0 +1,17 @@ +opam-version: "1.2" +name: "coq-mathcomp-solvable" +version: "dev" +maintainer: "Mathematical Components " + +homepage: "https://math-comp.github.io/math-comp/" +bug-reports: "Mathematical Components " +dev-repo: "https://github.com/math-comp/math-comp.git" +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" ] +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 <>" ] diff --git a/coq-mathcomp-ssreflect.opam b/coq-mathcomp-ssreflect.opam new file mode 100644 index 0000000..d5052f8 --- /dev/null +++ b/coq-mathcomp-ssreflect.opam @@ -0,0 +1,17 @@ +opam-version: "1.2" +name: "coq-mathcomp-ssreflect" +version: "dev" +maintainer: "Mathematical Components " + +homepage: "https://math-comp.github.io/math-comp/" +bug-reports: "Mathematical Components " +dev-repo: "https://github.com/math-comp/math-comp.git" +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"))} ] + +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 <>" ] diff --git a/mathcomp/algebra/opam b/mathcomp/algebra/opam deleted file mode 100644 index e60cdc2..0000000 --- a/mathcomp/algebra/opam +++ /dev/null @@ -1,17 +0,0 @@ -opam-version: "1.2" -name: "coq-mathcomp-algebra" -version: "dev" -maintainer: "Mathematical Components " - -homepage: "https://math-comp.github.io/math-comp/" -bug-reports: "Mathematical Components " -dev-repo: "https://github.com/math-comp/math-comp.git" -license: "CeCILL-B" - -build: [ make "-j" "%{jobs}%" ] -install: [ make "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" ] -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 <>" ] diff --git a/mathcomp/character/opam b/mathcomp/character/opam deleted file mode 100644 index 0f3dcf1..0000000 --- a/mathcomp/character/opam +++ /dev/null @@ -1,17 +0,0 @@ -opam-version: "1.2" -name: "coq-mathcomp-character" -version: "dev" -maintainer: "Mathematical Components " - -homepage: "https://math-comp.github.io/math-comp/" -bug-reports: "Mathematical Components " -dev-repo: "https://github.com/math-comp/math-comp.git" -license: "CeCILL-B" - -build: [ make "-j" "%{jobs}%" ] -install: [ make "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" ] -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 <>" ] diff --git a/mathcomp/field/opam b/mathcomp/field/opam deleted file mode 100644 index 2624714..0000000 --- a/mathcomp/field/opam +++ /dev/null @@ -1,17 +0,0 @@ -opam-version: "1.2" -name: "coq-mathcomp-field" -version: "dev" -maintainer: "Mathematical Components " - -homepage: "https://math-comp.github.io/math-comp/" -bug-reports: "Mathematical Components " -dev-repo: "https://github.com/math-comp/math-comp.git" -license: "CeCILL-B" - -build: [ make "-j" "%{jobs}%" ] -install: [ make "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" ] -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 <>" ] diff --git a/mathcomp/fingroup/opam b/mathcomp/fingroup/opam deleted file mode 100644 index 862c2f1..0000000 --- a/mathcomp/fingroup/opam +++ /dev/null @@ -1,17 +0,0 @@ -opam-version: "1.2" -name: "coq-mathcomp-fingroup" -version: "dev" -maintainer: "Mathematical Components " - -homepage: "https://math-comp.github.io/math-comp/" -bug-reports: "Mathematical Components " -dev-repo: "https://github.com/math-comp/math-comp.git" -license: "CeCILL-B" - -build: [ make "-j" "%{jobs}%" ] -install: [ make "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" ] -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 <>" ] diff --git a/mathcomp/solvable/opam b/mathcomp/solvable/opam deleted file mode 100644 index 6e0bd16..0000000 --- a/mathcomp/solvable/opam +++ /dev/null @@ -1,17 +0,0 @@ -opam-version: "1.2" -name: "coq-mathcomp-solvable" -version: "dev" -maintainer: "Mathematical Components " - -homepage: "https://math-comp.github.io/math-comp/" -bug-reports: "Mathematical Components " -dev-repo: "https://github.com/math-comp/math-comp.git" -license: "CeCILL-B" - -build: [ make "-j" "%{jobs}%" ] -install: [ make "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" ] -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 <>" ] diff --git a/mathcomp/ssreflect/opam b/mathcomp/ssreflect/opam deleted file mode 100644 index c0ee83b..0000000 --- a/mathcomp/ssreflect/opam +++ /dev/null @@ -1,17 +0,0 @@ -opam-version: "1.2" -name: "coq-mathcomp-ssreflect" -version: "dev" -maintainer: "Mathematical Components " - -homepage: "https://math-comp.github.io/math-comp/" -bug-reports: "Mathematical Components " -dev-repo: "https://github.com/math-comp/math-comp.git" -license: "CeCILL-B" - -build: [ make "-j" "%{jobs}%" ] -install: [ make "install" ] -remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp'" ] -depends: [ "coq" { ((>= "8.6" & < "8.9~") | (= "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 <>" ] -- cgit v1.2.3 From 6fd03806214dccc7b54915da32299b9d6e64e5c7 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 20 Dec 2018 17:10:49 +0100 Subject: Avoid a warning regarding opam files """ Failed checks on coq-mathcomp-ssreflect package definition from source at file:///home/coq/mathcomp/ssreflect: error 57: Synopsis and description must not be both empty """ --- coq-mathcomp-algebra.opam | 1 + coq-mathcomp-character.opam | 1 + coq-mathcomp-field.opam | 1 + coq-mathcomp-fingroup.opam | 1 + coq-mathcomp-solvable.opam | 1 + coq-mathcomp-ssreflect.opam | 1 + 6 files changed, 6 insertions(+) diff --git a/coq-mathcomp-algebra.opam b/coq-mathcomp-algebra.opam index b466385..7cc4946 100644 --- a/coq-mathcomp-algebra.opam +++ b/coq-mathcomp-algebra.opam @@ -2,6 +2,7 @@ opam-version: "1.2" name: "coq-mathcomp-algebra" version: "dev" maintainer: "Mathematical Components " +synopsis: "The Mathematical Components library" homepage: "https://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " diff --git a/coq-mathcomp-character.opam b/coq-mathcomp-character.opam index 684e450..47c72a7 100644 --- a/coq-mathcomp-character.opam +++ b/coq-mathcomp-character.opam @@ -2,6 +2,7 @@ opam-version: "1.2" name: "coq-mathcomp-character" version: "dev" maintainer: "Mathematical Components " +synopsis: "The Mathematical Components library" homepage: "https://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " diff --git a/coq-mathcomp-field.opam b/coq-mathcomp-field.opam index 5c31290..e823f93 100644 --- a/coq-mathcomp-field.opam +++ b/coq-mathcomp-field.opam @@ -2,6 +2,7 @@ opam-version: "1.2" name: "coq-mathcomp-field" version: "dev" maintainer: "Mathematical Components " +synopsis: "The Mathematical Components library" homepage: "https://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " diff --git a/coq-mathcomp-fingroup.opam b/coq-mathcomp-fingroup.opam index 2c741b7..57d3a95 100644 --- a/coq-mathcomp-fingroup.opam +++ b/coq-mathcomp-fingroup.opam @@ -2,6 +2,7 @@ opam-version: "1.2" name: "coq-mathcomp-fingroup" version: "dev" maintainer: "Mathematical Components " +synopsis: "The Mathematical Components library" homepage: "https://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " diff --git a/coq-mathcomp-solvable.opam b/coq-mathcomp-solvable.opam index 736d5bc..f238333 100644 --- a/coq-mathcomp-solvable.opam +++ b/coq-mathcomp-solvable.opam @@ -2,6 +2,7 @@ opam-version: "1.2" name: "coq-mathcomp-solvable" version: "dev" maintainer: "Mathematical Components " +synopsis: "The Mathematical Components library" homepage: "https://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " diff --git a/coq-mathcomp-ssreflect.opam b/coq-mathcomp-ssreflect.opam index d5052f8..5d31846 100644 --- a/coq-mathcomp-ssreflect.opam +++ b/coq-mathcomp-ssreflect.opam @@ -2,6 +2,7 @@ opam-version: "1.2" name: "coq-mathcomp-ssreflect" version: "dev" maintainer: "Mathematical Components " +synopsis: "The Mathematical Components library" homepage: "https://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " -- cgit v1.2.3 From 036e10fc07ca816e9c0587e2bde55a2928c37388 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 20 Dec 2018 16:31:39 +0100 Subject: Add .dockerignore (partly whitelist-based, partly like .gitignore) --- .dockerignore | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 .dockerignore diff --git a/.dockerignore b/.dockerignore new file mode 100644 index 0000000..82209d9 --- /dev/null +++ b/.dockerignore @@ -0,0 +1,36 @@ +* +# Begin files referenced by symlinks +!README.md +!AUTHORS +!INSTALL.md +!CeCILL-B +# End files referenced by symlinks +!*.opam +!plugin +!mathcomp + +**/*.d +**/*.vo +**/*.vio +**/*.cm* +**/*~ +**/*.glob +**/*.aux +**/*.a +**/*.o +**/*# +**/Make*.coq +**/Make*.coq.bak +**/Make*.coq.conf +mathcomp/ssreflect/ssreflect.ml4 +mathcomp/ssreflect/ssrmatching.ml4 +mathcomp/ssreflect/ssrmatching.mli +# mathcomp/ssreflect/ssrmatching.v +mathcomp/ssreflect/ssreflect_plugin.mllib +mathcomp/ssreflect/ssreflect_plugin.mlpack +mathcomp/ssreflect.ml4 +mathcomp/ssrmatching.ml4 +mathcomp/ssrmatching.mli +mathcomp/ssrmatching.v +mathcomp/ssreflect_plugin.mllib +mathcomp/ssreflect_plugin.mlpack -- cgit v1.2.3 From 25630e23f09cd9c1b4b8bb9dbb2b3172111a92f1 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 20 Dec 2018 01:36:37 +0100 Subject: Add Dockerfile to build mathcomp using its opam files --- Dockerfile | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 Dockerfile diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 0000000..58f2d12 --- /dev/null +++ b/Dockerfile @@ -0,0 +1,33 @@ +ARG coq_image="coqorg/coq:dev" +FROM ${coq_image} + +ENV MATHCOMP_VERSION="dev" +ENV MATHCOMP_PACKAGE="coq-mathcomp-character" + +WORKDIR /home/coq/mathcomp + +COPY . . + +ARG compiler="base" +# other possible value: "edge" + +RUN ["/bin/bash", "--login", "-c", "set -x \ + && declare -A switch_table \ + && switch_table=( [\"base\"]=\"${COMPILER}\" [\"edge\"]=\"${COMPILER_EDGE}\" ) \ + && compiler=\"${switch_table[${compiler}]}\" \ + && [ -n \"$compiler\" ] \ + && opam switch set ${compiler} \ + && eval $(opam env) \ + && opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev \ + && opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev \ + && opam update -y \ + && opam config list && opam repo list && opam list && coqc --version \ + && sudo chown -R coq:coq /home/coq/mathcomp \ + && opam pin add -n -k path coq-mathcomp-ssreflect . \ + && opam pin add -n -k path coq-mathcomp-fingroup . \ + && opam pin add -n -k path coq-mathcomp-algebra . \ + && opam pin add -n -k path coq-mathcomp-solvable . \ + && opam pin add -n -k path coq-mathcomp-field . \ + && opam pin add -n -k path coq-mathcomp-character . \ + && opam install -y -v -j ${NJOBS} coq-mathcomp-character \ + && opam clean -a -c -s --logs"] -- cgit v1.2.3 From 3b654a62d7938e674e99a6bfd3823016db067bee Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 20 Dec 2018 15:42:02 +0100 Subject: Add Docker-based GitLab CI configuration * Design: - build stage (e.g. docker build -t mathcomp-dev:$IID_$SLUG_coq-8.6 .) - choice of the OCaml compiler: var OPAM_SWITCH in {base, edge} (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 - 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) * Config for protected branches: - set vars HUB_REGISTRY, HUB_REGISTRY_USER, HUB_REGISTRY_IMAGE, HUB_TOKEN * Remark: - The name chosen for branches should ideally yield different values of CI_COMMIT_REF_SLUG. - But this is not mandatory as image tags start with "${CI_PIPELINE_IID}_". cf. doc: - CI_COMMIT_REF_NAME: The branch or tag name for which project is built. - CI_COMMIT_REF_SLUG: $CI_COMMIT_REF_NAME lowercased, shortened to 63 bytes, and with everything except 0-9 and a-z replaced with -. No leading / trailing -. Use in URLs, host names and domain names. - CI_PIPELINE_IID: The unique id of the current pipeline scoped to project. --- .gitlab-ci.yml | 126 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 126 insertions(+) create mode 100644 .gitlab-ci.yml diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml new file mode 100644 index 0000000..574a3b2 --- /dev/null +++ b/.gitlab-ci.yml @@ -0,0 +1,126 @@ +# Design: +# - build stage (e.g. docker build -t mathcomp-dev:$IID_$SLUG_coq-8.6 .) +# - choice of the OCaml compiler: var OPAM_SWITCH in {base, edge} +# (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 +# - 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) +# +# Config for protected branches: +# - set vars HUB_REGISTRY, HUB_REGISTRY_USER, HUB_REGISTRY_IMAGE, HUB_TOKEN +# +# Remark: +# - The name chosen for branches should ideally yield different values +# of CI_COMMIT_REF_SLUG. +# - But this is not mandatory as image tags start with "${CI_PIPELINE_IID}_". +# cf. doc: +# - CI_COMMIT_REF_NAME: The branch or tag name for which project is built. +# - CI_COMMIT_REF_SLUG: $CI_COMMIT_REF_NAME lowercased, shortened to 63 bytes, +# and with everything except 0-9 and a-z replaced with -. +# No leading / trailing -. Use in URLs, host names and domain names. +# - CI_PIPELINE_IID: The unique id of the current pipeline scoped to project. + +stages: + - build + - test + +# set var OPAM_SWITCH (if need be) when using +.build: + stage: build + image: docker:latest + services: + - docker:dind + variables: + IMAGE: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}_${CI_JOB_NAME}" + HUB_IMAGE: "${HUB_REGISTRY_IMAGE}:${CI_JOB_NAME}" + OPAM_SWITCH: "edge" + before_script: + - echo "${CI_JOB_TOKEN}" | docker login -u "${CI_REGISTRY_USER}" --password-stdin "${CI_REGISTRY}" + script: + - docker build --pull --build-arg=coq_image="coqorg/${CI_JOB_NAME//-/:}" --build-arg=compiler="${OPAM_SWITCH}" -t "${IMAGE}" . + - docker push "${IMAGE}" + - docker logout "${CI_REGISTRY}" + - | + if [ -n "${HUB_REGISTRY_IMAGE}" ]; then + set -e + echo "${HUB_TOKEN}" | docker login -u "${HUB_REGISTRY_USER}" --password-stdin "${HUB_REGISTRY}" + docker tag "${IMAGE}" "${HUB_IMAGE}" + docker push "${HUB_IMAGE}" + docker logout "${HUB_REGISTRY}" + set +e + fi + except: + - tags + - merge_requests + +coq-8.6: + extends: .build + variables: + OPAM_SWITCH: "base" + +coq-8.7: + extends: .build + +coq-8.8: + extends: .build + +coq-dev: + extends: .build + +# set CONTRIB_URL, script, COQ_VERSION, CONTRIB_VERSION when using +.ci: + stage: test + image: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}_coq-${COQ_VERSION}" + variables: + GIT_STRATEGY: none + before_script: + - cat /proc/{cpu,mem}info || true + # don't printenv if there are private tokens + - opam config list + - opam repo list + - opam list + - coqc --version + - git clone -b "${CONTRIB_VERSION}" --depth 1 "${CONTRIB_URL}" /home/coq/ci + - cd /home/coq/ci + except: + - tags + - merge_requests + +# Guidelines to add a library to mathcomp CI: +# - Add a hidden job (starting with a .) .ci-lib that extends the .ci job, +# sets var CONTRIB_URL (library Git URL), and defines a dedicated script +# - 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) + +.ci-fourcolor: + extends: .ci + variables: + CONTRIB_URL: "https://github.com/math-comp/fourcolor.git" + CONTRIB_VERSION: master + script: + - make -j "${NJOBS}" + - make install + +ci-fourcolor-8.6: + extends: .ci-fourcolor + variables: + COQ_VERSION: "8.6" + # CONTRIB_VERSION: "v8.6" + +ci-fourcolor-8.7: + extends: .ci-fourcolor + variables: + COQ_VERSION: "8.7" + +ci-fourcolor-8.8: + extends: .ci-fourcolor + variables: + COQ_VERSION: "8.8" + +ci-fourcolor-dev: + extends: .ci-fourcolor + variables: + COQ_VERSION: "dev" -- cgit v1.2.3 From 1c14614a2328d1854fd584d8d7ca54121faec0ee Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 20 Dec 2018 16:07:41 +0100 Subject: Improve the mathcomp-dev Dockerfile (using Docker's multi-stage build) * Install coq-mathcomp-character in only 1 switch (cf. the build-arg $compiler) * Remove the other switch * Base the final image on coqorg/base:bare (which has no OCaml compiler layers) --- Dockerfile | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/Dockerfile b/Dockerfile index 58f2d12..74ee396 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,8 +1,5 @@ ARG coq_image="coqorg/coq:dev" -FROM ${coq_image} - -ENV MATHCOMP_VERSION="dev" -ENV MATHCOMP_PACKAGE="coq-mathcomp-character" +FROM ${coq_image} as builder WORKDIR /home/coq/mathcomp @@ -14,10 +11,12 @@ ARG compiler="base" RUN ["/bin/bash", "--login", "-c", "set -x \ && declare -A switch_table \ && switch_table=( [\"base\"]=\"${COMPILER}\" [\"edge\"]=\"${COMPILER_EDGE}\" ) \ - && compiler=\"${switch_table[${compiler}]}\" \ - && [ -n \"$compiler\" ] \ - && opam switch set ${compiler} \ + && opam_switch=\"${switch_table[${compiler}]}\" \ + && [ -n \"opam_switch\" ] \ + && opam switch set ${opam_switch} \ && eval $(opam env) \ + && unset \"switch_table[${compiler}]\" \ + && for sw in \"${switch_table[@]}\"; do if [ -n \"$sw\" ]; then opam switch remove -y \"${sw}\"; fi; done \ && opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev \ && opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev \ && opam update -y \ @@ -31,3 +30,11 @@ RUN ["/bin/bash", "--login", "-c", "set -x \ && opam pin add -n -k path coq-mathcomp-character . \ && opam install -y -v -j ${NJOBS} coq-mathcomp-character \ && opam clean -a -c -s --logs"] + +FROM coqorg/base:bare + +ENV MATHCOMP_VERSION="dev" +ENV MATHCOMP_PACKAGE="coq-mathcomp-character" + +COPY --from=builder --chown=coq:coq /home/coq/.opam /home/coq/.opam +COPY --from=builder --chown=coq:coq /home/coq/.profile /home/coq/.profile -- cgit v1.2.3 From da5985eae6656be1bd30aee76c8d08dbc3a09c25 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 20 Dec 2018 16:18:28 +0100 Subject: chore: s/.build/.opam-build/ --- .gitlab-ci.yml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 574a3b2..6c70f50 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -28,7 +28,7 @@ stages: - test # set var OPAM_SWITCH (if need be) when using -.build: +.opam-build: stage: build image: docker:latest services: @@ -57,18 +57,18 @@ stages: - merge_requests coq-8.6: - extends: .build + extends: .opam-build variables: OPAM_SWITCH: "base" coq-8.7: - extends: .build + extends: .opam-build coq-8.8: - extends: .build + extends: .opam-build coq-dev: - extends: .build + extends: .opam-build # set CONTRIB_URL, script, COQ_VERSION, CONTRIB_VERSION when using .ci: -- cgit v1.2.3 From ab8aefdcff6cf02e8cfe51bd052242f9907c5e72 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 20 Dec 2018 16:24:14 +0100 Subject: Add hidden job .make-build to also test the Makefile build infra * This job is only instantiated with coqorg/coq:latest * Add the associated Dockerfile.make --- .gitlab-ci.yml | 22 ++++++++++++++++++++++ Dockerfile.make | 29 +++++++++++++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 Dockerfile.make diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 6c70f50..b8c9c8f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -70,6 +70,28 @@ coq-8.8: coq-dev: extends: .opam-build +# set var OPAM_SWITCH (if need be) and COQ_VERSION when using +.make-build: + stage: build + image: docker:latest + services: + - docker:dind + variables: + # This image will be built locally only (not pushed) + IMAGE: "mathcomp-dev:make_coq-${COQ_VERSION}" + OPAM_SWITCH: "edge" + before_script: + script: + - docker build -f Dockerfile.make --pull --build-arg=coq_image="coqorg/coq:${COQ_VERSION}" --build-arg=compiler="${OPAM_SWITCH}" -t "${IMAGE}" . + except: + - tags + - merge_requests + +make-coq-latest: + extends: .make-build + variables: + COQ_VERSION: "latest" + # set CONTRIB_URL, script, COQ_VERSION, CONTRIB_VERSION when using .ci: stage: test diff --git a/Dockerfile.make b/Dockerfile.make new file mode 100644 index 0000000..4a3787d --- /dev/null +++ b/Dockerfile.make @@ -0,0 +1,29 @@ +ARG coq_image="coqorg/coq:dev" +FROM ${coq_image} + +WORKDIR /home/coq/mathcomp + +COPY . . + +ARG compiler="base" +# other possible value: "edge" + +RUN ["/bin/bash", "--login", "-c", "set -x \ + && declare -A switch_table \ + && switch_table=( [\"base\"]=\"${COMPILER}\" [\"edge\"]=\"${COMPILER_EDGE}\" ) \ + && opam_switch=\"${switch_table[${compiler}]}\" \ + && [ -n \"opam_switch\" ] \ + && opam switch set ${opam_switch} \ + && eval $(opam env) \ + && unset \"switch_table[${compiler}]\" \ + && for sw in \"${switch_table[@]}\"; do [ -n \"$sw\" ] && opam switch remove -y \"${sw}\"; done \ + && opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev \ + && opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev \ + && opam update -y \ + && opam config list && opam repo list && opam list && coqc --version \ + && opam clean -a -c -s --logs \ + && sudo chown -R coq:coq /home/coq/mathcomp \ + && cd mathcomp \ + && make Makefile.coq \ + && make -f Makefile.coq -j ${NJOBS} all \ + && make -f Makefile.coq install"] -- cgit v1.2.3 From 11c1489d8906ef62485b9b9d145f44acc4b9471a Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 21 Dec 2018 12:09:49 +0100 Subject: README.md: Add GitLab CI badge --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 44ac8fd..0d09e10 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,4 @@ +[![pipeline status](https://gitlab.com/math-comp/math-comp/badges/master/pipeline.svg)](https://gitlab.com/math-comp/math-comp/commits/master) [![Build Status](https://travis-ci.org/math-comp/math-comp.svg?branch=master)](https://travis-ci.org/math-comp/math-comp) [![Join the chat at https://gitter.im/math-comp/](https://badges.gitter.im/math-comp.svg)](https://gitter.im/math-comp?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge) -- cgit v1.2.3