Skip to content

Instantly share code, notes, and snippets.

@patcon

patcon/INSTALL.md

Last active July 28, 2017 10:34
Show Gist options
  • Star 3 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save patcon/1a58a3e84fa36f4beb75 to your computer and use it in GitHub Desktop.
Save patcon/1a58a3e84fa36f4beb75 to your computer and use it in GitHub Desktop.
Download ZIP
Installing why3 IDE for verifying sample Ethereum contract (Ubuntu 14.04)
Raw
INSTALL.md 
# 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