Set-compile-fns
Have each function compiled as you go along.
Example Forms:
(set-compile-fns t) ; new functions compiled after DEFUN
(set-compile-fns nil) ; new functions not compiled after DEFUN
Note: 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 term is a variable-free term that evaluates to t or
nil. This macro is equivalent to
(table acl2-defaults-table :compile-fns term)
and hence is local to any books and encapsulate
events in which it occurs; see ACL2-defaults-table. However,
unlike the above simple call of the table event function (see table), no output results from a set-compile-fns event.
Set-compile-fns may be thought of as an event that merely sets a flag
to t or 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
evaluation). Otherwise, functions are not automatically compiled.
Exception: The flag has no effect when explicit compilation is suppressed; see
compilation.
Because set-compile-fns is an event, the old value of the flag is
restored when a set-compile-fns event is undone.
Even when :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, compilation via
set-compile-fns is suppressed when the state global variable
ld-skip-proofsp has value 'include-book.
