COMP

compile some ACL2 functions 
Major Section:  EVENTS


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 defined ACL2 functions that are currently
                          uncompiled
  :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 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 logic definition will not be compiled; and for (:exec fn), 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 keep these files around for some reason, 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.

:cited-by Programming