creating and loading of compiled and expansion files for books
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.