Compilation
Compiling ACL2 functions
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 (for example, if you get a raw Lisp error such as ``Wrong FASL
version''):
(set-compiler-enabled nil state)
Remark for users of make-event. If set-compiler-enabled is
invoked during make-event expansion, its effect on state global
variable 'compiler-enabled will persist after evaluation completes for
that make-event form. So for example, one might use the following idiom
in a book so that for all books included on behalf of a given include-book form, no compiled files are loaded, but (optionally) no such
effect takes place for later include-book forms in that book.
(make-event
(pprogn (f-put-global 'saved-compiler-enabled (@ compiler-enabled) state)
(set-compiler-enabled nil state)
(value '(value-triple nil)))
:check-expansion t)
(include-book "my-book")
; optional
(make-event
(pprogn (set-compiler-enabled (@ saved-compiler-enabled) state)
(value '(value-triple nil)))
:check-expansion t)
Upon completion of an invocation of include-book or certify-book, the value of state global variable
'compiler-enabled is restored to the value it had immediately before that
invocation.
See book-compiled-file for more discussion about compilation and
books.
We close with a discussion of a feature that allows control over the
loading of .port files in close analogy to how loading of compiled files
is controlled by set-compiler-enabled, as described above.
(See uncertified-books for a discussion of .port files.) A state global variable, 'port-file-enabled exists for this purpose, and
it is set as follows.
(set-port-file-enabled t state) ; permit loading of .port files (default)
(set-port-file-enabled nil state) ; skip loading of .port files
Just as described above for state global compiler-enabled, the value
of 'port-file-enabled persists after make-event expansion and is
restored after certify-book and include-book. The idiom
displayed above, for avoiding loading of compiled files, can be modified or
extended in the obvious way to avoid loading of .port files.
Subtopics
- Comp
- Compile some ACL2 functions
- The
- Special form for execution efficiency or run-time type checks
- Disassemble$
- Disassemble a function
- Set-compile-fns
- Have each function compiled as you go along.
- Comp-gcl
- Compile some ACL2 functions leaving .c and .h files
- Set-compiler-enabled
- Disable compilation.
