misc/Dockerfile.deploy

   1 # Stage 1: build setup and prover download; to be cached
   2
   3 FROM debian:bullseye-slim as builder
   4
   5 USER root
   6
   7 ARG DEBIAN_FRONTEND=noninteractive
   8 RUN apt-get update -yq && \
   9     apt-get upgrade -yq --with-new-pkgs --auto-remove && \
  10     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 && \
  11     apt-get clean
  12
  13 RUN adduser --disabled-password --gecos '' guest
  14
  15 ## CVC4 1.8
  16 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 && \
  17     chmod a+x /usr/local/bin/cvc4-1.8
  18
  19 ## Z3 4.10.2
  20 RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.10.2/z3-4.10.2-x64-glibc-2.31.zip && \
  21     unzip z3-4.10.2-x64-glibc-2.31.zip && \
  22     mv z3-4.10.2-x64-glibc-2.31/bin/z3 /usr/local/bin/z3-4.10.2 && \
  23     rm -r z3-4.10.2-x64-glibc-2.31.zip z3-4.10.2-x64-glibc-2.31
  24
  25
  26 # Stage 2: compilation and installation; to be pruned
  27
  28 FROM builder as artifact
  29
  30 USER guest
  31 ENV HOME /home/guest
  32 COPY --chown=guest:guest . /home/guest/why3
  33 WORKDIR /home/guest/why3
  34
  35 RUN ./autogen.sh && \
  36     ./configure --enable-ide --enable-zip && \
  37     make
  38
  39 USER root
  40 RUN make install && \
  41     install -T misc/deployed-wrapper.sh /usr/local/bin/why3-wrapper.sh
  42
  43
  44 # Stage 3: deployed image; to be cached (for its first layers)
  45 # Note that the first command after FROM decides which cache is used,
  46 # so we start with COPY instead of USER to make sure both caches are trivially different.
  47
  48 FROM debian:bullseye-slim
  49
  50 COPY --from=builder /usr/bin/alt-ergo /usr/local/bin/
  51 COPY --from=builder /usr/local/bin/cvc4-1.8 /usr/local/bin/
  52 COPY --from=builder /usr/local/bin/z3-4.10.2 /usr/local/bin/
  53
  54 USER root
  55
  56 ARG DEBIAN_FRONTEND=noninteractive
  57 RUN apt-get update -yq && \
  58     apt-get upgrade -yq --with-new-pkgs --auto-remove && \
  59     apt-get install -yq --no-install-recommends libcanberra-gtk3-module libgtk-3-bin libgtksourceview-3.0-1 zlib1g && \
  60     apt-get clean
  61
  62 RUN adduser --disabled-password --gecos '' guest
  63
  64 COPY --from=artifact /usr/local/bin/why3 /usr/local/bin/
  65 COPY --from=artifact /usr/local/lib/why3 /usr/local/lib/why3
  66 COPY --from=artifact /usr/local/share/why3 /usr/local/share/why3
  67
  68 COPY --from=artifact /usr/local/bin/why3-wrapper.sh /usr/local/bin/
  69
  70 USER guest
  71 ENV HOME /home/guest
  72 WORKDIR /home/guest
  73
  74 ENV NO_AT_BRIDGE 1
  75
  76 RUN why3 config detect
  77
  78 ENTRYPOINT [ "why3-wrapper.sh" ]