Major Section: BOOKS
An effect of compilation is to speed up the execution of the functions defined in a book. Compilation can also remove tail recursion, thus avoiding stack overflows. The presence of compiled code for the functions in the book should not otherwise affect the performance of ACL2. See guard for a discussion; also See compilation.
By default, the certify-book command compiles the book that it
certifies. see certify-book for how to control this behavior.
By default, the include-book command loads the compiled file for the
book. The details of how this loading works are subtle, and do not need to
be understood by most users. The ACL2 source code contains an ``Essay on
Hash Table Support for Compilation'' that explains such details for those
interested. All that users should generally need to know about this is that
the compiled file is always the result of compiling a so-called ``expansion
file'', which contains certain additional code besides the book itself. The
relevance to users of the expansion file is that it can be loaded if the
compiled file is missing (except when :load-compiled-file t is specified
by the include-book form), and its existence is required in order for
include-book to create a book's compiled file, as described below.
Most users can skip the remainder of this documentation topic, which
addresses the uncommon activity of using include-book to compile books.
Include-book can be made to compile a book by supplying its keyword
argument :load-compiled-file the value :comp. However, a compiled
file can only be produced if there is already an expansion file that is
at least as recent as the book's certificate. Such a file, whose name
happens to be the result of concatenating the string "@expansion.lsp"
to the book name (without the ".lisp" suffix), is created by
certify-book when state global variable 'save-expansion-file has a
non-nil value. That will be the case if ACL2 started up when environment
variable ACL2_SAVE_EXPANSION was t (or any value that is not the
empty string and whose string-upcase is not "NIL"), until the
time (if any) that 'save-expansion-file is assigned a different value by
the user. In most respects, the :comp setting is treated exactly the
same as :warn; but after all events in the book are processed, the
expansion file is compiled if a compiled file was not loaded, after which the
resulting compiled file is loaded.
One can thus, for example, compile books for several different host Lisps
-- useful when installing ACL2 executables at the same site that are built
on different host Lisps. A convenient way to do this in an environment that
provides Gnu `make' is to certify the community books using the shell
command ``make regression'' in the acl2-sources/ directory, after
setting environment variable ACL2_SAVE_EXPANSION to t, and then
moving to the books directory and executing the appropriate `make'
commands to compile the books (targets fasl, o, and so on, according
to the compiled file extension for the host Lisp).
We conclude by saying more about the :load-compiled-file argument of
include-book. We assume that state global 'compiler-enabled
has a non-nil value; otherwise :load-compiled-file is always treated
as nil.
We do not consider raw mode below (see set-raw-mode), which presents a
special case: ACL2 will attempt to load the book itself whenever it would
otherwise load the expansion or compiled file, but cannot (either because the
:load-compiled-file argument is nil, or for each of the expansion and
compiled files, either it does not exist or it is out of date with respect to
the .cert file).
The :load-compiled-file argument is not recursive: calls of
include-book that are inside the book supplied to include-book use
their own :load-compiled-file arguments. However, those subsidiary
include-book calls can nevertheless be sensitive to the
:load-compiled-file arguments of enclosing include-book calls, as
follows. If :load-compiled-file has value t, then every subsidiary
include-book is required to load a compiled file. Moreover, if a book's
compiled file or expansion file is loaded in raw Lisp, then an attempt will
be made to load the compiled file or expansion file for any
include-book form encountered during that load. If that attempt fails,
then that load immediately aborts, as does its parent load, and so on up the
chain. If, when going up the chain, an include-book is aborted for
which keyword argument :load-compiled-file has value t, then an error
occurs.
When loading a book's compiled file or expansion file, FILE, it is
possible to encounter an include-book form for a book that has no
suitable compiled file or expansion file. In that case, the load of FILE
is aborted at that point. Similarly, the load of FILE is aborted in the
case that this include-book form has a suitable compiled file or
expansion file whose load is itself aborted. Thus, whenever any
include-book aborts, so do all of its parent include-books, up the
chain. Such an abort causes an error when the include-book form
specifies a :load-compiled-file value of t.
