HOLTrace: Save

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 (or OpenTheory 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();;
holtrace_namethm !theorems;;

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, as the following comparison illustrates:

On rome1, a normal hol.sh run takes 154 seconds to load HOL Light's standard library (hol.ml), allocating 758MB RAM and using 495MB RAM.
A holtrace-save run after ./install instead takes 2145 seconds, allocating 2196MB RAM and using 1930MB RAM. The resulting trace for hol.ml is 82MB (gzip -9 reduces this to 20.7MB).
A holtrace-save run after ./install+hashtt takes 522 seconds, allocating 2348MB RAM and using 2074MB RAM.

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.30 of the "Save" web page.