# Design:
# - build stage (e.g. docker build -t mathcomp-dev:$IID_$SLUG_coq-8.7 .)
#   - choice of the OCaml compiler: var OPAM_SWITCH in {base, edge}
#     (Dockerfile containing: "opam switch set $compiler && eval $(opam env)")
#   - 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 "deployment")
#   - pull each built image from GitLab registry => push to Docker Hub
# + scheduled build & deploy for mathcomp/mathcomp-dev:coq-dev
#
# Config for protected environment "deployment":
# - 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}"
    OPAM_SWITCH: "edge"
  before_script:
    - echo "${OPAM_SWITCH}"
    - echo "${COQ_VERSION}"
  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
    - schedules

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}"
    OPAM_SWITCH: "edge"
  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:
    - tags
    - merge_requests

.opam-build-once:
  extends: .opam-build
  except:
    - tags
    - merge_requests
    - schedules
  
coq-8.7:
  extends: .opam-build-once

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

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

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

coq-dev:
  extends: .opam-build

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

# 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:
    - tags
    - merge_requests
    - schedules

# 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
  except:
    - tags
    - merge_requests
    - schedules
    - /^experiment\/order$/
    - /^pr-(270|388|402|419|446)$/

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

ci-fourcolor-8.10:
  extends: .ci-fourcolor
  variables:
    COQ_VERSION: "8.10"

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

.ci-fourcolor-270:
  extends: .ci
  variables:
    CONTRIB_URL: "https://github.com/pi8027/fourcolor.git"
    CONTRIB_VERSION: fix-mathcomp-270
  script:
    - make -j "${NJOBS}"
    - make install
  only:
    - /^experiment\/order$/
    - /^pr-(270|388|402|419|446)$/

ci-fourcolor-8.7-270:
  extends: .ci-fourcolor-270
  variables:
    COQ_VERSION: "8.7"

ci-fourcolor-8.8-270:
  extends: .ci-fourcolor-270
  variables:
    COQ_VERSION: "8.8"

ci-fourcolor-8.9-270:
  extends: .ci-fourcolor-270
  variables:
    COQ_VERSION: "8.9"

ci-fourcolor-8.10-270:
  extends: .ci-fourcolor-270
  variables:
    COQ_VERSION: "8.10"

ci-fourcolor-dev-270:
  extends: .ci-fourcolor-270
  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
  except:
    - tags
    - merge_requests
    - schedules
    - /^experiment\/order$/
    - /^pr-(270|388|402|419|446)$/

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

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

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

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

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

.ci-odd-order-270:
  extends: .ci
  variables:
    CONTRIB_URL: "https://github.com/pi8027/odd-order.git"
    CONTRIB_VERSION: fix-mathcomp-270
  script:
    - make -j "${NJOBS}"
    - make install
  only:
    - /^experiment\/order$/
    - /^pr-(270|388|402|419|446)$/

ci-odd-order-8.7-270:
 extends: .ci-odd-order-270
 variables:
   COQ_VERSION: "8.7"

ci-odd-order-8.8-270:
 extends: .ci-odd-order-270
 variables:
   COQ_VERSION: "8.8"

ci-odd-order-8.9-270:
 extends: .ci-odd-order-270
 variables:
   COQ_VERSION: "8.9"

ci-odd-order-8.10-270:
 extends: .ci-odd-order-270
 variables:
   COQ_VERSION: "8.10"

ci-odd-order-dev-270:
  extends: .ci-odd-order-270
  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.8:
  extends: .ci-lemma-overloading
  variables:
    COQ_VERSION: "8.8"

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

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

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

ci-bigenough-8.8:
  extends: .ci-bigenough
  variables:
    COQ_VERSION: "8.8"

ci-bigenough-8.9:
  extends: .ci-bigenough
  variables:
    COQ_VERSION: "8.9"

ci-bigenough-8.9:
  extends: .ci-bigenough
  variables:
    COQ_VERSION: "8.10"

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.7:
#   extends: .ci-real-closed
#   variables:
#     COQ_VERSION: "8.7"
# 
# ci-real-closed-8.8:
#   extends: .ci-real-closed
#   variables:
#     COQ_VERSION: "8.8"
# 
# ci-real-closed-8.9:
#   extends: .ci-real-closed
#   variables:
#     COQ_VERSION: "8.9"
# 
# ci-real-closed-dev:
#   extends: .ci-real-closed
#   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.8:
#   extends: .ci-analysis
#   variables:
#     COQ_VERSION: "8.8"
# 
# ci-analysis-8.9:
#   extends: .ci-analysis
#   variables:
#     COQ_VERSION: "8.9"
# 
# ci-analysis-dev:
#   extends: .ci-analysis
#   variables:
#     COQ_VERSION: "dev"

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

ci-finmap-8.8:
  extends: .ci-finmap
  variables:
    COQ_VERSION: "8.8"

ci-finmap-8.9:
  extends: .ci-finmap
  variables:
    COQ_VERSION: "8.9"

ci-finmap-8.10:
  extends: .ci-finmap
  variables:
    COQ_VERSION: "8.10"

ci-finmap-dev:
  extends: .ci-finmap
  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:
    name: deployment
    url: https://hub.docker.com/r/mathcomp/mathcomp-dev
  variables:
    GIT_STRATEGY: none
    HUB_IMAGE: "mathcomp/${CI_JOB_NAME}"
    IMAGE_PREFIX: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}"
  script:
    - export IMAGE="${IMAGE_PREFIX}_${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:
    - master

.docker-deploy-once:
  extends: .docker-deploy
  except:
    - schedules

mathcomp-dev:coq-8.7:
  extends: .docker-deploy-once

mathcomp-dev:coq-8.8:
  extends: .docker-deploy-once

mathcomp-dev:coq-8.9:
  extends: .docker-deploy-once

mathcomp-dev:coq-8.10:
  extends: .docker-deploy-once

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