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 'suppress-compile is set automatically when the system is built, according to the underlying Lisp implementation. A non-nil value of this variable -- that is, a nonnil value of (@ suppress-compile) -- avoids all explicit calls to the compiler: include-book and certify-book coerce their compilation arguments to nil, 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 OpenMCL. A key is that OpenMCL compiles on-the-fly even when the compiler is not called explicitly, and compiling a file in OpenMCL (at least as of early 2007) does not seem to improve appreciably the efficiency of the generated code.