mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
fa486b0370
The first command after FROM decides which cache will be used, and this decision is never overturned. So, this commit makes sure that both images start with different commands, in order for the correct cache to be picked.
76 lines
2.5 KiB
Docker
76 lines
2.5 KiB
Docker
# Stage 1: build setup and prover download; to be cached
|
|
|
|
FROM debian:buster-slim as builder
|
|
|
|
USER root
|
|
|
|
ARG DEBIAN_FRONTEND=noninteractive
|
|
RUN apt-get update -yq && \
|
|
apt-get upgrade -yq --with-new-pkgs --auto-remove && \
|
|
apt-get install -yq --no-install-recommends wget libcanberra-gtk3-module unzip build-essential autoconf automake ocaml-nox ca-certificates menhir libmenhir-ocaml-dev libzip-ocaml-dev liblablgtksourceview3-ocaml-dev ocaml-findlib alt-ergo && \
|
|
apt-get clean
|
|
|
|
RUN adduser --disabled-password --gecos '' guest
|
|
|
|
## 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 /usr/local/bin/cvc4-1.7 && \
|
|
chmod a+x /usr/local/bin/cvc4-1.7
|
|
## Z3 4.8.4
|
|
RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.8.4/z3-4.8.4.d6df51951f4c-x64-debian-8.11.zip && \
|
|
unzip z3-4.8.4.d6df51951f4c-x64-debian-8.11.zip && \
|
|
mv z3-4.8.4.d6df51951f4c-x64-debian-8.11/bin/z3 /usr/local/bin/z3-4.8.4 && \
|
|
rm -r z3-4.8.4.d6df51951f4c-x64-debian-8.11.zip z3-4.8.4.d6df51951f4c-x64-debian-8.11
|
|
|
|
|
|
# Stage 2: compilation and installation; to be pruned
|
|
|
|
FROM builder as artifact
|
|
|
|
USER guest
|
|
ENV HOME /home/guest
|
|
COPY --chown=guest:guest . /home/guest/why3
|
|
WORKDIR /home/guest/why3
|
|
|
|
RUN ./autogen.sh && \
|
|
./configure && \
|
|
make
|
|
|
|
USER root
|
|
RUN make install && \
|
|
install -T misc/deployed-wrapper.sh /usr/local/bin/why3-wrapper.sh
|
|
|
|
|
|
# Stage 3: deployed image; to be cached (for its first layers)
|
|
# Note that the first command after FROM decides which cache is used,
|
|
# so we start with COPY instead of USER to make sure both caches are trivially different.
|
|
|
|
FROM debian:buster-slim
|
|
|
|
COPY --from=builder /usr/bin/alt-ergo /usr/local/bin/
|
|
COPY --from=builder /usr/local/bin/cvc4-1.7 /usr/local/bin/
|
|
COPY --from=builder /usr/local/bin/z3-4.8.4 /usr/local/bin/
|
|
|
|
USER root
|
|
|
|
ARG DEBIAN_FRONTEND=noninteractive
|
|
RUN apt-get update -yq && \
|
|
apt-get upgrade -yq --with-new-pkgs --auto-remove && \
|
|
apt-get install -yq --no-install-recommends libcanberra-gtk3-module libgtk-3-bin libgtksourceview-3.0-1 libgomp1 zlib1g && \
|
|
apt-get clean
|
|
|
|
RUN adduser --disabled-password --gecos '' guest
|
|
|
|
COPY --from=artifact /usr/local/bin/why3 /usr/local/bin/
|
|
COPY --from=artifact /usr/local/lib/why3 /usr/local/lib/why3
|
|
COPY --from=artifact /usr/local/share/why3 /usr/local/share/why3
|
|
|
|
COPY --from=artifact /usr/local/bin/why3-wrapper.sh /usr/local/bin/
|
|
|
|
USER guest
|
|
ENV HOME /home/guest
|
|
WORKDIR /home/guest
|
|
|
|
RUN why3 config detect
|
|
|
|
ENTRYPOINT [ "why3-wrapper.sh" ]
|