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
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.Even without this problem it is important to enter the ACL2 loop (see lp), for example in order to set the
cbdand (to get more technical) the readtable.
ACL2 provides a ``raw mode'' for execution of raw Lisp forms. In
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
P'' (suggesting something like program mode, but more so).
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
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, includingUpon exiting raw mode, with
logic, are ignored, as are many other
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.
(set-raw-mode nil), the previous setting for guard checking is restored; see set-guard-checking.
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
[Note'' occurs one space
over in the second example, and no result is printed in the third
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>If you have trouble with large structures being printed out, you might want to execute appropriate Common Lisp forms in raw mode, for example,
(setq *print-length* 5)and
(setq *print-level* 5).
Packages. Raw mode disallows the use of
defpkg. If you want to
create a new package, first exit raw mode with
you can subsequently re-enter raw mode with
:set-raw-mode t if you