-rw-r--r-- 1174 holtrace-20250617/doc/prune.md raw
Running

    ./holtrace-prune < oldtrace.50 > newtrace.50

converts an existing HOLTrace file
into a new HOLTrace file
that focuses on proving the same named theorems.
Traces directly from HOL Light
normally include some automatically generated proofs
that did not end up being used for the named theorems,
so pruning saves space.
Pruning also speeds up subsequent trace processing.

This tool is written in Python.
On [`rome1`](install.html),
`holtrace-prune` takes 50.96 seconds and 3253MB RAM
to prune the
82MB trace of `hol.ml` from [`holtrace-save`](save.html)
down to 37.5MB (`gzip -9` reduces this to 10.4MB).

This tool is idempotent.
Given the 37.5MB pruned HOLTrace file as input,
the tool takes 34.60 seconds and 1606MB RAM,
generating an identical file as output.

This tool lets you provide a theorem name as a command-line argument.
The resulting trace then focuses on proving that theorem
(although the tool will preserve names for any lemmas relevant to that theorem).
For example, given the 37.5MB pruned trace for `hol.ml`,
`holtrace-prune ONE_OR_PRIME`
takes 16.25 seconds and 1438MB RAM,
and generates 2.4MB as output (`gzip -9` reduces this to 0.72MB).