.gitlab-ci.yml

# Design:
# - build stage (e.g. docker build -t mathcomp-dev:$IID_$SLUG_coq-8.12 .)
#   - all branches (not tags) => push on GitLab registry
#   - GitHub PRs => push on GitLab and report back thanks to @coqbot
# - test stage (image: mathcomp-dev:$IID_$SLUG_coq-8.7)
#   - script template foreach project (custom CONTRIB_URL, script)
#   - jobs foreach project and Coq version (custom COQ_VERSION, CONTRIB_VERSION)
# - deploy stage (only branch "master" and environment deployments "mathcomp/*")
#   - pull each built image from GitLab registry => push to Docker Hub
# + scheduled build & deploy for mathcomp/mathcomp-dev:coq-dev
#
# Config for protected environment deployments "mathcomp/*":
# - 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.

default:
  tags: ['large']

stages:
  - build
  - deploy
  - test

variables:
  # cf. https://hub.docker.com/r/coqorg/coq#supported-tags
  OCAML_VERSION: "4.14-flambda"

################
#### build stage
################

# 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}"
  before_script:
    - echo "${OPAM_SWITCH}"
    - echo "${COQ_VERSION}"
  script:
    - docker build -f Dockerfile.make --pull --build-arg=coq_image="coqorg/coq:${COQ_VERSION}-ocaml-${OCAML_VERSION}" -t "${IMAGE}" .
  except:
    refs:
      # - /^pr-.*$/
      - tags
      - merge_requests
      - schedules
    variables:
      - $CRON_MODE == "nightly"
      - $CRON_MODE == "minimal"

make-coq-latest:
  extends: .make-build
  variables:
    COQ_VERSION: "latest"

# 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}"
  before_script:
    - echo "${OPAM_SWITCH}"
    - 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//-/:}-ocaml-${OCAML_VERSION}" --build-arg=compiler="${OPAM_SWITCH}" -t "${IMAGE}" .
    - docker push "${IMAGE}"
    - docker logout "${CI_REGISTRY}"
  except:
    refs:
      # - /^pr-.*$/
      - tags
      - merge_requests

.opam-build-once:
  extends: .opam-build
  except:
    refs:
      # - /^pr-.*$/
      - tags
      - merge_requests
      - schedules
    variables:
      - $CRON_MODE == "nightly"

coq-8.18:
  extends: .opam-build-once

coq-8.19:
  extends: .opam-build-once

coq-8.20:
  extends: .opam-build-once

# coq-8.21: # to uncomment when 8.21+rc1 available
#   # to be replaced with .opam-build-once when 8.21.0 available
#   extends: .opam-build

coq-dev:
  extends: .opam-build

################
##### test stage
################

# run "make test-suite" (required variable: COQ_VERSION)
.test:
  stage: test
  image: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}_coq-${COQ_VERSION}"
  before_script:
    - cat /proc/{cpu,mem}info || true
    # don't printenv to avoid cluttering the log
    - opam config list
    - opam repo list
    - opam list
    - coqc --version
    - echo "${COQ_VERSION}"
    # adapt to Git's patch for CVE-2022-24765 that is off-topic here
    - git config --global --add safe.directory "${CI_PROJECT_DIR}"
    - git rev-parse --verify HEAD
    - git describe --all --long --abbrev=40 --always --dirty
    - pwd
  script:
    - cd mathcomp
    - make test-suite TEST_SKIP_BUILD=1
  except:
    refs:
      # - /^pr-.*$/
      - tags
      - merge_requests

# run "make test-suite" only for push pipelines (not for scheduled pipelines)
.test-once:
  extends: .test
  except:
    refs:
      # - /^pr-.*$/
      - tags
      - merge_requests
      - schedules
    variables:
      - $CRON_MODE == "nightly"
      - $CRON_MODE == "minimal"

test-coq-8.18:
  extends: .test-once
  variables:
    COQ_VERSION: "8.18"

test-coq-8.19:
  extends: .test-once
  variables:
    COQ_VERSION: "8.19"

test-coq-8.20:
  extends: .test-once
  variables:
    COQ_VERSION: "8.20"

# test-coq-8.21: # to uncomment when 8.21+rc1 available
#   # to be replaced with .test-once when 8.21.0 available
#   extends: .test
#   variables:
#     COQ_VERSION: "8.21"

test-coq-dev:
  extends: .test
  variables:
    COQ_VERSION: "dev"

# # 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 to avoid cluttering the log
#     - opam config list
#     - opam repo list
#     - opam list
#     - coqc --version
#     - echo "${COQ_VERSION}"
#     - echo "${CONTRIB_URL}"
#     - echo "${CONTRIB_VERSION}"
#     - git clone -b "${CONTRIB_VERSION}" --depth 1 "${CONTRIB_URL}" /home/coq/ci
#     - cd /home/coq/ci
#     - git rev-parse --verify HEAD
#     - git describe --all --long --abbrev=40 --always --dirty
#   except:
#     refs:
#       # - /^pr-.*$/
#       - tags
#       - merge_requests
#       - schedules
#     variables:
#       - $CRON_MODE == "nightly"
#       - $CRON_MODE == "minimal"
# 
# # 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)
# 
# # The Four Color Theorem
# .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-dev:
#   extends: .ci-fourcolor
#   variables:
#     COQ_VERSION: "dev"
# 
# # The Odd Order Theorem
# .ci-odd-order:
#   extends: .ci
#   variables:
#     CONTRIB_URL: "https://github.com/proux01/odd-order.git"
#     CONTRIB_VERSION: hierarchy-builder
#   script:
#     - make -j "${NJOBS}"
#     - make install
# 
# ci-odd-order-dev:
#   extends: .ci-odd-order
#   variables:
#     COQ_VERSION: "dev"
# 
# # The Lemma Overloading library
# .ci-lemma-overloading:
#   extends: .ci
#   variables:
#     CONTRIB_URL: "https://github.com/coq-community/lemma-overloading.git"
#     CONTRIB_VERSION: master
#   script:
#     - opam pin add -n -k path coq-lemma-overloading .
#     - opam install -y -v -j "${NJOBS}" coq-lemma-overloading
# 
# # commented out as it is currently broken with Coq master
# # ci-lemma-overloading-dev:
# #   extends: .ci-lemma-overloading
# #   variables:
# #     COQ_VERSION: "dev"
# 
# # The bigenough library (will be later subsumed by near)
# .ci-bigenough:
#   extends: .ci
#   variables:
#     CONTRIB_URL: "https://github.com/math-comp/bigenough.git"
#     CONTRIB_VERSION: master
#   script:
#     - opam pin add -n -k path coq-mathcomp-bigenough .
#     - opam install -y -v -j "${NJOBS}" coq-mathcomp-bigenough
# 
# ci-bigenough-dev:
#   extends: .ci-bigenough
#   variables:
#     COQ_VERSION: "dev"
# 
# # The real-closed library
# .ci-real-closed:
#   extends: .ci
#   variables:
#     CONTRIB_URL: "https://github.com/proux01/real-closed.git"
#     CONTRIB_VERSION: hierarchy-builder
#   script:
#     - opam pin add -n -k path coq-mathcomp-real-closed .
#     - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-real-closed
#     - opam install -y -v -j "${NJOBS}" coq-mathcomp-real-closed
# 
# ci-real-closed-dev:
#   extends: .ci-real-closed
#   variables:
#     COQ_VERSION: "dev"
# 
# # The finmap library
# .ci-finmap:
#   extends: .ci
#   variables:
#     CONTRIB_URL: "https://github.com/proux01/finmap.git"
#     CONTRIB_VERSION: hierarchy-builder
#   script:
#     - opam pin add -n -k path coq-mathcomp-finmap .
#     - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-finmap
#     - opam install -y -v -j "${NJOBS}" coq-mathcomp-finmap
# 
# ci-finmap-dev:
#   extends: .ci-finmap
#   variables:
#     COQ_VERSION: "dev"
# 
# # The multinomials library
# .ci-multinomials:
#   extends: .ci
#   variables:
#     CONTRIB_URL: "https://github.com/proux01/multinomials.git"
#     CONTRIB_VERSION: hierarchy-builder
#   script:
#     - opam pin add -n -k path coq-mathcomp-multinomials .
#     - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-multinomials
#     - opam install -y -v -j "${NJOBS}" coq-mathcomp-multinomials
# 
# ci-multinomials-dev:
#   extends: .ci-multinomials
#   variables:
#     COQ_VERSION: "dev"
# 
# # The analysis library
# .ci-analysis:
#   extends: .ci
#   variables:
#     CONTRIB_URL: "https://github.com/math-comp/analysis.git"
#     CONTRIB_VERSION: master
#   script:
#     - opam pin add -n -k path coq-mathcomp-analysis .
#     - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-analysis
#     - opam install -y -v -j "${NJOBS}" coq-mathcomp-analysis
# 
# ci-analysis-8.15:
#   extends: .ci-analysis
#   variables:
#     COQ_VERSION: "8.15"
# 
# ci-analysis-8.16:
#   extends: .ci-analysis
#   variables:
#     COQ_VERSION: "8.16"
# 
# # The FCSL-PCM library
# .ci-fcsl-pcm:
#   extends: .ci
#   variables:
#     CONTRIB_URL: "https://github.com/imdea-software/fcsl-pcm.git"
#     CONTRIB_VERSION: master
#   script:
#     - opam pin add -n -k path coq-fcsl-pcm .
#     - opam install -y -v -j "${NJOBS}" coq-fcsl-pcm
# 
# ci-fcsl-pcm-dev:
#   extends: .ci-fcsl-pcm
#   variables:
#     COQ_VERSION: "dev"

################
### deploy stage
################

# Changes below (or jobs extending .docker-deploy) should be carefully
# reviewed to avoid leaks of HUB_TOKEN
.docker-deploy:
  stage: deploy
  image: docker:latest
  services:
    - docker:dind
  environment:
    # here, CI_JOB_NAME must not contain any ':', hence the use of '_'
    name: "mathcomp/${CI_JOB_NAME}"
    url: https://hub.docker.com/r/mathcomp/mathcomp-dev
  variables:
    GIT_STRATEGY: none
    IMAGE_PREFIX: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}"
  script:
    - export IMAGE="${IMAGE_PREFIX}_${CI_JOB_NAME##*_}"
    - export HUB_IMAGE="mathcomp/${CI_JOB_NAME/_/:}"
    - echo "${IMAGE}"
    - docker pull "${IMAGE}"
    - echo "${HUB_IMAGE}"
    - docker tag "${IMAGE}" "${HUB_IMAGE}"
    - test -n "${HUB_REGISTRY}"
    - test -n "${HUB_REGISTRY_USER}"
    - echo "${HUB_TOKEN}" | docker login -u "${HUB_REGISTRY_USER}" --password-stdin "${HUB_REGISTRY}"
    - docker push "${HUB_IMAGE}"
    - docker logout "${HUB_REGISTRY}"
  only:
    refs:
      - master

.docker-deploy-once:
  extends: .docker-deploy
  except:
    refs:
      - schedules
    variables:
      - $CRON_MODE == "nightly"

mathcomp-dev_coq-8.18:
  extends: .docker-deploy-once

mathcomp-dev_coq-8.19:
  extends: .docker-deploy-once

mathcomp-dev_coq-8.20:
  extends: .docker-deploy-once

# mathcomp-dev_coq-8.21: # to uncomment when 8.21+rc1 available
#   # to be replaced with .docker-deploy-once when 8.21.0 available
#   extends: .docker-deploy

mathcomp-dev_coq-dev:
  extends: .docker-deploy