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.

1 files changed, 126 insertions, 0 deletions

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"