Create a (very imperfect) container to run framac

Work woth Makefile

content/conception_formelle/99-DM_framac/Dockerfile

@@ -0,0 +1,48 @@
+FROM debian:unstable AS framac-base
+ENV DEBIAN_FRONTEND=noninteractive
+RUN useradd frama-c -m -u 9000 && \
+    apt-get update && \
+    apt-get install -y --no-install-recommends opam \
+        autoconf \
+        ca-certificates \
+        git \
+        graphviz \
+        libcairo2-dev \
+        libexpat1-dev \
+        libgmp-dev \
+        libgtk-3-dev \
+        libgtksourceview-3.0-dev \
+        pkg-config \
+        wget \
+        zlib1g-dev && \
+    apt clean
+COPY container/* /
+RUN su frama-c -c /install_framac.sh
+
+FROM framac-base AS framac
+ENV DEBIAN_FRONTEND=noninteractive
+RUN apt-get remove --purge -y \
+        ca-certificates \
+        git \
+        graphviz \
+        libcairo2-dev \
+        libexpat1-dev \
+        libgmp-dev \
+        libgtk-3-dev \
+        libgtksourceview-3.0-dev \
+        zlib1g-dev \
+        autoconf && \
+    apt-get autoremove -y && \
+    apt-get install --no-install-recommends -y \
+        libgtk-3-0 \
+        libgtksourceview-3.0-1 \
+        dbus-user-session \
+        libgdk-pixbuf-2.0-0 \
+        libgtksourceview-3.0-1 \
+        zlib1g \
+        localepurge
+RUN rm -rf /usr/share/man/??; rm -rf /usr/share/man/??_*
+USER frama-c
+ENV OPAMROOT=/home/frama-c/.opam
+WORKDIR /data
+ENTRYPOINT ["/entrypoint.sh"]

content/conception_formelle/99-DM_framac/Makefile

@@ -19,7 +19,7 @@ build: $(OUTPUT_DIR)/$(pdf_file)
 
 $(OUTPUT_DIR)/$(pdf_file): $(TEX_FILE)
 	$(shell mkdir -p $(OUTPUT_DIR))
-	lualatex --interaction=nonstopmode --output-directory $(OUTPUT_DIR) $<
+	latexmk -xelatex -output-directory=$(OUTPUT_DIR) $<
 
 buildall: images build
 
@@ -35,4 +35,15 @@ echo:
 view: build
 	$(PDF_APP) $(OUTPUT_DIR)/$(pdf_file)
 
-.PHONY: echo view clean
+build-container:
+	podman build . -t framac
+
+framac:
+	podman run -it --rm \
+		--volume=/tmp/.X11-unix/:/tmp/.X11-unix/ \
+		--volume=./code/:/data \
+		--userns "keep-id:uid=9000,gid=9000" \
+		-e DISPLAY=$$DISPLAY \
+		--entrypoint=/bin/bash framac
+
+.PHONY: echo view clean build-container framac

content/conception_formelle/99-DM_framac/container/entrypoint.sh

@@ -0,0 +1,5 @@
+#!/bin/sh
+#
+export DBUS_SESSION_BUS_ADDRESS=`dbus-daemon --fork --config-file=/usr/share/dbus-1/session.conf --print-address`
+eval $(opam env) || exit 10
+frama-c-gui

content/conception_formelle/99-DM_framac/container/install_framac.sh

@@ -0,0 +1,7 @@
+#!/bin/sh
+
+opam init --compiler 4.14.1 --disable-sandboxing --shell-setup
+eval $(opam env)
+opam install frama-c z3 -y
+why3 config detect
+opam clean