-r--r--r-- 6252 holtrace-20250617/doc/html/test.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{padding:0;font-weight:bold;font-size:1.0em;vertical-align:top;padding-bottom:0.5em;color:#ffffff;background-color:#505050}
.navt{display:block;box-sizing:border-box;-moz-box-sizing:border-box;-webkit-box-sizing:border-box;margin:0;padding:0;vertical-align:center;font-size:1.0em}
.here{background-color:#505050}
.here{color:#ffffff}
.away{background-color:#505050}
.away a{text-decoration:none;display:block;color:#ffffff}
.away a:hover,.away a:active{text-decoration:underline}
.main{padding:5px}
.main{background-color:#ffffff}
.pagetitle{font-size:1.4em;font-weight:bold}
@media only screen and (min-width:512px) {
.fixed{margin:0;padding:0;width:160px;height:100%;position:fixed;overflow:auto}
.main{margin-left:170px}
}
</style>
<title>
HOLTrace: Test</title>
</head>
<body>
<div class=fixed>
<div class=headline>
HOLTrace</div>
<div class="navt away"><a href=index.html>Intro</a>
</div><div class="navt away"><a href=download.html>Download</a>
</div><div class="navt away"><a href=install.html>Install</a>
</div><div class="navt here">Test
</div><div class="navt away"><a href=save.html>Save</a>
</div><div class="navt away"><a href=prune.html>Prune</a>
</div><div class="navt away"><a href=verify.html>Verify</a>
</div><div class="navt away"><a href=tex.html>TeX</a>
</div><div class="navt away"><a href=ml.html>ML REPL</a>
</div><div class="navt away"><a href=prooftrace.html>ProofTrace</a>
</div><div class="navt away"><a href=format.html>Format</a>
</div><div class="navt away"><a href=license.html>License</a>
</div></div>
<div class=main>
<div class=pagetitle>HOLTrace: Test</div>
<p>Download and uncompress a trace:</p>
<pre><code>wget https://holtrace.cr.yp.to/prime.50.gz
gunzip prime.50
</code></pre>
<p>Start a HOL Light session
(not reusing a pre-HOLTrace session):</p>
<pre><code>hol.sh
</code></pre>
<p>In that session, verify the trace:</p>
<pre><code>holtrace_restore !theorems "prime.50";;
</code></pre>
<p>The expected outputs are many lines that start <code>matching</code>
and then the following, with more lines in place of <code>...</code>:</p>
<pre><code>type IDs: 597
term IDs: 176388
theorem IDs: 91115
inference IDs: 91115
typedef IDs: 6
tag / 0.000000 seconds 327 occurrences
...
tag t 0.000000 seconds 91115 occurrences
total 0.000000 seconds
val it : unit = ()
</code></pre>
<p>You can also try <code>holtrace_restore_time</code> instead of <code>holtrace_restore</code>;
then there will be actual timings instead of <code>0.000000 seconds</code>.</p>
<p>Inspect the restored <code>ONE_OR_PRIME</code> theorem:</p>
<pre><code>holtrace_restore_name2thm "ONE_OR_PRIME";;
</code></pre>
<p>The expected output is the following:</p>
<pre><code>val it : thm =
|- forall p.
p = 1 \/ prime p <=> (forall n. n divides p ==> n = 1 \/ n = p)
</code></pre>
<p>Check that the restored theorem matches the theorem from the HOL Light standard library:</p>
<pre><code>equals_thm it ONE_OR_PRIME;;
</code></pre>
<p>The expected output is <code>val it : bool = true</code>.</p>
<p>Outside the HOL Light session,
verify the same trace from the command line:</p>
<pre><code>./holtrace-verify-simple < prime.50
./holtrace-verify < prime.50
</code></pre>
<p>The expected output is</p>
<pre><code>verified 2399423 bytes, 359543 lines, 597 types, 176388 terms, 91115 infs, 91115 thms, 6 typedefs
</code></pre>
<p>from <code>holtrace-verify-simple</code>,
and the same from <code>holtrace-verify</code>.</p>
<p>Check that the trace is already pruned
down to what is needed for the <code>ONE_OR_PRIME</code> theorem:</p>
<pre><code>./holtrace-prune ONE_OR_PRIME < prime.50 | cmp - prime.50
</code></pre>
<p>The expected output is nothing.</p>
<p>Convert the trace to a TeX file:</p>
<pre><code>./holtrace2tex < prime.50 > prime.tex
xelatex prime
</code></pre>
<p>The last theorem on the last page of the resulting <code>prime.pdf</code> is expected to say 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>Test some libraries used by the Python scripts:</p>
<pre><code>./type.py
./term.py
./ptparse.py
</code></pre>
<p>The expected outputs are <code>test type</code> and <code>test term</code> and <code>test ptparse</code>.</p>
<p>Try the built-in suite of test traces:</p>
<pre><code>./testtraces < testtraces.in | cmp - testtraces.exp
</code></pre>
<p>This takes 22 seconds
on <a href="install.html"><code>rome1</code></a>.
The expected output is nothing.</p><hr><font size=1><b>Version:</b>
This is version 2025.06.17 of the "Test" web page.
</font>
</div>
</body>
</html>