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.