diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ff12675d8681a46043a06290dee53abc0499ea7b..72d8f4b2f3d163f6d961dbede6e0d2528b8f3260 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -38,12 +38,12 @@ bench: variables: COMPILER: system script: - - misc/ci-docker.sh misc/ci-local.sh bench + - misc/ci-docker.sh misc/ci-local.sh bench ide .bench_template: &bench_definition stage: test script: - - misc/ci-docker.sh misc/ci-local.sh bench + - misc/ci-docker.sh misc/ci-local.sh bench ide only: - tags - schedules diff --git a/misc/Dockerfile.init b/misc/Dockerfile.init index 04b6dea45e1f96444a238feb9dbc0bc2c060035d..d7499830e1ab77fd389e0238d02eaeab6361f4e5 100644 --- a/misc/Dockerfile.init +++ b/misc/Dockerfile.init @@ -1,8 +1,9 @@ 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 + apt-get install -y wget libgmp-dev gtk+-2.0 libgtksourceview2.0-dev gnome-themes-standard libcanberra-gtk-module opam xvfb $debian_packages # create user RUN sudo adduser --disabled-password --gecos '' why3 @@ -14,5 +15,5 @@ ARG compiler=system RUN opam init -a -y -j1 --compiler=$compiler RUN opam repository add coq-released https://coq.inria.fr/opam/released -ARG packages -RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo $packages +ARG opam_packages +RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo $opam_packages diff --git a/misc/ci-docker.sh b/misc/ci-docker.sh index 057199cdcfd9667fea0368ce5eb19f75652bb7bc..3db3fd06937a9043618a5c090316259d27408b71 100755 --- a/misc/ci-docker.sh +++ b/misc/ci-docker.sh @@ -3,12 +3,12 @@ set -e autoconf && (automake --add-missing 2> /dev/null || true) -if test -n "$PACKAGES"; then - IMAGE=bench-image-$COMPILER--$(echo $PACKAGES | sed -e 's/ /--/g') +if test -n "$DEBIAN_PACKAGES" -o -n "$OPAM_PACKAGES"; then + IMAGE=bench-image-$COMPILER--$(echo $DEBIAN_PACKAGES | sed -e 's/ /--/g')--$(echo $OPAM_PACKAGES | sed -e 's/ /--/g') else IMAGE=bench-image-$COMPILER fi -docker build -t $IMAGE -f misc/Dockerfile.init --build-arg compiler=$COMPILER --build-arg packages="$PACKAGES" . +docker build -t $IMAGE -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 diff --git a/misc/ci-local.sh b/misc/ci-local.sh index e9561d2f7bebda67798497a7841ab89776cc1d51..344956566d836c61e6404ae6edde280c38f3a2c0 100755 --- a/misc/ci-local.sh +++ b/misc/ci-local.sh @@ -20,7 +20,19 @@ eval `opam config env` ./configure --enable-local make -if test "$1" = bench; then -bin/why3config --detect-provers -make bench -fi +while test $# -gt 0 +do + case "$1" in + bench) + bin/why3config --detect-provers + make bench + ;; + ide) + WHY3CONFIG="" xvfb-run bin/why3 ide --batch "" examples/logic/einstein.why + ;; + doc) + make doc + ;; + esac + shift +done