Enter or exit ``raw mode,'' a raw Lisp environment
Below we discuss raw-mode. In brief: The simplest way to turn
raw-mode on is
ACL2 users often find its careful syntax checking to be helpful during code
development. Sometimes it is even useful to do code development in
However, loading code using include-book is much slower than using
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 cbd and (to get more technical) the readtable.
ACL2 provides a ``raw mode'' for execution of raw Lisp forms. In this
mode, include-book reduces essentially to a Common Lisp
:set-raw-mode t ; turn raw mode on :set-raw-mode-on! ; same as above, but no trust tag required :set-raw-mode nil ; turn raw mode off
The way you can tell that you are in raw mode is by looking at the prompt
(see default-print-prompt), which uses a capital ``
Typical benefits of raw mode are fast loading of source and compiled files and the capability to hack arbitrary Common Lisp code in an environment with the ACL2 sources loaded (and hence with ACL2 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, but also see break-on-error and break$. However, it probably is generally best to avoid raw mode unless these advantages seem important. We expect the main benefit of raw mode to be in deployment of applications, where raw Lisp code may be useful, and where load time is much faster than the time required for a full-blown include-book — but not that the fast loading of books and treatment of hard errors discussed above may be useful during development.
Raw mode is also useful for those who want to build extensions of ACL2. For example, the following form can be put into a certifiable book to load an arbitrary Common Lisp source or compiled file.
(progn (defttag my-application) (progn! (set-raw-mode t) (load "some-file")))
Also see include-raw with-raw-mode, defttag, and progn!.
Below are several disadvantages to using raw mode. These should discourage
users from using it for general code development, as
We conclude with some details.
Printing results. The rules for printing results are mostly unchanged for raw mode, even to the point of attempting appropriate printing for state and stobjs (though this is merely heuristic when the top-level function is defined in raw mode), for example as follows.
ACL2 !>(defstobj st fld) Summary Form: ( DEFSTOBJ ST ...) Rules: NIL Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) ST ACL2 !>(set-raw-mode-on!) TTAG NOTE: Adding ttag :RAW-MODE-HACK from the top level loop. ACL2 P>(defun f (st) st) F ACL2 P>(f st) <st> ACL2 P>(defun g (st state) (mv 3 st state)) G ACL2 P>(g st state) (3 <st> <state>) ACL2 P>(defun h (state) (mv nil 17 state)) H ACL2 P>(h state) ; notice the leading space; see below 17 ACL2 P>
There is however one major exception. If the value to be printed contains
any Lisp object that is not a legal ACL2 object, then the
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,
Evaluation in raw mode attempts to maintain global stobjs, but may not accommodate arbitrary raw Lisp hacks that hide the stobj returned by ACL2. This can happen in two cases: when array resizing is used on the unique (array) field of a stobj, and when swap-stobjs is used. Consider for example the following log. Evaluation behaves nicely for all forms except the last, where resizing seems not to have taken effect as explained after the log, below.
ACL2 !>(defstobj st fld) Summary Form: ( DEFSTOBJ ST ...) Rules: NIL Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) ST ACL2 !>(defstobj st2 (ar :type (array t (8)) :resizable t)) Summary Form: ( DEFSTOBJ ST2 ...) Rules: NIL Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) ST2 ACL2 !>(set-raw-mode-on!) TTAG NOTE: Adding ttag :RAW-MODE-HACK from the top level loop. ACL2 P>(progn (update-fld 3 st) 17) 17 ACL2 P>(resize-ar 20 st2) <st2> ACL2 P>(ar-length st2) 20 ACL2 P>(progn (resize-ar 30 st2) 17) 17 ACL2 P>(ar-length st2) ; Should be 30, but it's not! 20 ACL2 P>
The reason for the last form's ``wrong'' result (and the other ``correct''
results) is technical. A stobj with a single array field is exactly that
array in raw Lisp (except in some cases where that may be an array of
characters), in which case resizing completely replaces the stobj in the
global structure that stores the global stobj values. The use of raw-Lisp
Include-book. The events add-include-book-dir, add-include-book-dir!, delete-include-book-dir, and delete-include-book-dir! have been designed to work with raw mode. However, if you enter raw mode and then evaluate such forms, then the effects of these forms will disappear when you exit raw mode, in which case you can expect to see a suitable warning. Regarding include-book itself: it should work in raw mode as you might expect, at least if a compiled file or expansion file was created when the book was certified; see certify-book.