compiling ACL2 functions
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:
(set-compiler-enabled nil state)

See book-compiled-file for more discussion about compilation and books.