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)