# 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" ]