diff --git a/content/conception_formelle/99-DM_framac/Dockerfile b/content/conception_formelle/99-DM_framac/Dockerfile new file mode 100644 index 0000000..4b70afe --- /dev/null +++ b/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"] diff --git a/content/conception_formelle/99-DM_framac/Makefile b/content/conception_formelle/99-DM_framac/Makefile index d1aa13f..5ec72c0 100644 --- a/content/conception_formelle/99-DM_framac/Makefile +++ b/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 diff --git a/content/conception_formelle/99-DM_framac/container/entrypoint.sh b/content/conception_formelle/99-DM_framac/container/entrypoint.sh new file mode 100755 index 0000000..c86b2c7 --- /dev/null +++ b/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 diff --git a/content/conception_formelle/99-DM_framac/container/install_framac.sh b/content/conception_formelle/99-DM_framac/container/install_framac.sh new file mode 100755 index 0000000..75784ad --- /dev/null +++ b/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