COMP.html -- ACL2 Version 2.7

COMP

compile some ACL2 functions

Major Section:  OTHER

Examples:
:comp t          ; compile all uncompiled ACL2 functions
:comp foo        ; compile the defined function foo
:comp (foo bar)  ; compile the defined functions foo and bar


COMP-GCL -- compile some ACL2 functions leaving .c and .h files





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
  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.