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
Most people use Emacs (see Emacs
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.,
The ACL2 ``interactive loop'' is called lp (
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
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
If there is a ``
with or without the exclamation mark:
it means you are in
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
or to undo back through the introduction of
ACL2 !>:ubt rev
The first is equivalent to evaluating
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
and you can pop out one level with
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
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
Users of the Emacs interface may occasionally type commands directly in the
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.