Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
ACL2 is implemented in Common Lisp. There are many different Common Lisps
and they differ in details relating to interacting with the system. We
sometimes refer to the host Common Lisp as ``raw Lisp.'' The new user is
advised not to operate in raw Lisp as it is possible to, say, redefine ACL2
system faclities like
Most people use Emacs (see Emacs ) or the ACL2 Sedan (Eclipse) interface (see ACL2-Sedan ). They provide protection against certain common mistakes, e.g., trying to edit a block of input text after the operating system has buffered it up and sent it to the Lisp reader which is parsing it as you type. More on this below. In addition, the Sedan provides helpful syntax checking and a disciplined approach to the stack of lemmas generated by The Method. But the variety of interfaces to the variety of Lisps mean that there is great variation in what one must type to interact with ACL2.
The best example is perhaps trying to interrupt a running proof. If your
host Common Lisp is GCL or Allegro and you are typing directly to the Common
Lisp process, then you can interrupt a computation by typing
``ctrl-c'' (hold down the Control key and hit the ``c'' key once). But
other Lisps may require some other control sequence. If you are typing to
an Emacs process which is running the GCL or Allegro Common Lisp process in
a shell buffer, you should type ctrl-c ctrl-c. If you are running the ACL2
Sedan, you can use the Interrupt Session button on the tool bar. The
environment you enter when you interrupt depends on various factors and
basically you should endeavor to get back to the top level ACL2 command
loop, perhaps by typing some kind of Lisp depenent ``abort'' command like
:abort!. You can usually determine what environment
you're in by paying attention to the prompt, which we discuss below.
The ACL2 ``interactive loop'' is called
LP () and is generally
invoked automatically from your Common Lisp when you start up the ACL2
LP is just a special case of an ACL2 function called
, which the user can call from within the ACL2 interactive loop to
enter the loop recursively. New users don't have to know this except that
it helps explain why some commands have the string ``
-ld-'' in their
ACL2 presents itself as a ``read-eval-print'' loop: you're repeatedly prompted for some type-in, which is read, evaluated, and may cause some printing. The prompt tells you something about ACL2's state. In the standard environment, the prompt is
ACL2 !>The ``
ACL2'' tells you that the symbols you use in your command are those defined in the standard ACL2 namespace (or, in the jargon of Lisp, the ``current package,'' see current-package ). You could create a new namespace (see defpkg ) and set the current package to it (see in-package ). The next part of the prompt above (``
!''), the exclamation mark) tells you that before ACL2 evaluates your type-in it will check to see whether
guards () are respected, i.e., whether the functions used in your command are being supplied arguments in their ``expected domains.'' If evaluation is allowed by the guards, it proceeds exactly according to the ACL2 axioms; if evaluation is not allowed, an error is signaled. ACL2 event commands check their arguments thoroughly at run-time, regardless of Lisp's notion of ``expected domains.''
If the exclamation mark is missing from the prompt,
ACL2 >then evaluation occurs strictly according to the ACL2 axioms, without regard for any declared guards.
You can switch between these two prompts by typing
ACL2 !>:set-guard-checking nilto turn guard checking off and
ACL2 >:set-guard-checking tto turn it on. Try typing
(car 7)to each prompt.
If there is a ``
p'' in the prompt,
ACL2 p!>with or without the exclamation mark:
ACL2 p>it means you are in
program() mode rather than
logic() mode. In
defunjust defines Common Lisp programs that you can evaluation but it adds no axioms and you cannot use such defined functions in theorems or invoke
:Programmode is often used to prototype a model.
Most commands are just typical parenthesized Lisp expressions, like
ACL2 !>(defthm rev-rev (implies (true-listp x) (equal (rev (rev x)) x)))but some are typed as keywords followed by a certain number of arguments.
For example, to undo the last event you may type
ACL2 !>:uor to undo back through the introduction of
revyou may type
ACL2 !>:ubt revThe first is equivalent to evaluating
(u)and the second is equivalent to evaluating
(ubt 'rev). See keyword-commands . So if you see a sentence like ``to turn on the break rewrite facility, execute
:brr t,'' we mean type
ACL2 !>:brr tor equivalently
ACL2 !>(brr t)
If you see a prompt that doesn't look like those above you are probably not
typing commands to the standard ACL2 read-eval-print loop! If you've
LD recursively, the prompt ``gets deeper,'' e.g.,
ACL2 !>>and you can pop out one level with
q(for ``quit'') or pop to the outermost ACL2 loop with
abort!. If you are in the outermost call of the ACL2 interactive loop and you type
:q, you pop out into raw lisp. The prompt there is generally different from the ACL2 prompt but that is outside our our control and varies from Lisp to Lisp. We have arranged for many (but not all) Lisps to use a raw lisp prompt involving the string
"[RAW LISP]". To get back into the ACL2 interactive loop from raw lisp, evaluate
If you see a prompt that looks like an ACL2 prompt but has a number in front of it, e.g.,
1 ACL2 >then you're talking to the break rewrite facility (and you are 1 level deep in the example above). Presumably at earlier time in this session you enabled that facility, with
:brr t, installed a monitor on some rule, invoked the prover, entered the break, and forgot. Everything you have done (e.g., lemmas you might have proved with
defthm) inside that break will be lost when you exit the break.
Since the break rewrite facility is ``ours'' we can tell you how to exit it!
To exit our breaks and return to the top-level ACL2 loop, execute
If you discover you've been working in a
brr break, exit, turn off the
break facility wih
:brr nil, and redo whatever
defthms you did while in that break.
Users of the Emacs interface may occasionally type commands directly in the
buffer running ACL2. This can be ``dangerous'' for two reasons. One is that
if you type an event, like a
defthm, directly to the shell,
it will not be recorded in your ``script'' buffer and you may forget it in your
final script. The other is that if you attempt to edit a multi-line command on any
but the most recent line, e.g., to correct the spelling of
after you've typed the ``
(implies (true-listp x)'' you will confuse the
Lisp parser because it has already read ``
ACL2 !>(defth rev-rev (implies (true-listp x)This usually provokes the raw Lisp to enter a low level error break from which you must abort, possibly reenter the ACL2 loop, and re-type the corrected command from scratch.
Another common mistake when using interfaces other than the ACL2 Sedan is to type an ill-formed ACL2 expression containing dots or commas, which also often provokes a break into the raw Lisp's error handler.
The fundamental lesson is that you should pay attention to the prompt and learn what the different prompts mean -- or use the ACL2 Sedan. If you have been working your way through the tutorial introduction to the theorem prover, use your browser's Back Button now to return to introduction-to-the-theorem-prover.