Major Section: SWITCHES-PARAMETERS-AND-MODES
Example Forms: (set-compile-fns t) ; new functions compiled after DEFUN (set-compile-fns nil) ; new functions not compiled after DEFUNNote: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
Also see comp, because it may be more efficient in some Common Lisps to compile many functions at once rather than to compile each one as you go along.
General Form: (set-compile-fns term)where
termis a variable-free term that evaluates to
nil. This macro is equivalent to
(table acl2-defaults-table :compile-fns term)and hence is
localto any books and
encapsulateevents in which it occurs; see acl2-defaults-table. However, unlike the above simple call of the
tableevent function (see table), no output results from a
Set-compile-fns may be thought of as an event that merely sets a
nil. The flag's effect is felt when functions
are defined, as with
defun. If the flag is
t, functions are
automatically compiled after they are defined, as are their
executable counterparts (see executable-counterpart).
Otherwise, functions are not automatically compiled. Exception: The flag has
no effect when explicit compilation is suppressed; see compilation.
set-compile-fns is an event, the old value of the flag is
restored when a
set-compile-fns event is undone.
:set-compile-fns t has been executed, functions are not
individually compiled when processing an
include-book event. If
you wish to include a book of compiled functions, we suggest that
you first certify it with the compilation flag set
(see certify-book) or else compile the book by supplying the appropriate
load-compiled-file argument to
include-book. More generally,
set-compile-fns is suppressed when the state
ld-skip-proofsp has value