README
* REQUIREMENTS
====================================================================
* OCaml (>= 4.00)
Available at http://caml.inria.fr/
* Menhir
Available at http://gallium.inria.fr/~fpottier/menhir/
* Why3 (= 0.81)
Available at http://why3.lri.fr/
Why3 must be installed with a set a provers.
See [http://why3.lri.fr/#provers]
Why3 libraries must be installed (make byte && make install-lib)
* Unix extlib
Available at http://extunix.forge.ocamlcore.org/
* GNU Emacs (>= 23.3)
Available at http://www.gnu.org/software/emacs/
* ProofGeneral 4.2
Available at http://proofgeneral.inf.ed.ac.uk/
* LOCAL TOOLCHAIN
====================================================================
You can install a local copy of OCaml and all the needed libraries by
running [make toolchain]. You only need [curl] and the [gcc] compiler.
By default, the destination directory is ${PWD}/_tools. You can change
this by setting the $DEST variable, e.g.:
make DEST=/opt/ec-toolchain toolchain
Note that $DEST cannot contain spaces.
The toolchain is not activated by default. You have to:
`./scripts/activate-toolchain.sh`
This command has to be repeated each time you start a fresh terminal.
Regarding the Why3 configuration file, easycrypt is using the default
Why3 location, i.e. ~/.why3.conf, or _tools/why3.local.conf when it
exists. 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:
why3config --detect -C $DEST/why3.conf
./ec.native -why3 $DEST/why3.conf
We also provide an automated way to install a set of core
provers. After having installing the toolchain, type:
make provers
This also create a configuration file for Why3 in
_tools/why3.local.conf. This file is automatically loaded by EasyCrypt
when started locally.
* COMPILATION
====================================================================
The shell commands
make
make install
should build and install easycrypt.
It is possible to change the installation prefix by setting the
environment variable PREFIX:
make PREFIX=/my/prefix install
* INSTALLING THE PROOFGENERAL FRONT-END
====================================================================
Add the following entry to <proof-general-home>/generic/proof-site.el
in the definition of `proof-assistant-table-default':
(easycrypt "EasyCrypt" "ec")
Copy the directory easycrypt/ to <proof-general-home>/
If you have not done so, add the following line to your Emacs
configuration file (typically ~/.emacs):
(load-file "<proof-general-home>/generic/proof-site.el")
If the EasyCrypt executable is not in your $PATH, set the path to the
EasyCrypt executable by modifying the variable easycrypt-prog-name
inside Emacs:
Proof-General
-> Advanced
-> Customize
-> EasyCrypt
-> EasyCrypt prog name
setting its value to:
"<path-to-easycrypt>/easycrypt -emacs"