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
- stage-5 # Only dependencies in stage 1, 2, 3, and 4
- deploy
# When a job has no dependencies, it goes to stage 1. Otherwise, we
# set "needs" to contain all transitive dependencies (with "artifacts:
# false" when we don't want the artifacts). We include the transitive
# dependencies due to gitlab bugs sometimes starting the job even if a
# transitive dep failed, see #10699 / 7b59d8c9d9b2104de7162ec0e40f6182a6830046.
# some default values
variables:
# Format: $IMAGE-V$DATE-$hash
# The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
# echo $(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10)
CACHEKEY: "bionic_coq-V2021-05-22-9c7889b60a"
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"
include:
- local: '/dev/bench/gitlab-bench.yml'
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"
- $ONLY_WINDOWS == "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
- dev/tools/check-cachekey.sh
################ GITLAB CACHING ######################
# - use artifacts between jobs #
######################################################
# TODO figure out how to build doc for installed Coq
.build-template:
stage: stage-1
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
artifacts:
name: "$CI_JOB_NAME"
paths:
- _install_ci
- config/Makefile
- config/coq_config.py
- config/coq_config.ml
- config/dune.c_flags
- dmesg.txt
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" world $EXTRA_TARGET
- echo 'end:coq:build'
- echo 'start:coq.install'
- make install $EXTRA_INSTALL
- echo 'end:coq.install'
- set +e
# Template for building Coq + stdlib, typical use: overload the switch
.dune-template:
stage: stage-1
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
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
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
needs:
- 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 "needs" 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
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
needs:
- 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 "needs" when using
.test-suite-template:
stage: stage-2
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
needs:
- 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 "needs" when using
.validate-template:
stage: stage-2
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
needs:
- not-a-real-job
script:
# exit 0: workaround for https://gitlab.com/gitlab-org/gitlab/issues/202505
# the validate:quick job is sometimes started before build:quick, without artifacts
# we ignore these spurious errors so if the job fails it's a real error
- cd _install_ci || exit 0
- 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
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
script:
- set -e
- echo 'start:coq.test'
- make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}"
- echo 'end:coq.test'
- set +e
artifacts:
name: "$CI_JOB_NAME"
paths:
- _build_ci
when: always
needs:
- build:base
.ci-template-flambda:
extends: .ci-template
needs:
- build:edge+flambda
variables:
OPAM_SWITCH: "edge"
OPAM_VARIANT: "+flambda"
.platform-template:
stage: stage-1
interruptible: true
variables:
PLATFORM: "https://github.com/coq/platform/archive/dev-ci.zip"
artifacts:
name: "$CI_JOB_NAME"
paths:
- artifacts
when: always
expire_in: 1 week
before_script: [] # We don't want to use the shared 'before_script'
.deploy-template:
stage: deploy
except:
variables:
- $ONLY_WINDOWS == "true"
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"
after_script:
- dmesg > dmesg.txt
timeout: 100m
allow_failure: true # See https://github.com/coq/coq/issues/9658
only:
variables:
- $UNRELIABLE =~ /enabled/
artifacts:
when: always
build:quick:
extends: .build-template
variables:
COQ_EXTRA_CONF: "-native-compiler no"
QUICK: "1"
after_script:
- dmesg > dmesg.txt
timeout: 100m
allow_failure: true # See https://github.com/coq/coq/issues/9637
only:
variables:
- $UNRELIABLE =~ /enabled/
artifacts:
when: always
windows64:
extends: .platform-template
variables:
ARCH: "64"
script:
- call dev/ci/platform-windows.bat
tags:
- windows-inria
only:
variables:
- $WINDOWS =~ /enabled/
lint:
stage: stage-1
except:
variables:
- $ONLY_WINDOWS == "true"
script: dev/lint-repository.sh
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
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
# OPAM will build out-of-tree so no point in importing artifacts
script:
- set -e
- opam pin add --kind=path coq-core.dev .
- opam pin add --kind=path coq-stdlib.dev .
- opam pin add --kind=path coqide-server.dev .
- opam pin add --kind=path coqide.dev .
- set +e
variables:
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=
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.*\..*$/
except:
variables:
- $ONLY_WINDOWS == "true"
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
needs:
- pkg:nix:deploy
script:
- echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null
# Remove all pr branches because they could be missing when we run git fetch --unshallow
- git branch --list 'pr-*' | xargs -r git branch -D
- 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:
refs:
- master
- /^v.*\..*$/
variables:
- $ONLY_WINDOWS == "true"
doc:refman:
extends: .doc-template
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
# currently bugged: dune cleans up the glob files so no links
# see #12699
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
needs:
- doc:ml-api:odoc
- doc:refman:dune
- build:base
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 _install_ci/share/doc/coq/html/stdlib _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
needs:
- build:base
test-suite:base+32bit:
extends: .test-suite-template
needs:
- build:base+32bit
variables:
OPAM_VARIANT: "+32bit"
only: *full-ci
test-suite:edge+flambda:
extends: .test-suite-template
needs:
- build:edge+flambda
variables:
OPAM_SWITCH: edge
OPAM_VARIANT: "+flambda"
only: *full-ci
test-suite:edge:dune:dev:
stage: stage-2
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
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:ocaml+beta+dune-template:
stage: stage-1
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
script:
- opam switch create $OCAMLVER --empty
- eval $(opam env)
- opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git
- opam update
- opam install ocaml-variants=$OCAMLVER
- opam install dune zarith
- 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:4.12+trunk+dune:
# extends: .test-suite:ocaml+beta+dune-template
# variables:
# OCAMLVER: 4.12.0+trunk
test-suite:base+async:
extends: .test-suite-template
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
needs:
- build:base
validate:base+32bit:
extends: .validate-template
needs:
- build:base+32bit
variables:
OPAM_VARIANT: "+32bit"
only: *full-ci
validate:edge+flambda:
extends: .validate-template
needs:
- build:edge+flambda
variables:
OPAM_SWITCH: edge
OPAM_VARIANT: "+flambda"
only: *full-ci
validate:quick:
extends: .validate-template
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
variables:
NJOBS: "1"
library:ci-color:
extends: .ci-template-flambda
stage: stage-3
needs:
- build:edge+flambda
- plugin:ci-bignums
library:ci-compcert:
stage: stage-3
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-flocq
- library:ci-menhir
library:ci-coq_performance_tests:
extends: .ci-template
library:ci-coq_tools:
extends: .ci-template
library:ci-coqprime:
stage: stage-3
extends: .ci-template-flambda
needs:
- build:edge+flambda
- plugin:ci-bignums
library:ci-coqtail:
extends: .ci-template
library:ci-coquelicot:
stage: stage-3
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-mathcomp
library:ci-cross_crypto:
extends: .ci-template
library:ci-engine_bench:
extends: .ci-template
library:ci-fcsl_pcm:
extends: .ci-template-flambda
stage: stage-3
needs:
- build:edge+flambda
- library:ci-mathcomp
library:ci-fiat_crypto:
extends: .ci-template-flambda
stage: stage-4
needs:
- build:edge+flambda
- library:ci-coqprime
- plugin:ci-bignums
- plugin:ci-rewriter
library:ci-fiat_crypto_legacy:
extends: .ci-template-flambda
allow_failure: true # See https://github.com/coq/coq/wiki/Coq-Call-2020-06-24#adding-back-fiat-crypto-legacy
# 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_ocaml:
extends: .ci-template
stage: stage-5
needs:
- build:edge+flambda
- library:ci-coqprime
- plugin:ci-bignums
- plugin:ci-rewriter
- library:ci-fiat_crypto
library:ci-flocq:
extends: .ci-template-flambda
library:ci-menhir:
extends: .ci-template-flambda
library:ci-oddorder:
extends: .ci-template-flambda
stage: stage-3
needs:
- build:edge+flambda
- library:ci-mathcomp
library:ci-fourcolor:
extends: .ci-template-flambda
stage: stage-3
needs:
- build:edge+flambda
- library:ci-mathcomp
library:ci-corn:
extends: .ci-template-flambda
stage: stage-4
needs:
- build:edge+flambda
- plugin:ci-bignums
- library:ci-math_classes
plugin:ci-gappa:
extends: .ci-template-flambda
stage: stage-3
needs:
- build:edge+flambda
- library:ci-flocq
library:ci-geocoq:
extends: .ci-template-flambda
stage: stage-3
needs:
- build:edge+flambda
- library:ci-mathcomp
library:ci-hott:
extends: .ci-template
library:ci-iris:
extends: .ci-template-flambda
library:ci-math_classes:
extends: .ci-template-flambda
stage: stage-3
needs:
- build:edge+flambda
- plugin:ci-bignums
library:ci-mathcomp:
extends: .ci-template-flambda
library:ci-mczify:
extends: .ci-template-flambda
stage: stage-3
needs:
- build:edge+flambda
- library:ci-mathcomp
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
stage: stage-3
needs:
- build:edge+flambda
- library:ci-flocq
library:ci-deriving:
extends: .ci-template-flambda
stage: stage-3
needs:
- build:edge+flambda
- library:ci-mathcomp
# 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
plugin:ci-coq_dpdgraph:
extends: .ci-template
plugin:ci-coqhammer:
extends: .ci-template-flambda
plugin:ci-elpi:
extends: .ci-template
plugin:ci-equations:
extends: .ci-template
plugin:ci-fiat_parsers:
extends: .ci-template
plugin:ci-metacoq:
extends: .ci-template
stage: stage-3
needs:
- 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
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
script:
- ./configure -local -warn-error yes
- make -j "$NJOBS" plugin-tutorial
plugin:ci-quickchick:
extends: .ci-template-flambda
stage: stage-3
needs:
- build:edge+flambda
- library:ci-mathcomp
plugin:ci-reduction_effects:
extends: .ci-template
plugin:ci-relation_algebra:
extends: .ci-template
plugin:ci-rewriter:
extends: .ci-template-flambda
plugin:ci-vscoq:
extends: .ci-template