LP

Major Section:  MISCELLANEOUS

To enter the ACL2 command loop from Common Lisp, call the Common Lisp program lp (which stands for ``loop,'' as in ``read-eval-print loop'' or ``command loop.'') The ACL2 command loop is actually coded in ACL2 as the function ld (which stands for ``load''). The command loop is just what you get by loading from the standard object input channel, *standard-oi*. Calling ld directly from Common Lisp is possible but fragile because hard lisp errors or aborts throw you out of ld and back to the top-level of Common Lisp. Lp calls ld in such a way as to prevent this and is thus the standard way to get into the ACL2 command loop. Also see acl2-customization for information on the loading of an initialization file.

All of the visible functionality of lp is in fact provided by ld, which is written in ACL2 itself. Therefore, you should see ld for detailed documentation of the ACL2 command loop. We sketch it below, for novice users.

Every expression typed to the ACL2 top-level must be an ACL2 expression.

Any ACL2 expression may be submitted for evaluation. Well-formedness is checked. Some well-formed expressions cannot be evaluated because they involve (at some level) undefined constrained functions (see encapsulate). In addition, ACL2 does not allow ``global variables'' in expressions to be evaluated. Thus, (car '(a b c)) is legal and evaluates to A, but (car x) is not, because there is no ``global context'' or binding environment that gives meaning to the variable symbol x.

There is an exception to the global variable rule outlined above: single-threaded objects (see stobj) may be used as global variables in top-level expressions. The most commonly used such object is the ACL2 ``current state,'' which is the value of the variable symbol state. This variable may occur in the top-level form to be evaluated, but must be passed only to ACL2 functions ``expecting'' state as described in the documentation for state and for stobjs in general. If the form returns a new state object as one of its values, then that is considered the new ``current'' state for the evaluation of the subsequent form. See state.

ACL2 provides some support for the functionality usually provided by global variables in a read-eval-print loop, namely the saving of the result of a computation for subsequent re-use in another expression. See assign and see @.

If the form read is a single keyword, e.g., :pe or :ubt, then special procedures are followed. See keyword-commands.

The command loop keeps track of the commands you have typed and allows you to review them, display them, and roll the logical state back to that created by any command. See history.

ACL2 makes the convention that if a top-level form returns three values, the last of which is an ACL2 state, then the first is treated as a flag that means ``an error occurred,'' the second is the value to be printed if no error occurred, and the third is (of course) the new state. When ``an error occurs'' no value is printed. Thus, if you execute a top-level form that happens to return three such values, only the second will be printed (and that will only happen if the first is nil!). See ld for details.