-r--r--r-- 6474 holtrace-20250714/doc/html/tex.html raw
<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<style type="text/css">
html{overflow-y:scroll;background-color:#505050}
body{font-family:"Noto Sans","Droid Sans","DejaVu Sans","Arial",sans-serif;line-height:1.5}
tt,code{background-color:#f0f0f0;font-family:"Noto Sans Mono","Droid Sans Mono","DejaVu Sans Mono","Courier New",monospace,sans-serif;font-size:1em;}
pre{margin-left:3em}
p,ul,ol,blockquote,pre{font-size:1.0em;line-height:1.6}
li p{font-size:1.0em}
blockquote p{font-size:1.0em}
h1{font-size:1.5em}
h2{font-size:1.3em}
h3{font-size:1.0em}
h1 a{text-decoration:none}
table{border-collapse:collapse}
th,td{border:1px solid black}
table a{text-decoration:none}
table tr{font-size:1.0em;line-height:1.6em}
table tr{font-size:1.0em;line-height:1.5}
tbody tr:nth-child(12n+1){background-color:#f0ffff}
tbody tr:nth-child(12n+2){background-color:#f0ffff}
tbody tr:nth-child(12n+3){background-color:#f0ffff}
tbody tr:nth-child(12n+4){background-color:#f0ffff}
tbody tr:nth-child(12n+5){background-color:#f0ffff}
tbody tr:nth-child(12n+6){background-color:#f0ffff}
tbody tr:nth-child(12n+7){background-color:#fffff0}
tbody tr:nth-child(12n+8){background-color:#fffff0}
tbody tr:nth-child(12n+9){background-color:#fffff0}
tbody tr:nth-child(12n+10){background-color:#fffff0}
tbody tr:nth-child(12n+11){background-color:#fffff0}
tbody tr:nth-child(12n+12){background-color:#fffff0}
#headline{display:block;margin:0;padding:0;color:#ffffff;background-color:#505050}
#headline .text{font-weight:bold;font-size:1.0em}
#headline input{display:none}
#nav ul{margin:0;padding:0}
#nav li{list-style-type:none;margin:0;padding:0}
.navtop{padding-bottom:0.5em;font-weight:bold;font-size:1.0em}
.navtop{background-color:#505050;color:#ffffff}
#nav .here{background-color:#505050;color:#ffffff}
#nav .away{background-color:#505050;color:#ffffff}
#nav .away a{text-decoration:none;display:block;color:#ffffff}
#nav .away a:hover,.away a:active{text-decoration:underline}
#hidemenu{visibility:hidden;display:none;overflow:hidden;position:fixed;top:0;left:0;height:100%;width:100%}
.main{padding:5px}
.main{background-color:#ffffff}
.pagetitle{font-size:1.4em;font-weight:bold}
@media only screen and (min-width:512px) {
.navtop{padding-top:5px}
#headline{top:0;margin:0;width:160px;height:100%;position:fixed;overflow:auto}
#headline .noselect{display:none}
#headline #nav{visibility:visible;display:block;width:auto;height:auto}
.main{margin-left:170px}
#headline #hidemenu{visibility:hidden}
}
@media not screen and (min-width:512px) {
#headline .noselect{-webkit-user-select:none;-ms-user-select:none;user-select:none;}
#headline #nav #navbot{visibility:hidden;position:fixed;top:0;left:-70%;z-index:2;transition:0.2s;margin:0;padding:0}
#headline input:checked ~ #nav #navbot{height:100%;position:fixed;top:0;left:0;visibility:visible;display:block;box-sizing:border-box;-moz-box-sizing:border-box;-webkit-box-sizing:border-box;vertical-align:center;font-size:1.0em;width:70%;overflow:auto}
#headline input:checked ~ #hidemenu{visibility:visible;display:block;background:black;opacity:0.3;z-index:1}
}
</style>
<title>
HOLTrace: TeX</title>
</head>
<body>
<label id=headline>
<input type=checkbox />
<nav id=nav>
<div class=navtop>
<span class=noselect>≡</span>
HOLTrace</div>
<ul id=navbot>
<li class=away><a href=index.html>Intro</a>
</li><li class=away><a href=download.html>Download</a>
</li><li class=away><a href=install.html>Install</a>
</li><li class=away><a href=test.html>Test</a>
</li><li class=away><a href=save.html>Save</a>
</li><li class=away><a href=prune.html>Prune</a>
</li><li class=away><a href=verify.html>Verify</a>
</li><li class=here>TeX
</li><li class=away><a href=ml.html>ML REPL</a>
</li><li class=away><a href=prooftrace.html>ProofTrace</a>
</li><li class=away><a href=opentheory.html>OpenTheory</a>
</li><li class=away><a href=format.html>Format</a>
</li><li class=away><a href=license.html>License</a>
</li><li class=away><a href=bib.html>Literature</a>
</li></ul></nav>
<div id=hidemenu></div>
</label>
<div class=main>
<div class=pagetitle>HOLTrace: TeX</div>
<p><code>holtrace2tex</code> 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 <code>xelatex</code> or <code>lualatex</code>
produces output such as the following:
"Theorem (ONE_OR_PRIME). Fix <em>p</em> ∈ ℕ. Then <em>p</em> = 1 or <em>p</em> is prime if and only if we have <em>n</em> = 1 or <em>n</em> = <em>p</em> for each <em>n</em> ∈ ℕ such that <em>n</em> divides <em>p</em>."</p>
<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.</p>
<p>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
<a href="https://www.cs.ru.nl/F.Wiedijk/pubs/rap.pdf">creating ambiguities</a>.</p>
<p>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.</p>
<p>On <a href="install.html"><code>rome1</code></a>,
<code>holtrace2tex</code> takes roughly 15 seconds (with some variability)
to convert the 37.6MB pruned trace of <code>hol.ml</code>
into a LaTeX file presenting 3520 theorem statements.
(There are 2981 named theorems in the original file;
<code>holtrace2tex</code> 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.</p>
<h2>Other tools</h2>
<p>See the journal
<a href="https://fm.mizar.org/">Formalized Mathematics</a>
for many examples of English proofs obtained from annotated Mizar proofs.
See
<a href="https://naproche.github.io/">Naproche</a>
for a system to computer-check (some) English proofs.
See the
<a href="bib.html#english">bibliography</a>
for more tools.</p><hr><font size=1><b>Version:</b>
This is version 2025.06.30 of the "TeX" web page.
</font>
</div>
</body>
</html>