Merge branch 'feature/andre/dockerfile-internal' into 'master'

[Dev] add Dockerfile and instructions for internal images

See merge request frama-c/frama-c!2834

devel_tools/docker/frama-c.20.0/Dockerfile

 FROM debian:sid as base
 
+# Install non-OCaml dependencies + opam
 RUN apt-get update && apt-get install -y \
     cvc4 \
     opam \

devel_tools/docker/frama-c.21.0/Dockerfile

 FROM debian:sid as base
 
+# Install non-OCaml dependencies + opam
 RUN apt-get update && apt-get install -y \
     cvc4 \
     opam \
@@ -32,9 +33,6 @@ RUN apt-get update && opam update -y && opam depext --install -y --verbose \
     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

devel_tools/docker/frama-c.21.1/Dockerfile

 FROM debian:sid as base
 
+# Install non-OCaml dependencies + opam
 RUN apt-get update && apt-get install -y \
     cvc4 \
     opam \
@@ -32,9 +33,6 @@ RUN apt-get update && opam update -y && opam depext --install -y --verbose \
     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

devel_tools/docker/frama-c.custom/.gitignore

+# ignore an eventual frama-c subfolder in this directory
+frama-c

devel_tools/docker/frama-c.custom/Dockerfile

+FROM debian:sid as base
+
+# Install non-OCaml dependencies + opam
+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/*
+
+RUN why3 config --full-config
+
+# with_source: keep Frama-C sources
+ARG with_source=no
+
+# copies a cloned, non-public Frama-C
+COPY frama-c /root/frama-c
+
+RUN cd /root && \
+    (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

devel_tools/docker/frama-c.custom/README.md

+Building a Frama-C Docker image with a custom git clone
+=========================================================================
+
+In order to build a Frama-C Docker image with custom plug-ins, or using
+a custom git repository, do the following:
+
+1. Locally clone Frama-C into the `frama-c` directory, e.g. via
+
+        git clone git@frama-c.com:frama-c/frama-c.git
+
+   If needed, modify the clone to add other plug-ins and/or files inside
+   `frama-c`.
+
+2. If needed, add Debian and opam prerequisites to the appropriate lines in the
+   Dockerfile (after `apt update` and before removing the `apt` cache).
+   If you need to change the opam version, also edit the `ENV` lines.
+
+3. For a "minimal" image (with installed Frama-C, but no source code), run:
+
+        docker build . -t fc-custom # or another tag if you prefer
+
+    For an image with the Frama-C source code (in `/root/frama-c`), run:
+
+        docker build . -t fc-custom-with-source --build-arg=with_source=yes
+
+    For an image with source code + tests (e.g. which runs `make tests`), run:
+
+        docker build . -t fc-custom-with-test --build-arg=with_source=yes --build-arg=with_test=yes
+
+4. In all cases, after building the image, run it with:
+
+        docker run -it fc-custom # or another tag
+
+Frama-C will be installed and its sources will be in `/root/frama-c`.
+
+### Notes
+
+1. If you keep the sources, remember that the Docker image may contain
+   non-public code.
+
+2. Using different tags for the `*-with-source` and `*-with-test` images may
+   allow layer reuse by Docker.
+
+3. If you need files outside `/root/frama-c`, add them to the directory
+   containing this README and add a `COPY` instruction to the `Dockerfile`,
+   e.g. `COPY dir /root/dir`.

devel_tools/docker/frama-c.dev/Dockerfile

 FROM debian:sid as base
 
+# Install non-OCaml dependencies + opam
 RUN apt-get update && apt-get install -y \
     cvc4 \
     opam \
@@ -32,9 +33,6 @@ RUN apt-get update && opam update -y && opam depext --install -y --verbose \
     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