), ACL2 prints a summary.
The summary for app is:
At the conclusion of most events (click here for a
brief discussion of events or see events ), ACL2 prints a summary.
The summary for app is:
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
The ``rules'' listed are those used in function admission or proof
summarized. What is actually listed are ``runes'' (see rune) ) which
are list-structured names for rules in the ACL2 database or ``world''
. Using theories you can ``enable'' and ``disable''
rules so as to make them available (or not) to the ACL2 theorem prover.
The ``warnings'' mentioned (none are listed for app) 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.
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 database updates. Despite the fact that ACL2 is an
applicative language it is possible to measure time with ACL2 programs. The
state contains a clock. The times are printed in decimal
notation but are actually counted in integral units. Note that each time is
a runtime, also known as a cpu time, as opposed to being a real time, also
known as a wall clock time.
The final APP is the value of the defun 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 APP), and the final state ).
See ld-post-eval-print for some details. If you really want to
follow that link, however, you might see ld first.
You should now return to the Walking Tour.
