aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.dockerignore36
-rw-r--r--.gitlab-ci.yml148
-rw-r--r--Dockerfile40
-rw-r--r--Dockerfile.make29
-rw-r--r--README.md1
-rw-r--r--coq-mathcomp-algebra.opam (renamed from mathcomp/algebra/opam)5
-rw-r--r--coq-mathcomp-character.opam (renamed from mathcomp/character/opam)5
-rw-r--r--coq-mathcomp-field.opam (renamed from mathcomp/field/opam)5
-rw-r--r--coq-mathcomp-fingroup.opam (renamed from mathcomp/fingroup/opam)5
-rw-r--r--coq-mathcomp-solvable.opam (renamed from mathcomp/solvable/opam)5
-rw-r--r--coq-mathcomp-ssreflect.opam (renamed from mathcomp/ssreflect/opam)5
11 files changed, 272 insertions, 12 deletions
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
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
new file mode 100644
index 0000000..b8c9c8f
--- /dev/null
+++ b/.gitlab-ci.yml
@@ -0,0 +1,148 @@
+# 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
+.opam-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: .opam-build
+ variables:
+ OPAM_SWITCH: "base"
+
+coq-8.7:
+ extends: .opam-build
+
+coq-8.8:
+ extends: .opam-build
+
+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
+ 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"
diff --git a/Dockerfile b/Dockerfile
new file mode 100644
index 0000000..74ee396
--- /dev/null
+++ b/Dockerfile
@@ -0,0 +1,40 @@
+ARG coq_image="coqorg/coq:dev"
+FROM ${coq_image} as builder
+
+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 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 \
+ && 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"]
+
+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
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"]
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)
diff --git a/mathcomp/algebra/opam b/coq-mathcomp-algebra.opam
index e60cdc2..7cc4946 100644
--- a/mathcomp/algebra/opam
+++ b/coq-mathcomp-algebra.opam
@@ -2,14 +2,15 @@ opam-version: "1.2"
name: "coq-mathcomp-algebra"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+synopsis: "The Mathematical Components library"
homepage: "https://math-comp.github.io/math-comp/"
bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
dev-repo: "https://github.com/math-comp/math-comp.git"
license: "CeCILL-B"
-build: [ make "-j" "%{jobs}%" ]
-install: [ make "install" ]
+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" } ]
diff --git a/mathcomp/character/opam b/coq-mathcomp-character.opam
index 0f3dcf1..47c72a7 100644
--- a/mathcomp/character/opam
+++ b/coq-mathcomp-character.opam
@@ -2,14 +2,15 @@ opam-version: "1.2"
name: "coq-mathcomp-character"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+synopsis: "The Mathematical Components library"
homepage: "https://math-comp.github.io/math-comp/"
bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
dev-repo: "https://github.com/math-comp/math-comp.git"
license: "CeCILL-B"
-build: [ make "-j" "%{jobs}%" ]
-install: [ make "install" ]
+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" } ]
diff --git a/mathcomp/field/opam b/coq-mathcomp-field.opam
index 2624714..e823f93 100644
--- a/mathcomp/field/opam
+++ b/coq-mathcomp-field.opam
@@ -2,14 +2,15 @@ opam-version: "1.2"
name: "coq-mathcomp-field"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+synopsis: "The Mathematical Components library"
homepage: "https://math-comp.github.io/math-comp/"
bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
dev-repo: "https://github.com/math-comp/math-comp.git"
license: "CeCILL-B"
-build: [ make "-j" "%{jobs}%" ]
-install: [ make "install" ]
+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" } ]
diff --git a/mathcomp/fingroup/opam b/coq-mathcomp-fingroup.opam
index 862c2f1..57d3a95 100644
--- a/mathcomp/fingroup/opam
+++ b/coq-mathcomp-fingroup.opam
@@ -2,14 +2,15 @@ opam-version: "1.2"
name: "coq-mathcomp-fingroup"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+synopsis: "The Mathematical Components library"
homepage: "https://math-comp.github.io/math-comp/"
bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
dev-repo: "https://github.com/math-comp/math-comp.git"
license: "CeCILL-B"
-build: [ make "-j" "%{jobs}%" ]
-install: [ make "install" ]
+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" } ]
diff --git a/mathcomp/solvable/opam b/coq-mathcomp-solvable.opam
index 6e0bd16..f238333 100644
--- a/mathcomp/solvable/opam
+++ b/coq-mathcomp-solvable.opam
@@ -2,14 +2,15 @@ opam-version: "1.2"
name: "coq-mathcomp-solvable"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+synopsis: "The Mathematical Components library"
homepage: "https://math-comp.github.io/math-comp/"
bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
dev-repo: "https://github.com/math-comp/math-comp.git"
license: "CeCILL-B"
-build: [ make "-j" "%{jobs}%" ]
-install: [ make "install" ]
+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" } ]
diff --git a/mathcomp/ssreflect/opam b/coq-mathcomp-ssreflect.opam
index c0ee83b..5d31846 100644
--- a/mathcomp/ssreflect/opam
+++ b/coq-mathcomp-ssreflect.opam
@@ -2,14 +2,15 @@ opam-version: "1.2"
name: "coq-mathcomp-ssreflect"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+synopsis: "The Mathematical Components library"
homepage: "https://math-comp.github.io/math-comp/"
bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
dev-repo: "https://github.com/math-comp/math-comp.git"
license: "CeCILL-B"
-build: [ make "-j" "%{jobs}%" ]
-install: [ make "install" ]
+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"))} ]
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:44:43 +0000