Commit de05b2c9 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'ci-docker' into 'master'

Fetch the build image from the registry instead of building it on the fly.

See merge request !187
parents 8d868967 16f729a4
stages:
- docker
- build
- test
- nightly
- deploy
variables:
BUILD_IMAGE: "$CI_REGISTRY_IMAGE:ci-master-2019-10-04"
GIT_CLEAN_FLAGS: "-ffdxq"
build-image:
stage: docker
script:
- docker login -u "$CI_REGISTRY_USER" -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
- if docker pull "$BUILD_IMAGE"; then echo "Image already exists!"; exit 1; fi
- docker build --force-rm -t "$BUILD_IMAGE" - < misc/Dockerfile.build
- docker push "$BUILD_IMAGE"
- docker rmi "$BUILD_IMAGE"
only:
variables:
- $NEW_BUILD_IMAGE
tags:
- shell
.docker_template: &docker_definition
image: "$BUILD_IMAGE"
tags:
- docker
.build_template: &build_definition
stage: build
script:
- misc/ci-docker.sh misc/ci-local.sh
- misc/ci-local.sh
<<: *docker_definition
build-system:
variables:
COMPILER: system
<<: *build_definition
build-4.02.3:
variables:
COMPILER: 4.02.3
<<: *build_definition
build-4.03.0:
variables:
COMPILER: 4.03.0
<<: *build_definition
build-4.04.2:
variables:
COMPILER: 4.04.2
COMPILER: ocaml-system
<<: *build_definition
build-4.05.0:
......@@ -44,10 +54,21 @@ build-4.07.1:
COMPILER: 4.07.1
<<: *build_definition
build-4.08.1:
variables:
COMPILER: 4.08.1
<<: *build_definition
build-4.09.0:
variables:
COMPILER: 4.09.0
<<: *build_definition
.bench_template1: &bench_definition_always
stage: test
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide
- misc/ci-local.sh bench ide
<<: *docker_definition
.bench_template2: &bench_definition
<<: *bench_definition_always
......@@ -58,21 +79,6 @@ build-4.07.1:
bench-system:
<<: *bench_definition_always
bench-4.02.3:
variables:
COMPILER: 4.02.3
<<: *bench_definition
bench-4.03.0:
variables:
COMPILER: 4.03.0
<<: *bench_definition
bench-4.04.2:
variables:
COMPILER: 4.04.2
<<: *bench_definition
bench-4.05.0:
variables:
COMPILER: 4.05.0
......@@ -88,45 +94,59 @@ bench-4.07.1:
COMPILER: 4.07.1
<<: *bench_definition_always
full-4.07.1:
bench-4.08.1:
variables:
COMPILER: 4.08.1
<<: *bench_definition
bench-4.09.0:
variables:
COMPILER: 4.09.1
<<: *bench_definition
full:
stage: test
variables:
COMPILER: 4.07.1
DEBIAN_PACKAGES: hevea rubber texlive-latex-extra lmodern texlive-fonts-recommended
OPAM_PACKAGES: coq-flocq.3.1.0 js_of_ocaml-ppx alt-ergo.2.0.0
COMPILER: full
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide doc web_ide
- misc/ci-local.sh bench ide doc web_ide
<<: *docker_definition
nightly-bench:
stage: nightly
variables:
COMPILER: 4.05.0
DEBIAN_PACKAGES: cvc3 spass
OPAM_PACKAGES: alt-ergo.2.0.0 zenon.0.8.0 coq.8.7.2 coq-flocq.3.1.0
COMPILER: bench
script:
- misc/ci-docker.sh misc/ci-local.sh nightly-bench-reduced
- misc/ci-local.sh nightly-bench-reduced
<<: *docker_definition
ce-bench:
stage: nightly
variables:
COMPILER: 4.05.0
DEBIAN_PACKAGES: cvc3 spass
OPAM_PACKAGES: alt-ergo.2.0.0 zenon.0.8.0 coq.8.7.2 coq-flocq.3.1.0
COMPILER: bench
script:
- misc/ci-docker.sh misc/ci-local.sh ce-bench
- misc/ci-local.sh ce-bench
<<: *docker_definition
opam:
stage: build
variables:
COMPILER: system
script:
- misc/ci-docker.sh misc/ci-opam.sh
- opam pin -v -y add why3 .
- opam pin -v -y add why3-ide .
<<: *docker_definition
deploy:
stage: deploy
script:
- misc/ci-deploy.sh
- IMAGE=$CI_REGISTRY_IMAGE:$(echo $CI_COMMIT_REF_NAME | tr -cs "[:alnum:].\n" "-")
- docker login -u "$CI_REGISTRY_USER" -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
- docker pull "$IMAGE" || true
- docker build --force-rm --cache-from "$IMAGE" -t "$IMAGE" -f misc/Dockerfile.deploy .
- docker push "$IMAGE"
- docker rmi "$IMAGE"
only:
- master
- /^bugfix[/]v[0-9.]*$/
- tags
tags:
- shell
......@@ -6,13 +6,13 @@ finite_tarski
insertion_sort
# kmp # randomly fail with z3 4.8.4
leftist_heap
mergesort_array
# pairing_heap # currently uses Altergo 2.3.0
# mergesort_array # fail with Alt-Ergo 2.3.0
pairing_heap
rightmostbittrick
sieve
# sieve # fail with Alt-Ergo 2.3.0
# sudoku # some goals are too long for the continuous integration
toy_compiler
# tree_of_list # uses Alt-Ergo 2.2.0 and CVC4 1.6
vstte10_max_sum
warshall_algorithm
# warshall_algorithm # fail with Alt-Ergo 2.3.0
zeros
# If you modify this file, make sure to update the BUILD_IMAGE variable in .gitlab-ci.yml.
FROM debian:buster
USER root
# install dependencies
ARG DEBIAN_FRONTEND=noninteractive
RUN apt-get update -yq && \
apt-get upgrade -yq --with-new-pkgs --auto-remove && \
apt-get install -yq --no-install-recommends wget libgmp-dev gtk+-2.0 libgtksourceview2.0-dev xvfb unzip build-essential autoconf automake ocaml-nox ca-certificates git xauth hevea texlive-latex-extra lmodern texlive-plain-generic texlive-fonts-recommended && \
apt-get clean
RUN wget --quiet https://github.com/ocaml/opam/releases/download/2.0.0/opam-2.0.0-x86_64-linux -O /usr/local/bin/opam && \
chmod a+x /usr/local/bin/opam
# install provers
## CVC4 1.7
RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.7-x86_64-linux-opt -O /usr/local/bin/cvc4-1.7 && \
chmod a+x /usr/local/bin/cvc4-1.7
## CVC4 1.6
RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.6-x86_64-linux-opt -O /usr/local/bin/cvc4-1.6 && \
chmod a+x /usr/local/bin/cvc4-1.6
## CVC4 1.5
RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.5-x86_64-linux-opt -O /usr/local/bin/cvc4-1.5 && \
chmod a+x /usr/local/bin/cvc4-1.5
## CVC4 1.4
RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.4-x86_64-linux-opt -O /usr/local/bin/cvc4-1.4 && \
chmod a+x /usr/local/bin/cvc4-1.4
## Z3 4.6.0
RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.6.0/z3-4.6.0-x64-debian-8.10.zip && \
unzip z3-4.6.0-x64-debian-8.10.zip && \
mv z3-4.6.0-x64-debian-8.10/bin/z3 /usr/local/bin/z3-4.6.0 && \
rm -r z3-4.6.0-x64-debian-8.10.zip z3-4.6.0-x64-debian-8.10
## Z3 4.8.4
RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.8.4/z3-4.8.4.d6df51951f4c-x64-debian-8.11.zip && \
unzip z3-4.8.4.d6df51951f4c-x64-debian-8.11.zip && \
mv z3-4.8.4.d6df51951f4c-x64-debian-8.11/bin/z3 /usr/local/bin/z3-4.8.4 && \
rm -r z3-4.8.4.d6df51951f4c-x64-debian-8.11.zip z3-4.8.4.d6df51951f4c-x64-debian-8.11
# create user
RUN adduser --disabled-password --gecos '' why3
USER why3
ENV HOME /home/why3
WORKDIR /home/why3
# install opam
ENV OPAM_PACKAGES="menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo.2.3.0"
RUN opam init -y --no-setup -j1 --compiler=ocaml-system --disable-sandboxing && \
opam install -y $OPAM_PACKAGES && \
opam switch create 4.05.0 ocaml-base-compiler.4.05.0 && opam install -y $OPAM_PACKAGES && \
opam switch create 4.06.1 ocaml-base-compiler.4.06.1 && opam install -y $OPAM_PACKAGES && \
opam switch create 4.07.1 ocaml-base-compiler.4.07.1 && opam install -y $OPAM_PACKAGES && \
opam switch create 4.08.1 ocaml-base-compiler.4.08.1 && opam install -y $OPAM_PACKAGES && \
opam switch create 4.09.0 ocaml-base-compiler.4.09.0 && opam install -y $OPAM_PACKAGES && \
opam switch create bench ocaml-base-compiler.4.05.0 && opam install -y $OPAM_PACKAGES && \
opam switch create full ocaml-base-compiler.4.07.1 && opam install -y $OPAM_PACKAGES && \
opam repository add coq-released https://coq.inria.fr/opam/released --all-switches && \
opam install -y --switch=bench zenon.0.8.0 coq.8.7.2 coq-flocq.3.1.0 && \
opam install -y --switch=full coq-flocq.3.1.0 js_of_ocaml-ppx && \
opam clean -a
RUN opam switch ocaml-system
FROM bench-image-system-stable
FROM debian:stable
USER root
RUN adduser --disabled-password --gecos '' guest
# install dependencies
ARG DEBIAN_FRONTEND=noninteractive
RUN apt-get update -yq && \
apt-get upgrade -yq --with-new-pkgs --auto-remove && \
apt-get install -yq --no-install-recommends wget libgmp-dev gtk+-2.0 libgtksourceview2.0-dev gnome-themes-standard libcanberra-gtk-module build-essential autoconf automake ocaml-nox ca-certificates xauth unzip && \
apt-get clean
RUN wget --quiet https://github.com/ocaml/opam/releases/download/2.0.0/opam-2.0.0-x86_64-linux -O /usr/local/bin/opam && \
chmod a+x /usr/local/bin/opam
USER why3
# create user
RUN adduser --disabled-password --gecos '' guest
USER guest
ENV HOME /home/guest
COPY --chown=why3:why3 . why3
WORKDIR /home/why3/why3
RUN opam init -y --auto-setup -j1 --compiler=ocaml-system --disable-sandboxing && \
opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo && \
opam clean -a
RUN eval `opam config env` && \
COPY --chown=guest:guest . /home/guest/why3
WORKDIR /home/guest/why3
RUN eval `opam env` && \
./autogen.sh && \
./configure && \
make
......@@ -18,7 +33,6 @@ USER root
RUN make install
USER guest
ENV HOME /home/guest
WORKDIR /home/guest
RUN why3 config --detect
ARG debian_version=stable
FROM debian:$debian_version
USER root
# install dependencies
RUN apt-get update -yq && apt-get upgrade -yq --with-new-pkgs --auto-remove
RUN apt-get update -yq && apt-get upgrade -yq --with-new-pkgs --auto-remove && apt-get install -yq --no-install-recommends wget libgmp-dev gtk+-2.0 libgtksourceview2.0-dev gnome-themes-standard libcanberra-gtk-module xvfb unzip build-essential autoconf automake ocaml-nox ca-certificates git xauth
ARG debian_packages
RUN apt-get update -yq && apt-get upgrade -yq --with-new-pkgs --auto-remove && apt-get install -yq --no-install-recommends $debian_packages
RUN apt-get clean
RUN wget https://github.com/ocaml/opam/releases/download/2.0.0/opam-2.0.0-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
# install provers
## CVC4 1.7
RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.7-x86_64-linux-opt
RUN chmod a+x cvc4-1.7-x86_64-linux-opt
RUN cp cvc4-1.7-x86_64-linux-opt /usr/local/bin/cvc4-1.7
## CVC4 1.6
RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.6-x86_64-linux-opt
RUN chmod a+x cvc4-1.6-x86_64-linux-opt
RUN cp cvc4-1.6-x86_64-linux-opt /usr/local/bin/cvc4-1.6
## CVC4 1.5
RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.5-x86_64-linux-opt
RUN chmod a+x cvc4-1.5-x86_64-linux-opt
RUN cp cvc4-1.5-x86_64-linux-opt /usr/local/bin/cvc4-1.5
## CVC4 1.4
RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.4-x86_64-linux-opt
RUN chmod a+x cvc4-1.4-x86_64-linux-opt
RUN cp cvc4-1.4-x86_64-linux-opt /usr/local/bin/cvc4-1.4
## Z3 4.6.0
RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.6.0/z3-4.6.0-x64-debian-8.10.zip
RUN unzip z3-4.6.0-x64-debian-8.10.zip
RUN cp z3-4.6.0-x64-debian-8.10/bin/z3 /usr/local/bin/z3-4.6.0
## Z3 4.8.4
RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.8.4/z3-4.8.4.d6df51951f4c-x64-debian-8.11.zip
RUN unzip z3-4.8.4.d6df51951f4c-x64-debian-8.11.zip
RUN cp z3-4.8.4.d6df51951f4c-x64-debian-8.11/bin/z3 /usr/local/bin/z3-4.8.4
# create user
RUN adduser --disabled-password --gecos '' why3
USER why3
ENV HOME /home/why3
WORKDIR /home/why3
ARG compiler=ocaml-system
RUN opam init -a -y -j1 --compiler=$compiler --disable-sandboxing
RUN opam repository add coq-released https://coq.inria.fr/opam/released --all-switches
ARG opam_packages
RUN opam install -y depext
RUN opam depext --dry-run menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo
RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo
RUN test -z "$opam_packages" || opam depext --dry-run $opam_packages
RUN test -z "$opam_packages" || opam install -y $opam_packages
[uninstalled_prover altergo_2_3_0]
[uninstalled_prover altergo_2_2_0]
name = "Alt-Ergo"
version = "2.3.0"
version = "2.2.0"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.0.0"
target_version = "2.3.0"
[uninstalled_prover altergo_2_2_0]
[uninstalled_prover altergo_2_1_0]
name = "Alt-Ergo"
version = "2.2.0"
version = "2.1.0"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.0.0"
target_version = "2.3.0"
[uninstalled_prover altergo_2_1_0]
name = "Alt-Ergo"
version = "2.1.0"
version = "2.0.0"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.0.0"
target_version = "2.3.0"
[uninstalled_prover coq_8_7_1]
name = "Coq"
......@@ -38,10 +38,13 @@ target_version = "8.7.2"
name = "CVC3"
version = "2.2"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "CVC3"
target_version = "2.4.1"
policy = "remove"
[uninstalled_prover cvc3_2_4_1]
name = "CVC3"
version = "2.4.1"
alternative = ""
policy = "remove"
[uninstalled_prover cvc4_1_2]
name = "CVC4"
......
#!/bin/sh
set -e
autoconf && (automake --add-missing 2> /dev/null || true)
docker build -t bench-image-system-stable -f misc/Dockerfile.init .
IMAGE=$CI_REGISTRY_IMAGE:$(echo $CI_COMMIT_REF_NAME | tr -cs "[:alnum:].\n" "-")
docker build -t $IMAGE -f misc/Dockerfile.deploy .
docker login -u $CI_REGISTRY_USER -p $CI_REGISTRY_PASSWORD $CI_REGISTRY
docker push $IMAGE
docker rmi $IMAGE
#!/bin/bash
set -e
if test -z "$DEBIAN_VERSION"; then
DEBIAN_VERSION="stable"
fi
if test -z "$COMPILER"; then
COMPILER="system"
fi
if test "$COMPILER" = "system"; then
OCAML="ocaml-system"
else
OCAML="ocaml-base-compiler.$COMPILER"
fi
autoconf && (automake --add-missing 2> /dev/null || true)
IMAGE=bench-image-$COMPILER-$DEBIAN_VERSION
if test -n "$DEBIAN_PACKAGES"; then
IMAGE=$IMAGE--$(echo $DEBIAN_PACKAGES | sed -e 's/ /--/g')
fi
if test -n "$OPAM_PACKAGES"; then
IMAGE=$IMAGE--$(echo $OPAM_PACKAGES | sed -e 's/ /--/g')
fi
docker build -t $IMAGE --force-rm -f misc/Dockerfile.init --build-arg debian_version="$DEBIAN_VERSION" --build-arg compiler=$OCAML --build-arg debian_packages="$DEBIAN_PACKAGES" --build-arg opam_packages="$OPAM_PACKAGES" .
CID=$(docker create --rm -i -w /home/why3/why3 $IMAGE /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 <<EOF
exec $@
EOF
#!/bin/bash
set -e
eval `opam config env`
opam switch $COMPILER
eval `opam env`
export OCAMLRUNPARAM=o=20,O=200
./autogen.sh
./configure --enable-local
make
......
#!/bin/sh
set -e
opam pin -v -y add why3 .
opam pin -v -y add why3-ide .
......@@ -2,6 +2,13 @@ Continuous integration slaves are hosted on https://ci.inria.fr/ in the
`why3` project. They are of type `medium` (1 core at 2GHz and 2GB RAM)
with 40GB of storage.
Continuous integration is run inside Docker containers. The corresponding
Docker image is loaded from the Gitlab registry. It is built from the
`misc/Dockerfile.build` description. Changes to this file do not automatically
lead to a new Docker image. One should first modify the image name in the
`BUILD_IMAGE` variable of `.gitlab-ci.yml` and then manually trigger a pipeline
while setting the `NEW_BUILD_IMAGE` variable.
:warning: Do not write any sensible information in this file, e.g., the CI token!
# To create a new slave
......@@ -11,9 +18,9 @@ with 40GB of storage.
3. run:
```
hostname > /etc/hostname
gitlab-runner register
gitlab-runner register --url https://gitlab.inria.fr/ --executor docker --tag-list docker --docker-image alpine:latest
```
4. use the information from "CI/CD settings", `shell` for the type, and no tags
4. use the information from "CI/CD settings" to fill the token, keep the other fields to their default value
5. enjoy
# To create the initial slave template (once in a while)
......@@ -24,7 +31,7 @@ with 40GB of storage.
```
apt-get update
apt-get dist-upgrade
apt-get install curl autoconf automake
apt-get install curl
curl -L https://packages.gitlab.com/install/repositories/runner/gitlab-runner/script.deb.sh | bash
curl -fsSL https://download.docker.com/linux/debian/gpg | apt-key add -
apt-key fingerprint 0EBFCD88
......@@ -74,5 +81,6 @@ with 40GB of storage.
blkid
```
10. replace the `UUID` of `/dev/sda2` inside `/etc/fstab`
11. reboot
12. finish as if creating the initial template (see above)
11. replace the `UUID` inside `/etc/initramfs-tools/conf.d/resume`
12. reboot
13. finish as if creating the initial template (see above)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment