misc/Dockerfile.build

   1 # If you modify this file, make sure to update the BUILD_IMAGE variable in `.gitlab-ci.yml`.
   2 # Follow the detailed instructions given in `ci.md`.
   3
   4 FROM debian:bullseye-slim
   5
   6 USER root
   7
   8 # install dependencies
   9 ARG DEBIAN_FRONTEND=noninteractive
  10 RUN apt-get update -yq && \
  11     apt-get upgrade -yq --with-new-pkgs --auto-remove && \
  12     apt-get install -yq --no-install-recommends autoconf build-essential ca-certificates git graphviz libgmp-dev liblablgtksourceview3-ocaml-dev libmenhir-ocaml-dev libmpfr-dev libzarith-ocaml-dev libzip-ocaml-dev menhir ocaml-nox opam python3-sexpdata unzip wget xauth xvfb && \
  13     apt-get clean
  14
  15 # install provers
  16 ## CVC5 1.0.5
  17 RUN wget --quiet https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.5/cvc5-Linux -O /usr/local/bin/cvc5-1.0.5 && \
  18     chmod a+x /usr/local/bin/cvc5-1.0.5
  19 ## CVC4 1.8
  20 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 && \
  21     chmod a+x /usr/local/bin/cvc4-1.8
  22 ## CVC4 1.7
  23 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 && \
  24     chmod a+x /usr/local/bin/cvc4-1.7
  25 ## CVC4 1.6
  26 RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.6-x86_64-linux-opt -O /usr/local/bin/cvc4-1.6 && \
  27     chmod a+x /usr/local/bin/cvc4-1.6
  28 ## CVC4 1.5
  29 RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.5-x86_64-linux-opt -O /usr/local/bin/cvc4-1.5 && \
  30     chmod a+x /usr/local/bin/cvc4-1.5
  31 ## CVC4 1.4
  32 RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.4-x86_64-linux-opt -O /usr/local/bin/cvc4-1.4 && \
  33     chmod a+x /usr/local/bin/cvc4-1.4
  34 ## Z3 4.6.0
  35 RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.6.0/z3-4.6.0-x64-debian-8.10.zip && \
  36     unzip z3-4.6.0-x64-debian-8.10.zip && \
  37     mv z3-4.6.0-x64-debian-8.10/bin/z3 /usr/local/bin/z3-4.6.0 && \
  38     rm -r z3-4.6.0-x64-debian-8.10.zip z3-4.6.0-x64-debian-8.10
  39 ## Z3 4.8.4
  40 RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.8.4/z3-4.8.4.d6df51951f4c-x64-debian-8.11.zip && \
  41     unzip z3-4.8.4.d6df51951f4c-x64-debian-8.11.zip && \
  42     mv z3-4.8.4.d6df51951f4c-x64-debian-8.11/bin/z3 /usr/local/bin/z3-4.8.4 && \
  43     rm -r z3-4.8.4.d6df51951f4c-x64-debian-8.11.zip z3-4.8.4.d6df51951f4c-x64-debian-8.11
  44 ## Z3 4.8.10
  45 RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip && \
  46     unzip z3-4.8.10-x64-ubuntu-18.04.zip && \
  47     mv z3-4.8.10-x64-ubuntu-18.04/bin/z3 /usr/local/bin/z3-4.8.10 && \
  48     rm -r z3-4.8.10-x64-ubuntu-18.04.zip z3-4.8.10-x64-ubuntu-18.04
  49 ## Z3 4.11.2
  50 RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.11.2/z3-4.11.2-x64-glibc-2.31.zip && \
  51     unzip z3-4.11.2-x64-glibc-2.31.zip && \
  52     mv z3-4.11.2-x64-glibc-2.31/bin/z3 /usr/local/bin/z3-4.11.2 && \
  53     rm -r z3-4.11.2-x64-glibc-2.31.zip z3-4.11.2-x64-glibc-2.31
  54 ## Z3 4.12.2
  55 RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.12.2/z3-4.12.2-x64-glibc-2.31.zip && \
  56     unzip z3-4.12.2-x64-glibc-2.31.zip && \
  57     mv z3-4.12.2-x64-glibc-2.31/bin/z3 /usr/local/bin/z3-4.12.2 && \
  58     rm -r z3-4.12.2-x64-glibc-2.31.zip z3-4.12.2-x64-glibc-2.31
  59
  60 # create user
  61 RUN adduser --disabled-password --gecos '' why3
  62 USER why3
  63 ENV HOME /home/why3
  64 WORKDIR /home/why3
  65
  66 # install opam
  67 ENV OPAM_PACKAGES="menhir mlmpfr.4.1.0+bugfix2 lablgtk3-sourceview3 zarith camlzip conf-autoconf"
  68 RUN opam init -y --no-setup -j4 --bare --disable-sandboxing && \
  69     opam switch create latest ocaml-base-compiler.5.0.0 && \
  70     opam switch create bench  ocaml-base-compiler.4.09.1 && \
  71     opam switch create full   ocaml-base-compiler.4.13.1 && \
  72     opam repository add coq-released https://coq.inria.fr/opam/released --all-switches && \
  73     opam install -y --switch=latest $OPAM_PACKAGES && \
  74     opam install -y --switch=bench  $OPAM_PACKAGES zenon.0.8.5 coq.8.16.1 alt-ergo.2.5.4 && \
  75     opam install -y --switch=full   $OPAM_PACKAGES re coq.8.18.0 coq-flocq js_of_ocaml-ppx alt-ergo.2.5.4 sexplib ppx_deriving ppx_sexp_conv ocamlgraph zarith_stubs_js && \
  76     opam clean -a -c -r -s --logs
  77
  78 USER root
  79 RUN cp /home/why3/.opam/full/bin/alt-ergo /usr/local/bin/alt-ergo-2.5.4
  80 RUN cp /home/why3/.opam/bench/bin/alt-ergo /usr/local/bin/alt-ergo-2.5.4
  81
  82 USER why3