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 and verify traces.

Now test the installation.