How to build EverParse from source¶
You may want to use the sources instead of the binary package in any of the following cases:
- You are on a non-x86_64 platform (however, there is no guarantee that the sources will compile under any such non-x86_64 platform.)
- You are not on Windows or Linux (however, there is no guarantee that the sources will compile under any such non-Windows-Linux system.)
- You want to use your own copy of F*, KReMLin or z3.
- You want to contribute to EverParse.
To this end, you must first install dependencies, then compile the sources.
EverParse, F* and KReMLin are all components of the Everest project. Thus, the best way to install dependencies is to use the Everest script, as described below following the website of the Everest project, which EverParse is a member of.
Building EverParse on Windows requires Cygwin. Instead, you could also use the Windows Subsystem for Linux (WSL) and act as if you were on Linux (see below), but this has not been officially tested by anyone in the Everest project; you will obtain Linux binaries instead.
- Install Cygwin.
- Clone the Everest repository from GitHub.
- From inside the origin directory of the clone, run
./everest checkand follow the instructions on how to install compilation dependencies (OCaml, etc.)
./everest checkwill automatically install all such compilation dependencies, but you may need to re-run it several times after refreshing the environment.
You need to install opam 2.x, so beware of older distributions such as Ubuntu 18.04 packaging opam 1.x by default. The opam web page gives detailed installation instructions to install opam 2.x.
Make sure the system packages corresponding to the following commands are installed:
- GNU cp
- GNU date
- GNU getopt
- GNU make
- GNU sed
opam init --compiler=4.12.0and follow the instructions. This will install OCaml.
This step will modify your configuration scripts to add the path to OCaml and its libraries to the PATH environment variable every time you login, so you may need to evaluate those configuration scripts again or log out and back in for such changes to take effect.
You need to specify an OCaml version number (between 4.08.0 and 4.12.x), so that OCaml will be installed in your user profile, because some EverParse dependencies do not work well with a system-wide OCaml. Thus, if opam says that there is an ambiguity, you should re-run
opam initwith the non-system package for OCaml.
If this step fails, then you will need to remove the
~/.opamdirectory before trying again.
Clone the Everest repository from GitHub.
From inside the origin directory of the clone, run
./everest opamand follow the instructions. This step will install the relevant opam packages on which EverParse depends.
Compile the sources¶
There are two possible ways.
- If your platform is not supported (or if binary releases do not work for some reason) and if you just want to rebuild EverParse, then you can build a binary package.
- If you want to contribute to the EverParse sources, then you need to build in the source tree.
Build a binary package¶
If you just want to rebuild EverParse without contributing to its sources, you can build a binary package:
In the root directory of that EverParse clone, run one of the following commands:
That command will build ready-to-use binaries into the
everparse/subdirectory. That directory will behave as if you had downloaded and extracted a binary package archive from the releases page.
This process is fully automatic. In particular, it automatically downloads a binary release of z3, and downloads and builds F*, KReMLin and EverCrypt.
z3 is downloaded only for Windows or Linux. On other platforms, you need to have Z3 4.8.5 reachable from your PATH. You will most likely need to compile it from its sources.
If you encounter a linking issue when building
3d.exe, then it may be due to EverCrypt not supported on your platform (e.g. FreeBSD.) As a workaround, you can set the
NO_EVERCRYPTenvironment variable to any nonzero value, to use ocaml-sha instead of EverCrypt. In that case,
ocaml-shawill be automatically installed while building EverParse.
That command will build a binary package,
.tar.gzon Linux, by producing the
everparse/subdirectory as with
make everparseand compressing it into an archive.
That command will build a binary package, as with
make package, but only the name of the archive will change:
In all cases, the produced package offers
everparse.sh on Linux, which you can use as directed
elsewhere in this manual.
Build in the source tree¶
If you want to contribute to the sources of EverParse, you need to rebuild in the source tree. To do so, you first need to setup a development environment for Everest (steps 1 to 6 below). Then you can fetch and build EverParse sources:
You cannot use
everparse.cmd from the
source tree. You need to use
In the root directory of the Everest clone, run
./everest z3and follow the instructions to install z3 on your system.
This step will modify your configuration scripts to add the path to z3 to the PATH environment variable every time you login, so you may need to evaluate those configuration scripts again or log out and back in for such changes to take effect.
./everest pullto fetch and pull the latest versions of F*, KReMLin and EverParse.
./everest -j 1 FStar make kremlin maketo build F* and KReMLin. The
-joption introduces a parallelism factor. You can also speed up the build by skipping F*, KReMLin and EverCrypt library proofs by setting the
OTHERFLAGSenvironment variable to
If, at this point, you immediately get an error of the form “menhir not found”, then it means that the path to opam packages is not properly set up in your environment. To do so, you need to run
eval $(opam env)(as instructed during
./everest opam), or log out and back in.
make -C hacl-star/dist/gcc-compatible install-ocamlto build and install EverCrypt (needed for hash checking with
In fact, this step builds and installs the
hacl-starOCaml packages. If, at this point, you get an error of the form “hacl-star-raw already installed” or “hacl-star already installed”, it means that either package is already present because of an earlier compilation, so you can remove it, using
ocamlfind remove hacl-star-rawand/or
ocamlfind remove hacl-star, and try again.
Even if you manage to build EverCrypt at this stage, you may still encounter a linking issue when building
3d.exelater, maybe due to EverCrypt not supported on your platform (e.g. FreeBSD.) As a workaround, you can set the
NO_EVERCRYPTenvironment variable to any nonzero value, to use ocaml-sha instead of EverCrypt. In that case, you first need to run
opam install ocaml-shato install that package beforehand.
FSTAR_HOMEenvironment variable to the
FStarsubdirectory of your Everest clone, which contains a clone of the latest F*.
KREMLIN_HOMEenvironment variable to the
kremlinsubdirectory of your Everest clone, which contains a clone of the latest KReMLin.
If you already have your own copy of F* or KReMLin, and if you already know how to build them, then you can skip steps 1 to 5 and set the environment variables accordingly.)
Everest contains a clone of the EverParse sources in the
quackyduckysubdirectory. You can work from there. Alternatively, you can clone it yourself anywhere else.
QD_HOMEenvironment variable to your EverParse clone as you chose it.
Then, once you are all set up in your EverParse clone, you can build EverParse by
make. Then, the EverParse/3d executable will be located at