-r--r--r-- 5022 holtrace-20250629/doc/html/opentheory.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: OpenTheory</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 away"><a href=test.html>Test</a>
</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 here">OpenTheory
</div><div class="navt away"><a href=format.html>Format</a>
</div><div class="navt away"><a href=license.html>License</a>
</div><div class="navt away"><a href=bib.html>Literature</a>
</div></div>
<div class=main>
<div class=pagetitle>HOLTrace: OpenTheory</div>
<p><a href="https://joe.leslie-hurd.com/opentheory/">OpenTheory</a> from Joe Hurd
is an existing library of traces
originally obtained from HOL Light, HOL4, and ProofPower.
One way to generate HOLTrace files is by
(1) downloading traces from the OpenTheory library and
(2) using <code>ot2holtrace</code> from the HOLTrace package
to convert traces from OpenTheory format to HOLTrace format.</p>
<p>The traces currently produced by <code>ot2holtrace</code>
from the OpenTheory library
will be rejected by <code>holtrace_restore</code> since they rely on different axioms and definitions
from the normal HOL Light axioms and definitions,
but will be accepted by <code>holtrace_restore_allownew</code>.</p>
<h2>Obtaining traces in OpenTheory format</h2>
<p>If you install the <code>opentheory</code>
<a href="https://joe.leslie-hurd.com/software/opentheory/download.html">tool</a>
and run</p>
<pre><code>opentheory install base
</code></pre>
<p>then <code>$HOME/.opentheory/packages</code> will contain
various subdirectories such as <code>base-1.221</code>.</p>
<p>Internally,
these subdirectories contain traces
split across "article" (<code>.art</code>) files.
Article dependencies are specified by "theory" (<code>.thy</code>) files.</p>
<h2>Converting OpenTheory traces to HOLTrace format</h2>
<p>To use <code>ot2holtrace</code>:</p>
<pre><code>./ot2holtrace $HOME/.opentheory/packages base > base.50
</code></pre>
<p>This tool is written in Python.
On <a href="install.html"><code>rome1</code></a>,
running <code>ot2holtrace</code> for <code>base</code> takes 111 seconds and 421MB RAM,
and converts 13.6MB of OpenTheory article files
into a 7.3MB HOLTrace file.</p><hr><font size=1><b>Version:</b>
This is version 2025.06.29 of the "OpenTheory" web page.
</font>
</div>
</body>
</html>