Major Section: PROGRAMMING
ACL2 has several mechanisms to speed up the evaluation of function calls by compiling functions: see comp, see set-compile-fns, and see certify-book. The intention is that compilation never changes the value returned by a function call, though it could cause the call to succeed rather than fail, for example by avoiding a stack overflow.
The state global variable 'compiler-enabled is set automatically
when the system is built, and may depend on the underlying Lisp
implementation. (In order to disable the compiler at build time, which will
defeat the speed-up but usually be pretty harmless when the host Lisp is CCL
or SBCL, see the discussion of ACL2_COMPILER_DISABLED in distributed file
GNUmakefile.) The value of 'compiler-enabled, as returned by
(@ compiler-enabled), can be t, :books, or nil. If the value
is nil, then include-book and certify-book coerce their
arguments :load-compile-file and compile-flg arguments (respectively)
to nil. Otherwise, the value is :books or t and there is no such
coercion; but if the value is not t, then comp and
set-compile-fns are no-ops, which is probably desirable for Lisps such
as CCL and SBCL that compile on-the-fly even when the compiler is not
explicitly invoked.
However, you may have reason to want to change the above (default) behavior.
To enable compilation by default for certify-book and
include-book but not for comp or set-compile-fns:
(set-compiler-enabled :books state)To enable compilation not only as above but also for
comp and
set-compile-fns:
(set-compiler-enabled t state)To suppress compilation and loading of compiled files by
include-book
(for example, if you get a raw Lisp error such as ``Wrong FASL version''):
(set-compiler-enabled nil state)
See book-compiled-file for more discussion about compilation and books.
