control checking guards during execution of top-level forms
Major Section:  OTHER

The top-level ACL2 loop has a variable which controls which sense of execution is provided. To turn ``guard checking on,'' by which we mean that guards are checked at runtime, execute the top-level form :set-guard-checking t. To turn it off, do :set-guard-checking nil. The status of this variable is reflected in the prompt.

ACL2 !>
means guard checking is on and
ACL2 >
means guard checking is off. The exclamation mark can be thought of as ``barring'' certain computations. The absence of the mark suggests the absence of error messages or unbarred access to the logical axioms. Thus, for example
ACL2 !>(car 'abc)
will signal an error, while
ACL2 >(car 'abc)
will return nil.

Whether guards are checked during evaluation is independent of the default-defun-mode. We note this simply because it is easy to confuse ``:program mode'' with ``evaluation in Common Lisp'' and thus with ``guard checking on;'' and it is easy to confuse ``:logic mode'' with ``evaluation in the logic'' and with ``guard checking off.'' But the default-defun-mode determines whether newly submitted definitions introduce programs or add logical axioms. That mode is independent of whether evaluation checks guards or not. You can operate in :logic mode with runtime guard checking on or off. Analogously, you can operate in :program mode with runtime guard checking on or off.

However, one caveat is appropriate: functions introduced only as programs have no logical definitions and hence when they are evaluated their Common Lisp definitions must be used and thus their guards (if any) checked. That is, if you are defining functions in :program mode and evaluating expressions containing only such functions, guard checking may as well be on because guards are checked regardless. This same caveat applies to a few ACL2 system functions that take state as an argument. This list of functions includes all the keys of the alist *super-defun-wart-table* and all function whose names are members of the list *initial-untouchables*.

See guard for a general discussion of guards.