The mechanics of interaction with 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 facilities like defthm.
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. For most
host Common Lisp implementations, if 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). If you are typing to an
Emacs process which is running ACL2 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 normally, you will be put back into
the top level ACL2 command loop. If not, then you may be in a Lisp break, and
you can probably get back into the ACL2 command loop by using an ``abort''
command that depends on the host Common Lisp (e.g., :q for GCL and CCL).
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 process. LP is just a special case of an ACL2 function called
ld , 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 names!
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
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
If the exclamation mark is missing from the prompt,
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 nil
to turn guard checking off and
ACL2 >:set-guard-checking t
to turn it on. Try typing (car 7) to each prompt.
If there is a ``p'' in the prompt,
with or without the exclamation mark:
it means you are in :program ()
mode rather than :logic ()
mode. In :program mode, defun just defines Common Lisp programs
that you can evaluation but it adds no axioms and you cannot use such defined
functions in theorems or invoke defthm. :Program mode 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
For example, to undo the last event you may type
or to undo back through the introduction of rev you may type
ACL2 !>:ubt rev
The 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 t
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 somehow
called LD recursively, the prompt ``gets deeper,'' e.g.,
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 (LP).
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 with :brr nil, and redo whatever defuns and
defthms you did while in that break.
Users of the Emacs interface may occasionally type commands directly in the
*shell* buffer running ACL2. This can be ``dangerous'' for two reasons.
One is that if you type an event, like a defun or 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 defthm below after you've typed the ``(implies (true-listp
x)'' you will confuse the Lisp parser because it has already read
ACL2 !>(defthm 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.