Commits (83)
## Shared Iris CI
# Shared Iris CI
This repository contains the shared Iris CI. It contains common code for Iris projects' CI.
This repository contains the shared Iris CI. It contains common code for Iris
projects' CI.
Projects automatically use the latest commit of some branch for their CI, so branches should remain reasonably compatible.
Every branch here comes with a corresponding branch [in the Docker repo](https://github.com/RalfJung/opam-ci), providing the Docker image that should be used.
Currently, we have the following branches:
Projects automatically use the latest commit of some branch for their CI, so
branches should remain reasonably compatible. Every branch here comes with a
corresponding branch [in the Docker repo](https://github.com/RalfJung/opam-ci),
providing the Docker image that should be used. Currently, we have the
following branches:
* [`opam2`](https://gitlab.mpi-sws.org/FP/iris-ci/tree/opam2), using opam 2.0.
## How to configure CI for your project
First of all, your project needs to have a CI runner. We have two runners
dedicated for Iris projects, where `coop-timing` is used for jobs that do timing
measurements (so these runners are more isolated from each other, at the cost of
overall parallelism) and `coop` performs all the "normal" jobs. Talk to a
GitLab admin to get them added to your project. The timing runner should only
be added to "official" projects in the Iris group, both because of the lack of
parallelism and because the [timing visualization website][coq-speed] assumes
this. See the [timing section](#timing) for more information.
Inside your project, create a `.gitlab-ci.yml` with the following prelude:
image: ralfjung/opam-ci:opam2
- build
.template: &template
stage: build
- fp
- git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
- ci/buildjob
key: "$CI_JOB_NAME"
- opamroot/
- master
- /^ci/
- triggers
- schedules
- api
## Build jobs
This sets up a template that we will use for the jobs. The `tags` determine the
CI runner that will pick up these jobs; `only` and `except` make this run only
when things get pushed to master and branches whose name start with `ci` and not
when the pipeline gets triggered though the API or an automatic schedule. See
[the GitLab CI documentation][gitlab-ci] for more information.
[gitlab-ci]: https://docs.gitlab.com/ce/ci/yaml/README.html
Below this, you can configure your build jobs. A normal job looks like this:
<<: *template
OPAM_PINS: "coq version 8.10.1"
This builds your project against Coq 8.8.2. The first line determines the job
name shown in GitLab. The second line imports the template we defined in the
prelude. The last two lines configure the job; `OPAM_PINS` sets up the pins for
the environment that the job will be built in. You can add `CI_COQCHK: "1"` to
run `coqchk` after the build is done; be aware that can be very slow and hence
use a lot of CI time.
See [buildjob](buildjob) for a list of available configuration variables. Some
of them require a secret or a key to be configured for the project; these are
passed in as "Environment variables" setup in the GitLab UI. Below, we describe
some of the things that are common amongst Iris build jobs.
## Nightly builds
To make sure that a project keeps working as we update Iris, we can set up
nightly builds against the latest Iris version, and often we pin that to a
*branch* of Coq to make sure we keep working with the next patch release. To
this end, add a job like this:
<<: *template
OPAM_PINS: "coq version 8.10.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
- triggers
- schedules
- api
The last four lines configure this job to *not* run when new commits are pushed
to the repo, and instead make it run when a pipeline is triggered through the
REST API or by a schedule. The pins are set up to install a development version
of all the dependencies, and the `8.10` branch of Coq.
Now ask an admin to set up a pipeline schedule. The schedule should set all the
`_REV` variables to the branches that should be tested against. We usually only
do nightly builds for projects in the iris group; those schedules should be
"owned" by the `iris-dev` user so that the Iris development team gets the emails
about broken builds. This can be achieved by having an admin follow these steps:
* At <https://gitlab.mpi-sws.org/admin/users/iris-dev>, click "Impersonate".
* Go to the schedule settings for the project you are setting up, and add the
schedule. It will be owned by `iris-dev`. If you already created the schedule,
you can "Take ownership" to make `iris-dev` own it.
* Click the button in the top-right corner to stop impersonating `iris-dev`.
## Timing
To track performance of the project, one of the jobs should look like this:
<<: *template
OPAM_PINS: "coq version 8.10.0"
TIMING_CONF: "coq-8.10.0"
- fp-timing
The last two lines makes this job run on the more isolated runner. The
`TIMING_CONF` variable triggers measuring the performance of building every
single file of this project. This information is submitted to the [coq-speed]
server where you can browse it in a web UI. Be careful to pick a unique
`TIMING_CONF` if you are timing in multiple jobs, or the build will fail because
of duplicate timing data.
This requires setting the `TIMING_SECRET` CI variable. Talk to an admin about
this. The variable should *not* be protected because we do timing measurements
on all branches, not just `master`!
[coq-speed]: https://coq-speed.mpi-sws.org/
## Opam publishing
Those of our projects that have reverse dependencies get automatically published
on [our opam repo][opam]. Set the `OPAM_PKG` variable to the name of the
package to make that happen. This requires a per-project secret, see
[the private opam-updater documentation][opam-updater] for more details. Be
careful to only set `OPAM_PKG` in one job, or your builds will fail because the
same commit gets published several times!
[opam]: https://gitlab.mpi-sws.org/iris/opam
[opam-updater]: https://gitlab.mpi-sws.org/iris/opam-updater
## coqdoc publishing
We can automatically deploy the generated coqdoc for a project to
[the web][coqdoc]. To make this happens, set `DOC_DIR` to an rsync path where
the docs should be pushed to; usually that's something like
`"coqdoc@center.mpi-sws.org:projectname"`. You also need to add the secret part
of an SSH key that can access this location in the `DOC_KEY` variable (that
should be a protected variable because it is only needed by the `master`
branch). Preferably, use a fresh key for each project. For
`coqdoc@center.mpi-sws.org`, these keys should be set up as follows in
command="$HOME/rrsync /www/sws-websites/plv.mpi-sws.org/coqdoc/",no-port-forwarding,no-X11-forwarding,no-agent-forwarding,no-pty
This restricts the key to only be able to run rsync for this particular
[coqdoc]: https://plv.mpi-sws.org/coqdoc
......@@ -19,3 +19,16 @@ echo_color() {
# $2: the string
echo -e "\e[${1}m${2}\e[0m"
status() {
echo_color "$BOLDGREEN" "$1"
warn() {
echo_color "$BOLDYELLOW" "$1"
panic() {
echo_color "$BOLDRED" "$1"
exit 1
set -e
set -o pipefail
set -eo pipefail
#set -x
. ci/ansi-colors.sh
## This runs a default build job. The following variables are noteworthy:
## - $OCAML: The OCaml version to use. Defaults to `ocaml-system`. This MUST
## start with a package name, e.g. `ocaml-base-compiler.4.07.0`.
## - $OPAM_PINS: Space-separated list of packages to pin in opam, in the format
## - $VALIDATE: If non-empty, run `make validate`
## - $CI_COQCHK: If non-empty, run `coqchk` via `make validate`
## - $MANGLE_NAMES: If non-empty, add `-mangle-names` parameter to Coq
## invocation.
## non-empty, release this commit as a new package on opam when done.
## Requires the $OPAM_UPDATE_SECRET variable to be set. This only happens if
## the current branch is $OPAM_PKG_BRANCH, or master if that variable is
## empty.
## non-empty, submit timing information to coq-speed with the given project
## name and configuration string. Reqires the $TIMING_SECRET variable to be
## set.
## - $DOC_DIR, $DOC_BRANCH, $DOC_KEY: If $DOC_DIR is non-empty, run coqdoc and
## upload the results to the given directory. This only happens if the
## current branch is $DOC_BRANCH (defaults to master). Requires the $DOC_KEY
## variable to be set to the secret key for uploading.
## name and configuration string. The project names defaults to the
## repository name. Reqires the $TIMING_SECRET variable to be set.
## - $DOC_DIR, $DOC_BRANCH, $DOC_KEY, $DOC_OPTS: If $DOC_DIR is non-empty, run
## coqdoc and upload the results to the given directory. This only happens if
## the current branch is $DOC_BRANCH (defaults to master). Requires the
## $DOC_KEY variable to be set to the secret key for uploading. $DOC_OPTS can
## be set to pass additional flags to coqdoc (particularly useful for
## --external).
echo_color "$BOLDGREEN" "[buildjob] Using CI branch $(cd ci && git rev-parse --abbrev-ref HEAD) ($(cd ci && git rev-parse HEAD))"
status "[buildjob] Using CI branch $(cd ci && git rev-parse --abbrev-ref HEAD) ($(cd ci && git rev-parse HEAD))"
# Environment sanity checks
if [[ -n "$VALIDATE" ]]; then
panic "[buildjob] Do not use the VALIDATE variable, it has been replaced by CI_COQCHK"
# Parepare
. ci/prepare-opam.sh $OPAM_PINS # deliberately not quoted
......@@ -31,27 +46,30 @@ env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
if [[ -n "$MANGLE_NAMES" ]]; then
export COQEXTRAFLAGS="$COQEXTRAFLAGS -mangle-names mangled_"
if [[ -n "$TIMING_PROJECT" ]]; then
if [[ -n "$TIMING_CONF" ]]; then
export TIMECMD=ci/perf
# Build
echo_color "$BOLDGREEN" "[buildjob] Perfoming build"
status "[buildjob] Perfoming build"
time make --output-sync --no-print-directory -k -j$CPU_CORES 2>&1
# maybe submit timing information
if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then
if [[ -n "$TIMING_CONF" ]]; then
# collect all information into one file
echo_color "$BOLDGREEN" "[buildjob] Build performance information"
status "[buildjob] Build performance information"
find -name "*.v.perf" -print0 | xargs -0 cat > build-times.txt
cat build-times.txt
# make sure we run on the timing machine
if [[ "$CI_RUNNER_TAGS" != "fp-timing" ]]; then
panic "[buildjob] Timing jobs must be tagged with fp-timing to get the right runner"
# check if we have the secret
echo_color "$BOLDGREEN" "[buildjob] Submitting timing information to coq-speed"
if [[ -z "$TIMING_SECRET" ]]; then
echo_color "$BOLDRED" "[buildjob] TIMING_SECRET variable is missing"
exit 1
panic "[buildjob] TIMING_SECRET variable is missing"
# Submit to webhook endpoint
status "[buildjob] Submitting timing information to coq-speed"
curl --fail -sS -X POST https://coq-speed.mpi-sws.org/webhook/build_times \
--user "$TIMING_SECRET" \
-H "X-Commit: $CI_COMMIT_SHA" \
......@@ -63,12 +81,10 @@ if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then
# maybe create opam package
if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == "${OPAM_PKG_BRANCH:-master}" ]]; then
echo_color "$BOLDGREEN" "[buildjob] Releasing package on opam"
if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == "$OPAM_PKG_BRANCH" ]]; then
# check if we have the secret
if [[ -z "$OPAM_UPDATE_SECRET" ]]; then
echo_color "$BOLDRED" "[buildjob] OPAM_UPDATE_SECRET variable is missing"
exit 1
panic "[buildjob] OPAM_UPDATE_SECRET variable is missing"
# determine package name prefix
if [[ "$CI_COMMIT_REF_NAME" == master ]]; then
......@@ -77,6 +93,7 @@ if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == "${OPAM_PKG_BRANCH:-master}" ]]
# Trigger opam updater
status "[buildjob] Releasing package $OPAM_PKG on opam"
curl --fail -sS -X POST https://gitlab.mpi-sws.org/api/v4/projects/581/trigger/pipeline \
-F "ref=master" \
......@@ -89,18 +106,17 @@ if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == "${OPAM_PKG_BRANCH:-master}" ]]
# maybe validate
if [[ -n "$VALIDATE" ]]; then
echo_color "$BOLDGREEN" "[buildjob] Performing validation"
make validate
if [[ -n "$CI_COQCHK" ]]; then
status "[buildjob] Running coqchk"
time make validate
# maybe generate and upload documentation
if [[ -n "$DOC_DIR" && "$CI_COMMIT_REF_NAME" == "${DOC_BRANCH:-master}" ]]; then
echo_color "$BOLDGREEN" "Publishing documentation from branch $CI_COMMIT_REF_NAME to $DOC_DIR"
if [[ -n "$DOC_DIR" && "$CI_COMMIT_REF_NAME" == "$DOC_BRANCH" ]]; then
status "Publishing documentation from branch $CI_COMMIT_REF_NAME to $DOC_DIR"
# check if we have the secret
if [[ -z "$DOC_KEY" ]]; then
echo_color "$BOLDRED" "[buildjob] DOC_KEY variable is missing"
exit 1
panic "[buildjob] DOC_KEY variable is missing"
# We need a custom wrapper around SSH to use our settings, and ssh-agent for the key
......@@ -108,8 +124,9 @@ if [[ -n "$DOC_DIR" && "$CI_COMMIT_REF_NAME" == "${DOC_BRANCH:-master}" ]]; then
echo "${DOC_KEY}" | tr -d '\r' | ssh-add -
export GIT_SSH=$(readlink -e ci/ssh)
# Generate documentation
make html
# Generate documentation and web server configuration
echo "DirectoryIndex toc.html" > html/.htaccess
# Upload documentation
rsync -a --delete -e "$GIT_SSH" html/ "$DOC_DIR/"
......@@ -4,33 +4,32 @@
export OPAMROOT="$(pwd)/opamroot"
export OPAMJOBS="$((2*$CPU_CORES))"
export OPAM_EDITOR="$(which false)"
# Delete OPAM 1.2 root, if that's what we got
if test -d "$OPAMROOT" && fgrep 'opam-version: "1.2"' "$OPAMROOT/config" > /dev/null; then
echo_color "$BOLDYELLOW" "[prepare-opam] Deleting opam 1.2 root"
if test -d "$OPAMROOT" && fgrep 'opam-version: "1.2"' "$OPAMROOT/config" -q; then
warn "[prepare-opam] Deleting opam 1.2 root"
rm -rf "$OPAMROOT"
# Delete root if compiler does not match
if test -d "$OPAMROOT" && ! opam list -s -i "$OCAML" | egrep . -q; then
warn "[prepare-opam] Deleting opam root with outdated compiler"
rm -rf "$OPAMROOT"
# Make sure we got a good OPAM.
if test -d "$OPAMROOT"; then
echo_color "$BOLDGREEN" "[prepare-opam] Re-using cached opam root"
status "[prepare-opam] Refreshing cached opam root"
echo_color "$BOLDYELLOW" "[prepare-opam] Creating new opam root"
warn "[prepare-opam] Creating new opam root (compiler: $OCAML)"
mkdir "$OPAMROOT"
opam init --no-setup --disable-sandboxing -y
opam init --no-setup --disable-sandboxing --compiler="$OCAML" -y
eval `opam conf env`
if [[ -z "$FRESH_OPAM" ]]; then # skip if this is a fresh opam root
# Make sure the pin for the builddep package exists and is up-to-date.
# This avoids opam complaining about pins pointing to a non-existing file.
make build-dep/opam
# Update repositories
opam update
# Make sure we got the right set of repositories registered
if echo "$@" | egrep "(dev|beta)" > /dev/null; then
# We are compiling against a dev version of something. Get ourselves the dev repositories.
......@@ -45,40 +44,57 @@ test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.
test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git --rank 20
# We really want to run all of the following in one opam transaction, but due to opam limitations,
# that is not currently possible. Once we use opam 2 for CI, we can first do all the pinning (with `-n`)
# followed by `opam upgrade --all build-dep/` (and hope this will also --fixup).
# Make sure the the builddep package exists and is up-to-date.
make build-dep/opam
# Update old opam, if we got a cache.
if [[ -z "$FRESH_OPAM" ]]; then # skip if this is a fresh opam root
# Update repositories and reinit. build-dep/opam must exist here because it
# might be installed, and opam would complain if it had went missing.
opam init --no-setup --disable-sandboxing --reinit -y
# We need `opam update` anyway to update git branches.
opam update --development
# Install fixed versions of some dependencies.
echo_color "$BOLDGREEN" "[prepare-opam] Processing pins"
# Print some version numbers
status "[prepare-opam] Version report"
opam config report
# Unpin all the things, to kill stale pins
status "[prepare-opam] Removing old pins"
for PACKAGE in $(opam pin | cut -d '.' -f 1); do
opam pin remove -y -n "$PACKAGE"
# Pin fixed versions of some dependencies.
status "[prepare-opam] Processing pins"
while (( "$#" )); do # while there are arguments left
PACKAGE="$1" ; shift
KIND="$1" ; shift
VERSION="$1" ; shift
# Check if the pin is already set
read -a PIN <<< $(opam pin list | (egrep "^$PACKAGE[. ]"))
if [[ "${PIN[1]}" == "$KIND" && "${PIN[2]}" == "$VERSION" ]]; then
echo_color "$BOLDGREEN" "[prepare-opam] $PACKAGE already $KIND-pinned to $VERSION"
echo_color "$BOLDYELLOW" "[prepare-opam] $KIND-pinning $PACKAGE to $VERSION"
opam pin add -y -k "$KIND" "$PACKAGE" "$VERSION"
status "[prepare-opam] $KIND-pinning $PACKAGE to $VERSION"
opam pin add -y -n -k "$KIND" "$PACKAGE" "$VERSION"
if [[ -z "$FRESH_OPAM" ]]; then # skip if this is a fresh opam root
# Upgrade cached things
echo_color "$BOLDGREEN" "[prepare-opam] Upgrading packages"
opam upgrade -y --fixup && opam upgrade -y
# Install build-dependencies.
echo_color "$BOLDGREEN" "[prepare-opam] Installing build-dependencies"
make build-dep OPAMFLAGS="-y"
# Pin build-dep and install everything.
warn "[prepare-opam] Pinning and installing build-dep and upgrading everything"
opam pin add -y -n build-dep/ # we have to do this first, or `opam upgrade` cannot pick it up
# We would really like to do these two in one transaction, but that does not work -- see opam issue #3737.
# Also, we have to list the packages we pinned explicitly here, or else opam fails to upgrade them if they
# are pinned to a git branch (it ignores changes in the git branch) -- see opam issue #3727.
opam upgrade -y build-dep/ $PINNED_PACKAGES
opam upgrade -y
# done
status "[prepare-opam] Done! Some version information:"
opam show "$PACKAGE" -f name,version,source-hash
coqc -v
# center.mpi-sws.org
center.mpi-sws.org ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIHG8dNazSgw2XgGFi9/vEs8+VKYX66SlWVy6wx+3rZU5
center.mpi-sws.org ssh-rsa AAAAB3NzaC1yc2EAAAADAQABAAACAQDC4vIw4pgkQc2mKEpl99wERvpBsvAqU6UwKVL02n+fNuRn2FAzH+sD4NbmVoSjoCuQ+NlGI+HSbdJDzfQUtAoWcPv+65LeJF9IK67YerAl1Kc9m0srs0QbEPKFMB2Ef48FS7QN+aJtljz28qObytsxYxwsCVX+3vcZnEiYRZVixqWCA1MBkDePnOIbUysbqoBEKG1urf0h8K72Qtpo1IO20jLUnWUSuGy+WdfVW8pDnUTFn1z+Diex0uvMvlPrgJ74S81tklTMIRaMmqBhMs6hDtAg2EmR6GMV0N8RlPnhDeKxJOHwSM786yWqiLB4BQ82l6UCyr5tizOH0LryImII1Wwx5RQivUlFGf+NwVIcUsOg4eGcXxqOEr55vg5B8P4z2iL3M5SUbg1htA8N4QmxRaamCVkNvXP6hwTdI8CIx2LUZP1OKbohT4FmiMOfNh6TiHsJw4Ke/cgo3oNDvxnadEOGhOezw4LolzB0N9UCMRxYw3nn16KqasB2gJWme0vpkKEmiCi5RoJ93rSfkfjyqjKYgsNaP3qMZm/i6NM/M008HPmG0a7nx6SYTlYK4D7YMzBmaaMgtzDQF0edvL3FCmTFmt6pc6DHhP/UqPSQJHIGzSomOTiRTR5PoXciket3W1z4ZpGUcsCl12cA3MSvcAKor7QGveR+ENUEuvzhew==
center.mpi-sws.org ssh-rsa AAAAB3NzaC1yc2EAAAADAQABAAACAQDOlygxT+Bs5JVCSYlYjn6cAF210agd03ZtgcWPjuOB88Apo2YwZznZF87FSumFfZ5R9rrDb/sVAHQl/qWebnUgCVgPfTzbefh32CNMHcicqLmjVJCxGEeE4yftSsApVwQ0/Q9+av6ogc6gfet2RaVz1Nt3UgA0qERUclz+rffnGquMRdMbKViQJHvHgTGju9w+GUOwOj6PL+iIag+7Y7t1LdFazoa5FDOpuqiCKQPYfoSJ0ms2RYYthvZC82kKDUaqjUDPa8bWdGFD2mjEwep1r7/5mNLh05h8bp4uG7ZT7xobnHw39k1r/ngnKx8ZSHnXDMp4/wgqMIkYevOApSMaaruo9lsB61elcrhXaE7havJo+HQ6c+rU2HwGnnJeT+AAR1eaFqbViLegOBe4/gQDBiTQdHxByfVoQkQQl+kSaWYrtWt93j+W39+RUiXNkiJCf3KrdaovIUx7BwLmSb917NGJdObl+Ax+cHScn5EDVwHDK3iYHqn5vHKn6tc7cpPzs9gixpUAFLDPbUa2Ujt4LVe2qMsoHm5uxg4J8VJU4aYOsWJykUpkLHPOAzK7oYwyJRWseIW8iOnSJOjedsSSbc7x75nC2HHJLqoXGQXcMmseTTAIS9ytGLqxdnUU3PHhu0JJTLR7Jkyj3FjZHkG9ge68UStAzM2u7zLQaWmnTQ==
center.mpi-sws.org ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIGdp/+YAuARyfIq3JZ0GaF3jLSnXbUNaJyzKQdOZN4AJ