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, holtrace-prune takes 50.96 seconds and 3253MB RAM to prune the 82MB trace of hol.ml from holtrace-save 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).