.gitlab-ci.yml

image: "$IMAGE"

stages:
  - docker
  - stage-1 # No dependencies
  - stage-2 # Only dependencies in stage 1
  - stage-3 # Only dependencies in stage 1 and 2
  - stage-4 # Only dependencies in stage 1, 2 and 3
  - deploy

# When a job has no dependencies, it goes to stage 1.  Otherwise, we
# set both "needs" and "dependencies". "needs" is a superset of
# "dependencies" that should include all the transitive dependencies.
# "dependencies" only list the previous jobs whose artifact we need to
# keep.

# some default values
variables:
  # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
  # for reference]
  CACHEKEY: "bionic_coq-V2020-03-13-V69"
  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: ""
  GIT_DEPTH: "10"

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 set -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
  - eval $(opam env)
  - opam list
  - opam config list

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

# TODO figure out how to build doc for installed Coq
.build-template:
  stage: stage-1
  interruptible: true
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _install_ci
      - config/Makefile
      - config/coq_config.py
      - config/coq_config.ml
      - 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 -warn-error yes -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 install-byte $EXTRA_INSTALL
    - make install-byte
    - cp bin/fake_ide _install_ci/bin/
    - echo 'end:coq.install'

    - set +e

# Template for building Coq + stdlib, typical use: overload the switch
.dune-template:
  stage: stage-1
  interruptible: true
  dependencies: []
  script:
    # flambda can be pretty stack hungry, specially with -O3
    # See also https://github.com/ocaml/ocaml/issues/7842#issuecomment-596863244
    # and https://github.com/coq/coq/pull/11916#issuecomment-609977375
    - ulimit -s 16384
    - set -e
    - make -f Makefile.dune world
    - set +e
    - tar cfj _build.tar.bz2 _build
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
  artifacts:
    name: "$CI_JOB_NAME"
    when: always
    paths:
      - _build/log
      - _build.tar.bz2
    expire_in: 1 week

.dune-ci-template:
  stage: stage-2
  interruptible: true
  needs:
    - build:edge+flambda:dune:dev
  dependencies:
    - build:edge+flambda:dune:dev
  script:
    - tar xfj _build.tar.bz2
    - set -e
    - echo 'start:coq.test'
    - make -f Makefile.dune "$DUNE_TARGET"
    - echo 'end:coq.test'
    - set +e
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
  artifacts:
    when: always
    name: "$CI_JOB_NAME"
    expire_in: 2 months

# 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-template:
  stage: stage-2
  interruptible: true
  dependencies:
    - not-a-real-job
  script:
    - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/"'
    - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= refman
    - make install-doc-sphinx
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _install_ci/share/doc/coq/
    expire_in: 2 months

# set dependencies when using
.test-suite-template:
  stage: stage-2
  interruptible: true
  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)/
    - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH"
    - COQEXTRAFLAGS="${COQEXTRAFLAGS}" make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" all
  artifacts:
    name: "$CI_JOB_NAME.logs"
    when: on_failure
    paths:
      - test-suite/logs
    # Gitlab doesn't support yet "expire_in: never" so we use the instance default
    # expire_in: never

# set dependencies when using
.validate-template:
  stage: stage-2
  interruptible: true
  dependencies:
    - not-a-real-job
  script:
    - cd _install_ci
    - find lib/coq/ -name '*.vo' -fprint0 vofiles
    - xargs -0 --arg-file=vofiles bin/coqchk -o -m -coqlib lib/coq/ > ../coqchk.log 2>&1 || touch coqchk.failed
    - tail -n 1000 ../coqchk.log # the log is too big for gitlab so pipe to a file and display the tail
    - "[ ! -f coqchk.failed ]" # needs quoting for yml syntax reasons
  artifacts:
    name: "$CI_JOB_NAME.logs"
    paths:
      - coqchk.log
    expire_in: 2 months

.ci-template:
  stage: stage-2
  interruptible: true
  script:
    - set -e
    - echo 'start:coq.test'
    - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}"
    - echo 'end:coq.test'
    - set +e
  needs:
    - build:base
  dependencies:
    - build:base

.ci-template-flambda:
  extends: .ci-template
  needs:
    - build:edge+flambda
  dependencies:
    - build:edge+flambda
  variables:
    OPAM_SWITCH: "edge"
    OPAM_VARIANT: "+flambda"

.windows-template:
  stage: stage-1
  interruptible: true
  artifacts:
    name: "%CI_JOB_NAME%"
    paths:
      - artifacts
    when: always
    expire_in: 1 week
  dependencies: []
  tags:
    - windows-inria
  before_script: []
  script:
    - call dev/ci/gitlab.bat
  only:
    variables:
      - $WINDOWS =~ /enabled/

.deploy-template:
  stage: deploy
  before_script:
    - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y )
    - eval $(ssh-agent -s)
    - mkdir -p ~/.ssh
    - chmod 700 ~/.ssh
    - ssh-keyscan -t rsa github.com >> ~/.ssh/known_hosts
    - git config --global user.name "coqbot"
    - git config --global user.email "coqbot@users.noreply.github.com"

build:base:
  extends: .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: "doc-stdlib"
    EXTRA_INSTALL: "install-doc-stdlib-html install-doc-printable"

# no coqide for 32bit: libgtk installation problems
build:base+32bit:
  extends: .build-template
  variables:
    OPAM_VARIANT: "+32bit"
    COQ_EXTRA_CONF: "-native-compiler yes"
  only: &full-ci
    variables:
      - $FULL_CI == "true"

build:edge+flambda:
  extends: .build-template
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -flambda-opts "
    COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures"

build:edge+flambda:dune:dev:
  extends: .dune-template

build:base+async:
  extends: .build-template
  stage: stage-1
  variables:
    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
    COQUSERFLAGS: "-async-proofs on"
  timeout: 100m
  allow_failure: true # See https://github.com/coq/coq/issues/9658
  only:
    variables:
      - $UNRELIABLE =~ /enabled/

build:quick:
  extends: .build-template
  variables:
    COQ_EXTRA_CONF: "-native-compiler no"
    QUICK: "1"
  timeout: 100m
  allow_failure: true # See https://github.com/coq/coq/issues/9637
  only:
    variables:
      - $UNRELIABLE =~ /enabled/

windows64:
  extends: .windows-template
  variables:
    ARCH: "64"

windows32:
  extends: .windows-template
  variables:
    ARCH: "32"
  except:
    - /^pr-.*$/

lint:
  stage: stage-1
  script: dev/lint-repository.sh
  dependencies: []
  variables:
    GIT_DEPTH: "" # we need an unknown amount of history for per-commit linting
    OPAM_SWITCH: "edge"
    OPAM_VARIANT: "+flambda"

pkg:opam:
  stage: stage-1
  interruptible: true
  # OPAM will build out-of-tree so no point in importing artifacts
  dependencies: []
  script:
    - set -e
    - opam pin add --kind=path coq.$COQ_VERSION .
    - opam pin add --kind=path coqide-server.$COQ_VERSION .
    - opam pin add --kind=path coqide.$COQ_VERSION .
    - set +e
  variables:
    COQ_VERSION: "8.12"
    OPAM_SWITCH: "edge"
    OPAM_VARIANT: "+flambda"
  only: *full-ci

.nix-template:
  image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git
  interruptible: true
  stage: stage-1
  variables:
    # By default we use coq.cachix.org as an extra substituter but this can be overridden
    EXTRA_SUBSTITUTERS: https://coq.cachix.org
    EXTRA_PUBLIC_KEYS: coq.cachix.org-1:5QW/wwEnD+l2jvN6QRbRRsa4hBHG3QiQQ26cxu1F5tI=
    # The following variables should not be overridden
    GIT_STRATEGY: none
    NIXOS_PUBLIC_KEY: cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=

  dependencies: [] # We don't need to download build artifacts
  before_script: [] # We don't want to use the shared 'before_script'
  script:
    - cat /proc/{cpu,mem}info || true
    # Use current worktree as tmpdir to allow exporting artifacts in case of failure
    - export TMPDIR=$PWD
    # We build an expression rather than a direct URL to not be dependent on
    # the URL location; we are forced to put the public key of cache.nixos.org
    # because there is no --extra-trusted-public-key option.
    - nix-build -E "import (fetchTarball $CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz) {}" -K --extra-substituters "$EXTRA_SUBSTITUTERS" --trusted-public-keys "$NIXOS_PUBLIC_KEY $EXTRA_PUBLIC_KEYS" | if [ ! -z "$CACHIX_SIGNING_KEY" ]; then cachix push coq; fi
  artifacts:
    name: "$CI_JOB_NAME.logs"
    when: on_failure
    paths:
      - nix-build-coq.drv-0/*/test-suite/logs
    # Gitlab doesn't support yet "expire_in: never" so we use the instance default
    # expire_in: never

pkg:nix:deploy:
  extends: .nix-template
  environment:
    name: cachix
    url: https://coq.cachix.org
  before_script:
    # Install Cachix as documented at https://github.com/cachix/cachix
    - nix-env -iA cachix --prebuilt-only -f https://cachix.org/api/v1/install
  only:
    - master
    - /^v.*\..*$/

pkg:nix:deploy:channel:
  extends: .deploy-template
  environment:
    name: cachix
    url: https://coq.cachix.org
  only:
    refs: # Repeat conditions from pkg:nix:deploy
      - master
      - /^v.*\..*$/
    variables:
      - $CACHIX_DEPLOYMENT_KEY
  dependencies: []
  needs:
    - pkg:nix:deploy
  script:
    - echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null
    - git fetch --unshallow
    - git branch -v
    - git push git@github.com:coq/coq-on-cachix "${CI_COMMIT_SHA}":"refs/heads/${CI_COMMIT_REF_NAME}"

pkg:nix:
  extends: .nix-template
  except:
    - master
    - /^v.*\..*$/

doc:refman:
  extends: .doc-template
  dependencies:
    - build:base
  needs:
    - build:base

doc:refman:dune:
  extends: .dune-ci-template
  variables:
    DUNE_TARGET: refman-html
  artifacts:
    paths:
      - _build/log
      - _build/default/doc/refman-html

doc:refman-pdf:dune:
  extends: .dune-ci-template
  variables:
    DUNE_TARGET: refman-pdf
  artifacts:
    paths:
      - _build/log
      - _build/default/doc/refman-pdf

doc:stdlib:dune:
  extends: .dune-ci-template
  variables:
    DUNE_TARGET: stdlib-html
  artifacts:
    paths:
      - _build/log
      - _build/default/doc/stdlib/html

doc:refman:deploy:
  extends: .deploy-template
  environment:
    name: deployment
    url: https://coq.github.io/
  only:
    variables:
      - $DOCUMENTATION_DEPLOY_KEY
  dependencies:
    - doc:ml-api:odoc
    - doc:refman:dune
    - doc:stdlib:dune
  needs:
    - doc:ml-api:odoc
    - doc:refman:dune
    - doc:stdlib:dune
  script:
    - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null
    - git clone git@github.com:coq/doc.git _deploy
    - rm -rf _deploy/$CI_COMMIT_REF_NAME/api
    - rm -rf _deploy/$CI_COMMIT_REF_NAME/refman
    - rm -rf _deploy/$CI_COMMIT_REF_NAME/stdlib
    - mkdir -p _deploy/$CI_COMMIT_REF_NAME
    - cp -rv _build/default/_doc/_html _deploy/$CI_COMMIT_REF_NAME/api
    - cp -rv _build/default/doc/refman-html _deploy/$CI_COMMIT_REF_NAME/refman
    - cp -rv _build/default/doc/stdlib/html _deploy/$CI_COMMIT_REF_NAME/stdlib
    - cd _deploy/$CI_COMMIT_REF_NAME/
    - git add api refman stdlib
    - git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA"
    - git push # TODO: rebase and retry on failure

doc:ml-api:odoc:
  extends: .dune-ci-template
  variables:
    DUNE_TARGET: apidoc
  artifacts:
    paths:
      - _build/log
      - _build/default/_doc/

test-suite:base:
  extends: .test-suite-template
  dependencies:
    - build:base
  needs:
    - build:base

test-suite:base+32bit:
  extends: .test-suite-template
  dependencies:
    - build:base+32bit
  needs:
    - build:base+32bit
  variables:
    OPAM_VARIANT: "+32bit"
  only: *full-ci

test-suite:edge+flambda:
  extends: .test-suite-template
  dependencies:
    - build:edge+flambda
  needs:
    - build:edge+flambda
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
  only: *full-ci

test-suite:edge:dune:dev:
  stage: stage-2
  dependencies:
    - build:edge+flambda:dune:dev
  needs:
    - build:edge+flambda:dune:dev
  script:
    - tar xfj _build.tar.bz2
    - make -f Makefile.dune test-suite
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
  artifacts:
    name: "$CI_JOB_NAME.logs"
    when: on_failure
    paths:
      - _build/default/test-suite/logs
    # Gitlab doesn't support yet "expire_in: never" so we use the instance default
    # expire_in: never

test-suite:edge+4.11+trunk+dune:
  stage: stage-1
  dependencies: []
  script:
    - opam switch create 4.11.0 --empty
    - eval $(opam env)
    - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git
    - opam update
    - opam install ocaml-variants=4.11.0+trunk
    - opam install dune num
    - eval $(opam env)
    - export COQ_UNIT_TEST=noop
    - make -f Makefile.dune test-suite
  variables:
    OPAM_SWITCH: base
  artifacts:
    name: "$CI_JOB_NAME.logs"
    when: always
    paths:
      - _build/log
      - _build/default/test-suite/logs
    expire_in: 2 week
  allow_failure: true

test-suite:base+async:
  extends: .test-suite-template
  dependencies:
    - build:base
  needs:
    - build:base
  variables:
    COQEXTRAFLAGS: "-async-proofs on -async-proofs-cache force"
  timeout: 100m
  allow_failure: true
  only:
    variables:
      - $UNRELIABLE =~ /enabled/

validate:base:
  extends: .validate-template
  dependencies:
    - build:base
  needs:
    - build:base

validate:base+32bit:
  extends: .validate-template
  dependencies:
    - build:base+32bit
  needs:
    - build:base+32bit
  variables:
    OPAM_VARIANT: "+32bit"
  only: *full-ci

validate:edge+flambda:
  extends: .validate-template
  dependencies:
    - build:edge+flambda
  needs:
    - build:edge+flambda
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
  only: *full-ci

validate:quick:
  extends: .validate-template
  dependencies:
    - build:quick
  needs:
    - build:quick
  only:
    variables:
      - $UNRELIABLE =~ /enabled/

# Libraries are by convention the projects that depend on Coq
# but not on its ML API

library:ci-argosy:
  extends: .ci-template

library:ci-bbv:
  extends: .ci-template

library:ci-bedrock2:
  extends: .ci-template-flambda
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _build_ci
  variables:
    NJOBS: "1"

library:ci-color:
  extends: .ci-template-flambda
  stage: stage-3
  needs:
  - build:edge+flambda
  - plugin:ci-bignums
  dependencies:
  - build:edge+flambda
  - plugin:ci-bignums

library:ci-compcert:
  extends: .ci-template-flambda

library:ci-coqprime:
  stage: stage-3
  extends: .ci-template-flambda
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _build_ci
  needs:
  - build:edge+flambda
  - plugin:ci-bignums
  dependencies:
  - build:edge+flambda
  - plugin:ci-bignums

library:ci-coquelicot:
  extends: .ci-template

library:ci-cross-crypto:
  extends: .ci-template

library:ci-fcsl-pcm:
  extends: .ci-template

# We cannot use flambda due to
# https://github.com/ocaml/ocaml/issues/7842, see
# https://github.com/coq/coq/pull/11916#issuecomment-609977375
library:ci-fiat-crypto:
  extends: .ci-template
  stage: stage-4
  needs:
  - build:edge+flambda
  - library:ci-coqprime
  - plugin:ci-bignums
  - plugin:ci-rewriter
  dependencies:
  - build:edge+flambda
  - library:ci-coqprime
  - plugin:ci-rewriter

library:ci-flocq:
  extends: .ci-template

library:ci-corn:
  extends: .ci-template-flambda
  stage: stage-4
  needs:
  - build:edge+flambda
  - plugin:ci-bignums
  - library:ci-math-classes
  dependencies:
  - build:edge+flambda
  - library:ci-math-classes

library:ci-geocoq:
  extends: .ci-template-flambda

library:ci-hott:
  extends: .ci-template

library:ci-iris-lambda-rust:
  extends: .ci-template-flambda

library:ci-math-classes:
  extends: .ci-template-flambda
  stage: stage-3
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _build_ci
  needs:
  - build:edge+flambda
  - plugin:ci-bignums
  dependencies:
  - build:edge+flambda
  - plugin:ci-bignums

library:ci-math-comp:
  extends: .ci-template-flambda

library:ci-sf:
  extends: .ci-template

library:ci-stdlib2:
  extends: .ci-template-flambda

library:ci-tlc:
  extends: .ci-template

library:ci-unimath:
  extends: .ci-template-flambda

library:ci-verdi-raft:
  extends: .ci-template-flambda

library:ci-vst:
  extends: .ci-template-flambda

# Plugins are by definition the projects that depend on Coq's ML API

plugin:ci-aac_tactics:
  extends: .ci-template

plugin:ci-bignums:
  extends: .ci-template-flambda
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _build_ci

plugin:ci-coq_dpdgraph:
  extends: .ci-template

plugin:ci-coqhammer:
  extends: .ci-template

plugin:ci-elpi:
  extends: .ci-template

plugin:ci-equations:
  extends: .ci-template
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _build_ci

plugin:ci-fiat_parsers:
  extends: .ci-template

plugin:ci-metacoq:
  extends: .ci-template
  stage: stage-3
  needs:
  - build:base
  - plugin:ci-equations
  dependencies:
  - build:base
  - plugin:ci-equations

plugin:ci-mtac2:
  extends: .ci-template

plugin:ci-paramcoq:
  extends: .ci-template

plugin:ci-perennial:
  extends: .ci-template-flambda

plugin:plugin-tutorial:
  stage: stage-1
  dependencies: []
  script:
    - ./configure -local -warn-error yes
    - make -j "$NJOBS" plugin-tutorial

plugin:ci-quickchick:
  extends: .ci-template-flambda

plugin:ci-reduction_effects:
  extends: .ci-template

plugin:ci-relation_algebra:
  extends: .ci-template

plugin:ci-rewriter:
  extends: .ci-template-flambda
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _build_ci