image: coqci/base:V2018-05-07

stages:
  - 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-05-03
  # 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: ""

before_script:
  - cat /proc/{cpu,mem}info || true
  - ls -a # figure out if artifacts are around
  - printenv | sort
  - declare -A switch_table
  - switch_table=( ["base"]="$COMPILER" ["be"]="$COMPILER_BE" )
  - 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
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _install_ci
      - config/Makefile
      - test-suite/misc/universes/all_stdlib.v
    expire_in: 1 week
  script:
    - set -e

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

    - echo 'start:coq.build'
    - make -j "$NJOBS" byte
    - make -j "$NJOBS"
    - 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.config'
    - ./configure -local ${EXTRA_CONF}
    - echo 'end:coq.config'

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

    - set +e
  variables: &warnings-variables
    EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only"

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

# 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
  variables: &ci-template-vars
    TEST_TARGET: "$CI_JOB_NAME"

build:
  <<: *build-template
  variables:
    EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes"

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

build:bleeding-edge:
  <<: *build-template
  variables:
    OPAM_SWITCH: be
    EXTRA_CONF: "-native-compiler yes -coqide opt"

warnings:
  <<: *warnings-template

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

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

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

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

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

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

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

ci-bignums:
  <<: *ci-template

ci-color:
  <<: *ci-template

ci-compcert:
  <<: *ci-template

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

ci-coquelicot:
  <<: *ci-template

ci-elpi:
  <<: *ci-template

ci-equations:
  <<: *ci-template

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

# ci-fiat-crypto:
#   <<: *ci-template
#   # out of memory error
#   allow_failure: true

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

ci-flocq:
  <<: *ci-template

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

ci-geocoq:
  <<: *ci-template

ci-hott:
  <<: *ci-template

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

ci-ltac2:
  <<: *ci-template

ci-math-classes:
  <<: *ci-template

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

ci-mtac2:
  <<: *ci-template

ci-pidetop:
  <<: *ci-template

ci-sf:
  <<: *ci-template

ci-unimath:
  <<: *ci-template

ci-vst:
  <<: *ci-template