.gitlab-ci.yml

image: "$IMAGE"

stages:
  - docker
  - build
  - test

# some default values
variables:
  # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
  # for reference]
  CACHEKEY: "bionic_coq-V2018-06-13-V1"
  IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
  # By default, jobs run in the base switch; override to select another switch
  OPAM_SWITCH: "base"
  # Used to select special compiler switches such as flambda, 32bits, etc...
  OPAM_VARIANT: ""

docker-boot:
  stage: docker
  image: docker:stable
  services:
    - docker:dind
  before_script: []
  script:
    - docker login -u gitlab-ci-token -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
    - cd dev/ci/docker/bionic_coq/
    - if docker pull "$IMAGE"; then echo "Image prebuilt!"; exit 0; fi
    - docker build -t "$IMAGE" .
    - docker push "$IMAGE"
  except:
    variables:
      - $SKIP_DOCKER == "true"
  tags:
    - docker

before_script:
  - cat /proc/{cpu,mem}info || true
  - ls -a # figure out if artifacts are around
  - printenv -0 | sort -z | tr '\0' '\n'
  - declare -A switch_table
  - switch_table=( ["base"]="$COMPILER" ["edge"]="$COMPILER_EDGE" )
  - opam switch -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
  - eval $(opam config env)
  - opam list
  - opam config list

################ GITLAB CACHING ######################
# - use artifacts between jobs                       #
######################################################

# TODO figure out how to build doc for installed Coq
.build-template: &build-template
  stage: build
  retry: 1
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _install_ci
      - config/Makefile
      - config/coq_config.py
      - test-suite/misc/universes/all_stdlib.v
    expire_in: 1 week
  script:
    - set -e

    - echo 'start:coq.clean'
    - make clean # ensure that `make clean` works on a fresh clone
    - echo 'end:coq.clean'

    - echo 'start:coq.config'
    - ./configure -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE"
    - echo 'end:coq.config'

    - echo 'start:coq.build'
    - make -j "$NJOBS" byte
    - make -j "$NJOBS" world $EXTRA_TARGET
    - make test-suite/misc/universes/all_stdlib.v
    - echo 'end:coq:build'

    - echo 'start:coq.install'
    - make install
    - make install-byte
    - cp bin/fake_ide _install_ci/bin/
    - echo 'end:coq.install'

    - set +e

.warnings-template: &warnings-template
  # keep warnings in test stage so we can test things even when warnings occur
  stage: test
  script:
    - set -e

    - echo 'start:coq.clean'
    - make clean # ensure that `make clean` works on a fresh clone
    - echo 'end:coq.clean'

    - echo 'start:coq.config'
    - ./configure -local ${COQ_EXTRA_CONF}
    - echo 'end:coq.config'

    - echo 'start:coq.build'
    - make -j "$NJOBS" coqocaml
    - echo 'end:coq:build'

    - set +e
  variables: &warnings-variables
    COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only -warn-error yes"

# every non build job must set dependencies otherwise all build
# artifacts are used together and we may get some random Coq. To that
# purpose, we add a spurious dependency `not-a-real-job` that must be
# overridden otherwise the CI will fail.

.doc-templare: &doc-template
  stage: test
  dependencies:
    - not-a-real-job
  script:
    - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no'
    - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= sphinx
    - make install-doc-sphinx
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _install_ci/share/doc/coq/

# set dependencies when using
.test-suite-template: &test-suite-template
  stage: test
  dependencies:
    - not-a-real-job
  script:
    - cd test-suite
    - make clean
    # careful with the ending /
    - BIN=$(readlink -f ../_install_ci/bin)/
    - LIB=$(readlink -f ../_install_ci/lib/coq)/
    - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all
  artifacts:
    name: "$CI_JOB_NAME.logs"
    when: on_failure
    paths:
      - test-suite/logs

# set dependencies when using
.validate-template: &validate-template
  stage: test
  dependencies:
    - not-a-real-job
  script:
    - cd _install_ci
    - find lib/coq/ -name '*.vo' -print0 > vofiles
    - for regexp in 's/.vo//' 's:lib/coq/plugins:Coq:' 's:lib/coq/theories:Coq:' 's:/:.:g'; do sed -z -i "$regexp" vofiles; done
    - xargs -0 --arg-file=vofiles bin/coqchk -boot -silent -o -m -coqlib lib/coq/

.ci-template: &ci-template
  stage: test
  script:
    - set -e
    - echo 'start:coq.test'
    - make -f Makefile.ci -j "$NJOBS" ${TEST_TARGET}
    - echo 'end:coq.test'
    - set +e
  dependencies:
    - build:base
  variables: &ci-template-vars
    TEST_TARGET: "$CI_JOB_NAME"

.ci-template-flambda: &ci-template-flambda
  <<: *ci-template
  dependencies:
    - build:edge+flambda
  variables:
    <<: *ci-template-vars
    OPAM_SWITCH: "edge"
    OPAM_VARIANT: "+flambda"

.windows-template: &windows-template
  stage: test
  artifacts:
    name: "%CI_JOB_NAME%"
    paths:
      - dev\nsis\*.exe
      - coq-opensource-archive-windows-*.zip
    expire_in: 1 week
  dependencies: []
  tags:
    - windows
  before_script: []
  script:
    - call dev/ci/gitlab.bat
  only:
    variables:
      - $WINDOWS == "enabled"

build:base:
  <<: *build-template
  variables:
    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
    # coqdoc for stdlib, until we know how to build it from installed Coq
    EXTRA_TARGET: "stdlib"

# no coqide for 32bit: libgtk installation problems
build:base+32bit:
  <<: *build-template
  variables:
    OPAM_VARIANT: "+32bit"
    COQ_EXTRA_CONF: "-native-compiler yes"

build:edge:
  <<: *build-template
  variables:
    OPAM_SWITCH: edge
    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"

build:edge+flambda:
  <<: *build-template
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
    COQ_EXTRA_CONF: "-native-compiler no -coqide opt -flambda-opts "
    COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures"

windows64:
  <<: *windows-template
  variables:
    ARCH: "64"

windows32:
  <<: *windows-template
  variables:
    ARCH: "32"

warnings:base:
  <<: *warnings-template

# warnings:32bit:
#   <<: *warnings-template
#   variables:
#     <<: *warnings-variables

warnings:edge:
  <<: *warnings-template
  variables:
    <<: *warnings-variables
    OPAM_SWITCH: edge

documentation:
  <<: *doc-template
  dependencies:
    - build:base

test-suite:base:
  <<: *test-suite-template
  dependencies:
    - build:base

test-suite:base+32bit:
  <<: *test-suite-template
  dependencies:
    - build:base+32bit
  variables:
    OPAM_VARIANT: "+32bit"

test-suite:edge:
  <<: *test-suite-template
  dependencies:
    - build:edge
  variables:
    OPAM_SWITCH: edge

test-suite:edge+flambda:
  <<: *test-suite-template
  dependencies:
    - build:edge+flambda
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"

validate:base:
  <<: *validate-template
  dependencies:
    - build:base

validate:base+32bit:
  <<: *validate-template
  dependencies:
    - build:base+32bit
  variables:
    OPAM_VARIANT: "+32bit"

validate:edge:
  <<: *validate-template
  dependencies:
    - build:edge
  variables:
    OPAM_SWITCH: edge

validate:edge+flambda:
  <<: *validate-template
  dependencies:
    - build:edge+flambda
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"

ci-bignums:
  <<: *ci-template

ci-color:
  <<: *ci-template-flambda

ci-compcert:
  <<: *ci-template-flambda

ci-coq-dpdgraph:
  <<: *ci-template

ci-coquelicot:
  <<: *ci-template

ci-cross-crypto:
  <<: *ci-template

ci-elpi:
  <<: *ci-template

ci-equations:
  <<: *ci-template

ci-fcsl-pcm:
  <<: *ci-template

ci-fiat-crypto:
  <<: *ci-template-flambda

ci-fiat-parsers:
  <<: *ci-template

ci-flocq:
  <<: *ci-template

ci-formal-topology:
  <<: *ci-template-flambda

ci-geocoq:
  <<: *ci-template-flambda

ci-hott:
  <<: *ci-template

ci-iris-lambda-rust:
  <<: *ci-template-flambda

ci-ltac2:
  <<: *ci-template

ci-math-comp:
  <<: *ci-template-flambda

ci-mtac2:
  <<: *ci-template

ci-pidetop:
  <<: *ci-template

ci-quickchick:
  <<: *ci-template-flambda

ci-sf:
  <<: *ci-template

ci-unimath:
  <<: *ci-template-flambda

ci-vst:
  <<: *ci-template-flambda