% !TeX root = easycrypt.tex

\chapter{Getting Started}
\section{Building and Running \EasyCrypt}
The easiest way to install \EasyCrypt on a Unix-based OS is to use the local
toolchain-based installation scripts available from our public \texttt{git}
repository. Other solutions exist, but the wide variety of machines and
configurations we expect \EasyCrypt users to own prevent us from documenting or
supporting them all. We strongly recommend using the local installation scripts
unless you are ready to deal with configuration issues yourself.

\subsection{Building \EasyCrypt}
To build \EasyCrypt from scratch, you will need the following standard tools:
\texttt{git}, \texttt{make}, \texttt{curl}, \texttt{autoconf}, \texttt{gcc} and \texttt{g++}.

The following bash script clones our public \texttt{git} repository, builds the
local toolchain (including the provers), activates it and builds \EasyCrypt.

\begin{verbatim}
  git clone http://ci.easycrypt.info/easycrypt.git 
  cd easycrypt
  make toolchain provers
  $(./scripts/activate-toolchain.sh)
  make && make check
\end{verbatim}

The toolchain and provers may take up to an hour to build, but this only has to
be done once, although you will need to activate it using the following command
every time you wish to work with \EasyCrypt.

\begin{verbatim}
  $(./scripts/activate-toolchain.sh)
\end{verbatim}

To keep your version of \EasyCrypt up to date, simply run the following command
(the toolchain must be active).

\begin{verbatim}
  git pull && make
\end{verbatim}

\paragraph{On the test suite}
The final \texttt{make check} runs \EasyCrypt on our test suite and
the standard libraries. Please do report any failure in the test suite
(if possible, attach the .xml file produced by \texttt{make
  check-xunit}) to
\url{easycrypt-support@lists.gforge.inria.fr}. Unless a large number
of tests fail, a failure at this point does not necessarily mean that
the installation failed: SMT solvers can be fickle beasts and the
computing capacity of computers varies greatly. We are doing our best
to make calls to SMT in the standard library as stable as possible
over a wide variety of machines, but we need your help to test them in
as many scenarios as possible and are counting on you to report
failures.

\paragraph{Included provers}
The local toolchain contains a minimal set of provers to which you can easily
add your own. Please look at \WhyThree's and your favourite prover's
documentation for installation instructions. By default, all installed provers
are used when SMT is called. This behaviour can be changed using a command-line
option and language pragmas.

\subsection{\EasyCrypt's interactive mode}
The instructions above give you a command-line version of \EasyCrypt that can be
used to check proof scripts, but is difficult to use to develop proofs. We also
provide an interactive interface based on \texttt{emacs} and ProofGeneral.
Again, we recommend using our local installation scripts and will only provide
limited support if you choose not to.

To install \EasyCrypt's interactive mode, ensure that you have \texttt{emacs}
version 23.3 or higher, and that it is in your \texttt{\$PATH}. Under MacOSX,
\texttt{emacs} is detected when installed in the system Applications or using
MacPorts. The following command, run from the public repository's root, will
fetch and compile the latest version of Proof General, along with the \EasyCrypt
definitions.
\begin{verbatim}
  make -C proofgeneral local
\end{verbatim}
You can then run \texttt{emacs} using this fresh configuration of Proof General
by running the following command from the repository's root and opening files as
normal.
\begin{verbatim}
  make pg
\end{verbatim}

\subsection{Bug reporting}
For now, please use the GForge tracker
(\url{https://gforge.inria.fr/tracker/?group_id=2622}) to report bugs and
unsightly behaviours. This requires an account on the forge (which will ask you
for an INRIA project-team name %that you can probably fill in at random
to create an account). We are working on setting up an alternative bug tracking
system.

\subsection{About this documentation}
The source for this document, along with the macros and language definitions
used, are available in the public repository. Feel free to use the language
definitions to typeset your \EasyCrypt-related documents, and to contribute
improvements to the macros if you have any.

This document is intended as a user manual for the \EasyCrypt tool, and not as
a tutorial on how to build a cryptographic proof, or how to perform interactive
proofs. We attempt to provide some detailed examples in later sections of this
document, but they are still simple and may still be obscure even with a good
understanding of the issues. We recommend experimenting.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "easycrypt"
%%% End: