1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
<html>
<head><title>TRACE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h1>TRACE</h1>tracing functions in ACL2
<pre>Major Section: <a href="acl2-doc-major-topics.html">ACL2 Documentation</a>
</pre><p>
ACL2 provides utilities that rely on the underlying Lisp image to trace
functions. There are two interfaces to the underlying lisp trace:
<blockquote><p>
o Macros <code><a href="TRACE$.html">trace$</a></code> and <code><a href="UNTRACE$.html">untrace$</a></code> call the underlying Lisp's <code>trace</code>
and <code>untrace</code>, respectively. See <a href="TRACE$.html">trace$</a> and see <a href="UNTRACE$.html">untrace$</a>.<p>
o Macro <code><a href="WITH-ERROR-TRACE.html">with-error-trace</a></code>, or <code><a href="WET.html">wet</a></code> for short, provides a backtrace
showing function calls that lead to an error. See <a href="WET.html">wet</a>.<p>
</blockquote>
NOTES:<p>
1. <code><a href="WET.html">Wet</a></code> turns off all tracing (i.e., executes Lisp <code>(untrace)</code>) other
than temporarily doing some tracing under-the-hood in the evaluation of the
form supplied to it.<p>
2. The underlying Lisp <code>trace</code> and <code>untrace</code> utilities have been modified
for GCL and Allegro CL to trace the executable counterparts. Other Lisps may
give unsatisfying results. For GCL and Allegro CL, you can invoke the
original <code>trace</code> and <code>untrace</code> by exiting the ACL2 loop and invoking
<code>old-trace</code> and <code>old-untrace</code>, respectively..<p>
3. Trace output for <code><a href="TRACE$.html">trace$</a></code> and <code><a href="UNTRACE$.html">untrace$</a></code> can be redirected to a
file. See <a href="OPEN-TRACE-FILE.html">open-trace-file</a> and see <a href="CLOSE-TRACE-FILE.html">close-trace-file</a>. However, the backtrace
printed by <code><a href="WET.html">wet</a></code> always goes to <code><a href="STANDARD-CO.html">standard-co</a></code>.
<p>
<ul>
<li><h3><a href="BREAK-ON-ERROR.html">BREAK-ON-ERROR</a> -- break when encountering a hard or soft error caused by ACL2.
</h3>
</li>
<li><h3><a href="CLOSE-TRACE-FILE.html">CLOSE-TRACE-FILE</a> -- stop redirecting trace output to a file
</h3>
</li>
<li><h3><a href="OPEN-TRACE-FILE.html">OPEN-TRACE-FILE</a> -- redirect trace output to a file
</h3>
</li>
<li><h3><a href="TRACE$.html">TRACE$</a> -- trace the indicated functions
</h3>
</li>
<li><h3><a href="UNTRACE$.html">UNTRACE$</a> -- untrace functions
</h3>
</li>
<li><h3><a href="WET.html">WET</a> -- evaluate a form and print subsequent error trace
</h3>
</li>
<li><h3><a href="WITH-ERROR-TRACE.html">WITH-ERROR-TRACE</a> -- evaluate a form and print subsequent error trace
</h3>
</li>
</ul>
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
