-rw-r--r-- 1748 holtrace-20250629/doc/install.md raw
## Prerequisites

The instructions below
have been tested on a server named `rome1` running Debian 11
with the `build-essential`, `opam`, `python3`, `pypy3`, `texlive-xetex`, and `xdot` packages installed,
in a user account that ran

    time opam init github git+https://github.com/ocaml/opam-repository.git --disable-sandboxing -a
    time opam switch create 5.2.0
    time opam install 'hol_light=3.0.0' -y
    eval `opam env`

to install HOL Light 3.0.0 with the OCaml 5.2 bytecode compiler.

The server has two AMD EPYC 7742 CPUs,
but timings reported in this documentation
use only one core (except for `holtrace2tex`).
Overclocking on the server has been (manually) disabled,
so the CPUs run at 2.245GHz.

## HOLTrace installation

Make sure you are in the `holtrace-*` package directory.

Run `make -j8` to compile the C/C++ tools.

Find the HOL Light installation directory,
and set `HOLLIGHT_DIR` to the name of that directory.
For example:

    HOLLIGHT_DIR=$HOME/.opam/5.2.0/lib/hol_light

Copy `holtrace.ml` into that directory:

    cp holtrace.ml $HOLLIGHT_DIR/

Patch `hol_lib.ml` in that directory to use `holtrace.ml`:

    sed -i '/nets.ml/iloads "holtrace.ml";;' $HOLLIGHT_DIR/hol_lib.ml

This should have no effect on normal HOL Light usage,
but lets you use HOL Light to
[save](save.html)
and
[verify](verify.html)
traces.

Optionally, patch the installation in that directory
to precompute hashes of types and terms:

    ./hashtt $HOLLIGHT_DIR

This speeds up saving traces.
However, this is more invasive than just using `holtrace.ml`,
has a higher risk of bugs,
and increases CPU time for normal usage by about 15%.
You can run

    ./hashtt-undo $HOLLIGHT_DIR

to undo the patch.

Now [test](test.html) the installation.