## Prerequisites

The instructions below
have been tested on a server named `rome1` running Debian 11
with the `build-essential`, `opam`, 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:
e.g.,
`$HOME/.opam/5.2.0/lib/hol_light`.

Copy `holtrace.ml` into that directory.

Edit `hol_lib.ml` in that directory
to add a line

    loads "holtrace.ml";;

after the existing `basics.ml` line.
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.

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