From 1328d6f4f3dbe52f470a379deedca2d965d0ebf2 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 10 Jul 2020 22:26:54 +0200
Subject: [PATCH] [Dev] improve Docker files with best practices; add file for
dev version
---
devel_tools/docker/frama-c.20.0/Dockerfile | 22 +++++---
devel_tools/docker/frama-c.21.0/Dockerfile | 23 +++++---
devel_tools/docker/frama-c.21.1/Dockerfile | 23 +++++---
devel_tools/docker/frama-c.dev/Dockerfile | 65 ++++++++++++++++++++++
4 files changed, 111 insertions(+), 22 deletions(-)
create mode 100644 devel_tools/docker/frama-c.dev/Dockerfile
diff --git a/devel_tools/docker/frama-c.20.0/Dockerfile b/devel_tools/docker/frama-c.20.0/Dockerfile
index d73738fb950..66dcd40c025 100644
--- a/devel_tools/docker/frama-c.20.0/Dockerfile
+++ b/devel_tools/docker/frama-c.20.0/Dockerfile
@@ -1,7 +1,11 @@
FROM debian:sid as base
-RUN apt update
-RUN apt install opam -y
+RUN apt-get update && apt-get install -y \
+ cvc4 \
+ opam \
+ z3 \
+ && rm -rf /var/lib/apt/lists/*
+
RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.05.0 -y
# "RUN eval $(opam env)" does not work, so we manually set its variables
@@ -11,11 +15,10 @@ ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/toplevel"
ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.05.0/man"
ENV PATH "/root/.opam/ocaml-base-compiler.4.05.0/bin:$PATH"
-RUN opam update -y
-RUN opam install depext -y
+RUN opam update -y && opam install depext -y
# Install packages from reference configuration
-RUN opam depext --install -y \
+RUN apt-get update && opam update -y && opam depext --install -y --verbose \
alt-ergo.2.0.0 \
apron.20160125 \
conf-graphviz.0.1 \
@@ -26,7 +29,8 @@ RUN opam depext --install -y \
why3.1.2.0 \
yojson.1.7.0 \
zarith.1.9.1 \
- --verbose # intentionally left as last line in this RUN command
+ && rm -rf /var/lib/apt/lists/*
+
RUN why3 config --detect-provers
# with_source: keep Frama-C sources
@@ -47,12 +51,14 @@ RUN cd /root && \
ARG with_test=no
RUN if [ "${with_test}" != "no" ]; then \
- opam depext --install -y \
+ apt-get update && \
+ opam update -y && opam depext --install -y \
conf-python-3.1.0.0 \
conf-time.1 \
--verbose \
&& \
- apt install python -y && \
+ apt-get install python -y && \
+ rm -rf /var/lib/apt/lists/* && \
cd /root/frama-c-* && \
make tests; \
fi
diff --git a/devel_tools/docker/frama-c.21.0/Dockerfile b/devel_tools/docker/frama-c.21.0/Dockerfile
index 3a615a7bf0f..472d6dce9eb 100644
--- a/devel_tools/docker/frama-c.21.0/Dockerfile
+++ b/devel_tools/docker/frama-c.21.0/Dockerfile
@@ -1,7 +1,11 @@
FROM debian:sid as base
-RUN apt update
-RUN apt install opam -y
+RUN apt-get update && apt-get install -y \
+ cvc4 \
+ opam \
+ z3 \
+ && rm -rf /var/lib/apt/lists/*
+
RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.07.1 -y
# "RUN eval $(opam env)" does not work, so we manually set its variables
@@ -11,11 +15,10 @@ ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/toplevel"
ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.07.1/man"
ENV PATH "/root/.opam/ocaml-base-compiler.4.07.1/bin:$PATH"
-RUN opam update -y
-RUN opam install depext -y
+RUN opam update -y && opam install depext -y
# Install packages from reference configuration
-RUN opam depext --install -y \
+RUN apt-get update && opam update -y && opam depext --install -y --verbose \
alt-ergo.2.0.0 \
apron.v0.9.12 \
conf-graphviz.0.1 \
@@ -27,7 +30,11 @@ RUN opam depext --install -y \
yojson.1.7.0 \
zarith.1.9.1 \
zmq.5.1.3 \
- --verbose # intentionally left as last line in this RUN command
+ && rm -rf /var/lib/apt/lists/*
+
+# Install non-OCaml solvers
+RUN apt install z3 cvc4 -y
+
RUN why3 config --full-config
# with_source: keep Frama-C sources
@@ -48,11 +55,13 @@ RUN cd /root && \
ARG with_test=no
RUN if [ "${with_test}" != "no" ]; then \
- opam depext --install -y \
+ apt-get update && \
+ opam update -y && opam depext --install -y \
conf-python-3.1.0.0 \
conf-time.1 \
--verbose \
&& \
+ rm -rf /var/lib/apt/lists/* && \
cd /root/frama-c-* && \
make tests; \
fi
diff --git a/devel_tools/docker/frama-c.21.1/Dockerfile b/devel_tools/docker/frama-c.21.1/Dockerfile
index 8852ac14805..c37b6441aa8 100644
--- a/devel_tools/docker/frama-c.21.1/Dockerfile
+++ b/devel_tools/docker/frama-c.21.1/Dockerfile
@@ -1,7 +1,11 @@
FROM debian:sid as base
-RUN apt update
-RUN apt install opam -y
+RUN apt-get update && apt-get install -y \
+ cvc4 \
+ opam \
+ z3 \
+ && rm -rf /var/lib/apt/lists/*
+
RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.07.1 -y
# "RUN eval $(opam env)" does not work, so we manually set its variables
@@ -11,11 +15,10 @@ ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/toplevel"
ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.07.1/man"
ENV PATH "/root/.opam/ocaml-base-compiler.4.07.1/bin:$PATH"
-RUN opam update -y
-RUN opam install depext -y
+RUN opam update -y && opam install depext -y
# Install packages from reference configuration
-RUN opam depext --install -y \
+RUN apt-get update && opam update -y && opam depext --install -y --verbose \
alt-ergo.2.0.0 \
apron.v0.9.12 \
conf-graphviz.0.1 \
@@ -27,7 +30,11 @@ RUN opam depext --install -y \
yojson.1.7.0 \
zarith.1.9.1 \
zmq.5.1.3 \
- --verbose # intentionally left as last line in this RUN command
+ && rm -rf /var/lib/apt/lists/*
+
+# Install non-OCaml solvers
+RUN apt install z3 cvc4 -y
+
RUN why3 config --full-config
# with_source: keep Frama-C sources
@@ -48,11 +55,13 @@ RUN cd /root && \
ARG with_test=no
RUN if [ "${with_test}" != "no" ]; then \
- opam depext --install -y \
+ apt-get update && \
+ opam update -y && opam depext --install -y \
conf-python-3.1.0.0 \
conf-time.1 \
--verbose \
&& \
+ rm -rf /var/lib/apt/lists/* && \
cd /root/frama-c-* && \
make tests; \
fi
diff --git a/devel_tools/docker/frama-c.dev/Dockerfile b/devel_tools/docker/frama-c.dev/Dockerfile
new file mode 100644
index 00000000000..aa819b0a661
--- /dev/null
+++ b/devel_tools/docker/frama-c.dev/Dockerfile
@@ -0,0 +1,65 @@
+FROM debian:sid as base
+
+RUN apt-get update && apt-get install -y \
+ cvc4 \
+ opam \
+ z3 \
+ && rm -rf /var/lib/apt/lists/*
+
+RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.08.1 -y
+
+# "RUN eval $(opam env)" does not work, so we manually set its variables
+ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.08.1"
+ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.08.1/lib/stublibs:/root/.opam/ocaml-base-compiler.4.08.1/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.08.1/lib/ocaml"
+ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.08.1/lib/toplevel"
+ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.08.1/man"
+ENV PATH "/root/.opam/ocaml-base-compiler.4.08.1/bin:$PATH"
+
+RUN opam update -y && opam install depext -y
+
+# Install packages from reference configuration
+RUN apt-get update && opam update -y && opam depext --install -y --verbose \
+ alt-ergo.2.0.0 \
+ apron.v0.9.12 \
+ conf-graphviz.0.1 \
+ mlgmpidl.1.2.12 \
+ ocamlfind.1.8.1 \
+ ocamlgraph.1.8.8 \
+ ppx_deriving_yojson.3.5.2 \
+ why3.1.3.1 \
+ yojson.1.7.0 \
+ zarith.1.9.1 \
+ zmq.5.1.3 \
+ && rm -rf /var/lib/apt/lists/*
+
+# Install non-OCaml solvers
+RUN apt install z3 cvc4 -y
+
+RUN why3 config --full-config
+
+# with_source: keep Frama-C sources
+ARG with_source=no
+
+RUN cd /root && \
+ git clone https://git.frama-c.com/pub/frama-c.git && \
+ (cd frama-c && \
+ autoconf && ./configure --disable-gui && \
+ make -j && \
+ make install \
+ ) && \
+ [ "${with_source}" != "no" ] || rm -rf frama-c
+
+# with_test: run Frama-C tests; requires "with_source=yes"
+ARG with_test=no
+
+RUN if [ "${with_test}" != "no" ]; then \
+ apt-get update && \
+ opam update -y && opam depext --install -y \
+ conf-python-3.1.0.0 \
+ conf-time.1 \
+ --verbose \
+ && \
+ rm -rf /var/lib/apt/lists/* && \
+ cd /root/frama-c && \
+ make tests; \
+ fi
--
GitLab