-rw-r--r-- 2547 holtrace-20250617/doc/save.md raw
The main mechanism to create new traces is `holtrace-save`,
after which the traces will typically be processed by
[`holtrace-prune`](prune.html) and further tools.
It is also possible to convert
[ProofTrace](prooftrace.html) 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`](install.html),
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](verify.html).