# install ocaml and deps
apt-get install ocaml ocaml-native-compilers
apt-get install liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev libocamlgraph-ocaml-dev
# install opam from binaries (ocaml package manager)
# See https://opam.ocaml.org/doc/Install.html#Binarydistribution
wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin/
#### OR
# Can use system package manager if opam >= v1.1.1
apt-get install opam
# install why3
opam install why3
# install alt-ergo prover
opam install alt-ergo altgr-ergo satML-plugin
why3 config --detect
# Open pre-generated output file in why3 IDE
cd /tmp
git clone https://gist.github.com/chriseth/0c671e0dac08c3630f47 eth-binsearch-proof.gist
why3 ide eth-binsearch-proof.gist/Output_BinarySearch.mlw
Last active
July 28, 2017 10:34
-
-
Save patcon/1a58a3e84fa36f4beb75 to your computer and use it in GitHub Desktop.
Installing why3 IDE for verifying sample Ethereum contract (Ubuntu 14.04)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment