Major Section: OTHER
Examples:
:comp t ; compile all uncompiled ACL2 functions
:comp foo ; compile the defined function foo
:comp (:raw foo) ; compile the raw Lisp version of the defined function foo
but not the corresponding function in the logic
:comp (foo bar) ; compile the defined functions foo and bar
:comp (foo (:raw bar)) ; compile the defined functions foo and bar, but for
; bar do not compile the corresponding function in
; the logic
General Form:
:comp specifier
where specifier is one of the following:
t compile all defined ACL2 functions that are currently
uncompiled
:raw same as t, except that only raw Lisp definitions are
compiled, not executable counterparts (see below)
(name-1 ... name-k) a non-empty list of names of functions defined by
DEFUN in ACL2, except that each name-i can be of
the form (:raw sym), where sym is the name of such
a function
name same as (name)
Note: Unless a single function is specified (either as a symbol or
as a one-element list containing its name), ACL2 will write out
files "TMP.lisp" and "TMP1.lisp" (the latter is for the
executable counterparts; see executable-counterpart) that are
subsequently compiled. An exception is made for :raw, where only
"TMP.lisp" is written out and compiled; executable counterparts
are ignored with :raw. Also see set-compile-fns for a way to
get each function to be compiled as you go along.
As suggested by the examples above, if a function specifier is of the form
(:raw fn), then fn will be compiled in raw Common Lisp but its
corresponding function in the logic (sometimes called its ``*1* function'')
will not be compiled.
