holtrace2tex is a command-line tool that takes a trace on standard input, and produces a LaTeX file on standard output with statements of the named theorems. Running the file through xelatex or lualatex produces output such as the following: "Theorem (ONE_OR_PRIME). Fix p ∈ ℕ. Then p = 1 or p is prime if and only if we have n = 1 or n = p for each n ∈ ℕ such that n divides p."

This was the original motivation for HOLTrace: making it easier for readers of a paper to see what a theorem checked by HOL Light says. Hopefully the tool is less error-prone than an author carrying out a similar conversion by hand. (For earlier work, see the journal Formalized Mathematics reporting what was checked by Mizar.)

This tool includes printouts of axioms and definitions, but currently does not check for anything unusual in these. Also, the tool's conversion from traced theorems to output is not necessarily invertible, although the tool tries harder than HOL Light's default pretty-printer to avoid creating ambiguities.

This tool is currently a pipeline from a tool written in C to a tool written in Python. The C tool is not necessarily safe to run on untrusted input; a VM is recommended.

On rome1, holtrace2tex takes about 11 seconds (with some variability) to convert the 37.5MB pruned trace of hol.ml into a LaTeX file presenting 3513 theorem statements. (There are 2975 named theorems in the original file; holtrace2tex automatically expands multi-part theorems into multiple theorems.) The bottleneck is the Python tool; the C tool is faster and will typically run on a separate core.