[docker] create new Docker image for running tests

docker/Dockerfile

-FROM ocaml/opam:debian-10-ocaml-4.11
-
-RUN sudo apt-get update &&\
-    sudo apt-get install -y cvc4 z3
-
-RUN opam repository set-url default "https://opam.ocaml.org" &&\
-    opam repository add lustrec "https://gitlab.isae-supaero.fr/lustrec/opam-repository.git" &&\
-    opam update &&\
-    opam depext -i\
-    dune.2.9.1 dune-site menhir zarith ppx_deriving_yojson ocamlgraph alt-ergo frama-c.24.0 re
-ENV PATH=$PATH:/home/opam/.opam/4.11/bin
-
-RUN curl https://sh.rustup.rs -sSf | sh -s -- -y
-ENV PATH=$PATH:/home/opam/.cargo/bin
-RUN cargo install tokei
-
-RUN why3 config detect
-
-COPY init.sh $HOME/
-
-CMD ["/bin/bash", "--init-file", "~/init.sh"]

docker/Dockerfile-run

+# This Dockerfile builds a Debian testing docker image with OCaml
+# 4.11, Frama-C 26.1, Z3 4.11.2 installed through Opam and CVC4 1.8
+# installed as an external binary.
+#
+# It could be run "over" a clone of LustreC repository to test
+# it. Notice that you have to install the LustreC Frama-C
+# lustrec_wp_plugin in order to be able to prove ACSL specifications.
+
+# use Debian image with OCaml and opam installed
+FROM ocaml/opam:debian-testing-ocaml-4.14
+
+# update repository
+RUN sudo apt update
+
+# upgrade opam
+RUN sudo apt install -y opam
+
+# install CVC4 and Z3 from Debian repository
+RUN sudo apt install -y cvc4
+
+# install tokei
+RUN curl https://sh.rustup.rs -sSf | sh -s -- -y
+ENV PATH=$PATH:/home/opam/.cargo/bin
+RUN cargo install tokei
+
+# update local opam repository
+RUN opam repository set-url default "https://opam.ocaml.org" && \
+    opam update
+
+# install Frama-C and Z3
+RUN opam install frama-c.26.1 z3
+
+# set shell and PATH for opam
+SHELL ["/bin/bash", "-c"]
+ENV PATH=$PATH:/home/opam/.opam/4.14/bin
+
+# config Why3 solvers
+RUN why3 config detect
+
+# add init shell script
+ADD init.sh /home/opam/
+
+# start
+CMD /bin/bash --init-file /home/opam/init.sh
+
+# Local Variables:
+# mode: Dockerfile
+# End:

docker/README.md

+You will find here Dockerfiles needed to build Docker images for
+LustreC.
+
+* `Dockerfile-run`
+
+`Dockerfile-run` builds a Docker image composed of:
+
+- a Debian testing distribution with OCaml 4.14 and CVC4 installed
+- an opam distribution with Frama-C and Z3 installed
+
+This can be used to test LustreC: clone the LustreC repository, pull
+the image and run the `run_docker.sh` script available in the
+`scripts` directory. LustreC and the associated WP strategies are
+built in the host clone of LustreC and you can run tests inside the
+container.

docker/init.sh

-#!/usr/bin/env bash
+# init commands when starting LustreC "run" docker
 
-cd $HOME/lustrec
+# echo PATH
+echo "PATH:" $PATH
 
-echo "Compiling LustreC..."
+# compile LustreC
+cd lustrec
+echo "compiling LustreC..."
 dune clean
 dune build @install
-echo "Done."
+echo "... done!"
+
+# compile LustreC strategies
+cd lustrec_wp_strategies
+echo "installing LustreC WP strategies..."
+opam install .
+echo "... done!"
+
+# get ready
+cd /home/opam/lustrec

scripts/rundocker.sh

@@ -14,9 +14,15 @@ usage () {
 }
 
 # default values
-CONTAINER_ID=leliobrun/lustrec-env
+CONTAINER_ID=gitlab-registry.isae-supaero.fr/lustrec/lustrec/lustrec-run:latest
 TMP_DIR=/tmp
 
+# check if docker is available
+command -v docker >/dev/null 2>&1 || { \
+        echo >&2 "docker is required but could not be found.  Aborting."; \
+        echo >&2 "To setup Docker: https://docs.docker.com/engine/getstarted/step_one/"; \
+        exit 1; }
+
 # use getopt to get arguments
 TEMP=$(getopt -o 'hi:t:' --long 'help,id:,tmp:' -n 'rundocker.sh' -- "$@")
 
@@ -46,14 +52,8 @@ while true; do
     esac
 done
 
-# check if docker is available
-command -v docker >/dev/null 2>&1 || { \
-        echo >&2 "docker is required but could not be found.  Aborting."; \
-        echo >&2 "To setup Docker: https://docs.docker.com/engine/getstarted/step_one/"; \
-        exit 1; }
-
 # launch docker
-docker run -it --rm --user $(id -u):$(id -g)\
-       -name "lustrec_docker" \
+docker run -it --rm \
+       --name "lustrec-from-${CONTAINER_ID}" \
        -v ${TMP_DIR}:/tmp -v ${PWD}:/home/opam/lustrec \
        ${CONTAINER_ID} $@