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 barNote: Unless a single function is specified (either as a symbol or as a one-element list containing its name), ACL2 will write out 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)
"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.