EasyCrypt uses the following third-party tools/libraries:
OCaml (>= 4.02)
Available at http://caml.inria.fr/
OCamlbuild (only for OCaml >= 4.03)
Why3 (>= 0.87)
Available at http://why3.lri.fr/
Why3 must be installed with a set a provers.
Why3 libraries must be installed (make byte && make install-lib)
OCaml Batteries Included http://batteries.forge.ocamlcore.org/
OCaml PCRE (>= 7) https://github.com/mmottl/pcre-ocaml
OCaml ZArith https://forge.ocamlcore.org/projects/zarith
OCaml ini-files http://archive.ubuntu.com/ubuntu/pool/universe/o/ocaml-inifiles/
On POSIX systems (GNU/Linux, *BSD, OS-X), we recommend people to
install EasyCrypt and all its dependencies via
Installing requirements using OPAM (POSIX systems)
Starting with opam 1.2.0, you can install all the needed dependencies
via the opam OCaml packages manager.
Optionally, switch to a dedicated compiler for EasyCrypt:
$> opam switch -A $OVERSION easycrypt
where $OVERSION is a valid OCaml version (e.g. 4.02.1)
Add the EasyCrypt repository:
$> opam repository add easycrypt git://github.com/EasyCrypt/opam.git
$> opam update
Optionally, select the EasyCrypt (git) branch you want to use:
$> opam pin -n add easycrypt https://github.com/EasyCrypt/easycrypt.git#branch
branchis the branch name you want to use (e.g.
In that case, we advise you to create a dedicated opam switch
(see first step above).
Optionally, use opam to install the system dependencies:
$> opam install depext
$> opam depext easycrypt
Add the EasyCrypt meta-packages:
$> opam install --deps-only easycrypt
$> opam install ec-provers
Opam can be easily installed from source or via your packages manager:
On Ubuntu and derivatives:
$> add-apt-repository ppa:avsm/ppa $> apt-get update $> apt-get install ocaml ocaml-native-compilers camlp4-extra opam
On MacOSX using brew:
$> brew install ocaml opam
See [https://opam.ocaml.org/doc/Install.html] for how to install opam.
See [https://opam.ocaml.org/doc/Usage.html] for how to initialize opam
Before running EasyCrypt and after the installation/removal/update
of an SMT prover, you need to (re)configure Why3.
$> why3 config --detect
By EasyCrypt is using the default Why3 location, i.e. ~/.why3.conf.
If you have several versions of Why3 installed, it may be impossible
to share the same configuration file among them. EasyCrypt via the
option -why3, allows you to load a Why3 configuration file from a
custom location. For instance:
$> why3 config --detect -C $WHY3CONF.conf $> ./ec.native -why3 $WHY3CONF.conf
$WHY3CONF must be replaced by some custom location.
If installing from source, running
$> make $> make install
builds and install EasyCrypt (under the binary named
assuming that all dependencies have been successfully installed. If
you choose not to install EasyCrypt system wide, you can use the
ec.native that is located at the root of the source tree.
It is possible to change the installation prefix by setting the
environment variable PREFIX:
$> make PREFIX=/my/prefix install
EasyCrypt comes also with an opam package. Running
$> opam install easycrypt
installs EasyCrypt and its dependencies via opam. In that case, the
EasyCrypt binary is named
Proof General Front-End
Installing using opam
If you installed the EasyCrypt dependencies using opam, you can
install ProofGeneral via opam too. Running
$> opam install proofgeneral
installs ProofGeneral along with its EasyCrypt mode. You still have to
tweak your emacs configuration file (~/.emacs) to load
ProofGeneral by adding the following line to it
where $proof-general-home should be replaced by
with $prefix being set to the output of
$> opam config var prefix
Installing from sources
EasyCrypt mode has been integrated upstream. Please, go to
https://github.com/ProofGeneral/PG and follow the instructions.