Skip to content

Instantly share code, notes, and snippets.

@patcon

patcon/INSTALL.md

Last active Jul 28, 2017
Embed
What would you like to do?
Installing why3 IDE for verifying sample Ethereum contract (Ubuntu 14.04)
# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.