Book-compiled-file
Creating and loading of compiled and expansion files for 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's filename after removing 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.
