formal toolset

README

Building:
docker build -t formal . 

Run on host for GUI support:
xhost local:root

Running the container with GUI support and mounting ~/formal_work as /work:
docker run -ti --rm -e DISPLAY=$DISPLAY  -v /tmp/.X11-unix:/tmp/.X11-unix -v ~/formal_work:/work formal

Dockerfile

FROM ubuntu:16.04
MAINTAINER Sami Mäkelä

RUN apt-get update && \
  apt-get install -y coq wget gcc ocaml menhir libmenhir-ocaml-dev libcoq-ocaml-dev libzarith-ocaml-dev libocamlgraph-ocaml-dev unzip liblablgtksourceview2-ocaml-dev libzip-ocaml-dev vim libxtst6

env PATH="/src/Isabelle2016/bin:${PATH}"

RUN mkdir src ; cd src && \
  wget https://alt-ergo.ocamlpro.com/download_manager.php?target=alt-ergo-static-1.01-x86_64 -O alt-ergo && \
  chmod 755 alt-ergo && \
  mv alt-ergo /usr/bin && \
  wget https://github.com/Z3Prover/bin/raw/master/releases/z3-4.4.1-x64-ubuntu-14.04.zip && \
  unzip z3-4.4.1-x64-ubuntu-14.04.zip && \
  cp z3-4.4.1-x64-ubuntu-14.04/bin/z3 /usr/bin && \
  wget http://cvc4.cs.nyu.edu/builds/x86_64-linux-opt/cvc4-1.4-x86_64-linux-opt -O cvc4 && \
  chmod 755 cvc4 && \
  mv cvc4 /usr/bin && \
  wget http://isabelle.in.tum.de/dist/Isabelle2016_app.tar.gz && \
  tar xzf Isabelle2016_app.tar.gz

RUN echo /src/why3-0.87.2/lib/isabelle >> /src/Isabelle2016/etc/components

RUN cd src && \
  wget https://gforge.inria.fr/frs/download.php/file/36133/why3-0.87.2.tar.gz && \
  tar xvf why3-0.87.2.tar.gz && \
  cd why3-0.87.2 && \
  ./configure && \
  make && \
  make install && \
  why3 config --detect

RUN mv /usr/bin/coqc /usr/bin/coqc_orig && \
echo '#!/usr/bin/env bash\n\
coqc_orig -R /usr/local/lib/why3/coq-tactic/ Why3 -R /usr/local/lib/why3/coq/ Why3 $@'\
>> /usr/bin/coqc && \
chmod +x /usr/bin/coqc