-rw-r--r-- 1039 holtrace-20250617/doc/ml.md raw
The command-line tool `holtrace2ml`
takes a trace on standard output
and prints OCaml commands on standard output.
The OCaml commands are essentially a series of HOL Light kernel calls,
and if they are provided as input to HOL Light
then they will verify proofs similarly to
[`holtrace_restore`](verify.html),
while printing out each lemma
(not just the named theorems).
These commands will also check definitions against existing definitions,
but (unlike `holtrace_restore`) will not allow new definitions.

This tool is written in C
and is not necessarily safe to run on untrusted input.
A VM is recommended.

On [`rome1`](install.html),
`holtrace2ml` takes 1.53 seconds and 42MB RAM
to convert the 37.5MB pruned trace of `hol.ml`
into a 252MB file containing OCaml commands (`gzip -9` reduces this to 40.5MB).

Reading the commands into OCaml
is much less efficient than `holtrace_restore`.
(Also, OCaml's `.ml` parser produces `Uncaught exception: Stack overflow`
around 9MB of input.)
However, the verbosity can be useful for humans.