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 and verify 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 the installation.

---

Version: This is version 2025.06.29 of the "Install" web page.