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
|
<html>
<head><title>The_Event_Summary.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>The Event Summary</h2>
<p>
At the conclusion of most events (click <a href="About_the_Prompt.html">here</a> for a
brief discussion of events or see <a href="EVENTS.html">events</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>), ACL2 prints a
summary. The summary for <code>app</code> is:
<pre>
Summary
Form: ( DEFUN APP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
APP
</pre>
<p>
The ``rules'' listed are those used in function admission or proof
summarized. What is actually listed are ``runes'' (see <a href="RUNE.html">rune</a>) <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>)
which are list-structured names for rules in the ACL2 data base or
``<a href="WORLD.html">world</a>'' <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>. Using <a href="THEORIES.html">theories</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> you can ``enable'' and
``disable'' rules so as to make them available (or not) to the ACL2
theorem prover.<p>
The ``warnings'' mentioned (none are listed for <code>app</code>) remind the
reader whether the event provoked any warnings. The warnings
themselves would have been printed earlier in the processing and
this part of the summary just names the earlier warnings printed.<p>
The ``time'' indicates how much processing time was used and is
divided into three parts: the time devoted to proof, to printing,
and to syntactic checks, pre-processing and data base updates.
Despite the fact that ACL2 is an applicative language it is possible
to measure time with ACL2 programs. The <code><a href="STATE.html">state</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> contains a
clock. The times are printed in decimal notation but are actually
counted in integral units.<p>
The final <code>APP</code> is the value of the <code>defun</code> command and was
printed by the read-eval-print loop. The fact that it is indented
one space is a subtle reminder that the command actually returned an
``error triple'', consisting of a flag indicating (in this case)
that no error occurred, a value (in this case the symbol <code>APP</code>),
and the final <code><a href="STATE.html">state</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>). See <a href="LD-POST-EVAL-PRINT.html">ld-post-eval-print</a>
<a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> for some details. If you really want to follow that link,
however, you might see <a href="LD.html">ld</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> first.<p>
You should now return to <a href="Revisiting_the_Admission_of_App.html">the Walking Tour</a>.
<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>
|
