Merge pull request #266 from erikmd/setup-gitlab-ci

Setup Docker-based configuration for GitLab CI

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"))} ]