INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS

the mechanics of interaction with the theorem prover 
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 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. 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 A or :q, or :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 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 

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 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, 

ACL2 p!>
with or without the exclamation mark: 
ACL2 p>
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 arguments.

For example, to undo the last event you may type 

ACL2 !>:u
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
or 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 somehow called 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 (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 :abort!.

If you discover you've been working in a brr break, exit, turn off the break facility wih :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 ``(defth rev-rev''. 

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.