.gitlab-ci.yml

image: ocaml/opam:ubuntu

# this doesn't seem to work
cache:
  paths:
    - .opamcache

stages:
  - build
  - test

variables:
  # some default values
  NJOBS: "2"
  COMPILER: "system"
  CAMLP5_VER: "6.14"

  # 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: "num 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"
  COQDOC_OPAM: "hevea"


before_script:
  - ls # figure out if artifacts are around
  - printenv
#  - if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi
  - if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -qq && sudo apt-get install -y -qq ${EXTRA_PACKAGES}; fi

  # setup cache
  - if [ ! "(" -d .opamcache ")" ]; then mv ~/.opam .opamcache; else mv ~/.opam ~/.opam-old; fi
  - ln -s $(readlink -f .opamcache) ~/.opam

  # 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 repository set-url default https://opam.ocaml.org
  - opam update
  - opam switch ${COMPILER}
  - eval $(opam config env)
  - opam config list
  - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM}
  - rm -rf ~/.opam/log/
  - opam list

# 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
  variables: &build-variables
    EXTRA_CONF: "-native-compiler yes -coqide opt"
    EXTRA_PACKAGES: "$COQIDE_PACKAGES"
    EXTRA_OPAM: "$COQIDE_OPAM"

.warnings-template: &warnings-template
  # keep warnings in test stage so we can test things even when warnings occur
  stage: test
  dependencies: []
  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"

.test-suite-template: &test-suite-template
  stage: test
  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

.validate-template: &validate-template
  stage: test
  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/

.documentation-template: &documentation-template
  stage: test
  script:
    - INSTALLDIR=$(readlink -f _install_ci)
    - cp "$INSTALLDIR/lib/coq/tools/coqdoc/coqdoc.sty" .

    - LIB="$INSTALLDIR/lib/coq"
    # WTF using a newline makes make sigsev
    # see https://gitlab.com/SkySkimmer/coq/builds/17313312
    - DOCVFILES=$(find "$LIB/" -name '*.v' -printf "%p ")
    - DOCLIGHTDIRS="$LIB/theories/Init/ $LIB/theories/Logic/ $LIB/theories/Unicode/ $LIB/theories/Arith/"
    - DOCLIGHTVOFILES=$(find $DOCLIGHTDIRS -name '*.vo' -printf "%p ")

    - make doc QUICK=true COQDOC_NOBOOT=true COQTEX="$INSTALLDIR/bin/coq-tex" COQDOC="$INSTALLDIR/bin/coqdoc" VFILES="$DOCVFILES" THEORIESLIGHTVO="$DOCLIGHTVOFILES"

    - make install-doc
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _install_ci/share/doc
    expire_in: 1 week

.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"
    EXTRA_PACKAGES: "$TIMING_PACKAGES"

build:
  <<: *build-template

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

build:bleeding-edge:
  <<: *build-template
  variables:
    <<: *build-variables
    COMPILER: "$COMPILER_BLEEDING_EDGE"
    CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE"
    EXTRA_OPAM: "$COQIDE_OPAM_BE"

warnings:
  <<: *warnings-template

# warnings:32bit:
#   <<: *warnings-template
#   variables:
#     <<: *warnings-variables
#     EXTRA_PACKAGES: "$gcc-multilib COQIDE_PACKAGES_32BIT"
#     COMPILER: "$COMPILER_32BIT"

warnings:bleeding-edge:
  <<: *warnings-template
  variables:
    <<: *warnings-variables
    COMPILER: "$COMPILER_BLEEDING_EDGE"
    CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE"
    EXTRA_OPAM: "$COQIDE_OPAM_BE"

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

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

test-suite:bleeding-edge:
  <<: *test-suite-template
  dependencies:
    - build:bleeding-edge
  variables:
    COMPILER: "$COMPILER_BLEEDING_EDGE"
    CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE"
    EXTRA_PACKAGES: "$TIMING_PACKAGES"

documentation:
  <<: *documentation-template
  dependencies:
    - build
  variables:
    EXTRA_PACKAGES: "$COQDOC_PACKAGES"
    EXTRA_OPAM: "$COQDOC_OPAM"

documentation:bleeding-edge:
  <<: *documentation-template
  dependencies:
    - build:bleeding-edge
  variables:
    COMPILER: "$COMPILER_BLEEDING_EDGE"
    CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE"
    EXTRA_PACKAGES: "$COQDOC_PACKAGES"
    EXTRA_OPAM: "$COQDOC_OPAM"

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

validate:32bit:
  <<: *validate-template
  dependencies:
    - build:32bit
  variables:
    COMPILER: "$COMPILER_32BIT"
    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_OPAM: "ocamlgraph"
    EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf"

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

ci-elpi:
  <<: *ci-template
  variables:
    <<: *ci-template-vars
    EXTRA_OPAM: "ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree"

ci-equations:
  <<: *ci-template

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

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

ci-unimath:
  <<: *ci-template

ci-vst:
  <<: *ci-template