...
 
Commits (60)
## 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
stages:
- build
variables:
CPU_CORES: "10"
.template: &template
stage: build
tags:
- fp
script:
- git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
- ci/buildjob
cache:
key: "$CI_JOB_NAME"
paths:
- opamroot/
only:
- master
- /^ci/
except:
- 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:
```
build-coq.8.10.1:
<<: *template
variables:
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:
```
build-iris.dev:
<<: *template
variables:
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"
except:
only:
- 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:
```
build-coq.8.10.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.10.0"
TIMING_CONF: "coq-8.10.0"
tags:
- 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
`~/.ssh/authorized_keys`:
```
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
directory.
[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
}
#!/bin/bash
set -e
set -o pipefail
set -eo pipefail
#set -x
. ci/ansi-colors.sh
......@@ -9,7 +8,7 @@ set -o pipefail
## 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
## "PACKAGE KIND TARGET PACKAGE KIND TARGET ..."
## - $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.
## - $OPAM_PKG, $OPAM_UPDATE_SECRET, $OPAM_PKG_BRANCH: IF $OPAM_PKG is
......@@ -17,20 +16,28 @@ set -o pipefail
## 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.
## - $TIMING_PROJECT, $TIMING_CONF, $TIMING_SECRET: If $TIMING_PROJECT is
## - $TIMING_PROJECT, $TIMING_CONF, $TIMING_SECRET: If $TIMING_CONF is
## 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))"
OCAML=${OCAML:-ocaml-system}
OCAML=${OCAML:-ocaml-base-compiler.4.07.1}
OPAM_PKG_BRANCH=${OPAM_PKG_BRANCH:-master}
DOC_BRANCH=${DOC_BRANCH:-master}
TIMING_PROJECT=${TIMING_PROJECT:-$CI_PROJECT_NAME}
# Environment sanity checks
if [[ -n "$VALIDATE" ]]; then
panic "[buildjob] Do not use the VALIDATE variable, it has been replaced by CI_COQCHK"
fi
# Parepare
. ci/prepare-opam.sh $OPAM_PINS # deliberately not quoted
......@@ -39,27 +46,30 @@ env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
if [[ -n "$MANGLE_NAMES" ]]; then
export COQEXTRAFLAGS="$COQEXTRAFLAGS -mangle-names mangled_"
fi
if [[ -n "$TIMING_PROJECT" ]]; then
if [[ -n "$TIMING_CONF" ]]; then
export TIMECMD=ci/perf
fi
# 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"
fi
# 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"
fi
# 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" \
......@@ -72,11 +82,9 @@ fi
# maybe create opam package
if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == "$OPAM_PKG_BRANCH" ]]; then
echo_color "$BOLDGREEN" "[buildjob] Releasing package on opam"
# 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"
fi
# determine package name prefix
if [[ "$CI_COMMIT_REF_NAME" == master ]]; then
......@@ -85,6 +93,7 @@ if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == "$OPAM_PKG_BRANCH" ]]; then
OPAM_PKG_PREFIX="branch.$CI_COMMIT_REF_NAME"
fi
# 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 "token=$OPAM_UPDATE_SECRET" \
-F "ref=master" \
......@@ -97,18 +106,17 @@ if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == "$OPAM_PKG_BRANCH" ]]; then
fi
# 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
fi
# maybe generate and upload documentation
if [[ -n "$DOC_DIR" && "$CI_COMMIT_REF_NAME" == "$DOC_BRANCH" ]]; then
echo_color "$BOLDGREEN" "Publishing documentation from branch $CI_COMMIT_REF_NAME to $DOC_DIR"
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"
fi
# We need a custom wrapper around SSH to use our settings, and ssh-agent for the key
......@@ -116,8 +124,9 @@ if [[ -n "$DOC_DIR" && "$CI_COMMIT_REF_NAME" == "$DOC_BRANCH" ]]; 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
COQDOCEXTRAFLAGS="$DOC_OPTS" make html
echo "DirectoryIndex toc.html" > html/.htaccess
# Upload documentation
rsync -a --delete -e "$GIT_SSH" html/ "$DOC_DIR/"
fi
......@@ -4,24 +4,26 @@
export OPAMROOT="$(pwd)/opamroot"
export OPAMJOBS="$((2*$CPU_CORES))"
export OPAM_EDITOR="$(which false)"
export OPAMDROPWORKINGDIR=1
export OPAMRETRES=3
# Delete OPAM 1.2 root, if that's what we got
if test -d "$OPAMROOT" && fgrep 'opam-version: "1.2"' "$OPAMROOT/config" -q; then
echo_color "$BOLDYELLOW" "[prepare-opam] Deleting opam 1.2 root"
warn "[prepare-opam] Deleting opam 1.2 root"
rm -rf "$OPAMROOT"
fi
# Delete root if compiler does not match
if test -d "$OPAMROOT" && ! opam list -s -i "$OCAML" | egrep . -q; then
echo_color "$BOLDYELLOW" "[prepare-opam] Deleting opam root with outdated compiler"
warn "[prepare-opam] Deleting opam root with outdated compiler"
rm -rf "$OPAMROOT"
fi
# Make sure we got a good OPAM.
if test -d "$OPAMROOT"; then
echo_color "$BOLDGREEN" "[prepare-opam] Refreshing cached opam root"
status "[prepare-opam] Refreshing cached opam root"
else
echo_color "$BOLDYELLOW" "[prepare-opam] Creating new opam root (compiler: $OCAML)"
warn "[prepare-opam] Creating new opam root (compiler: $OCAML)"
mkdir "$OPAMROOT"
opam init --no-setup --disable-sandboxing --compiler="$OCAML" -y
FRESH_OPAM=yes
......@@ -47,50 +49,52 @@ 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. build-dep/opam must exist here because it might be installed,
# and opam would complain if it had went missing.
opam update
# 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
fi
# Print some version numbers
echo_color "$BOLDGREEN" "[prepare-opam] Version report"
status "[prepare-opam] Version report"
opam config report
git --version
echo -n "OCaml version " && ocaml -vnum
echo -n "OCamlc version (/usr/bin) " && /usr/bin/ocamlc -vnum
# 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).
# 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"
done
# Pin fixed versions of some dependencies.
echo_color "$BOLDGREEN" "[prepare-opam] Processing pins"
status "[prepare-opam] Processing pins"
PINNED_PACKAGES=""
while (( "$#" )); do # while there are arguments left
PACKAGE="$1" ; shift
KIND="$1" ; shift
VERSION="$1" ; shift
read -a PIN <<< $(opam pin list | (egrep "^$PACKAGE[. ]"))
echo_color "$BOLDGREEN" "[prepare-opam] $KIND-pinning $PACKAGE to $VERSION"
# We try twice, because opam...
opam pin add -y -n -k "$KIND" "$PACKAGE" "$VERSION" || opam pin add -y -n -k "$KIND" "$PACKAGE" "$VERSION" -vv --debug
status "[prepare-opam] $KIND-pinning $PACKAGE to $VERSION"
opam pin add -y -n -k "$KIND" "$PACKAGE" "$VERSION"
PINNED_PACKAGES="$PINNED_PACKAGES $PACKAGE"
done
echo
# Pin build-dep and install everything
echo_color "$BOLDYELLOW" "[prepare-opam] Pinning and installing build-dep and upgrading everything"
# 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
if ! opam upgrade -y --all build-dep/; then
# Something went wrong. Try again with more debugging, but then fail anyway.
echo_color "$BOLDRED" "[prepare-opam] Installation failed! Let's try again, sometimes this helps... but more verbose this time"
set -x
opam config list -vv
opam upgrade -y --all build-dep/ -vv --debug
set +x
fi
# 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
echo
# done
echo_color "$BOLDGREEN" "[prepare-opam] Done! Coq version we are going to use:"
status "[prepare-opam] Done! Some version information:"
for PACKAGE in $PINNED_PACKAGES; do
opam show "$PACKAGE" -f name,version,source-hash
echo
done
coqc -v
echo
# 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