Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 34c24364 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make sure containers are removed on build failures.

This commit also improves sharing between images.
parent a30d8be7
......@@ -2,8 +2,10 @@ FROM ocaml/ocaml:debian-stable
# install dependencies
ARG debian_packages
RUN apt-get update && \
apt-get install -y wget libgmp-dev gtk+-2.0 libgtksourceview2.0-dev gnome-themes-standard libcanberra-gtk-module opam xvfb $debian_packages
RUN apt-get update
RUN apt-get install -y wget libgmp-dev gtk+-2.0 libgtksourceview2.0-dev gnome-themes-standard libcanberra-gtk-module opam xvfb
RUN apt-get install -y $debian_packages
RUN apt-get clean
# create user
RUN sudo adduser --disabled-password --gecos '' why3
......@@ -16,4 +18,5 @@ RUN opam init -a -y -j1 --compiler=$compiler
RUN opam repository add coq-released https://coq.inria.fr/opam/released
ARG opam_packages
RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo $opam_packages
RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo
RUN test -z "$opam_packages" || opam install -y $opam_packages
......@@ -8,7 +8,7 @@ if test -n "$DEBIAN_PACKAGES" -o -n "$OPAM_PACKAGES"; then
else
IMAGE=bench-image-$COMPILER
fi
docker build -t $IMAGE -f misc/Dockerfile.init --build-arg compiler=$COMPILER --build-arg debian_packages="$DEBIAN_PACKAGES" --build-arg opam_packages="$OPAM_PACKAGES" .
docker build -t $IMAGE --force-rm -f misc/Dockerfile.init --build-arg compiler=$COMPILER --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
......
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