Travis

.gitmodules

@@ -1,3 +1,3 @@
 [submodule "tests"]
 	path = tests
-	url = git@github.com:ethereum/tests.git
+	url = https://github.com/ethereum/tests.git

.travis.yml

@@ -0,0 +1,16 @@
+sudo: required
+before_install:
+- sudo apt-get -qq update
+- sudo apt-get -qq install libgmp3-dev
+- wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sudo sh -s /usr/local/bin
+- opam init -y --comp=4.02.3
+- eval `opam config env`
+- opam install -y ocamlbuild ocamlfind batteries yojson bignum easy-format bisect_ppx zarith depext
+- git clone https://bitbucket.org/Peter_Sewell/lem.git lemdir
+- cd lemdir
+- make || echo "failure expected"
+- cd ..
+- export PATH=./lemdir:$PATH
+script:
+- make lem-ocaml
+- make lem-thy

README.md

@@ -21,7 +21,7 @@ When you see `\<Rightarrow>` in the source, try using the [Isabelle2016-1](https
 * [lem](http://www.cl.cam.ac.uk/~pes20/lem/built-doc/lem-manual.html#installation)
 * [OCaml](http://www.ocaml.org/) 4.02.3
 * [opam](https://opam.ocaml.org/) 1.2.2
-* Some opam packages: use `opam install ocamlfind batteries yojson bignum easy-format bisect_ppx`
+* Some opam packages: use `opam install ocamlfind batteries yojson bignum easy-format bisect_ppx ocamlbuild`
 
 ## How to read the proofs