From dd3d53131ffc200ade327aac993a6822a71261b5 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 29 Mar 2018 15:15:30 +0200 Subject: [PATCH] Move to Docker-based CI. --- .dockerignore | 1 + .gitlab-ci.yml | 86 ++++++++++++++++++++++++++++++++++++++++-- misc/Dockerfile.deploy | 24 ++++++++++++ misc/Dockerfile.init | 18 +++++++++ misc/ci-bench.sh | 29 -------------- misc/ci-docker.sh | 13 +++++++ misc/ci-local.sh | 26 +++++++++++++ 7 files changed, 164 insertions(+), 33 deletions(-) create mode 100644 .dockerignore create mode 100644 misc/Dockerfile.deploy create mode 100644 misc/Dockerfile.init delete mode 100755 misc/ci-bench.sh create mode 100755 misc/ci-docker.sh create mode 100755 misc/ci-local.sh diff --git a/.dockerignore b/.dockerignore new file mode 100644 index 000000000..6b8710a71 --- /dev/null +++ b/.dockerignore @@ -0,0 +1 @@ +.git diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a087af51c..7b38bbb69 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,6 +1,84 @@ -before_script: - - . $HOME/.opam/opam-init/variables.sh +stages: + - build + - test + - deploy -ci-bench: +.build_template: &build_definition + stage: build script: - - misc/ci-bench.sh + - misc/ci-docker.sh misc/ci-local.sh + +build: + variables: + COMPILER: system + <<: *build_definition + +build-4.03.0: + variables: + COMPILER: 4.03.0 + <<: *build_definition + +build-4.04.0: + variables: + COMPILER: 4.04.0 + <<: *build_definition + +build-4.05.0: + variables: + COMPILER: 4.05.0 + <<: *build_definition + +build-4.06.0: + variables: + COMPILER: 4.06.0 + <<: *build_definition + +bench: + stage: test + variables: + COMPILER: system + script: + - misc/ci-docker.sh misc/ci-local.sh bench + +.bench_template: &bench_definition + stage: test + script: + - misc/ci-docker.sh misc/ci-local.sh bench + only: + - tags + - schedules + +bench-4.03.0: + variables: + COMPILER: 4.03.0 + <<: *bench_definition + +bench-4.04.0: + variables: + COMPILER: 4.04.0 + <<: *bench_definition + +bench-4.05.0: + variables: + COMPILER: 4.05.0 + <<: *bench_definition + +bench-4.06.0: + variables: + COMPILER: 4.06.0 + <<: *bench_definition + +deploy: + stage: deploy + script: + - autoconf && (automake --add-missing 2> /dev/null || true) + - docker build -t bench-image -f misc/Dockerfile.init . + - docker build -t deploy-image -f misc/Dockerfile.deploy . + - docker login -u gitlab-ci-token -p $CI_JOB_TOKEN $CI_REGISTRY + - docker tag deploy-image $CI_REGISTRY_IMAGE:$CI_COMMIT_REF_SLUG + - docker push $CI_REGISTRY_IMAGE:$CI_COMMIT_REF_SLUG + - docker image prune -f + only: + - master + - /^bugfix[/]v[0-9.]*$/ + - tags diff --git a/misc/Dockerfile.deploy b/misc/Dockerfile.deploy new file mode 100644 index 000000000..9ed076441 --- /dev/null +++ b/misc/Dockerfile.deploy @@ -0,0 +1,24 @@ +FROM bench-image + +USER root + +RUN adduser --disabled-password --gecos '' guest + +USER why3 + +COPY --chown=why3:why3 . why3 +WORKDIR /home/why3/why3 + +RUN eval `opam config env` && \ + ./configure && \ + make -j2 + +USER root + +RUN make install + +USER guest +ENV HOME /home/guest +WORKDIR /home/guest + +RUN why3 config --detect diff --git a/misc/Dockerfile.init b/misc/Dockerfile.init new file mode 100644 index 000000000..5e56db563 --- /dev/null +++ b/misc/Dockerfile.init @@ -0,0 +1,18 @@ +FROM ocaml/ocaml:debian-stable + +# install dependencies +RUN apt-get update && \ + apt-get install -y wget libgmp-dev gtk+-2.0 libgtksourceview2.0-dev gnome-themes-standard libcanberra-gtk-module opam + +# create user +RUN sudo adduser --disabled-password --gecos '' why3 +USER why3 +ENV HOME /home/why3 +WORKDIR /home/why3 + +ARG compiler=system +RUN opam init -a -y -j2 --compiler=$compiler +RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip + +# Alt-Ergo +RUN opam install alt-ergo.1.30 diff --git a/misc/ci-bench.sh b/misc/ci-bench.sh deleted file mode 100755 index 030cd20d5..000000000 --- a/misc/ci-bench.sh +++ /dev/null @@ -1,29 +0,0 @@ -#!/bin/bash - -# runner: -# apt-get install curl opam automake libgmp-dev zlib1g-dev -# curl -L https://packages.gitlab.com/install/repositories/runner/gitlab-runner/script.deb.sh | bash -# apt-get install gitlab-runner -# gitlab-runner register -# https://gitlab.inria.fr/ -# shell -# su gitlab-runner -# cd -# opam init -# opam install menhir alt-ergo - -set -e - -# configuration -autoconf -automake --add-missing 2> /dev/null || true -./configure --enable-local - -# compilation -make -j2 - -# detection of provers -bin/why3config --detect-provers - -# run the bench -make bench diff --git a/misc/ci-docker.sh b/misc/ci-docker.sh new file mode 100755 index 000000000..d146d181e --- /dev/null +++ b/misc/ci-docker.sh @@ -0,0 +1,13 @@ +#!/bin/bash + +set -e -x + +autoconf && (automake --add-missing 2> /dev/null || true) +docker build -t bench-image-$COMPILER -f misc/Dockerfile.init --build-arg compiler=$COMPILER . +CID=$(docker create --rm -i -w /home/why3/why3 bench-image-$COMPILER /bin/sh) +docker start $CID +docker cp . $CID:/home/why3/why3 +docker exec -u root $CID chown -R why3:why3 /home/why3/why3 +docker attach $CID <> /etc/apt/sources.list +# apt-get update +# apt-get install gitlab-runner docker-ce +# gitlab-runner register +# https://gitlab.inria.fr/ +# shell +# usermod -aG docker gitlab-runner + +set -e +eval `opam config env` + +./configure --enable-local +make -j2 + +if test "$1" = bench; then +bin/why3config --detect-provers +make bench +fi -- GitLab