Major Section: EVENTS
Comp is a no-op if explicit compilation is suppressed;
see compilation. The documentation here assumes that this is not the case.
Examples: :comp t ; compile all uncompiled ACL2 functions (comp t) ; same as above, but can be put into a book (comp :exec) ; compile all uncompiled logic (``*1*'') definitions :comp foo ; compile the defined function foo :comp (:raw foo) ; compile the raw Lisp version of the defined function foo but not the corresponding logic definition :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 logic definition
General Form: :comp specifier where specifier is one of the following:
t compile all user-defined ACL2 functions that are currently uncompiled (redefined built-in functions are not recompiled) :exec same as t, except that only logic versions are compiled (see below), not raw Lisp definitions :raw same as t, except that only raw Lisp definitions are compiled, not logic version (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) or (:exec sym), where sym is the name of such a function name same as (name)
When you define a function in ACL2, you are really causing two definitions to be made ``under the hood'' in Common Lisp: the definition is submitted explicitly to raw Lisp, but so is a corresponding ``logic definition''. If guards have not been verified, then only the logic definition will be evaluated; see guards-and-evaluation, in particular the section titled ``Guards and evaluation V: efficiency issues''.
Thus, if you are not verifying guards and you want the benefit of Lisp
compilation for speed and space efficiency, then you may want to place the
(comp :exec) in your books.
Generally it is not necessary to place the form
(comp t), or the form
(comp :raw), in a book, because
certify-book compiles the raw Lisp
definitions anyhow, by default. But you may wish to put
(comp t) or
(comp fn1 fn2 ... fnk) in a book when such a form precedes expensive
calls of functions, for example for proofs involving calls of functions on
large constants, or to support computationally expensive macroexpansion.
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 logic definition will not be compiled; and for
it's the other way around.
The use of
:comp creates various files whose names start with
TMP*'', but then deletes them. If you want to save these files,
(assign keep-tmp-files t).
set-compile-fnsis ignored during
Note that if functions are traced (see trace$), then
comp will first
untrace the functions that are to be compiled, then will do the compile(s),
and finally will re-trace the functions that it untraced (using their
original trace specs). In particular, if you have traced a function and then
you compile it using
:comp, the resulting traced function will be
compiled as well unless you specified
:compile nil in your trace spec;
and after you untrace the function it will definitely run compiled.