HACL* OCaml bindings: use proposal from hacl-star/hacl-star#456

doc/3d.rst

@@ -467,7 +467,7 @@ 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 5 below). Then you can
+development environment for Everest (steps 1 to 6 below). Then you can
 fetch and build EverParse sources:
 
 1. In the root directory of the Everest clone, run ``./everest z3``
@@ -481,18 +481,13 @@ fetch and build EverParse 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 hacl-star make`` to
-   build F\*, KReMLin and EverCrypt (needed for hash checking with
-   ``--check_hashes``, etc.). The ``-j`` option introduces a
+3. Run ``./everest -j 1 FStar make kremlin make hacl-star`` 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::
-
-      Even with proofs disabled, this step takes very long time.
-
    .. note::
 
       If, at this point, you immediately get an error of the form
@@ -501,12 +496,25 @@ fetch and build EverParse sources:
       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.
 
-4. Set the ``FSTAR_HOME`` environment variable to the ``FStar``
+5. Set the ``FSTAR_HOME`` environment variable to the ``FStar``
    subdirectory of your Everest clone, which contains a clone of the
    latest F\*.
 
-5. Set the ``KREMLIN_HOME`` environment variable to the ``kremlin``
+6. Set the ``KREMLIN_HOME`` environment variable to the ``kremlin``
    subdirectory of your Everest clone, which contains a clone of the
    latest KReMLin.
 
@@ -516,16 +524,16 @@ fetch and build EverParse sources:
       already know how to build them, then you can skip steps 1 to 5
       and set the environment variables accordingly.)
 
-6. Everest contains a clone of the EverParse sources in the
+7. Everest contains a clone of the EverParse sources in the
    ``quackyducky`` subdirectory. You can work from
    there. Alternatively, you can `clone it yourself
    <https://github.com/project-everest/everparse>`_
    anywhere else.
 
-7. Set the ``QD_HOME`` environment variable to your EverParse clone
+8. Set the ``QD_HOME`` environment variable to your EverParse clone
    as you chose it.
 
-8. Then, once you are all set up in your EverParse clone, you can
+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``.