path: root/.gitlab-ci.yml

image: ubuntu:latest

stages:
  - opam-boot
  - build
  - test

variables:
  # some default values
  NJOBS: "2"
  COMPILER: "4.02.3"
  CAMLP5_VER: "6.14"
  OPAMROOT: "$CI_PROJECT_DIR/.opamcache"
  OPAMROOTISOK: "true"

  # some useful values
  COMPILER_32BIT: "4.02.3+32bit"

  COMPILER_BLEEDING_EDGE: "4.06.0"
  CAMLP5_VER_BLEEDING_EDGE: "7.03"

  TIMING_PACKAGES: "time python"

  COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev"
  #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386"
  COQIDE_OPAM: "lablgtk-extras"
  COQIDE_OPAM_BE: "lablgtk.2.18.6 lablgtk-extras.1.6"
  COQDOC_PACKAGES: "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa python3-pip"
  COQDOC_OPAM: "hevea"
  SPHINX_PACKAGES: "bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex"
  ELPI_OPAM: "ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree"


before_script:
  - ls -a # figure out if artifacts are around
  - printenv
#  - if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi
  - apt-get update -qq && apt-get install -y -qq m4 opam ${EXTRA_PACKAGES}
  - if [ -n "${PIP_PACKAGES}" ]; then pip3 install ${PIP_PACKAGES}; fi
  # if no cache running opam config fails!
  - if [ -d .opamcache ]; then eval $(opam config env); fi

################ OPAM SYSTEM ######################
# - use cache between pipelines
# - use artifacts between jobs
#   (in https://gitlab.com/SkySkimmer/coq/-/jobs/63255417
#    the cache wasn't available at the build step)
# every non opam-boot job must set dependencies (for ci it's in the template)
# otherwise all opam-boot artifacts are used together and we get some random switch

# set cache key when using
.opam-boot-template: &opam-boot-template
  stage: opam-boot
  artifacts:
    name: "opam-$COMPILER"
    paths:
      - .opamcache
    expire_in: 1 week
  script:
    # the default repo in this docker image is a local directory
    # at the time of 4aaeb8abf it lagged behind the official
    # repository such that camlp5 7.01 was not available
    - opam init -a -y -j $NJOBS --compiler=${COMPILER} default https://opam.ocaml.org
    - eval $(opam config env)
    - opam update
    - opam config list
    - opam list
    - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind num ${EXTRA_OPAM}
    - rm -rf ~/.opam/log/
    - opam list

# TODO figure out how to build doc for installed coq
# set dependencies when using
.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
  dependencies:
    - not-a-real-job
  script:
    - set -e
    - printenv
    - opam config list
    - opam list

    - 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

# set dependencies when using
.warnings-template: &warnings-template
  # keep warnings in test stage so we can test things even when warnings occur
  stage: test
  dependencies:
    - not-a-real-job
  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"
    EXTRA_PACKAGES: "$COQIDE_PACKAGES"
    EXTRA_OPAM: "$COQIDE_OPAM"

# 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:
    - opam-boot
    - build
  variables: &ci-template-vars
    TEST_TARGET: "$CI_JOB_NAME"
    EXTRA_PACKAGES: "$TIMING_PACKAGES"

opam-boot:
  <<: *opam-boot-template
  cache:
    paths: &cache-paths
      - .opamcache
    key: main
  variables:
    EXTRA_OPAM: "$COQIDE_OPAM $COQDOC_OPAM ocamlgraph $ELPI_OPAM"
    EXTRA_PACKAGES: "$COQIDE_PACKAGES"

opam-boot:32bit:
  <<: *opam-boot-template
  cache:
    paths: *cache-paths
    key: 32bit
  variables:
    COMPILER: "$COMPILER_32BIT"
    EXTRA_PACKAGES: "gcc-multilib"

opam-boot:bleeding-edge:
  <<: *opam-boot-template
  cache:
    paths: *cache-paths
    key: be
  variables:
    COMPILER: "$COMPILER_BLEEDING_EDGE"
    CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE"
    EXTRA_PACKAGES: "$COQIDE_PACKAGES"
    EXTRA_OPAM: "$COQIDE_OPAM_BE"

build:
  <<: *build-template
  dependencies:
    - opam-boot
  variables:
    EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes"
    EXTRA_PACKAGES: "$COQIDE_PACKAGES $COQDOC_PACKAGES"
    PIP_PACKAGES: "$SPHINX_PACKAGES"

# no coqide for 32bit: libgtk installation problems
build:32bit:
  <<: *build-template
  dependencies:
    - opam-boot:32bit
  variables:
    EXTRA_CONF: "-native-compiler yes"
    EXTRA_PACKAGES: "gcc-multilib"

build:bleeding-edge:
  <<: *build-template
  dependencies:
    - opam-boot:bleeding-edge
  variables:
    EXTRA_CONF: "-native-compiler yes -coqide opt"
    EXTRA_PACKAGES: "$COQIDE_PACKAGES"

warnings:
  <<: *warnings-template
  dependencies:
    - opam-boot

# warnings:32bit:
#   <<: *warnings-template
#   variables:
#     <<: *warnings-variables
#     EXTRA_PACKAGES: "$gcc-multilib COQIDE_PACKAGES_32BIT"
#   dependencies:
#     - opam-boot:32bit

warnings:bleeding-edge:
  <<: *warnings-template
  dependencies:
    - opam-boot:bleeding-edge

test-suite:
  <<: *test-suite-template
  dependencies:
    - opam-boot
    - build
  variables:
    EXTRA_PACKAGES: "$TIMING_PACKAGES"

test-suite:32bit:
  <<: *test-suite-template
  dependencies:
    - opam-boot:32bit
    - build:32bit
  variables:
    EXTRA_PACKAGES: "gcc-multilib $TIMING_PACKAGES"

test-suite:bleeding-edge:
  <<: *test-suite-template
  dependencies:
    - opam-boot:bleeding-edge
    - build:bleeding-edge
  variables:
    EXTRA_PACKAGES: "$TIMING_PACKAGES"

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

validate:32bit:
  <<: *validate-template
  dependencies:
    - opam-boot:32bit
    - build:32bit
  variables:
    EXTRA_PACKAGES: "gcc-multilib"

ci-bignums:
  <<: *ci-template

ci-color:
  <<: *ci-template
  variables:
    <<: *ci-template-vars
    EXTRA_PACKAGES: "$TIMING_PACKAGES"

ci-compcert:
  <<: *ci-template

ci-coq-dpdgraph:
  <<: *ci-template
  variables:
    <<: *ci-template-vars
    EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf"

ci-coquelicot:
  <<: *ci-template
  variables:
    <<: *ci-template-vars
    EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf"

ci-elpi:
  <<: *ci-template

ci-equations:
  <<: *ci-template

ci-geocoq:
  <<: *ci-template
  allow_failure: true

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

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

ci-fiat-parsers:
  <<: *ci-template
  variables:
    <<: *ci-template-vars
    EXTRA_PACKAGES: "$TIMING_PACKAGES"

ci-flocq:
  <<: *ci-template
  variables:
    <<: *ci-template-vars
    EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf"

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

ci-hott:
  <<: *ci-template
  variables:
    <<: *ci-template-vars
    EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf"

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-sf:
  <<: *ci-template
  variables:
    <<: *ci-template-vars
    EXTRA_PACKAGES: "$TIMING_PACKAGES wget"

ci-unimath:
  <<: *ci-template

ci-vst:
  <<: *ci-template