From c0cba938d4ec55c74aef964feccea2ad51ba40ab Mon Sep 17 00:00:00 2001
From: Christophe Garion <tofgarion@runbox.com>
Date: Wed, 8 Mar 2023 13:25:05 +0100
Subject: [PATCH] [docker] create new Docker image for running tests
---
docker/Dockerfile | 21 -------------------
docker/Dockerfile-run | 48 +++++++++++++++++++++++++++++++++++++++++++
docker/README.md | 15 ++++++++++++++
docker/init.sh | 20 ++++++++++++++----
scripts/rundocker.sh | 18 ++++++++--------
5 files changed, 88 insertions(+), 34 deletions(-)
delete mode 100644 docker/Dockerfile
create mode 100644 docker/Dockerfile-run
create mode 100644 docker/README.md
diff --git a/docker/Dockerfile b/docker/Dockerfile
deleted file mode 100644
index 9caefb8a..00000000
--- a/docker/Dockerfile
+++ /dev/null
@@ -1,21 +0,0 @@
-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"]
diff --git a/docker/Dockerfile-run b/docker/Dockerfile-run
new file mode 100644
index 00000000..fa0591e5
--- /dev/null
+++ b/docker/Dockerfile-run
@@ -0,0 +1,48 @@
+# 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:
diff --git a/docker/README.md b/docker/README.md
new file mode 100644
index 00000000..47c98117
--- /dev/null
+++ b/docker/README.md
@@ -0,0 +1,15 @@
+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.
diff --git a/docker/init.sh b/docker/init.sh
index 20f1894f..da8f9e31 100644
--- a/docker/init.sh
+++ b/docker/init.sh
@@ -1,8 +1,20 @@
-#!/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
diff --git a/scripts/rundocker.sh b/scripts/rundocker.sh
index 361e87e2..7a92ec90 100644
--- a/scripts/rundocker.sh
+++ b/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} $@
--
GitLab