`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.

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](https://www.cs.ru.nl/F.Wiedijk/pubs/rap.pdf).

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`](install.html),
`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.

## Related work

[1976 Chester](https://www.sciencedirect.com/science/article/abs/pii/0004370276900072)
described a program EXPOUND
to convert inference sequences into English proofs.

[1987 Felty–Miller](https://www.site.uottawa.ca/~afelty/dist/proof87.pdf)
described the χ-proof system,
with extra information attached to inferences to improve presentation as English proofs.

[1995 Coscoy–Kahn–Thery](https://inria.hal.science/inria-00074217/file/RR-2459.pdf)
described a converter (part of ctcoq)
to convert Coq inference sequences into English proofs,
including various compression mechanisms.
[1997 Coscoy](https://link.springer.com/chapter/10.1007/BFb0052156)
presented further compression mechanisms.

[1999 Holland-Minkley–Barzilay–Constable](https://www.cs.columbia.edu/nlp/papers/1999/holland-minkley_al_99.pdf)
converted tactic sequences for Nuprl into English proofs.

[2005 Cairns–Gow](https://www-users.york.ac.uk/paul.cairns/pubs/Maze.pdf)
described a tool Maze
to convert annotated Mizar proofs into English proofs.

[2009 Cramer–Fisseni–Koepke–Kühlwein–Schröder–Veldman](https://ids-pub.bsz-bw.de/frontdoor/deliver/index/docId/8193/file/Cramer_Fisseni_Koepke_Kuehlwein_Schroeder_Veldman_The_Naproche_Project_2010.pdf)
described Naproche,
a system to computer-check (some) English proofs.

[2013 Ganesalingam–Gowers](https://arxiv.org/pdf/1309.4501)
described a tool to generate some types of proofs
and convert them into English proofs.

[2017 Bedford](https://arxiv.org/pdf/1712.03894)
presented a tool Coqatoo
to convert tactic sequences for Coq into English proofs.

See the journal
[Formalized Mathematics](https://fm.mizar.org/)
for many examples of English proofs obtained from annotated Mizar proofs.