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.

Install dependencies

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.

Windows

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.

  1. Install Cygwin.
  2. Clone the Everest repository from GitHub.
  3. From inside the origin directory of the clone, run ./everest check and follow the instructions on how to install compilation dependencies (OCaml, etc.) ./everest check will automatically install all such compilation dependencies, but you may need to re-run it several times after refreshing the environment.

Linux

  1. Install opam, a package manager for the OCaml ecosystem.

    Note

    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.

  2. Make sure the system packages corresponding to the following commands are installed:

    • GNU cp
    • GNU date
    • diff
    • find
    • gcc
    • GNU getopt
    • git
    • GNU make
    • patch
    • GNU sed
    • wget
    • which
  3. Run opam init --compiler=4.12.0 and 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.

    Note

    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 init with the non-system package for OCaml.

    If this step fails, then you will need to remove the ~/.opam directory before trying again.

  4. Clone the Everest repository from GitHub.

  5. From inside the origin directory of the clone, run ./everest opam and 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:

  1. Clone the EverParse repository .

  2. In the root directory of that EverParse clone, run one of the following commands:

    • make everparse

      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.

      Note

      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.

      Note

      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_EVERCRYPT environment variable to any nonzero value, to use ocaml-sha instead of EverCrypt. In that case, ocaml-sha will be automatically installed while building EverParse.

    • make package

      That command will build a binary package, everparse-<version>-<platform>.zip on Windows, .tar.gz on Linux, by producing the everparse/ subdirectory as with make everparse and compressing it into an archive.

    • make package-noversion

      That command will build a binary package, as with make package, but only the name of the archive will change: everparse.zip on Windows, everparse.tar.gz on Linux.

In all cases, the produced package offers everparse.cmd on Windows, 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:

Note

You cannot use everparse.sh or everparse.cmd from the source tree. You need to use bin/3d.exe instead.

  1. In the root directory of the Everest clone, run ./everest z3 and 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.

    Note

    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.

  2. Run ./everest pull to fetch and pull the latest versions of F*, KReMLin and EverParse.

  3. Run ./everest -j 1 FStar make kremlin make to build F* and KReMLin. The -j option introduces a parallelism factor. You can also speed up the build by skipping F*, KReMLin and EverCrypt library proofs by setting the OTHERFLAGS environment variable to "--admit_smt_queries true".

    Note

    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 opam init or ./everest opam), or log out and back in.

  4. Run make -C hacl-star/dist/gcc-compatible install-ocaml to build and install EverCrypt (needed for hash checking with --check_hashes, etc.)

    Note

    In fact, this step builds and installs the hacl-star-raw and hacl-star OCaml 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-raw and/or ocamlfind remove hacl-star, and try again.

    Note

    Even if you manage to build EverCrypt at this stage, you may still encounter a linking issue when building 3d.exe later, maybe due to EverCrypt not supported on your platform (e.g. FreeBSD.) As a workaround, you can set the NO_EVERCRYPT environment variable to any nonzero value, to use ocaml-sha instead of EverCrypt. In that case, you first need to run opam install ocaml-sha to install that package beforehand.

  5. Set the FSTAR_HOME environment variable to the FStar subdirectory of your Everest clone, which contains a clone of the latest F*.

  6. Set the KREMLIN_HOME environment variable to the kremlin subdirectory of your Everest clone, which contains a clone of the latest KReMLin.

    Note

    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.)

  7. Everest contains a clone of the EverParse sources in the quackyducky subdirectory. You can work from there. Alternatively, you can clone it yourself anywhere else.

  8. Set the QD_HOME environment variable to your EverParse clone as you chose it.

  9. 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 bin/3d.exe.