SET-RAW-MODE

Major Section:  OTHER

ACL2 users often find its careful syntax checking to be helpful during code development. Sometimes it is even useful to do code development in :logic mode, where ACL2 can be used to check termination of (mutually) recursive functions, verify guards, or even prove properties of the functions.

However, loading code using include-book is much slower than using Common Lisp load in raw Lisp, and in this sense ACL2 can get in the way of efficient execution. Unfortunately, it is error-prone to use ACL2 sources (or their compilations) in raw Lisp, primarily because a number of ACL2 primitives will not let you do so. Perhaps you have seen this error message when trying to do so:

HARD ACL2 ERROR in ACL2-UNWIND-PROTECT:  Apparently you have tried
to execute a form in raw Lisp that is only intended to be executed
inside the ACL2 loop.

ACL2 provides a ``raw mode'' for execution of raw Lisp forms. In this mode, include-book reduces essentially to a Common Lisp load. More generally, the ACL2 logical world is not routinely extended in raw mode (some sneaky tricks are probably required to make that happen). To turn raw mode off or on:

:set-raw-mode t   ; turn raw mode on
:set-raw-mode nil ; turn raw mode off

• ADD-RAW-ARITY -- add arity information for raw mode

• REMOVE-RAW-ARITY -- remove arity information for raw mode

ACL2 P>

The main benefits of raw mode are fast loading of source (or compiled) files and the capability to hack arbitrary Common Lisp code in an environment with the ACL2 sources loaded (and hence its primitives available). In addition, ACL2 hard errors will put you into the Lisp debugger, rather than returning you to the ACL2 loop, and this may be helpful for debugging; see hard-error and see illegal. However, we do not recommend using raw mode unless these advantages seem important. We expect the main benefit of raw mode to be in deployment of applications, where load time is much faster than the time required for a full-blown include-book, although in certain cases the fast loading of books and treatment of hard errors discussed above may be useful during development.

Below are several disadvantages to raw mode. These should discourage users from using it for general code development, as :program mode is generally preferable.

-- Forms are in essence executed in raw Lisp.  Hence:
   -- Syntax checking is turned off (a big loss during code
      development!); and
   -- Guard checking is COMPLETELY disabled.
-- Table events, including logic, are ignored, as are many
   other events, including defthm.
-- All soundness claims are withdrawn for any ACL2 session in which
   raw mode was ever entered.
-- No book may be certified after raw mode has been entered, even if
   you later leave raw mode.

We conclude with some details.

Printing results. The rules for printing results are unchanged for raw mode, with one exception. If the value to be printed would contain any Lisp object that is not a legal ACL2 object, then the print routine is used from the host Lisp, rather than the usual ACL2 printing routine. The following example illustrates the printing used when an illegal ACL2 object needs to be printed. Notice how that ``command conventions'' are observed (see ld-post-eval-print); the ``[Note'' occurs one space over in the second example, and no result is printed in the third example.

ACL2 P>(find-package "ACL2")
[Note:  Printing non-ACL2 result.]
#<The ACL2 package> 
ACL2 P>(mv nil (find-package "ACL2") state)
 [Note:  Printing non-ACL2 result.]
#<The ACL2 package> 
ACL2 P>(mv t (find-package "ACL2") state)
ACL2 P>(mv 3 (find-package "ACL2"))
[Note:  Printing non-ACL2 result.]
(3 #<The ACL2 package>) 
ACL2 P>

Packages. Raw mode disallows the use of defpkg. If you want to create a new package, first exit raw mode with :set-raw-mode nil; you can subsequently re-enter raw mode with :set-raw-mode t if you wish.