mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
79 lines
2.5 KiB
Docker
79 lines
2.5 KiB
Docker
# Stage 1: build setup and prover download; to be cached
|
|
|
|
FROM debian:bullseye-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 alt-ergo autoconf build-essential ca-certificates libgmp-dev liblablgtksourceview3-ocaml-dev libmenhir-ocaml-dev libnum-ocaml-dev libzarith-ocaml-dev libzip-ocaml-dev menhir ocaml-findlib ocaml-nox unzip wget && \
|
|
apt-get clean
|
|
|
|
RUN adduser --disabled-password --gecos '' guest
|
|
|
|
## CVC4 1.8
|
|
RUN wget --quiet https://github.com/CVC4/CVC4-archived/releases/download/1.8/cvc4-1.8-x86_64-linux-opt -O /usr/local/bin/cvc4-1.8 && \
|
|
chmod a+x /usr/local/bin/cvc4-1.8
|
|
|
|
## Z3 4.10.2
|
|
RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.10.2/z3-4.10.2-x64-glibc-2.31.zip && \
|
|
unzip z3-4.10.2-x64-glibc-2.31.zip && \
|
|
mv z3-4.10.2-x64-glibc-2.31/bin/z3 /usr/local/bin/z3-4.10.2 && \
|
|
rm -r z3-4.10.2-x64-glibc-2.31.zip z3-4.10.2-x64-glibc-2.31
|
|
|
|
|
|
# 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 --enable-ide --enable-zip && \
|
|
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:bullseye-slim
|
|
|
|
COPY --from=builder /usr/bin/alt-ergo /usr/local/bin/
|
|
COPY --from=builder /usr/local/bin/cvc4-1.8 /usr/local/bin/
|
|
COPY --from=builder /usr/local/bin/z3-4.10.2 /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 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
|
|
|
|
ENV NO_AT_BRIDGE 1
|
|
|
|
RUN why3 config detect
|
|
|
|
ENTRYPOINT [ "why3-wrapper.sh" ]
|