The main mechanism to create new traces is holtrace-save, after which the traces will typically be processed by holtrace-prune and further tools. It is also possible to convert ProofTrace files to HOLTrace format, but generating HOLTrace format directly from HOL Light is faster than generating ProofTrace format.

holtrace-save is a command-line tool that starts HOL Light, similarly to hol.sh:

./holtrace-save

The difference is that holtrace-save saves the proofs and theorems in the HOL Light session. These are saved in a file with a name of the form holtrace-*.50. The * part includes the date and process ID, so this name is very likely to be new, but if it is not then the old file will be removed.

The trace file automatically accumulates proofs and theorems as HOL Light is running. It does not record names of theorems until you run

holtrace_namethm !theorems;;

using HOL Light's built-in list !theorems of name-theorem pairs. The built-in list has only the HOL Light standard library by default, but you can use the following HOL Light commands to extend the list to cover further named theorems proven in this session:

needs "update_database.ml";;
update_database();;

There is also holtrace_nameonethm to handle a single name-theorem pair.

You can stop the tracing in this session:

holtrace_stop();;

Restarting tracing within the same session is not supported. Also, checkpointing is not supported in combination with tracing.

Tracing slows down HOL Light. On rome1, a normal hol.sh run takes 153 seconds to load HOL Light's standard library (hol.ml), allocating 750MB RAM and using 488MB RAM. A holtrace-save run instead takes 35 minutes, allocating 2258MB RAM and using 1996MB RAM. The resulting trace for hol.ml is 82MB (gzip -9 reduces this to 20.6MB).

Internally, holtrace-save is a simple shell script that picks a filename, sets the HOLTRACE_SAVE environment variable to that filename, and runs hol.sh. The main work is then handled by the Holtrace_save module in holtrace.ml. This module is a wrapper around the HOL Light kernel. The wrapper redefines new_axiom, new_basic_definition, new_basic_type_definition, and the primitive inference rules such as REFL. If HOLTRACE_SAVE is not set, the wrapper keeps the original definitions, except that it modifies new_basic_type_definition to keep a !holtrace_typedef_thms list used by the Holtrace_restore module for verification.

---

Version: This is version 2025.06.17 of the "Save" web page.