diff --git a/.gitattributes b/.gitattributes
index 8ef1e4377b4d746cdc290c0888f708148c905058..175efe37d0a716458d0c6cb2dc56d462ea91fe6a 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -170,7 +170,8 @@ README* header_spec=.ignore
/bin/sed_get_* header_spec=.ignore
-/dev/docker/*.template header_spec=.ignore
+/dev/docker/*.sh header_spec=.ignore
+/dev/docker/Dockerfile header_spec=.ignore
# TODO: header_spec=JCF_LGPL_2_only
/dev/size.mli header_spec=.ignore
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 55d0f71f9070061a792ee1210464ac94a4aaf035..c40941fc5b002f73e74ea6fca2baf700414695e6 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -434,13 +434,19 @@ src-distrib-tests:
variables:
- $RELEASE == "yes"
-src-distrib-tests-long:
+src-distrib-tests-scheduled:
<<: *src_distrib_tests_template
# The Opam target may affect this job
timeout: 2h
only:
refs:
- schedules
+
+src-distrib-tests-release:
+ <<: *src_distrib_tests_template
+ # The Opam target may affect this job
+ timeout: 2h
+ only:
variables:
- $RELEASE == "yes"
@@ -468,8 +474,9 @@ release-branch:
release-create:
stage: release
+ <<: *prepare_ssh_template
script:
- - nix-shell -p curl --run './nix/frama-c-public/publish-release.sh'
+ - nix-shell -p git git-lfs coreutils openssh curl --run './nix/frama-c-public/publish-release.sh'
needs:
- release-branch
- release-content
@@ -483,7 +490,7 @@ release-opam:
stage: release
<<: *prepare_ssh_template
script:
- - nix-shell -p openssh --run './nix/frama-c-public/publish-opam.sh'
+ - nix-shell -p git git-lfs coreutils openssh --run './nix/frama-c-public/publish-opam.sh'
only:
variables:
- $RELEASE == "yes"
@@ -493,7 +500,7 @@ release-website:
stage: release
<<: *prepare_ssh_template
script:
- - nix-shell -p openssh --run './nix/frama-c-public/publish-website.sh'
+ - nix-shell -p git git-lfs coreutils openssh --run './nix/frama-c-public/publish-website.sh'
only:
variables:
- $RELEASE == "yes"
@@ -503,7 +510,7 @@ release-wiki:
stage: release
<<: *prepare_ssh_template
script:
- - nix-shell -p openssh --run './nix/frama-c-public/publish-wiki.sh'
+ - nix-shell -p git git-lfs coreutils openssh --run './nix/frama-c-public/publish-wiki.sh'
only:
variables:
- $RELEASE == "yes"
diff --git a/dev/build-release.sh b/dev/build-release.sh
index 144efd3926ff6ce40529b0c6b6192825fbb95d29..33e322c71daa31482d5bba774d0990efd38c57c4 100755
--- a/dev/build-release.sh
+++ b/dev/build-release.sh
@@ -112,15 +112,15 @@ if [ "$VERSION_SAFE" != "$TAG" ]; then
fi
if test -n "$VERSION_MODIFIER"; then
- FINAL=no
+ FINAL_RELEASE=no
else
- FINAL=yes
+ FINAL_RELEASE=yes
fi
echo "Ready to build release: Frama-C $VERSION - $CODENAME"
echo "MAJOR: $VERSION_MAJOR"
echo "MINOR: $VERSION_MINOR"
-echo "FINAL: $FINAL"
+echo "FINAL: $FINAL_RELEASE"
##########################################################################
# Check input files
@@ -216,18 +216,24 @@ function version_name {
# $2 : extension
function copy_manual_normal {
- cp "$MANUALS_DIR/$1.$2" "$MANS_TARGET_DIR/$(generic_name "$1").$2"
+ if [ "$FINAL_RELEASE" = "yes" ]; then
+ cp "$MANUALS_DIR/$1.$2" "$MANS_TARGET_DIR/$(generic_name "$1").$2"
+ fi
cp "$MANUALS_DIR/$1.$2" "$MANS_TARGET_DIR/$(version_name "$1").$2"
}
function copy_manual_e_acsl {
EACSL_TARGET_DIR="$MANS_TARGET_DIR/e-acsl"
- cp "$MANUALS_DIR/$1.$2" "$EACSL_TARGET_DIR/$(generic_name "$1").$2"
+ if [ "$FINAL_RELEASE" = "yes" ]; then
+ cp "$MANUALS_DIR/$1.$2" "$EACSL_TARGET_DIR/$(generic_name "$1").$2"
+ fi
cp "$MANUALS_DIR/$1.$2" "$EACSL_TARGET_DIR/$(version_name "$1").$2"
}
function copy_api {
- cp "$API_DIR/$1-api.$2" "$MANS_TARGET_DIR/$1-api.$2"
+ if [ "$FINAL_RELEASE" = "yes" ]; then
+ cp "$API_DIR/$1-api.$2" "$MANS_TARGET_DIR/$1-api.$2"
+ fi
cp "$API_DIR/$1-api.$2" "$MANS_TARGET_DIR/$1-$VERSION_AND_CODENAME-api.$2"
}
@@ -243,14 +249,18 @@ function copy_files {
copy_manual_normal "$companion" "tar.gz"
done
for api in "${API_FILES[@]}"; do
- copy_api "$file" "tar.gz"
+ copy_api "$api" "tar.gz"
done
# Eva has an old manual name that might be in use:
- cp "$MANS_TARGET_DIR/frama-c-eva-manual.pdf" "$MANS_TARGET_DIR/frama-c-value-analysis.pdf"
+ if [ "$FINAL_RELEASE" = "yes" ]; then
+ cp "$MANS_TARGET_DIR/frama-c-eva-manual.pdf" "$MANS_TARGET_DIR/frama-c-value-analysis.pdf"
+ fi
cp $TARGZ_BASE "$GZ_TARGET_DIR/$TARGZ_VERSION"
- cp $TARGZ_BASE "$GZ_TARGET_DIR/$TARGZ_GENERIC"
+ if [ "$FINAL_RELEASE" = "yes" ]; then
+ cp $TARGZ_BASE "$GZ_TARGET_DIR/$TARGZ_GENERIC"
+ fi
}
##########################################################################
@@ -436,7 +446,8 @@ VERSION_WEBPAGE="$WEBSITE_DIR/_fc-versions/$LOWER_CODENAME.md"
if [ "$FINAL_RELEASE" = "no" ]; then
ACSL_OR_BETA="beta: true"
else
- ACSL_OR_BETA="acsl: $ACSL_VERSION"
+ ACSL_VERSION_WEBSITE="$(echo $ACSL_VERSION | sed -n 's/1.\([0-9][0-9]\)/\1/p')"
+ ACSL_OR_BETA="acsl: $ACSL_VERSION_WEBSITE"
fi
cat >$VERSION_WEBPAGE <<EOL
@@ -473,16 +484,16 @@ releases:
link: /download/aorai-manual-$VERSION_AND_CODENAME.pdf
help: Aoraï example
help_link: /download/aorai-example-$VERSION_AND_CODENAME.tar.gz
- - name: Metrics manual"
- link: /download/metrics-manual-$VERSION_AND_CODENAME.pdf"
- - name: Rte manual"
- link: /download/rte-manual-$VERSION_AND_CODENAME.pdf"
- - name: Eva manual"
- link: /download/eva-manual-$VERSION_AND_CODENAME.pdf"
- - name: WP manual"
- link: /download/wp-manual-$VERSION_AND_CODENAME.pdf"
- - name: E-ACSL manual"
- link: /download/e-acsl/e-acsl-manual-$VERSION_AND_CODENAME.pdf"
+ - name: Metrics manual
+ link: /download/metrics-manual-$VERSION_AND_CODENAME.pdf
+ - name: Rte manual
+ link: /download/rte-manual-$VERSION_AND_CODENAME.pdf
+ - name: Eva manual
+ link: /download/eva-manual-$VERSION_AND_CODENAME.pdf
+ - name: WP manual
+ link: /download/wp-manual-$VERSION_AND_CODENAME.pdf
+ - name: E-ACSL manual
+ link: /download/e-acsl/e-acsl-manual-$VERSION_AND_CODENAME.pdf
---
EOL
diff --git a/dev/docker/.gitignore b/dev/docker/.gitignore
index 7762191a2d2e4e1fcc7889d279426890c04f02ae..7845ce79398f785fa42b0720d45cfa484bb9961f 100644
--- a/dev/docker/.gitignore
+++ b/dev/docker/.gitignore
@@ -1,10 +1,2 @@
-Dockerfile.dev*
-Dockerfile.1*
-Dockerfile.2*
-Dockerfile.3*
-Dockerfile.4*
-Dockerfile.5*
-Dockerfile.6*
-Dockerfile.7*
-Dockerfile.8*
-Dockerfile.9*
+# reference-configuration.md is copied from ../..
+/reference-configuration.md
diff --git a/dev/docker/Dockerfile b/dev/docker/Dockerfile
new file mode 100644
index 0000000000000000000000000000000000000000..23c29c91e5646bdd75c91f20e2b16de187471103
--- /dev/null
+++ b/dev/docker/Dockerfile
@@ -0,0 +1,331 @@
+# Inspired by https://github.com/Frederic-Boulanger-UPS/docker-framac and
+# https://gitlab.inria.fr/why3/why3/-/blob/master/misc/Dockerfile.deploy
+
+# DISTRO must be passed via --build-arg (see Makefile)
+ARG DISTRO
+FROM $DISTRO AS base
+
+# Stage 1: install opam 2.1 and create 'opam' user
+
+ENV DEBIAN_FRONTEND=noninteractive
+
+COPY install.sh /init/
+RUN chmod +x /init/install.sh
+RUN /init/install.sh \
+ bash \
+ bubblewrap \
+ build-base \
+ bzip2 \
+ curl \
+ diffutils \
+ gcc \
+ git \
+ make \
+ patch \
+ unzip \
+ wget
+
+RUN bash -c "yes '' | sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)" --version 2.1.3
+
+# Avoid using root (opam dislikes it)
+COPY add-user.sh /init/
+RUN /init/add-user.sh opam
+USER opam
+WORKDIR /home/opam
+
+# Stage 2: initialize opam
+
+FROM base AS opam-init
+ARG OCAML_VERSION
+
+ENV DEBIAN_FRONTEND=noninteractive
+
+COPY reference-configuration.md /init/
+COPY opam-init-from-ref-config.sh /init/
+RUN sudo chmod +x /init/opam-init-from-ref-config.sh
+RUN /init/opam-init-from-ref-config.sh "${OCAML_VERSION}"
+
+# "RUN eval $(opam env)" does not work, so we manually set its variables.
+# We also set other potentially useful environment variables
+
+## Avoid prompts for time zone
+ENV TZ=Europe/Paris
+## Fix issue with libGL on Windows
+ENV LIBGL_ALWAYS_INDIRECT=1
+
+ENV OPAM_SWITCH_PREFIX "/home/opam/.opam/${OCAML_VERSION}"
+ENV CAML_LD_LIBRARY_PATH "/home/opam/.opam/${OCAML_VERSION}/lib/stublibs:/home/opam/.opam/${OCAML_VERSION}/lib/ocaml/stublibs:/home/opam/.opam/${OCAML_VERSION}/lib/ocaml"
+ENV OCAML_TOPLEVEL_PATH "/home/opam/.opam/${OCAML_VERSION}/lib/toplevel"
+ENV MANPATH "$MANPATH:/home/opam/.opam/${OCAML_VERSION}/man"
+ENV PATH "/home/opam/.opam/${OCAML_VERSION}/bin:$PATH"
+
+## Add file to help with interactive Docker image use
+RUN if [ ! -e /home/opam/.bashrc ]; then echo ". .bash_profile" > /home/opam/.bashrc; fi
+
+# Stage 3: install Frama-C dependencies
+
+FROM opam-init AS fc-deps
+ARG OCAML_VERSION
+
+ENV DEBIAN_FRONTEND=noninteractive
+
+# Install external provers
+## CVC4 1.7
+RUN \
+ wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.7-x86_64-linux-opt -O cvc4-1.7 \
+ && chmod a+x cvc4-1.7 \
+ && sudo mv cvc4-1.7 /usr/local/bin/
+RUN /init/install.sh z3
+
+# Install Frama-C depexts and dependencies
+COPY opam-install-fc-deps-from-ref-config.sh /init/
+RUN sudo chmod +x /init/opam-install-fc-deps-from-ref-config.sh
+RUN /init/opam-install-fc-deps-from-ref-config.sh
+
+RUN why3 config detect
+
+# Stage 4: install Frama-C itself
+
+FROM fc-deps AS frama-c
+ARG OCAML_VERSION
+
+ENV DEBIAN_FRONTEND=noninteractive
+
+## from_archive: if "git", clone from public Git; if prefixed with http,
+## wget it; otherwise, use the given archive name.
+## Note: the archive must contain a root directory
+## starting with 'frama-c'
+ARG from_archive=git
+
+## The following line copies a frama-c archive if it exists, else nothing
+COPY --chown=opam:opam README.md frama-c-*.tar.gz /frama-c/
+
+RUN \
+if [ "${from_archive}" != "git" ]; then \
+ (cd /frama-c && \
+ case "${from_archive}" in \
+ "http"*) wget "${from_archive}" ;; \
+ *) ;; \
+ esac && \
+ tar xvf "${from_archive##*/}" --strip 1 && \
+ rm -f frama-c-*.tar.gz) \
+; else \
+ (cd /frama-c && rm -f * && git clone --depth 1 https://git.frama-c.com/pub/frama-c.git .) \
+; fi
+
+RUN cd /frama-c && ./dev/disable-plugins.sh gui && make clean && make && make install
+
+## Run quick sanity checks
+RUN \
+printf "int g;\n//@assigns g;\nvoid f(){g = 1;}\nint main() {f(); return g;}" > /tmp/simple.c && \
+frama-c -eva -wp -report /tmp/simple.c && \
+rm -f /tmp/simple.c
+
+## Cleanup
+RUN \
+ opam clean --yes --switch-cleanup && \
+ rm -rf /home/opam/opam-repository && \
+ rm -rf /home/opam/.opam/repo/default/.git*
+
+# Stage 5 (optional): tests
+
+FROM frama-c AS tests
+ARG OCAML_VERSION
+
+ENV DEBIAN_FRONTEND=noninteractive
+
+## Run standard Frama-C tests
+RUN cd /frama-c && make run-ptests && dune build @ptests_config
+
+## Run an extra test for WP with provers
+RUN cd /frama-c/ && cd src/plugins/wp/tests/ && frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,z3
+
+# Stage 6 (optional): GUI
+
+FROM frama-c AS frama-c-gui
+ARG OCAML_VERSION
+
+ENV DEBIAN_FRONTEND=noninteractive
+
+RUN /init/install.sh adwaita-icon-theme font-noto gdk-pixbuf
+RUN cd /frama-c && ./dev/disable-plugins.sh none && make clean && make && make install
+
+## Sanity check
+RUN which frama-c-gui
+
+# Stage 7 (to be deployed): 'slim' image
+
+FROM $DISTRO AS frama-c-slim
+ARG OCAML_VERSION
+
+ENV DEBIAN_FRONTEND=noninteractive
+
+# Transfers ownership of /home/opam to user opam
+# Note: Fedora does not recognize --disabled-password, but it does not need it
+RUN adduser --disabled-password opam 2>/dev/null || adduser opam
+
+COPY --from=frama-c /bin /bin/
+COPY --from=frama-c /etc /etc/
+COPY --from=frama-c /lib /lib/
+COPY --from=frama-c /sbin /sbin/
+## RUN true cmds are a workaround against
+## obscure docker bug (https://github.com/moby/moby/issues/37965)
+## manifesting in sequences of COPY
+RUN true
+COPY --from=frama-c /usr /usr/
+RUN true
+COPY --from=frama-c --chown=opam:opam /home/opam/.opam /home/opam/.opam/
+COPY --from=frama-c /home/opam/.bashrc /home/opam/
+
+USER opam
+WORKDIR /home/opam
+ENV OPAM_SWITCH_PREFIX "/home/opam/.opam/${OCAML_VERSION}"
+ENV CAML_LD_LIBRARY_PATH "/home/opam/.opam/${OCAML_VERSION}/lib/stublibs:/home/opam/.opam/${OCAML_VERSION}/lib/ocaml/stublibs:/home/opam/.opam/${OCAML_VERSION}/lib/ocaml"
+ENV OCAML_TOPLEVEL_PATH "/home/opam/.opam/${OCAML_VERSION}/lib/toplevel"
+ENV MANPATH "$MANPATH:/home/opam/.opam/${OCAML_VERSION}/man"
+ENV PATH "/home/opam/.opam/${OCAML_VERSION}/bin:$PATH"
+## Avoid prompts for time zone
+ENV TZ=Europe/Paris
+## Fix issue with libGL on Windows
+ENV LIBGL_ALWAYS_INDIRECT=1
+
+RUN why3 config detect
+
+# Stage 8 (optional, to be deployed): 'slim' image with frama-c-gui
+
+FROM $DISTRO AS frama-c-gui-slim
+ARG OCAML_VERSION
+
+ENV DEBIAN_FRONTEND=noninteractive
+
+# Transfers ownership of /home/opam to user opam
+RUN adduser --disabled-password opam 2>/dev/null || adduser opam
+
+COPY --from=frama-c-gui /bin /bin/
+COPY --from=frama-c-gui /etc /etc/
+COPY --from=frama-c-gui /lib /lib/
+COPY --from=frama-c-gui /sbin /sbin/
+RUN true
+COPY --from=frama-c-gui /usr /usr/
+RUN true
+COPY --from=frama-c-gui --chown=opam:opam /home/opam/.opam /home/opam/.opam/
+COPY --from=frama-c /home/opam/.bashrc /home/opam/
+
+USER opam
+WORKDIR /home/opam
+ENV OPAM_SWITCH_PREFIX "/home/opam/.opam/${OCAML_VERSION}"
+ENV CAML_LD_LIBRARY_PATH "/home/opam/.opam/${OCAML_VERSION}/lib/stublibs:/home/opam/.opam/${OCAML_VERSION}/lib/ocaml/stublibs:/home/opam/.opam/${OCAML_VERSION}/lib/ocaml"
+ENV OCAML_TOPLEVEL_PATH "/home/opam/.opam/${OCAML_VERSION}/lib/toplevel"
+ENV MANPATH "$MANPATH:/home/opam/.opam/${OCAML_VERSION}/man"
+ENV PATH "/home/opam/.opam/${OCAML_VERSION}/bin:$PATH"
+## Avoid prompts for time zone
+ENV TZ=Europe/Paris
+## Fix issue with libGL on Windows
+ENV LIBGL_ALWAYS_INDIRECT=1
+
+RUN why3 config detect
+
+## Sanity check
+RUN which frama-c-gui
+
+## Stage 9: preparation of 'stripped' image (~200 MB compressed)
+## Note: this image only contains the Frama-C binaries and files closely
+## related to it; most other OCaml tools have been removed.
+## Even recompilation of Frama-C is not guaranteed to work.
+
+FROM frama-c-slim AS frama-c-stripped-prepare
+ARG OCAML_VERSION
+
+ENV DEBIAN_FRONTEND=noninteractive
+
+ENV OPAM_SWITCH_PREFIX "/home/opam/.opam/${OCAML_VERSION}"
+ENV CAML_LD_LIBRARY_PATH "/home/opam/.opam/${OCAML_VERSION}/lib/stublibs:/home/opam/.opam/${OCAML_VERSION}/lib/ocaml/stublibs:/home/opam/.opam/${OCAML_VERSION}/lib/ocaml"
+ENV OCAML_TOPLEVEL_PATH "/home/opam/.opam/${OCAML_VERSION}/lib/toplevel"
+ENV MANPATH "$MANPATH:/home/opam/.opam/${OCAML_VERSION}/man"
+ENV PATH "/home/opam/.opam/${OCAML_VERSION}/bin:$PATH"
+## Avoid prompts for time zone
+ENV TZ=Europe/Paris
+## Fix issue with libGL on Windows
+ENV LIBGL_ALWAYS_INDIRECT=1
+
+
+## Remove all non-essential ocaml binaries
+RUN \
+mkdir -p /home/opam/minimal/bin && \
+(cd /home/opam/.opam/*/bin && \
+ cp -P $(ls -d frama-c frama-c-config frama-c-script e-acsl-gcc.sh alt-ergo ocaml ocamlc ocamlc.opt ocamlfind ocamlopt ocamlopt.opt why3) /home/opam/minimal/bin/) && \
+rm -rf /home/opam/.opam/${OCAML_VERSION}/bin && \
+mv /home/opam/minimal/bin /home/opam/.opam/${OCAML_VERSION}/bin/
+
+## Remove non-essential opam files
+RUN rm -rf /home/opam/.opam/repo/default/packages
+RUN rm -rf /home/opam/.opam/download-cache
+RUN rm -rf /home/opam/.opam/repo/state.cache
+RUN rm -f /home/opam/.opam/repo/default.tar.gz
+
+## Further stripping: remove non-essential files from tools used by Frama-C
+## (Apron, Alt-Ergo, large OCaml compiler files, etc)
+RUN rm -f /home/opam/.opam/${OCAML_VERSION}/share/apron/lib/*.a
+RUN rm -f /home/opam/.opam/${OCAML_VERSION}/share/apron/lib/*_debug.so
+RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/share/apron/bin
+RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/share/apron/include
+RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/alt-ergo
+RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/lablgtk3
+RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/lablgtk3-sourceview3
+RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/ppx_deriving
+RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/ppx_import
+RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/ppx_tools
+RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/ppxlib
+RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/psmt2-frontend
+RUN rm -rf /home/opam/.opam/*/lib/ocaml/expunge
+RUN rm -rf /home/opam/.opam/*/lib/ocaml-migrate-parsetree
+
+## Remove all non-essential OCaml files (everything else other than
+## *.cmxs, *.cmx and *.cmi)
+## Exceptions: libeacsl-dlmalloc.a (used by e-acsl-gcc.sh during linking)
+RUN find /home/opam/.opam \( -name "*.cmt*" -o -name "*.[ao]" -o -name "*.cm[ao]" -o -name "*.cmxa" \) -a -not -name "libeacsl-dlmalloc.a" -exec rm {} \;
+
+## Remove non-essential installed files
+RUN sudo rm -r /usr/share/gtk-3.0 /usr/share/X11
+RUN sudo rm -f /usr/bin/*gnu-lto-dump*
+
+## Stage 10 (optional): stripped, slimmest image (running Frama-C works,
+## but almost everything else does not (e.g. recompiling OCaml modules))
+
+FROM $DISTRO AS frama-c-stripped
+ARG OCAML_VERSION
+
+ENV DEBIAN_FRONTEND=noninteractive
+
+# Transfers ownership of /home/opam to user opam
+RUN adduser --disabled-password opam 2>/dev/null || adduser opam
+
+COPY --from=frama-c-stripped-prepare /bin /bin/
+COPY --from=frama-c-stripped-prepare /etc /etc/
+COPY --from=frama-c-stripped-prepare /lib /lib/
+COPY --from=frama-c-stripped-prepare /sbin /sbin/
+RUN true
+COPY --from=frama-c-stripped-prepare /usr /usr/
+RUN true
+COPY --from=frama-c-stripped-prepare --chown=opam:opam /home/opam/.opam /home/opam/.opam/
+COPY --from=frama-c /home/opam/.bashrc /home/opam/
+
+USER opam
+WORKDIR /home/opam
+ENV OPAM_SWITCH_PREFIX "/home/opam/.opam/${OCAML_VERSION}"
+ENV CAML_LD_LIBRARY_PATH "/home/opam/.opam/${OCAML_VERSION}/lib/stublibs:/home/opam/.opam/${OCAML_VERSION}/lib/ocaml/stublibs:/home/opam/.opam/${OCAML_VERSION}/lib/ocaml"
+ENV OCAML_TOPLEVEL_PATH "/home/opam/.opam/${OCAML_VERSION}/lib/toplevel"
+ENV MANPATH "$MANPATH:/home/opam/.opam/${OCAML_VERSION}/man"
+ENV PATH "/home/opam/.opam/${OCAML_VERSION}/bin:$PATH"
+## Avoid prompts for time zone
+ENV TZ=Europe/Paris
+## Fix issue with libGL on Windows
+ENV LIBGL_ALWAYS_INDIRECT=1
+
+RUN why3 config detect
+
+## Re-run quick sanity checks
+RUN \
+printf "int g;\n//@assigns g;\nvoid f(){g = 1;}\nint main() {f(); return g;}" > /tmp/simple.c && \
+frama-c -val -wp -report /tmp/simple.c && \
+rm -f /tmp/simple.c
diff --git a/dev/docker/Dockerfile.template b/dev/docker/Dockerfile.template
deleted file mode 100644
index 98c7b11295341b771fb353d95bc7d575ebcec698..0000000000000000000000000000000000000000
--- a/dev/docker/Dockerfile.template
+++ /dev/null
@@ -1,220 +0,0 @@
-# Inspired by https://github.com/Frederic-Boulanger-UPS/docker-framac and
-# https://gitlab.inria.fr/why3/why3/-/blob/master/misc/Dockerfile.deploy
-
-FROM @ALPINE_OPAM_BASE@ AS base
-
-# Stage 1: switch opam if needed (only for very old versions),
-# then install external provers (see .template files)
-
-FROM base AS frama-c
-
-## Install packages from reference configuration
-## Note: Python and time packages are only required for tests, but if so,
-## they need to be present before running './configure'
-RUN \
-@OPAM_CACHE_FIX@ \
-opam update -y && \
-opam install depext -y
-
-RUN @OPAM_SWITCH@
-
-# "RUN eval $(opam env)" does not work, so we manually set its variables
-@ENV@
-
-# Install external provers
-@CVC4@
-@Z3@
-
-RUN opam depext --install -y @OPAM_DEPS@
-
-RUN @WHY3_CONFIG@
-
-# from_archive: if "git", clone from public Git; if prefixed with http,
-# wget it; otherwise, use the given archive name.
-# Note: the archive must contain a root directory
-# starting with 'frama-c'
-ARG from_archive=git
-
-# The following line copies a frama-c archive if it exists, else nothing
-COPY --chown=opam:opam README.md frama-c-*.tar.gz /frama-c/
-
-RUN \
-if [ "${from_archive}" != "git" ]; then \
- (cd /frama-c && \
- case "${from_archive}" in \
- "http"*) wget "${from_archive}" ;; \
- *) ;; \
- esac && \
- tar xvf "${from_archive##*/}" --strip 1 && \
- rm -f frama-c-*.tar.gz) \
-; else \
- sudo apk add git && \
- (cd /frama-c && rm -f * && git clone --depth 1 https://git.frama-c.com/pub/frama-c.git .) \
-; fi
-
-RUN cd /frama-c && @PATCH_FRAMAC@ && @CONFIGURE@
-RUN cd /frama-c && @MAKE_MAKE_INSTALL@
-
-# Run quick sanity checks
-RUN \
-printf "int g;\n//@assigns g;\nvoid f(){g = 1;}\nint main() {f(); return g;}" > /tmp/simple.c && \
-frama-c -val @WP_REPORT@ /tmp/simple.c && \
-rm -f /tmp/simple.c
-
-## Cleanup
-RUN \
-opam clean --yes --switch-cleanup && \
-rm -rf /home/opam/opam-repository && \
-rm -rf /home/opam/.opam/repo/default/.git*
-
-# Stage 3 (optional): tests
-
-FROM frama-c AS tests
-
-# Run standard Frama-C tests
-RUN @FRAMAC_TESTS@
-
-# Run an extra test for WP with provers
-# Note: we use ';' instead of '&&' because, for older Frama-C's, such directory
-# does not exist.
-RUN cd /frama-c/ && cd src/plugins/wp/tests/; @WP_TEST@
-
-
-# Stage 4 (optional): GUI
-
-FROM frama-c AS frama-c-gui
-
-RUN sudo apk add adwaita-icon-theme font-noto gdk-pixbuf @GUI_ALPINE_DEPS@
-RUN opam depext -y --install @GUI_OPAM_DEPS@
-RUN cd /frama-c && @GUI_REMAKE@
-
-# Stage 5 (to be deployed): 'slim' image
-
-FROM @ALPINE_BASE@ AS frama-c-slim
-
-RUN adduser --disabled-password --gecos '' opam
-
-COPY --from=frama-c /bin /bin/
-COPY --from=frama-c /etc /etc/
-COPY --from=frama-c /lib /lib/
-COPY --from=frama-c /sbin /sbin/
-# RUN true cmds are a workaround against
-# obscure docker bug (https://github.com/moby/moby/issues/37965)
-# manifesting in sequences of COPY
-RUN true
-COPY --from=frama-c /usr /usr/
-RUN true
-COPY --from=frama-c --chown=opam:opam /home/opam/.opam /home/opam/.opam/
-COPY --from=frama-c /home/opam/.profile /home/opam/
-
-RUN apk add sudo
-USER opam
-WORKDIR /home/opam
-@ENV@
-
-RUN @WHY3_CONFIG@
-
-# Stage 6 (optional, to be deployed): 'slim' image with frama-c-gui
-
-FROM @ALPINE_BASE@ AS frama-c-gui-slim
-
-RUN adduser --disabled-password --gecos '' opam
-
-COPY --from=frama-c-gui /bin /bin/
-COPY --from=frama-c-gui /etc /etc/
-COPY --from=frama-c-gui /lib /lib/
-COPY --from=frama-c-gui /sbin /sbin/
-RUN true
-COPY --from=frama-c-gui /usr /usr/
-RUN true
-COPY --from=frama-c-gui --chown=opam:opam /home/opam/.opam /home/opam/.opam/
-COPY --from=frama-c-gui /home/opam/.profile /home/opam/
-
-RUN apk add sudo
-USER opam
-WORKDIR /home/opam
-@ENV@
-
-RUN @WHY3_CONFIG@
-
-# sanity check
-RUN which frama-c-gui
-
-# Stage 7: preparation of 'stripped' image (~200 MB compressed)
-# Note: this image only contains the Frama-C binaries and files closely
-# related to it; most other OCaml tools have been removed.
-# Even recompilation of Frama-C is not guaranteed to work.
-
-FROM frama-c-slim AS frama-c-stripped-prepare
-
-@ENV@
-
-# Remove all non-essential ocaml binaries
-RUN \
-mkdir -p /home/opam/.opam/minimal/bin && \
-(cd /home/opam/.opam/*/bin && \
- cp -P $(ls -d frama-c frama-c-config frama-c-gui frama-c-script e-acsl-gcc.sh alt-ergo ocaml ocamlc ocamlc.opt ocamlfind ocamlopt ocamlopt.opt why3 2>/dev/null) /home/opam/.opam/minimal/bin/) && \
-rm -rf /home/opam/.opam/@OCAMLV@/bin && \
-mv /home/opam/.opam/minimal/bin /home/opam/.opam/@OCAMLV@/bin/
-
-# Remove non-essential opam files
-RUN rm -rf /home/opam/.opam/repo/default/packages
-RUN rm -rf /home/opam/.opam/download-cache
-RUN rm -rf /home/opam/.opam/repo/state.cache
-
-# Further stripping: remove non-essential files from tools used by Frama-C
-# (Apron, Alt-Ergo, large OCaml compiler files, etc)
-RUN rm -f /home/opam/.opam/@OCAMLV@/share/apron/lib/*.a
-RUN rm -f /home/opam/.opam/@OCAMLV@/share/apron/lib/*_debug.so
-RUN rm -rf /home/opam/.opam/@OCAMLV@/share/apron/bin
-RUN rm -rf /home/opam/.opam/@OCAMLV@/share/apron/include
-RUN rm -rf /home/opam/.opam/@OCAMLV@/lib/alt-ergo
-RUN rm -rf /home/opam/.opam/@OCAMLV@/lib/lablgtk2
-RUN rm -rf /home/opam/.opam/@OCAMLV@/lib/ppx_tools
-RUN rm -rf /home/opam/.opam/@OCAMLV@/lib/psmt2-frontend
-RUN rm -rf /home/opam/.opam/*/lib/ocaml/expunge
-RUN rm -rf /home/opam/.opam/*/lib/ocaml-migrate-parsetree
-RUN (cd /home/opam/.opam/@OCAMLV@/lib/why3/commands && mv why3config config && rm -f why3* && mv config why3config) || true
-
-# Remove all non-essential OCaml files (everything else other than
-# *.cmxs, *.cmx and *.cmi)
-RUN find /home/opam/.opam \( -name "*.cmt*" -o -name "*.[ao]" -o -name "*.cm[ao]" -o -name "*.cmxa" \) -exec rm {} \;
-
-# Remove non-essential installed files
-RUN sudo rm -f /usr/bin/opam-2.*
-RUN sudo rm -f /usr/local/bin/frama-c.byte
-RUN sudo find /usr/local/lib/frama-c \( -name "*.[ao]" -o -name "*.cm[ao]" -o -name "*.cmxa" \) -exec rm {} \; || true
-RUN cd /usr/share && sudo rm -rf gtk-2.0 X11 xml/docbook
-
-# Remove non-essential apk libraries
-RUN sudo apk del libxcb libx11-dev graphviz pango cairo gtk+2.0-dev gtksourceview2-dev pango-dev
-
-# Stage 7 (optional): stripped, slimmest image (running Frama-C works,
-# but almost everything else does not (e.g. recompiling OCaml modules))
-
-FROM @ALPINE_BASE@ AS frama-c-stripped
-
-RUN adduser --disabled-password --gecos '' opam
-
-COPY --from=frama-c-stripped-prepare /bin /bin/
-COPY --from=frama-c-stripped-prepare /etc /etc/
-COPY --from=frama-c-stripped-prepare /lib /lib/
-COPY --from=frama-c-stripped-prepare /sbin /sbin/
-RUN true
-COPY --from=frama-c-stripped-prepare /usr /usr/
-RUN true
-COPY --from=frama-c-stripped-prepare --chown=opam:opam /home/opam/.opam /home/opam/.opam/
-COPY --from=frama-c-stripped-prepare /home/opam/.profile /home/opam/
-
-RUN apk add sudo
-USER opam
-WORKDIR /home/opam
-@ENV@
-
-RUN @WHY3_CONFIG@
-
-# Re-run quick sanity checks
-RUN \
-printf "int g;\n//@assigns g;\nvoid f(){g = 1;}\nint main() {f(); return g;}" > /tmp/simple.c && \
-frama-c -val @WP_REPORT@ /tmp/simple.c && \
-rm -f /tmp/simple.c
diff --git a/dev/docker/Makefile b/dev/docker/Makefile
index e3dc256c932dd9c520bee84b5999ac0d8bec5eb3..1830aa7ae72fef3f3637bac5e9248e817b1ffa58 100644
--- a/dev/docker/Makefile
+++ b/dev/docker/Makefile
@@ -20,1069 +20,79 @@
# #
##########################################################################
-.PHONY: *-stripped *-gui push-*
+.ONESHELL:
+.PHONY: dev* custom* help push
help:
- @echo "Targets: $(TARGETS)"
-
-##########################
-# LIST OF VARIABLES IN TEMPLATE FILES, TO BE REPLACED VIA SED
-# @ALPINE_BASE@
-# @ALPINE_OPAM_BASE@
-# @CONFIGURE@
-# @CVC4@
-# @CVC4_VERSION@
-# @ENV@
-# @FRAMAC_TESTS@
-# @GUI_ALPINE_DEPS@
-# @GUI_OPAM_DEPS@
-# @GUI_REMAKE@
-# @MAKE_MAKE_INSTALL@
-# @OCAMLV@
-# @OPAM_CACHE_FIX@
-# @OPAM_DEPS@
-# @OPAM_SWITCH@
-# @PATCH_FRAMAC@
-# @TEST_FLAGS@
-# @WHY3_CONFIG@
-# @WP_PROVERS@
-# @WP_REPORT@
-# @WP_TEST@
-# @Z3@
-
-
-## TEST_FLAGS:
-## PTESTS_OPTS=-error-code : if all tests pass
-## (nothing) : if tests compile, but fail
-## || true : if tests fail to compile
-
-push-dev: dev dev-gui dev-stripped
- docker push framac/frama-c:dev
- docker push framac/frama-c-gui:dev
- docker push framac/frama-c:dev-stripped
-
-dev: Dockerfile.dev
- @echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
- @echo "Docker to rebuild all layers."
- docker build . -t framac/frama-c:dev --target frama-c-slim -f $^ $(ARGS)
-
-dev-gui: Dockerfile.dev
- @echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
- @echo "Docker to rebuild all layers."
- docker build . -t framac/frama-c-gui:dev --target frama-c-gui-slim -f $^ $(ARGS)
-TARGETS += dev-gui
-
-dev-stripped: Dockerfile.dev
- @echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
- @echo "Docker to rebuild all layers."
- docker build . -t framac/frama-c:dev-stripped --target frama-c-stripped -f $^ $(ARGS)
-TARGETS += dev-stripped
-
-release: Dockerfile.dev Dockerfile.template
- @export archive="frama-c-$$(cat ../../VERSION)-$$(cat ../../VERSION_CODENAME).tar.gz"; \
- if [ ! -e "$$archive" ]; then \
- echo "error: $$archive not found; run 'make src-distrib' and put the .tar.gz in this directory."; \
- exit 1; \
- fi; \
- docker build . -t framac/frama-c:release --target frama-c-slim --build-arg=from_archive="$$archive" -f $<
- @echo "Now run: 'docker tag framac/frama-c:release framac/frama-c:<version>'"
-TARGETS += release
-
-release-gui: Dockerfile.dev
- @echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
- @echo "Docker to rebuild all layers."
- docker build . -t framac/frama-c-gui:release --target frama-c-gui-slim -f $^ $(ARGS)
- @echo "Now run: 'docker tag framac/frama-c-gui:release framac/frama-c-gui:<version>'"
-TARGETS += release-gui
-
-release-stripped: Dockerfile.dev
- @echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
- @echo "Docker to rebuild all layers."
- docker build . -t framac/frama-c:release-stripped --target frama-c-stripped -f $^ $(ARGS)
- @echo "Now run: 'docker tag framac/frama-c:release-stripped framac/frama-c:<version>-stripped'"
-TARGETS += release-stripped
-
-# Note: alpine-3.14 has Z3 version 4.8.11, which is not supported in some
-# versions of Why3, so we remain with alpine-3.13 for now.
-Dockerfile.dev: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.7|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|opam repository set-url default https://opam.ocaml.org \&\&|g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.2.2.0 \\\
-apron.v0.9.12 \\\
-conf-graphviz.0.1 \\\
-dune.3.3.1 \\\
-dune-site.3.3.1 \\\
-mlmpfr.4.1.0-bugfix2 \\\
-ocamlfind.1.8.1 \\\
-ocamlgraph.1.8.8 \\\
-ppx_deriving_yojson.3.6.1 \\\
-ppx_import.1.9.0 \\\
-why3.1.5.1 \\\
-yojson.1.7.0 \\\
-zarith.1.10 \\\
-zmq.5.1.3 \\\
-conf-python-3.1.0.0 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|./dev/disable-plugins.sh gui \&\& make clean|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make \&\& make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@||g' | \
-sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g' | \
-sed 's|@GUI_REMAKE@|./dev/disable-plugins.sh none \&\& make clean \&\& make \&\& make install|g' | \
-sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make run-ptests \&\& dune build @ptests_config|g' | \
-sed 's|@OCAMLV@|4.08|g' | \
-cat > $@
-
-25.0-stripped: Dockerfile.25.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-25.0-Manganese.tar.gz $(ARGS)
-TARGETS += 25.0-stripped
-
-25.0: Dockerfile.25.0
- docker build . -t framac/frama-c:$@ --target frama-c-slim -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-25.0-Manganese.tar.gz $(ARGS)
-TARGETS += 25.0
-
-25.0-gui: Dockerfile.25.0
- docker build . -t framac/frama-c-gui:25.0 --target frama-c-gui-slim -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-25.0-Manganese.tar.gz $(ARGS)
-TARGETS += 25.0-gui
-
-push-25.0: 25.0 25.0-gui 25.0-stripped
- docker push framac/frama-c:25.0
- docker push framac/frama-c-gui:25.0
- docker push framac/frama-c:25.0-stripped
-
-Dockerfile.25.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.7|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|opam repository set-url default https://opam.ocaml.org \&\&|g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.2.2.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.6.1 \\\
-ppx_import.1.9.0 \\\
-why3.1.5.0 \\\
-yojson.1.7.0 \\\
-zarith.1.10 \\\
-zmq.5.1.3 \\\
-conf-python-3.1.0.0 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@||g' | \
-sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g' | \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests PTESTS_OPTS=-error-code|g' | \
-sed 's|@OCAMLV@|4.08|g' | \
-cat > $@
-
-24.0-stripped: Dockerfile.24.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-24.0-Chromium.tar.gz $(ARGS)
-TARGETS += 24.0-stripped
-
-24.0: Dockerfile.24.0
- docker build . -t framac/frama-c:$@ --target frama-c-slim -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-24.0-Chromium.tar.gz $(ARGS)
-TARGETS += 24.0
-
-24.0-gui: Dockerfile.24.0
- docker build . -t framac/frama-c-gui:24.0 --target frama-c-gui-slim -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-24.0-Chromium.tar.gz $(ARGS)
-TARGETS += 24.0-gui
-
-push-24.0: 24.0 24.0-gui 24.0-stripped
- docker push framac/frama-c:24.0
- docker push framac/frama-c-gui:24.0
- docker push framac/frama-c:24.0-stripped
-
-# Note: alpine-3.14 has Z3 version 4.8.11, which is not supported in some
-# versions of Why3, so we remain with alpine-3.13 for now.
-Dockerfile.24.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.7|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|opam repository set-url default https://opam.ocaml.org \&\&|g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.2.2.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.4.0 \\\
-yojson.1.7.0 \\\
-zarith.1.9.1 \\\
-zmq.5.1.3 \\\
-conf-python-3.1.0.0 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@||g' | \
-sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g' | \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests PTESTS_OPTS=-error-code|g' | \
-sed 's|@OCAMLV@|4.08|g' | \
-cat > $@
-
-23.1-stripped: Dockerfile.23.1
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.1-Vanadium.tar.gz $(ARGS)
-TARGETS += 23.1-stripped
-
-23.1: Dockerfile.23.1
- docker build . -t framac/frama-c:$@ --target frama-c-slim -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.1-Vanadium.tar.gz $(ARGS)
-TARGETS += 23.1
-
-23.1-gui: Dockerfile.23.1
- docker build . -t framac/frama-c-gui:23.1 --target frama-c-gui-slim -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.1-Vanadium.tar.gz $(ARGS)
-TARGETS += 23.1-gui
-
-push-23.1: 23.1 23.1-gui 23.1-stripped
- docker push framac/frama-c:23.1
- docker push framac/frama-c-gui:23.1
- docker push framac/frama-c:23.1-stripped
-
-Dockerfile.23.1: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.7|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@||g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.2.2.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.4.0 \\\
-yojson.1.7.0 \\\
-zarith.1.9.1 \\\
-zmq.5.1.3 \\\
-conf-python-3.1.0.0 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@||g'| \
-sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests|g' | \
-sed 's|@OCAMLV@|4.08|g' | \
-cat > $@
-
-23.0-stripped: Dockerfile.23.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.0-Vanadium.tar.gz $(ARGS)
-TARGETS += 23.0-stripped
-
-23.0: Dockerfile.23.0
- docker build . -t framac/frama-c:$@ --target frama-c-slim -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.0-Vanadium.tar.gz $(ARGS)
-TARGETS += 23.0
-
-23.0-gui: Dockerfile.23.0
- docker build . -t framac/frama-c-gui:23.0 --target frama-c-gui-slim -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.0-Vanadium.tar.gz $(ARGS)
-TARGETS += 23.0-gui
-
-push-23.0: 23.0 23.0-gui 23.0-stripped
- docker push framac/frama-c:23.0
- docker push framac/frama-c-gui:23.0
- docker push framac/frama-c:23.0-stripped
-
-Dockerfile.23.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.7|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@||g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.2.2.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.4.0 \\\
-yojson.1.7.0 \\\
-zarith.1.9.1 \\\
-zmq.5.1.3 \\\
-conf-python-3.1.0.0 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@||g'| \
-sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests|g' | \
-sed 's|@OCAMLV@|4.08|g' | \
-cat > $@
-
-22.0-stripped: Dockerfile.22.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-22.0-Titanium.tar.gz $(ARGS)
-TARGETS += 22.0-stripped
-
-Dockerfile.22.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.7|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@||g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.2.2.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.3 \\\
-yojson.1.7.0 \\\
-zarith.1.9.1 \\\
-zmq.5.1.3 \\\
-conf-python-3.1.0.0 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@||g'| \
-sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests|g' | \
-sed 's|@OCAMLV@|4.08|g' | \
-cat > $@
-
-21.1-stripped: Dockerfile.21.1
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-21.1-Scandium.tar.gz $(ARGS)
-TARGETS += 21.1-stripped
-
-Dockerfile.21.1: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.07|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.7|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@||g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-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 \\\
-conf-python-3.1.0.0 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --full-config|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@||g'| \
-sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests|g' | \
-sed 's|@OCAMLV@|4.07|g' | \
-cat > $@
-
-# Note: Frama-C 20.0 and older do not work with GCC >= 10 due to issue with
-# handling of Unicode characters
-20.0-stripped: Dockerfile.20.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-20.0-Calcium.tar.gz $(ARGS)
-TARGETS += 20.0-stripped
-
-# Note: cairo2.0.6.1 is used for the GUI because the 0.6.2 requires 'dune-configurator'
-Dockerfile.20.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.6|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.2.0.0 \\\
-apron.20160125 \\\
-conf-graphviz.0.1 \\\
-mlgmpidl.1.2.11 \\\
-ocamlfind.1.8.0 \\\
-ocamlgraph.1.8.8 \\\
-ppx_deriving_yojson.3.5.2 \\\
-why3.1.2.0 \\\
-yojson.1.7.0 \\\
-zarith.1.9.1 \\\
-zmq.5.1.3 \\\
-conf-python-3.1.0.0 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@||g'| \
-sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests \|\| true |g' | \
-sed 's|@OCAMLV@|4.05|g' | \
-cat > $@
-
-19.1-stripped: Dockerfile.19.1
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-19.1-Potassium.tar.gz $(ARGS)
-TARGETS += 19.1-stripped
-
-Dockerfile.19.1: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.6|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo-free.2.0.0 \\\
-apron.20160125 \\\
-conf-graphviz.0.1 \\\
-mlgmpidl.1.2.9 \\\
-ocamlfind.1.8.0 \\\
-ocamlgraph.1.8.8 \\\
-ppx_deriving_yojson.3.5.2 \\\
-why3.1.2.0 \\\
-yojson.1.7.0 \\\
-zarith.1.7 \\\
-conf-python-3.1.0.0 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@||g'| \
-sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|4.05|g' | \
-cat > $@
-
-18.0-stripped: Dockerfile.18.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-18.0-Argon.tar.gz $(ARGS)
-TARGETS += 18.0-stripped
-
-Dockerfile.18.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.30 \\\
-apron.20160125 \\\
-conf-graphviz.0.1 \\\
-mlgmpidl.1.2.7 \\\
-ocamlfind.1.8.0 \\\
-ocamlgraph.1.8.8 \\\
-why3.0.88.3 \\\
-yojson.1.7.0 \\\
-zarith.1.7 \\\
-conf-python-3.1.0.0 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|4.05|g' | \
-cat > $@
-
-17.1-stripped: Dockerfile.17.1
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Chlorine-20180502.tar.gz $(ARGS)
-TARGETS += 17.1-stripped
-
-# frama-c-script is not shipped from here on, so no need for conf-python
-Dockerfile.17.1: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.30 \\\
-apron.20160125 \\\
-conf-graphviz.0.1 \\\
-mlgmpidl.1.2.7 \\\
-ocamlfind.1.8.0 \\\
-ocamlgraph.1.8.8 \\\
-why3.0.88.3 \\\
-yojson.1.7.0 \\\
-zarith.1.7 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|4.05|g' | \
-cat > $@
-
-16.0-stripped: Dockerfile.16.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Sulfur-20171101.tar.gz $(ARGS)
-TARGETS += 16.0-stripped
-
-# yojson is no longer marked in the opam depends from here on
-Dockerfile.16.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.30 \\\
-apron.20160125 \\\
-conf-graphviz.0.1 \\\
-mlgmpidl.1.2.7 \\\
-ocamlfind.1.8.0 \\\
-ocamlgraph.1.8.8 \\\
-why3.0.88.3 \\\
-zarith.1.7 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|4.05|g' | \
-cat > $@
-
-15.0-stripped: Dockerfile.15.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Phosphorus-20170501.tar.gz $(ARGS)
-TARGETS += 15.0-stripped
-
-Dockerfile.15.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.30 \\\
-apron.20160125 \\\
-conf-graphviz.0.1 \\\
-mlgmpidl.1.2.7 \\\
-ocamlfind.1.8.0 \\\
-ocamlgraph.1.8.8 \\\
-why3.0.88.3 \\\
-zarith.1.7 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|4.02|g' | \
-cat > $@
-
-14.0-stripped: Dockerfile.14.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Silicon-20161101.tar.gz $(ARGS)
-TARGETS += 14.0-stripped
-
-Dockerfile.14.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.30 \\\
-apron.20160125 \\\
-conf-graphviz.0.1 \\\
-mlgmpidl.1.2.7 \\\
-ocamlfind.1.8.0 \\\
-ocamlgraph.1.8.8 \\\
-why3.0.88.3 \\\
-zarith.1.7 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's#@WP_TEST@#! ( frama-c -wp wp_usage/reads.i -wp-timeout 1 -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" )#g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|4.02|g' | \
-cat > $@
-
-13.0-stripped: Dockerfile.13.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Aluminium-20160502.tar.gz $(ARGS)
-TARGETS += 13.0-stripped
-
-Dockerfile.13.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.30 \\\
-apron.20160125 \\\
-conf-graphviz.0.1 \\\
-mlgmpidl.1.2.7 \\\
-ocamlfind.1.8.0 \\\
-ocamlgraph.1.8.8 \\\
-why3.0.88.3 \\\
-zarith.1.7 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's#@WP_TEST@#! ( frama-c -wp wp_usage/reads.i -wp-timeout 1 -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" )#g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|4.02|g' | \
-cat > $@
-
-12.0-stripped: Dockerfile.12.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Magnesium-20151002.tar.gz $(ARGS)
-TARGETS += 12.0-stripped
-
-# apron is not shipped with Frama-C, from here on
-Dockerfile.12.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.30 \\\
-conf-graphviz.0.1 \\\
-ocamlfind.1.8.0 \\\
-ocamlgraph.1.8.8 \\\
-why3.0.88.3 \\\
-zarith.1.7 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's#@WP_TEST@#! ( frama-c -wp wp_usage/reads.i -wp-timeout 1 -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" )#g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|4.02|g' | \
-cat > $@
-
-11.0-stripped: Dockerfile.11.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Sodium-20150201.tar.gz $(ARGS)
-TARGETS += 11.0-stripped
-
-Dockerfile.11.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.30 \\\
-conf-graphviz.0.1 \\\
-ocamlfind.1.8.0 \\\
-ocamlgraph.1.8.8 \\\
-why3.0.88.3 \\\
-zarith.1.7 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|true|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|4.02|g' | \
-cat > $@
-
-10.1-stripped: Dockerfile.10.1
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Neon-20140301.tar.gz $(ARGS)
-TARGETS += 10.1-stripped
-
-# Starting from this version, due to the usage of a recent GCC, we need to
-# remove the `-no-pic` flag that was passed when compiling buckx_c.c.
-# Otherwise, we get the dreaded "relocation error".
-Dockerfile.10.1: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.30 \\\
-conf-graphviz.0.1 \\\
-ocamlfind.1.8.0 \\\
-why3-base.0.88.3 \\\
-zarith.1.7 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|4.02|g' | \
- cat > $@
-
-10.0-stripped: Dockerfile.10.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Neon-20140301.tar.gz $(ARGS)
-TARGETS += 10.0-stripped
-
-# Starting from this version, due to the usage of a recent GCC, we need to
-# remove the `-no-pic` flag that was passed when compiling buckx_c.c.
-# Otherwise, we get the dreaded "relocation error".
-Dockerfile.10.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|true|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.30 \\\
-conf-graphviz.0.1 \\\
-ocamlfind.1.8.0 \\\
-why3-base.0.88.3 \\\
-zarith.1.7 \\\
-conf-time.1|' | \
-sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|4.02|g' | \
-cat > $@
-
-9.2-stripped: Dockerfile.9.2
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Fluorine-20130601.tar.gz $(ARGS)
-TARGETS += 9.2-stripped
-
-# configure.in had a bug detecting Make versions > 4; instead of applying
-# the proper fix (which would be long), we simply "cheat" by replacing '81'
-# (from "make 3.81") with "1".
-Dockerfile.9.2: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.01 \\\
-conf-autoconf.0.1 \\\
-conf-graphviz.0.1 \\\
-ocamlfind.1.7.3-1 \\\
-why3-base.0.85 \\\
-zarith.1.7|' | \
-sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/ 1/" configure.in|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|3.12.1|g' | \
-cat > $@
-
-8.0-stripped: Dockerfile.8.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Oxygen-20120901.tar.gz $(ARGS)
-TARGETS += 8.0-stripped
-
-Dockerfile.8.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.01 \\\
-conf-autoconf.0.1 \\\
-conf-graphviz.0.1 \\\
-ocamlfind.1.7.3-1 \\\
-why3-base.0.85 \\\
-zarith.1.7|' | \
-sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/ 1/" configure.in|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|3.12.1|g' | \
-cat > $@
-
-7.0-stripped: Dockerfile.7.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Nitrogen-20111001.tar.gz $(ARGS)
-TARGETS += 7.0-stripped
-
-# For some reason, lablgtk2 files are installed in a directory other than the
-# one where Frama-C's configure expects them; the simplest fix seems to be
-# moving the files to the expected directory.
-Dockerfile.7.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
-sed 's|@CVC4_VERSION@|1.5|g' | \
-sed 's|@Z3@|$(shell cat z3.template)|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
-sed 's|@OPAM_DEPS@|\\\
-alt-ergo.1.01 \\\
-conf-autoconf.0.1 \\\
-conf-graphviz.0.1 \\\
-ocamlfind.1.7.3-1 \\\
-why3-base.0.85 \\\
-zarith.1.7|' | \
-sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/ 1/" configure.in|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@|-wp -report|g'| \
-sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview \&\& mv /home/opam/.opam/3.12.1/lib/lablgtk2/ /home/opam/.opam/3.12.1/lib/ocaml/|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|3.12.1|g' | \
-cat > $@
-
-6.0-stripped: Dockerfile.6.0
- docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
---build-arg=from_archive=https://www.frama-c.com/download/frama-c-Carbon-20110201.tar.gz $(ARGS)
-TARGETS += 6.0-stripped
-
-# TODO: find out how to make WP installation work; following the instructions, the
-# dynamic version fails during ./configure, with:
-# ./configure: export: line 1666: ENABLE_USAGE:_FRAMA_C_[OPTIONS_AND_FILES...]: bad variable name
-# And the static version (putting in src/wp) fails with:
-# src/wp/Makefile:46: *** recipe commences before first target. Stop.
-Dockerfile.6.0: Makefile Dockerfile.template env.template
- sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
-sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-sed 's|@ENV@|$(shell cat env.template)|g' | \
-sed 's|@CVC4@||g' | \
-sed 's|@CVC4_VERSION@||g' | \
-sed 's|@Z3@||g' | \
-sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
-sed 's|@OPAM_DEPS@|\\\
-conf-autoconf.0.1 \\\
-conf-graphviz.0.1 \\\
-ocamlfind.1.7.3-1|' | \
-sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/ 1/" configure.in|g' | \
-sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-sed 's|@WP_REPORT@||g'| \
-sed 's|@WHY3_CONFIG@|true|g' | \
-sed 's#@WP_TEST@#true#g' | \
-sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview \&\& mv /home/opam/.opam/3.12.1/lib/lablgtk2/ /home/opam/.opam/3.12.1/lib/ocaml/|g'| \
-sed 's|@GUI_REMAKE@|make clean \&\& autoconf \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-sed 's|@OCAMLV@|3.12.1|g' | \
-cat > $@
-
-#5.0-stripped: Dockerfile.5.0
-# docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
-#--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Boron-20100401-why-2.24.tar.gz $(ARGS)
-#TARGETS += 5.0-stripped
-#
-# Re-running the makefile for the GUI seems to cause issues,
-# so we restart everything from the archive
-# TODO: fix build and proceed with older Frama-C versions
-# Dockerfile.5.0: Makefile Dockerfile.template env.template
-# sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
-# sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
-# sed 's|@ENV@|$(shell cat env.template)|g' | \
-# sed 's|@CVC4@||g' | \
-# sed 's|@CVC4_VERSION@||g' | \
-# sed 's|@Z3@||g' | \
-# sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
-# sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
-# sed 's|@OPAM_DEPS@|\\\
-# conf-autoconf.0.1 \\\
-# conf-graphviz.0.1 \\\
-# ocamlfind.1.7.3-1 \\\
-# zarith.1.7|' | \
-# sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/ 1/" configure.in|g' | \
-# sed 's|@CONFIGURE@|autoconf \&\& ./configure --disable-gui|g' | \
-# sed 's|@MAKE_MAKE_INSTALL@|make -j \&\& sudo make install|g' | \
-# sed 's|@WP_REPORT@||g'| \
-# sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
-# sed 's#@WP_TEST@#true#g' | \
-# sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
-# sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview \&\& mv /home/opam/.opam/3.12.1/lib/lablgtk2/ /home/opam/.opam/3.12.1/lib/ocaml/|g'| \
-# sed 's|@GUI_REMAKE@|rm -rf * \&\& wget https://www.frama-c.com/download/frama-c-Boron-20100401-why-2.24.tar.gz \&\& tar xvf frama-c-Boron-20100401-why-2.24.tar.gz --strip 1 \&\& cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/ 1/" configure.in \&\& autoconf \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
-# sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
-# sed 's|@OCAMLV@|3.12.1|g' | \
-# cat > $@
+ @echo "Available targets are:"
+ echo "- dev.*: public Git development version (no gui)"
+ echo "- dev-gui.*: public Git development version (with gui)"
+ echo "- dev-stripped.*: public Git development version with minimal size (no gui)"
+ echo "- custom.*: version based on a frama-c-*.tar.gz archive (no gui)"
+ echo "- custom-gui.*: same as previous, but with gui"
+ echo "- custom-stripped.*: same as previous, but with minimal size (no gui)"
+ echo ""
+ echo "For each target, the suffix (.*) denotes the Docker base image:"
+ echo "- debian: based on debian:bullseye-slim"
+ echo " (default image in the Frama-C Docker Hub)"
+ echo "- fedora: based on fedora:36"
+ echo "- alpine: based on alpine:3.16"
+ echo " (smallest image, but E-ACSL does not work due to musl)"
+ echo
+ echo "Targets for users with write access to the framac Docker Hub:"
+ echo "- push TAG=<tag1> AS=<tag2>: perform a docker push with image"
+ echo " <tag1> sent as <tag2>. Usage example:"
+ echo " make push TAG=framac/frama-c:dev.debian AS=framac/frama-c:dev"
+
+DEPS=../../reference-configuration.md Dockerfile *.sh
+
+version=$(shell grep -o "^- OCaml [0-9.]\+" "../../reference-configuration.md" | grep -o "[0-9.]\+")
+BUILD_ARGS := --build-arg=OCAML_VERSION=$(version)
+
+%.debian: BUILD_ARGS += --build-arg=DISTRO=debian:bullseye-slim
+%.fedora: BUILD_ARGS += --build-arg=DISTRO=fedora:36
+%.alpine: BUILD_ARGS += --build-arg=DISTRO=alpine:3.16
+
+dev.%: $(DEPS)
+ cp ../../reference-configuration.md .
+ docker build . -t framac/frama-c:$@ $(BUILD_ARGS) --target frama-c-slim
+
+dev-gui.%: dev.%
+ docker build . -t framac/frama-c-gui:dev.$* $(BUILD_ARGS) --target frama-c-gui-slim
+
+dev-stripped.%: dev.%
+ docker build . -t framac/frama-c:$@ $(BUILD_ARGS) --target frama-c-stripped
+
+ifeq ($(FRAMAC_ARCHIVE),)
+custom.% custom-gui.% custom-stripped.%:
+ @echo "error: run '$(MAKE) $@ FRAMAC_ARCHIVE=frama-c-<version>.tar.gz',"
+ echo " where frama-c-<version>.tar.gz is the name of the archive."
+ echo "Note: the archive must be in the current directory and be named as"
+ echo " 'frama-c-<version>.tar.gz' (where <version> is at your choice)."
+ exit 1
+else
+BUILD_ARGS += --build-arg=from_archive=$(FRAMAC_ARCHIVE)
+custom.%: $(DEPS)
+ cp ../../reference-configuration.md .
+ docker build . -t frama-c-$@ $(BUILD_ARGS) --target frama-c-slim
+
+custom-gui.%: custom.%
+ docker build . -t frama-c-$@ $(BUILD_ARGS) --target frama-c-gui-slim
+
+custom-stripped.%: custom.%
+ docker build . -t frama-c-$@ $(BUILD_ARGS) --target frama-c-stripped
+endif
+
+# check if either TAG or AS are empty
+ifeq ($(TAG)$(AS),$(AS)$(TAG))
+push:
+ @echo "error: run '$(MAKE) $@ TAG=<orig> AS=<new>'"
+ echo " where <tag> is the current tag of the image to be pushed,"
+ echo " and <new> is the name used in the Docker Hub"
+ echo " e.g. framac/frama-c:dev, framac/frama-c-gui:dev, etc."
+ echo "(if you supplied identical tags, just run 'docker push $(TAG)')"
+else
+push:
+ docker tag $(TAG) $(AS)
+ docker push $(AS)
+endif
diff --git a/dev/docker/README.md b/dev/docker/README.md
index 71afa6d50e761de9111ecd8dc91d26939207a255..0b93e4b3d5eebec1d4e76e9afcf0535b5361d6a8 100644
--- a/dev/docker/README.md
+++ b/dev/docker/README.md
@@ -1,63 +1,54 @@
# Frama-C Docker images
-Frama-C Docker images are currently based on Alpine Linux,
-using opam's Docker images
-(from https://hub.docker.com/r/ocaml/opam/).
+Frama-C Docker images are currently based on Alpine Linux.
The user is `opam` and it has sudo rights.
-To add packages, run `sudo apk add <package>`.
-## Using the Makefile
+To add Alpine packages, run `sudo apk add <package>`.
-The `Makefile` contains several targets and templates to build most
-Frama-C versions. For each version, there are three images: one
-for the command-line version `frama-c`; a stripped-down version of the former,
-for a slimmer image, but which does not allow recompilation of Frama-C
-or of any external plugin; and a third image including the graphical
-interface (`frama-c-gui`), to be used with Singularity, x11docker, or any other
-tool which enables running a graphical application from a Docker image.
+An OCaml switch is set up with the packages mentioned in
+`reference-configuration.md`, plus a few external SMT solvers
+(CVC4, Z3).
-Run `make` to get a list of targets.
+There are 2 main images, each with 3 variants:
-If you have access to the Frama-C Docker Hub, you can also run a
-`push-<version>` target to upload images related to that version to
-the Docker Hub.
+- `dev` image: based on the public Frama-C git repository;
+- `custom` image: based on a custom .tar.gz archive put in this directory.
+ Note: it _must_ be named `frama-c-<something>.tar.gz`, where
+ `<something>` may be a version number, codename, etc.
+ It _must_ be put in this directory.
-## Commands to generate images
+Each of these is declined in 3 variants:
-Some commands in this section are those used by the above Makefile;
-others allow creating different images (e.g. with the Frama-C sources)
-which are not directly available as Makefile targets.
+- standard (no suffix): an image with the command line `frama-c` version,
+ without GUI;
+- `-gui`: the standard image + `frama-c-gui`. To be used with Singularity,
+ x11docker, or any other tool which enables running a graphical application
+ from a Docker image.
+- `-stripped`: the standard image reduced to a minimal set of files, for
+ smaller size. Note: this image has several files removed, rendering some
+ non-essential components unusable.
-Note: a Dockerfile is needed for the commands below.
- For most versions, running `make Dockerfile.dev` and then using it
- (adding `-f Dockerfile.dev` to the commands below) is enough.
- However, if specific build commands or dependencies are needed,
- you can copy the generated Dockerfile
- (e.g. `cp Dockerfile.dev Dockerfile`) and adapt it as needed,
- before running one of the commands below.
+Note that only _some_ usages of Frama-C have been tested; notify us if your
+intended plug-in or usage scenario does not work (and is not listed in the
+*Known issues* below).
-- Build slim development image (from public Git master branch):
+## Known issues
- docker build . -t framac/frama-c:dev --target frama-c-slim
+- E-ACSL does not currently work in these images: its `musl` libc does not
+ contain some debugging information required by E-ACSL.
+- The `-stripped` variants no longer have a working OCaml compiler;
+ loading some modules or compiling plug-ins may not work.
-- Build slim development image with GUI:
+## Built images
- docker build . -t framac/frama-c-gui:dev --target frama-c-gui-slim
+The `dev`: images are tagged with their default names in the Docker Hub:
+`framac/frama-c:dev`, `framac/frama-c-gui:dev`, `framac/frama-c:dev-stripped`.
-- Build stripped (minimal) version:
+The `custom` images are tagged with prefix `frama-c-custom`, since they are
+intended for local usage.
- docker build . -t framac/frama-c:dev-stripped --target frama-c-stripped
-
-- Build image from archive (note: it _must_ be named `frama-c-<something>.tar.gz`, where
- `<something>` may be a version number, codename, etc:
-
- docker build . -t framac/frama-c:dev --target frama-c-slim --build-arg=from_archive=frama-c-<version>.tar.gz
-
-- Build image containing Frama-C's source code in `/frama-c` (without and with GUI):
-
- docker build . -t framac/frama-c-source:dev --target frama-c
- docker build . -t framac/frama-c-gui-source:dev --target frama-c-gui
+## Helpful commands
- Start Singularity instance
diff --git a/dev/docker/add-user.sh b/dev/docker/add-user.sh
new file mode 100755
index 0000000000000000000000000000000000000000..410a22ba62c4b8ebdbe89c10a5c45249b10f742e
--- /dev/null
+++ b/dev/docker/add-user.sh
@@ -0,0 +1,41 @@
+#!/bin/bash -eu
+
+# Create user, add to wheel, allow sudo, avoid sudo lecture
+
+if [ $# -lt 1 ]; then
+ echo "usage: $0 user"
+ exit 2
+fi
+
+NEWUSER=$1
+if [ -e /etc/debian_version ]; then
+ # Debian
+ apt-get update -y
+ apt-get install -y sudo passwd
+ yes "y" | adduser $NEWUSER
+ usermod -a -G sudo $NEWUSER
+ passwd -d $NEWUSER
+elif [ -e /etc/fedora-release ]; then
+ # Fedora
+ dnf update -y
+ dnf install -y sudo passwd
+ groupadd $NEWUSER
+ yes "" | adduser -g "${NEWUSER}" -G wheel $NEWUSER
+ passwd -d $NEWUSER
+elif [ -e /etc/alpine-release ]; then
+ # Alpine
+ apk update
+ apk add sudo
+ yes "" | adduser -g "${NEWUSER}" $NEWUSER
+ addgroup $NEWUSER wheel
+ passwd -d $NEWUSER
+else
+ echo "error: unsupported Linux distribution"
+ exit 1
+fi
+
+# Add to sudoers and avoid lecture
+echo "$NEWUSER ALL=(ALL) ALL" > /etc/sudoers.d/$NEWUSER
+chmod 0440 /etc/sudoers.d/$NEWUSER
+echo "%wheel ALL=(ALL) NOPASSWD: ALL" > /etc/sudoers.d/wheel
+echo -e '\nDefaults lecture = never' >> /etc/sudoers
diff --git a/dev/docker/cvc4.template b/dev/docker/cvc4.template
deleted file mode 100644
index 951aa4ea617f12db51d78f5387aadab0b4c824d1..0000000000000000000000000000000000000000
--- a/dev/docker/cvc4.template
+++ /dev/null
@@ -1,5 +0,0 @@
-## CVC4 @CVC4_VERSION@\n
-RUN \\\n
-wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-@CVC4_VERSION@-x86_64-linux-opt -O cvc4-@CVC4_VERSION@ \&\& \\\n
-chmod a+x cvc4-@CVC4_VERSION@ \&\& \\\n
-sudo mv cvc4-@CVC4_VERSION@ /usr/local/bin/
diff --git a/dev/docker/env.template b/dev/docker/env.template
deleted file mode 100644
index 14b2666ef03ba5ae6f2ce6f8d718eb9e7b6145b6..0000000000000000000000000000000000000000
--- a/dev/docker/env.template
+++ /dev/null
@@ -1,11 +0,0 @@
-ENV OPAM_SWITCH_PREFIX "/home/opam/.opam/@OCAMLV@"\n
-ENV CAML_LD_LIBRARY_PATH "/home/opam/.opam/@OCAMLV@/lib/stublibs:/home/opam/.opam/@OCAMLV@/lib/ocaml/stublibs:/home/opam/.opam/@OCAMLV@/lib/ocaml"\n
-ENV OCAML_TOPLEVEL_PATH "/home/opam/.opam/@OCAMLV@/lib/toplevel"\n
-ENV MANPATH "$MANPATH:/home/opam/.opam/@OCAMLV@/man"\n
-ENV PATH "/home/opam/.opam/@OCAMLV@/bin:$PATH"\n
-\n
-## Avoid prompts for time zone\n
-ENV TZ=Europe/Paris\n
-\n
-## Fix issue with libGL on Windows\n
-ENV LIBGL_ALWAYS_INDIRECT=1\n
diff --git a/dev/docker/install.sh b/dev/docker/install.sh
new file mode 100755
index 0000000000000000000000000000000000000000..4aa1d638b93076750d4d4f1f00157b8dab52ceec
--- /dev/null
+++ b/dev/docker/install.sh
@@ -0,0 +1,48 @@
+#!/bin/sh -eu
+
+# (Note: this script cannot use bash, since Alpine does not have it by default)
+
+# Download and install packages, using the distribution's package manager
+# Note: package managers usually fail when a package name does not exist,
+# but we want to factorize the code, so we give as many package names as
+# possible (including all variants from all distributions) and hope for
+# the best. Therefore we install one by one and skip in case of failure.
+# If there are actual errors installing them, the Dockerfile will end up
+# failing later anyway (or so we hope).
+
+if [ $# -lt 1 ]; then
+ echo "usage: $0 package1 [package2 ...]"
+ exit 2
+fi
+
+# Use sudo if not root
+if [ $(id -u) -ne 0 ]; then
+ SUDO=sudo
+else
+ SUDO=
+fi
+
+
+# Update package cache once, then iterate over packages
+
+if [ -e /etc/debian_version ]; then
+ # Debian
+ $SUDO apt-get update -y
+ INSTALL="apt-get install -y"
+elif [ -e /etc/fedora-release ]; then
+ # Fedora
+ $SUDO dnf update -y
+ INSTALL="dnf install -y"
+elif [ -e /etc/alpine-release ]; then
+ # Alpine
+ $SUDO apk update
+ INSTALL="apk add"
+else
+ echo "error: unsupported Linux distribution"
+ exit 1
+fi
+
+for name in "$@"
+do
+ $SUDO $INSTALL $name || echo "$name not found, skipping"
+done
diff --git a/dev/docker/opam-init-from-ref-config.sh b/dev/docker/opam-init-from-ref-config.sh
new file mode 100755
index 0000000000000000000000000000000000000000..1b02bdad0e712082dfdd9486b2459b3dadc26510
--- /dev/null
+++ b/dev/docker/opam-init-from-ref-config.sh
@@ -0,0 +1,25 @@
+#!/usr/bin/env bash
+
+# Calls 'opam init' with the OCaml version given as argument
+
+if [ $# -lt 1 ]; then
+ echo "error: missing required version number"
+ exit 1
+fi
+
+if [[ ! $1 =~ ^[0-9] ]]; then
+ echo "error: version must start with a number: $1"
+ exit 1
+fi
+
+echo "Initializing opam repository with version: $1"
+
+opam init --bare --disable-sandboxing --shell-setup
+
+# detect if using musl
+if ldd /bin/ls | grep -q musl; then
+ opam switch create $1 \
+ --packages=ocaml-variants.$1+options,ocaml-option-musl
+else
+ opam switch create $1 $1
+fi
diff --git a/dev/docker/opam-install-fc-deps-from-ref-config.sh b/dev/docker/opam-install-fc-deps-from-ref-config.sh
new file mode 100755
index 0000000000000000000000000000000000000000..2390c46f43c5a76454021e4c1888c022f387228c
--- /dev/null
+++ b/dev/docker/opam-install-fc-deps-from-ref-config.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+# Installs Frama-C's dependencies via opam, from the reference configuration
+
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+
+deps=$(grep '^- ' $SCRIPT_DIR/reference-configuration.md | grep -v "^- OCaml" | sed 's/^- //' | sed 's/(.*)//' | xargs)
+
+opam install $deps --confirm-level=unsafe-yes
diff --git a/dev/docker/z3.template b/dev/docker/z3.template
deleted file mode 100644
index 9c4a430e978af90c8d5dc1b30811ddc6e6336f82..0000000000000000000000000000000000000000
--- a/dev/docker/z3.template
+++ /dev/null
@@ -1,3 +0,0 @@
-## Z3: there is no Github release archive with binaries for Alpine (musl), but\n
-## there is an Alpine package\n
-RUN sudo apk add z3
diff --git a/doc/release/deploy.tex b/doc/release/deploy.tex
index 1a90d5acbc17abf768ff514baec4d25c66c71984..a6fc41606db765acbd3ba965ceab4f7db7335e3e 100644
--- a/doc/release/deploy.tex
+++ b/doc/release/deploy.tex
@@ -159,43 +159,48 @@ Just update the \texttt{VERSION} file in \texttt{master}, by adding \texttt{"+de
\textbf{Note:} you need access to the \texttt{framac} Docker Hub account to be
able to upload the image.
-Make sure that \texttt{devel\_tools/docker/Makefile} is up-to-date:
+Copy the \texttt{.tar.gz} archive to the \texttt{dev/docker} directory.
-\begin{itemize}
-\item changes to \texttt{reference-configuration.md} must have been ported
- to the corresponding \texttt{Dockerfile.dev} entry inside the
- \texttt{Makefile}.
-\end{itemize}
-
-Copy the \texttt{.tar.gz} archive to the \texttt{devel\_tools/docker} directory.
-
-Run \texttt{make release}. It should decompress the archive, build and test
-the Frama-C Docker image.
+Run:
+\begin{lstlisting}
+make FRAMAC_ARCHIVE=<the_archive> custom.debian
+\end{lstlisting}
+It should decompress the archive, build and test the Frama-C Docker image.
If the local tests do not work, check that the OCaml version and package
dependencies are all up-to-date.
-If the image is built succesfully, you can also try building the GUI image
-(\texttt{make release-gui}) and the stripped image
-(\texttt{make release-stripped}).
+If the image is built succesfully, you can also try building the GUI image and
+the stripped image:
+\begin{lstlisting}
+make FRAMAC_ARCHIVE=<the_archive> custom-gui.debian
+make FRAMAC_ARCHIVE=<the_archive> custom-stripped.debian
+\end{lstlisting}
-If you want to upload these images to the Docker Hub, you can re-tag them, e.g.
+If you want to upload these images to the Docker Hub, you can re-tag them and
+upload them, e.g.
\begin{lstlisting}
-docker tag framac/frama-c:release framac/frama-c:<VERSION>
+make -C \
+ TAG="framac/frama-c:custom.debian" \
+ AS="framac/frama-c:<VERSION>" \
+ push
+
+make -C \
+ TAG="framac/frama-c:custom-stripped.debian" \
+ AS="framac/frama-c:<VERSION>-stripped" \
+ push
+
+make -C \
+ TAG="framac/frama-c:custom-gui.debian" \
+ AS="framac/frama-c-gui:<VERSION>" \
+ push
\end{lstlisting}
Where \texttt{<VERSION>} is the release number, possibly with a suffix, but
{\em without} characters such as \texttt{+}. For instance, you can use
\texttt{23.1-beta} for a beta release.
-Then upload the renamed image(s) with:
-
-\begin{lstlisting}
-docker push framac/frama-c:<VERSION>
-docker push framac/frama-c-gui:<VERSION>
-docker push framac/frama-c:<VERSION>-stripped
-\end{lstlisting}
You will need to have setup your \texttt{framac} Docker Hub account for this to work.
%%% Local Variables:
diff --git a/doc/release/validation.tex b/doc/release/validation.tex
index 89b21b4ba58e9e1991ae64afce01283dca5c8709..a67ecd661261e239546f109e03d0b561dbd0b77e 100644
--- a/doc/release/validation.tex
+++ b/doc/release/validation.tex
@@ -33,16 +33,24 @@ The tasks listed in this section are performed by the Release Manager.
\subsection{Versions in documentation files}
-Check the following files:
+Change version and codename in the following files:
\begin{itemize}
\item \texttt{ALL\_VERSIONS} (non-beta only)
\item \texttt{VERSION} (for beta releases, add suffix \texttt{\textasciitilde{}beta}, not \texttt{-beta})
\item \texttt{VERSION\_CODENAME}
+ \item \texttt{opam}
+ \begin{itemize}
+ \item change version (for beta releases, add suffix \texttt{\textasciitilde{}beta}, not \texttt{-beta})
+ \item change doc link: \texttt{…/download/user-manual-<version>-<codename>.pdf}
+ (with \texttt{-beta} in version for beta releases, not \texttt{\textasciitilde{}beta})
+ \end{itemize}
+\end{itemize}
+
+Also check the headers in Changelogs :
+\begin{itemize}
\item \texttt{Changelog}
\item \texttt{src/plugins/wp/Changelog}
\item \texttt{src/plugins/e-acsl/doc/Changelog}
- \item \texttt{INSTALL.md} ("Reference configuration")
- \item \texttt{opam} (for beta releases, add suffix \texttt{\textasciitilde{}beta}, not \texttt{-beta})
\end{itemize}
\subsection{Versions in source: API documentation}
@@ -193,8 +201,8 @@ expected format is:
It should only list main changes, that will be displayed on the event section
of the website and the wiki page.
-Create the version commit, tag it using \texttt{git tag \$(cat VERSION | sed -e "s/~/-/")}
-and push it (e.g. via \texttt{git push origin \$(cat VERSION | sed -e "s/~/-/")}).
+Create the version commit, tag it using \texttt{git tag \$(cat VERSION | sed -e "s/\textasciitilde /-/")}
+and push it (e.g. via \texttt{git push origin \$(cat VERSION | sed -e "s/\textasciitilde/-/")}).
%%%Local Variables:
%%%TeX-master: "release"
diff --git a/doc/userman/user-plugins.tex b/doc/userman/user-plugins.tex
index 13f3992c0f6f5d1202dde82f2b8019a8b28e4f4b..ab30e14d280d23887b67e729811e7081ad96af2e 100644
--- a/doc/userman/user-plugins.tex
+++ b/doc/userman/user-plugins.tex
@@ -13,22 +13,9 @@ There are two kinds of plug-ins: \emph{internal} and \emph{external} plug-ins.
\index{Plug-in!Internal|bfit}\index{Plug-in!External|bfit}
Internal plug-ins are those distributed within the \FramaC kernel while
external plug-ins are those distributed independently of the \FramaC
-kernel. They only differ in the way they are installed (see
-Sections~\ref{sec:install-internal} and~\ref{sec:install-external}).
-
-\section{Installing Internal Plug-ins}\label{sec:install-internal}
-\index{Plug-in!Internal}
-
-Internal plug-ins are automatically installed with the \FramaC kernel.
-
-If you use a source distribution of \FramaC, it is possible to disable (resp.
-force) the installation of a plug-in of name \texttt{<plug-in name>} by passing
-the {\tt configure} script the option \texttt{-{}-disable-<plug-in name>}
-(resp. \texttt{-{}-enable-<plug-in name>}). Disabling a plug-in means it is
-neither compiled nor installed. Forcing the compilation and installation of a
-plug-in against {\tt configure}'s autodetection-based default may cause the
-entire \FramaC configuration to fail. You can also use the option
-\optiondef{-{}-}{with-no-plugin} in order to disable all plug-ins.
+kernel. They only differ in the way they are installed:
+internal plug-ins are automatically installed with the \FramaC kernel,
+while external plug-ins must be installed separately.
\section{Installing External Plug-ins}\label{sec:install-external}
\index{Plug-in!External}
@@ -41,15 +28,9 @@ must return the directory where the \FramaC compiled library is installed (see
Section~\ref{sec:var-lib}).
The standard way for installing an external plug-in from source is to run the
-sequence of commands \texttt{make \&\& make install}, possibly preceded by
-\texttt{./configure}. Please refer to each
+sequence of commands \texttt{make \&\& make install}. Please refer to each
plug-in's documentation for installation instructions.
-External plug-ins may also be configured and compiled at the same time as
-the \FramaC kernel by using the option
-\texttt{-{}-enable-external=<path-to-plugin>}
-\optionidxdef{-{}-}{enable-external}. This option may be passed several times.
-
\section{Loading Plug-ins}\label{sec:use-plugins}
At launch, \FramaC loads all plug-ins in the
diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex
index ebabe0499ebaf6230e38ae0642cac3168264c959..af7ddd445d68f192633b3b8b63b6dd81592d51ed 100644
--- a/doc/userman/user-start.tex
+++ b/doc/userman/user-start.tex
@@ -471,11 +471,7 @@ External plug-ins (see Section~\ref{sec:install-external}) or scripts (see
Section~\ref{sec:use-plugins}) are compiled against the \FramaC compiled
library. The \FramaC option \optiondef{-}{print-lib-path} prints the path to
this library.
-
-The default path to this library may be set when configuring \FramaC by using
-the \texttt{configure} option \optiondef{-{}-}{libdir}. Once \FramaC is
-installed, you can also set the environment variable \textttdef{FRAMAC\_LIB}
-to change this path.
+It can be changed by setting the environment variable \textttdef{FRAMAC\_LIB}.
\subsection{Variable \texttt{FRAMAC\_PLUGIN}}\label{sec:var-plugin}
@@ -489,11 +485,7 @@ to this directory. It can be changed by setting the environment variable
\FramaC looks for all its other data (installed manuals, configuration files,
\C modelization libraries, \etc) in a single directory. The \FramaC option
\optiondef{-}{print-share-path} prints this path.
-
-The default path to this library may be set when configuring \FramaC by using
-the \texttt{configure} option \optiondef{-{}-}{datarootdir}. Once \FramaC is
-installed, you can also set the environment variable
-\textttdef{FRAMAC\_SHARE} to change this path.
+It can be changed by setting the environment variable \textttdef{FRAMAC\_SHARE}.
A \FramaC plug-in may have its own share directory (default is \texttt{`frama-c
-print-share-path `/<plug-in shortname>}). If the plug-in is not installed in
diff --git a/nix/frama-c-public/publish-opam.sh b/nix/frama-c-public/publish-opam.sh
index 14e55bf81cfe2ef8fb6fe15ae6bb0c828601d6ef..cb16d47eea871de74ef924c822634934cd630b79 100755
--- a/nix/frama-c-public/publish-opam.sh
+++ b/nix/frama-c-public/publish-opam.sh
@@ -44,9 +44,10 @@ PUB_OPAM_DIR="pub-opam-repository"
SRC_OPAM_DIR="opam-repository"
VERSION="$(cat VERSION)"
+VERSION_SAFE="$(cat VERSION | sed 's/~/-/')"
CODENAME="$(cat VERSION_CODENAME)"
-BRANCH="frama-c.$VERSION"
+BRANCH="frama-c.$VERSION_SAFE"
echo "$FRAMA_CI_BOT_SSH_PRIVATE" | base64 -d > nix/frama-c-public/id_ed25519
chmod 400 nix/frama-c-public/id_ed25519
diff --git a/nix/frama-c-public/publish-website.sh b/nix/frama-c-public/publish-website.sh
index 7a757bfe3b92cf7cdd575ffd0403f7e088e3b854..22eee20cc1ebb46bd331b8969e883c5b49d50f08 100755
--- a/nix/frama-c-public/publish-website.sh
+++ b/nix/frama-c-public/publish-website.sh
@@ -104,8 +104,7 @@ function push {
-o merge_request.create \
-o merge_request.title="Release $VERSION-$CODENAME" \
-o merge_request.assign="$GITLAB_USER_ID"\
- -o merge_request.draft \
- -o ci.skip
+ -o merge_request.draft
fi
if [ "$?" -ne "0" ]; then
echo "Failed to push branch"
diff --git a/src/plugins/callgraph/gui/dune b/src/plugins/callgraph/gui/dune
index ff7cfa689b1b5ac29dc40677ad8628516ddf2836..c409de4a1ac2515a3186879d105d7cc9f4cdda27 100644
--- a/src/plugins/callgraph/gui/dune
+++ b/src/plugins/callgraph/gui/dune
@@ -41,8 +41,8 @@
(libraries
frama-c.kernel frama-c.gui frama-c-callgraph.core
(select graph.ml from
- (ocamlgraph.dgraph -> graph.dgraph.ml)
- (ocamlgraph_gtk -> graph.gtk.ml)
+ (!lablgtk3-sourceview3 ocamlgraph.dgraph -> graph.dgraph.ml)
+ (!lablgtk3-sourceview3 ocamlgraph_gtk -> graph.gtk.ml)
)
)
)
diff --git a/src/plugins/gui/dune b/src/plugins/gui/dune
index 6bd7f4534326ed74b26ced2f6f503272d1a04a30..bc10179285b7779235d11aab1702f45cd182531b 100644
--- a/src/plugins/gui/dune
+++ b/src/plugins/gui/dune
@@ -30,7 +30,7 @@
(echo " - lablgtk2.sourceview2:" %{lib-available:lablgtk2.sourceview2} "\n")
(echo " - lablgtk3:" %{lib-available:lablgtk3} "\n")
(echo " - lablgtk3-sourceview3:" %{lib-available:lablgtk3-sourceview3} "\n")
- ; From a GUI hook registered by RteGen.
+ ; From a GUI hook registered by RteGen.
(echo " - Rtegen (optional):" %{lib-available:frama-c-rtegen.core} "\n")
)
)
@@ -62,23 +62,23 @@
(flags -open Frama_c_kernel -linkall :standard -w -9)
(libraries frama-c.init.gui frama-c.kernel
(select gtk_compat.ml from
- (lablgtk2 lablgtk2.gnomecanvas lablgtk2.sourceview2 -> gtk_compat.2.ml)
(lablgtk3 lablgtk3-sourceview3 -> gtk_compat.3.ml)
+ (lablgtk2 lablgtk2.gnomecanvas lablgtk2.sourceview2 -> gtk_compat.2.ml)
)
(select GSourceView.ml from
- (lablgtk2 lablgtk2.gnomecanvas lablgtk2.sourceview2 -> GSourceView.2.ml)
(lablgtk3 lablgtk3-sourceview3 -> GSourceView.3.ml)
+ (lablgtk2 lablgtk2.gnomecanvas lablgtk2.sourceview2 -> GSourceView.2.ml)
)
(select GSourceView.mli from
- (lablgtk2 lablgtk2.gnomecanvas lablgtk2.sourceview2 -> GSourceView.2.mli)
(lablgtk3 lablgtk3-sourceview3 -> GSourceView.3.mli)
+ (lablgtk2 lablgtk2.gnomecanvas lablgtk2.sourceview2 -> GSourceView.2.mli)
)
(select dgraph_helper.ml from
- (ocamlgraph.dgraph -> dgraph_helper.yes.ml)
+ (!lablgtk3-sourceview3 ocamlgraph.dgraph -> dgraph_helper.yes.ml)
( -> dgraph_helper.no.ml)
)
(select debug_manager.ml from
- (ocamlgraph.dgraph -> debug_manager.ok.ml)
+ (!lablgtk3-sourceview3 ocamlgraph.dgraph -> debug_manager.ok.ml)
( -> debug_manager.ko.ml)
)
)