Comp
Compile some ACL2 functions
NOTE: Comp is a no-op if explicit compilation is suppressed;
see compilation. The documentation here assumes that this is not the
case. See evaluation for background on executable-counterpart and
submitted functions.
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 executable-counterpart definitions
:comp foo ; compile the defined function foo (both its submitted and
; executable-counterpart functions)
:comp (:raw foo) ; compile the submitted function for the defined function foo
; but not the corresponding executable-counterpart
: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 executable-counterpart
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 executable-counterparts
are compiled (see below), not submitted definitions
:raw same as t, except that only submitted definitions are
compiled, not executable-counterparts
(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 executable-counterpart; see
evaluation. If guards have not been verified, then only the
executable-counterpart will be evaluated; see evaluation and 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 form (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 executable-counterpart definition will not be compiled; and for
(:exec fn), it's the other way around.
The use of :comp may create various files whose names start with
``TMP*'', but it then deletes them. If you want to save these files,
evaluate (assign keep-tmp-files t).
Also see set-compile-fns for a way to compile each function as it is
defined. But note that set-compile-fns is ignored during include-book.
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.
We conclude with a technical remark only for those who use trust tags to
write raw Lisp code. :Comp generally creates files to compile unless it
is given a single function to compile. Those files contain the ACL2
definitions of all functions to compile, omitting those in the lists obtained
by evaluating the forms (@ logic-fns-with-raw-code) and (@
program-fns-with-raw-code). :Comp skips compilation for functions that
are already compiled, as is typically the case when you redefine functions in
raw Lisp using include-raw. But if you define interpreted (as opposed
to compiled) functions with raw Lisp code, say by using trust tags (see defttag) and progn!, then you are advised to add all such symbols to
one of the lists stored in the two state globals above: to
logic-fns-with-raw-code if the function symbol is in :logic
mode, else to program-fns-with-raw-code. Then, instead of the
corresponding ACL2 definition (without raw Lisp code) being written to a file,
the function symbol will be passed directly to the Lisp compile function.
Note that the above two state globals are both untouchable, so you may need to
deal with that before modifying them, for example as follows (also see remove-untouchable).
(defttag t)
(progn!
:state-global-bindings
((acl2::temp-touchable-vars t acl2::set-temp-touchable-vars))
(f-put-global 'acl2::logic-fns-with-raw-code
(cons 'my-fn (@ acl2::logic-fns-with-raw-code))
state))
