-r--r--r-- 4689 holtrace-20250617/doc/html/install.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: Install</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 here">Install
</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 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: Install</div>
<h2>Prerequisites</h2>
<p>The instructions below
have been tested on a server named <code>rome1</code> running Debian 11
with the <code>build-essential</code>, <code>opam</code>, and <code>xdot</code> packages installed,
in a user account that ran</p>
<pre><code>time opam init github git+https://github.com/ocaml/opam-repository.git --disable-sandboxing -a
time opam switch create 5.2.0
time opam install 'hol_light=3.0.0' -y
eval `opam env`
</code></pre>
<p>to install HOL Light 3.0.0 with the OCaml 5.2 bytecode compiler.</p>
<p>The server has two AMD EPYC 7742 CPUs,
but timings reported in this documentation
use only one core (except for <code>holtrace2tex</code>).
Overclocking on the server has been (manually) disabled,
so the CPUs run at 2.245GHz.</p>
<h2>HOLTrace installation</h2>
<p>Make sure you are in the <code>holtrace-*</code> package directory.</p>
<p>Run <code>make -j8</code> to compile the C/C++ tools.</p>
<p>Find the HOL Light installation directory:
e.g.,
<code>$HOME/.opam/5.2.0/lib/hol_light</code>.</p>
<p>Copy <code>holtrace.ml</code> into that directory.</p>
<p>Edit <code>hol_lib.ml</code> in that directory
to add a line</p>
<pre><code>loads "holtrace.ml";;
</code></pre>
<p>after the existing <code>basics.ml</code> line.
This should have no effect on normal HOL Light usage,
but lets you use HOL Light to
<a href="save.html">save</a>
and
<a href="verify.html">verify</a>
traces.</p>
<p>Now <a href="test.html">test</a> the installation.</p><hr><font size=1><b>Version:</b>
This is version 2025.06.16 of the "Install" web page.
</font>
</div>
</body>
</html>