There are several ways to install EasyCrypt and its dependencies. The recommended method is to use OPAM, a package manager for OCaml (the programming language EasyCrypt is written in). Other installation methods include using Nix and directly from source. Whichever method you choose, be sure to follow the (post-installation) setup and configuration instructions afterward!
Note: We maintain a list of known installation quirks and corresponding troubleshooting tips. If you encounter any issues during installation, be sure to consult that document for assistance.
Installation via OPAM consists of three steps:
- Installing and Initializing OPAM
- Installing EasyCrypt's Dependencies via OPAM
- Installing EasyCrypt via OPAM
If you already have a working installation of OPAM on your system, you can skip ahead and start with installing EasyCrypt's dependencies via OPAM.
Note: This section takes most of its instructions from the official OPAM installation guide and the OCaml installation guide. If you encounter any issues, be sure to consult those resources first.
On most operating systems, the recommended way to install OPAM is through your system's package manager—we'll cover this approach first. Alternatively, OPAM provides scripts that automatically install the latest binary distribution for your system—we'll cover this method second. (For additional installation methods, consult the the official OPAM installation guide)
After installing OPAM, it must be initialized—we'll cover that immediately after installation.
Search for your operating system in the list below and expand its section to view the relevant instructions for installing OPAM. If your operating system is not listed, refer to the official OPAM installation guide.
Debian/Ubuntu
To install OPAM, run the following command. You may need elevated privileges
to do so—commonly by prefixing the command with sudo, though other methods
may apply depending on your system.
Note: The Debian/Ubuntu
opampackage includes the OCaml compiler as a recommended dependency, which is installed by default. If you wish to avoid this, runapt-get install --no-install-recommends opaminstead.
apt-get install opam
Once OPAM is installed, proceed to the initialization step.
Arch
To install OPAM, run the following command. You may need elevated privileges
to do so—commonly by prefixing the command with sudo, though other methods
may apply depending on your system.
pacman -S opam
Once OPAM is installed, proceed to the initialization step.
Fedora/OpenSUSE
To install OPAM, run the following command. You may need elevated privileges
to do so—commonly by prefixing the command with sudo, though other methods
may apply depending on your system.
dnf install opam
Once OPAM is installed, proceed to the initialization step.
macOS (Homebrew and MacPorts)
To install OPAM, run one of the following commands. You may need elevated privileges
to do so—commonly by prefixing the command with sudo, though other methods
may apply depending on your system.
-
Homebrew:
brew install opam -
MacPorts:
port install opam
Once OPAM is installed, proceed to the initialization step.
OpenBSD
To install OPAM, run the following command. You may need elevated privileges
to do so—commonly by prefixing the command with sudo, though other methods
may apply depending on your system.
pkg_add opam
Once OPAM is installed, proceed to the initialization step.
FreeBSD
To install OPAM, run the following command. You may need elevated privileges
to do so—commonly by prefixing the command with sudo, though other methods
may apply depending on your system.
pkg install ocaml-opam
Once OPAM is installed, proceed to the initialization step.
Windows
To install OPAM, run the following command. You may need elevated privileges to do so—commonly by opening the terminal as an administrator ("Run as administrator"), though other methods may apply depending on your system.
winget install Git.Git OCaml.opam
Once OPAM is installed, proceed to the initialization step.
An alternative to installing OPAM via the package manager is to use one of the dedicated scripts provided by OPAM. These scripts automatically install the appropriate binary distribution for your system.
Search for your system/situation in the list below and expand the corresponding section to view instructions for running the relevant script. If none of the options match your system/situation, refer to the official OPAM installation guide for more alternatives.
Unix-like system (including macOS)
Before proceeding, make sure the following system packages are installed:
gcc, build-essential, curl, bubblewrap, and unzip.
(Depending on your system, the package names may vary slightly).
To launch OPAM's script, run
bash -c "sh <(curl -fsSL https://opam.ocaml.org/install.sh)"
Alternatively, you can download the script manually from https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh and run it directly.
This script will automatically detect your system's configuration and install the appropriate binary distribution. At some point, it may prompt you to confirm options like the installation location. Be sure to read the output carefully and follow all instructions!
While the defaults usually suffice, exceptions exist. For example, on Ubuntu 24.04, you might want to set the installation location to
/usr/bin.
Once the script has completed and you've followed any additional instructions, proceed to initialize OPAM.
Windows system (using PowerShell)
To launch OPAM's script, run the following command (in PowerShell):
Invoke-Expression "& { $(Invoke-RestMethod https://opam.ocaml.org/install.ps1) }
Alternatively, you can download the script manually from https://raw.githubusercontent.com/ocaml/opam/master/shell/install.ps1 and run it directly.
This script will automatically detect your system's configuration and install the appropriate binary distribution. At some point, it may prompt you to confirm options like the installation location. Be sure to read the output carefully and follow all instructions!
Once the script has completed and you've followed any additional instructions, proceed to initialize OPAM.
After installing OPAM, initialize it by running
opam init
This command launches a program that may take several minutes to complete. At some point, it may provide additional instructions to ensure a working setup. Be sure to read the output carefully and follow all instructions!
Typically, these instructions involve running a command to configure your environment for both the current and future sessions. The exact command depends on your system, but usually looks something like
eval $(opam env)
for Unix-like systems; something like
for /f \"tokens=*\" %i in ('opam env') do @%i
for Windows systems using Windows Command Prompt; and something like
(& opam env) -split '\r?\n' | ForEach-Object { Invoke-Expression $_ }
for Windows systems using PowerShell.
Once the program has finished and you've followed its instructions, proceed to install EasyCrypt's dependencies.
At this stage, you should have a working OPAM installation. By default, such an installation
contains a single switch.
A switch is OPAM's take on an isolated environment, similar to Python's virtualenv.
To avoid conflicts with your EasyCrypt installation, it's recommended to create a dedicated switch.
You can create a new switch called easycrypt by running the following command.
(Optionally, you can specify a specific OCaml compiler for the switch by
appending the compiler version to the command and leaving out the --empty
option; you can list the available compilers by running opam switch list-available.
The compiler version must be >= 4.08 and < 5.0)
opam switch --empty create easycrypt
Once the switch is created, activate it with
opam switch set easycrypt
Make sure to read the output and follow any additional instructions provided by these commands!
(To check which switch is currently active, run opam switch list.
The active switch will be marked with an arrow on the left-hand side.)
Then, add the EasyCrypt package to your switch by running the following command.
Note: This requires
git, so make sure you have that installed first.
opam pin -yn add easycrypt https://github.com/EasyCrypt/easycrypt.git
At this point, you need to install EasyCrypt's (missing) dependencies. OPAM can automatically detect and install all required dependencies, including any system dependencies, but might need some additional setup depending on the version. To check your OPAM version, run
opam --version
If your OPAM version is below 2.1 (i.e., 2.0.x or lower), expand the section below to view necessary setup instructions. If your versions is 2.1.x or higher, you do not have to do this.
Installing System Dependencies with OPAM Version < 2.1
First, install OPAM's "system dependency manager plugin" with
opam install opam-depext
This may provide additional instructions to setup your environment properly—be sure to read the output carefully and follow any instructions.
Then, run the following command to let OPAM detect and install missing system dependencies:
opam depext easycrypt
This may prompt you to install certain dependencies via your system's package manager or some other appropriate mechanism. Be sure to read the output carefully and follow any instructions!
Let OPAM detect and install EasyCrypt's dependencies by running:
opam install --deps-only easycrypt
If your OPAM version is 2.1 or higher, this command will also detect and install any missing system dependencies. In this case, you may be prompted to install these dependencies via your system's package manager or some other appropriate mechanism. Be sure to read the output carefully and follow any instructions!
Finally, install at least one SMT solver compatible with the current version of Why3 used by EasyCrypt. A common choice is Alt-Ergo, which is conveniently packaged by OPAM. Although it's not a direct dependency of EasyCrypt (and you're free to use a different compatible SMT solver), the simplest option is to install the correct version of Alt-Ergo via OPAM by running
opam install alt-ergo.2.6.0
(If you accidentally installed a different version of Alt-Ergo, you can change
to version 2.6.0 by running opam pin alt-ergo 2.6.0)
At this point, you can proceed to install EasyCrypt. However, if you wish, you can also install additional SMT solvers. This allows you to pick and choose between multiple solvers, or use them simultaneously. A list of compatible solvers is available below.
Having installed EasyCrypt's dependencies and at least one suitable SMT solver, you may still want to install EasyCrypt from source—even if you used OPAM for the rest. This can be useful if you want more direct control over the version of EasyCrypt you're using.
Otherwise, to install EasyCrypt via OPAM, run the following command:
opam install easycrypt
If everything went according to plan, you now have everything you need to run EasyCrypt! But before you get ahead of yourself, make sure to complete the (post-installation) setup and configuration to ensure everything works as expected.
Note: As this is not the recommended installation method and is considered more advanced, we don't go into much detail here. If you are looking for a more guided installation process, consider installing via OPAM instead.
First, ensure you have Nix's package manager installed. You can do so by following the official installation guide.
Next, clone or download this repository and navigate to its root.
At this point, you have a few options. Find the item that best matches your situation and expand the corresponding section to view the relevant instructions.
Build EasyCrypt without SMT solvers
To build EasyCrypt without any SMT solvers, run the following command:
make nix-build
Once the build is complete, you'll find the EasyCrypt binary
in the result/bin directory.
Build EasyCrypt along with a set of SMT solvers
To build EasyCrypt along with a set of SMT solvers, run the following command:
make nix-build-with-provers
Once the build is complete, you'll find the EasyCrypt binary
in the result/bin directory.
Setup a development environment with all required dependencies and SMT solvers
To setup a development environment, run the following command:make nix-develop
This installs all required dependencies and SMT solvers, and drops you in a
shell afterward. From there, run make to build EasyCrypt.
Note: As this is not the recommended installation method and is considered more advanced, we don't go into much detail here and primarily refer to external sources. If you are looking for a more guided installation process, consider installing via OPAM instead.
Note: If you only want to install EasyCrypt itself from source but prefer to install its dependencies automatically, consider following the OPAM-based installation instructions up to and including the installation of EasyCrypt's dependencies, then proceed to install Easycrypt from source.
The following is a list of all the dependencies required to build and run EasyCrypt. For each dependency, we provide some installation resources along with any relevant details or caveats. Once all dependencies are installed, proceed to install EasyCrypt from Source.
- OCaml (version >= 4.08 and < 5.0)
Additional resources: - OCamlbuild
- Git
- Why3 (version >= 1.8 and < 1.9)
You also need to install Why3's libraries (typically by runningmake byte && make install-lib). Further, you might already want to install at least one compatible SMT solver.
Additional resources: - Menhir
Additional resources: - OCaml Batteries Included (version >= 3)
Additional resources: - OCaml PCRE (version >= 7)
- OCaml Zarith (version >= 1.10)
Additional resources: - OCaml ini-files (version >= 1.2)
Additional resources: - OCaml Markdown
Additional resources: - Python3
You also need to install the following libraries:- Python3 YAML
- Python3 Curses
Note: This might already be included with your Python installation. If so, you do not need to install it separately.
Having installed EasyCrypt's dependencies, you can build and install EasyCrypt from source as follows.
First, clone or download the repository (e.g., by running git clone https://github.com/EasyCrypt/easycrypt.git)
and navigate to its root.
Then, to build EasyCrypt, run
make
After the build completes, a symbolic link to the EasyCrypt binary (ec.native) will
have been created in the repository's root directory. (The actual binary will be located at src/ec.exe.)
You can use this symbolic link directly anywhere an EasyCrypt binary is expected.
If this is sufficient for your use, proceed to the (post-installation) setup and configuration.
However, if you prefer a system-wide installation, run
make install
Once installed, proceed to the (post-installation) setup and configuration.