* 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 (POSIX systems)
====================================================================

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.

* LOCAL TOOLCHAIN (cygwin)
====================================================================

WARNING: the ocaml compiler currently shipped with cygwin64 is
broken. You have to use the 32bits version of cygwin.

  git,wget,unzip,make,m4,gcc-core,gcc=g++,libmpfr4,autoconf,flexdll,
  libncurses-devel,curl,ocaml,ocaml-compiler-libs,patch,ncurses

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:

  `bash -o ingcr ./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 do NOT provide an automated way to install provers.

* 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"