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. A non-nil value of this variable -- that is, a nonnil value returned by evaluating (@ compiler-enabled) -- avoids explicit calls to the compiler by default: include-book and certify-book coerce arguments :load-compile-file and compile-flg arguments (respectively) to nil when they are not supplied or have value :DEFAULT, and both comp and set-compile-fns are no-ops. When this is the case, it is because our experience is that performance on the given platform when explicit compilation is suppressed may be slightly better than when the compiler is invoked explicitly. For example, this situation is the case when the underlying Lisp is CCL (OpenMCL). A key is that CCL compiles on-the-fly even when the compiler is not called explicitly, and our observation has been that compiling a file in CCL does not seem to improve appreciably the efficiency of the generated code.

However, you may have reason to want to change the above (default) behavior. To enable compilation of books:

(set-compiler-enabled t state)
To enable compilation of books, with a message printed whenever the compiled file for a book is loaded:
(set-compiler-enabled :verbose state)
To suppress compilation of books:
(set-compiler-enabled nil state)