From caa593c3f2b6c9ad0c99125f86a46d70949f6175 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 29 Jun 2020 11:53:33 +0200
Subject: [PATCH] [Dev] add Docker files for framac/frama-c images
---
devel_tools/docker/README.md | 29 +++++++++++
devel_tools/docker/frama-c.21.0/Dockerfile | 58 ++++++++++++++++++++++
devel_tools/docker/frama-c.21.1/Dockerfile | 58 ++++++++++++++++++++++
3 files changed, 145 insertions(+)
create mode 100644 devel_tools/docker/README.md
create mode 100644 devel_tools/docker/frama-c.21.0/Dockerfile
create mode 100644 devel_tools/docker/frama-c.21.1/Dockerfile
diff --git a/devel_tools/docker/README.md b/devel_tools/docker/README.md
new file mode 100644
index 00000000000..0a1c8e049e4
--- /dev/null
+++ b/devel_tools/docker/README.md
@@ -0,0 +1,29 @@
+Docker images for Frama-C
+=========================
+
+- To build a new image (slim, without Frama-C sources nor tests):
+
+ cd <tag>
+ docker build . --target base -t framac/frama-c:<tag>
+
+- To run an interactive shell:
+
+ docker run -it framac/frama-c:<tag>
+
+- To push to Docker Hub (requires access to the `framac/frama-c` repository):
+
+ docker push framac/frama-c:<tag>
+
+- To build an image containing Frama-C sources (downloaded from the .tar.gz, in
+ directory `/root`):
+
+ cd <tag>
+ docker build . --build-arg with_source=yes \
+ -t framac/frama-c:<tag>-with-source
+
+- To run Frama-C tests (and remove unnecessary image later):
+
+ cd <tag>
+ docker build . --build-arg with_source=yes --build-arg with_test=yes \
+ -t framac/frama-c:<tag>-with-test
+ docker image rm framac/frama-c:<tag>-with-test
diff --git a/devel_tools/docker/frama-c.21.0/Dockerfile b/devel_tools/docker/frama-c.21.0/Dockerfile
new file mode 100644
index 00000000000..3a615a7bf0f
--- /dev/null
+++ b/devel_tools/docker/frama-c.21.0/Dockerfile
@@ -0,0 +1,58 @@
+FROM debian:sid as base
+
+RUN apt update
+RUN apt install opam -y
+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
+ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.07.1"
+ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml"
+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
+
+# Install packages from reference configuration
+RUN opam depext --install -y \
+ alt-ergo.2.0.0 \
+ apron.v0.9.12 \
+ conf-graphviz.0.1 \
+ mlgmpidl.1.2.12 \
+ ocamlfind.1.8.0 \
+ 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 \
+ --verbose # intentionally left as last line in this RUN command
+RUN why3 config --full-config
+
+# with_source: keep Frama-C sources
+ARG with_source=no
+
+RUN cd /root && \
+ wget http://frama-c.com/download/frama-c-21.0-Scandium.tar.gz && \
+ tar xvf frama-c-*.tar.gz && \
+ (cd frama-c-* && \
+ ./configure --disable-gui && \
+ make -j && \
+ make install \
+ ) && \
+ rm -f frama-c-*.tar.gz && \
+ [ "${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 \
+ opam depext --install -y \
+ conf-python-3.1.0.0 \
+ conf-time.1 \
+ --verbose \
+ && \
+ 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
new file mode 100644
index 00000000000..8852ac14805
--- /dev/null
+++ b/devel_tools/docker/frama-c.21.1/Dockerfile
@@ -0,0 +1,58 @@
+FROM debian:sid as base
+
+RUN apt update
+RUN apt install opam -y
+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
+ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.07.1"
+ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml"
+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
+
+# Install packages from reference configuration
+RUN opam depext --install -y \
+ alt-ergo.2.0.0 \
+ apron.v0.9.12 \
+ conf-graphviz.0.1 \
+ mlgmpidl.1.2.12 \
+ ocamlfind.1.8.0 \
+ 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 \
+ --verbose # intentionally left as last line in this RUN command
+RUN why3 config --full-config
+
+# with_source: keep Frama-C sources
+ARG with_source=no
+
+RUN cd /root && \
+ wget http://frama-c.com/download/frama-c-21.1-Scandium.tar.gz && \
+ tar xvf frama-c-*.tar.gz && \
+ (cd frama-c-* && \
+ ./configure --disable-gui && \
+ make -j && \
+ make install \
+ ) && \
+ rm -f frama-c-*.tar.gz && \
+ [ "${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 \
+ opam depext --install -y \
+ conf-python-3.1.0.0 \
+ conf-time.1 \
+ --verbose \
+ && \
+ cd /root/frama-c-* && \
+ make tests; \
+ fi
--
GitLab