.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.

stages:
  - build
  - deploy
  - test

################
#### 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}" -t "${IMAGE}" .
  except:
    refs:
      # TODO: comment-out when we'll have more CI minutes
      - /^pr-.*$/
      - tags
      - merge_requests
      - schedules
    variables:
      - $CRON_MODE == "nightly"

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//-/:}" --build-arg=compiler="${OPAM_SWITCH}" -t "${IMAGE}" .
    - docker push "${IMAGE}"
    - docker logout "${CI_REGISTRY}"
  except:
    refs:
      # TODO: comment-out when we'll have more CI minutes
      - /^pr-.*$/
      - tags
      - merge_requests

.opam-build-once:
  extends: .opam-build
  except:
    refs:
      # TODO: comment-out when we'll have more CI minutes
      - /^pr-.*$/
      - tags
      - merge_requests
      - schedules
    variables:
      - $CRON_MODE == "nightly"

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

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

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

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

# coq-8.17: # to uncomment when 8.17+rc1 available
#   # to be replaced with .opam-build-once when 8.17.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}"
    - 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:
      # TODO: comment-out when we'll have more CI minutes
      - /^pr-.*$/
      - tags
      - merge_requests

# run "make test-suite" only for push pipelines (not for scheduled pipelines)
.test-once:
  extends: .test
  except:
    refs:
      # TODO: comment-out when we'll have more CI minutes
      - /^pr-.*$/
      - tags
      - merge_requests
      - schedules
    variables:
      - $CRON_MODE == "nightly"

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

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

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

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

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

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:
      # TODO: comment-out when we'll have more CI minutes
      - /^pr-.*$/
      - tags
      - merge_requests
      - schedules
    variables:
      - $CRON_MODE == "nightly"

# 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-8.13:
  extends: .ci-fourcolor
  variables:
    COQ_VERSION: "8.13"

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/math-comp/odd-order.git"
    CONTRIB_VERSION: master
  script:
    - make -j "${NJOBS}"
    - make install

ci-odd-order-8.13:
  extends: .ci-odd-order
  variables:
    COQ_VERSION: "8.13"

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

ci-lemma-overloading-8.13:
  extends: .ci-lemma-overloading
  variables:
    COQ_VERSION: "8.13"

# 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-8.13:
  extends: .ci-bigenough
  variables:
    COQ_VERSION: "8.13"

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/math-comp/real-closed.git"
    CONTRIB_VERSION: master
  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-8.13:
  extends: .ci-real-closed
  variables:
    COQ_VERSION: "8.13"
  except:
    - tags
    - merge_requests
    - schedules
    - /^pr-(464|697)$/

ci-real-closed-dev:
  extends: .ci-real-closed
  variables:
    COQ_VERSION: "dev"
  except:
    - tags
    - merge_requests
    - schedules
    - /^pr-(464|697)$/

ci-real-closed-8.11-464:
  extends: .ci-real-closed
  variables:
    COQ_VERSION: "8.11"
    CONTRIB_URL: "https://github.com/pi8027/real-closed.git"
    CONTRIB_VERSION: "semilattices"
  only:
    - /^pr-(464|697)$/

ci-real-closed-8.12-464:
  extends: .ci-real-closed
  variables:
    COQ_VERSION: "8.12"
    CONTRIB_URL: "https://github.com/pi8027/real-closed.git"
    CONTRIB_VERSION: "semilattices"
  only:
    - /^pr-(464|697)$/

ci-real-closed-8.13-464:
  extends: .ci-real-closed
  variables:
    COQ_VERSION: "8.13"
    CONTRIB_URL: "https://github.com/pi8027/real-closed.git"
    CONTRIB_VERSION: "semilattices"
  only:
    - /^pr-(464|697)$/

ci-real-closed-dev-464:
  extends: .ci-real-closed
  variables:
    COQ_VERSION: "dev"
    CONTRIB_URL: "https://github.com/pi8027/real-closed.git"
    CONTRIB_VERSION: "semilattices"
  only:
    - /^pr-(464|697)$/

# The finmap library
.ci-finmap:
  extends: .ci
  variables:
    CONTRIB_URL: "https://github.com/math-comp/finmap.git"
    CONTRIB_VERSION: master
  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-8.13:
  extends: .ci-finmap
  variables:
    COQ_VERSION: "8.13"
  except:
    - tags
    - merge_requests
    - schedules
    - /^pr-(464|697)$/

ci-finmap-dev:
  extends: .ci-finmap
  variables:
    COQ_VERSION: "dev"
  except:
    - tags
    - merge_requests
    - schedules
    - /^pr-(464|697)$/

ci-finmap-8.11-464:
  extends: .ci-finmap
  variables:
    COQ_VERSION: "8.11"
    CONTRIB_URL: "https://github.com/pi8027/finmap.git"
    CONTRIB_VERSION: "semilattices"
  only:
    - /^pr-(464|697)$/

ci-finmap-8.12-464:
  extends: .ci-finmap
  variables:
    COQ_VERSION: "8.12"
    CONTRIB_URL: "https://github.com/pi8027/finmap.git"
    CONTRIB_VERSION: "semilattices"
  only:
    - /^pr-(464|697)$/

ci-finmap-8.13-464:
  extends: .ci-finmap
  variables:
    COQ_VERSION: "8.13"
    CONTRIB_URL: "https://github.com/pi8027/finmap.git"
    CONTRIB_VERSION: "semilattices"
  only:
    - /^pr-(464|697)$/

ci-finmap-dev-464:
  extends: .ci-finmap
  variables:
    COQ_VERSION: "dev"
    CONTRIB_URL: "https://github.com/pi8027/finmap.git"
    CONTRIB_VERSION: "semilattices"
  only:
    - /^pr-(464|697)$/

# The multinomials library
.ci-multinomials:
  extends: .ci
  variables:
    CONTRIB_URL: "https://github.com/math-comp/multinomials.git"
    CONTRIB_VERSION: master
  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-8.13:
  extends: .ci-multinomials
  variables:
    COQ_VERSION: "8.13"

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.14:
  extends: .ci-analysis
  variables:
    COQ_VERSION: "8.14"

ci-analysis-dev:
  extends: .ci-analysis
  variables:
    COQ_VERSION: "dev"

# 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.13:
  extends: .docker-deploy-once

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

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

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

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

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