Major Section: BOOKS
This documentation topic explains an approach to certifying directories of books, which we call ``classic ACL2 `make'-based certification''.
Warning: The capability described in this section might be replaced at any time by a capability based on corresponding support for community books (see books-certification). If you think that would be a hardship, please contact the ACL2 implementors.
This topic discusses a way to certify a directory of books other than the ACL2 community books. See books-certification for how to certify the set of ACL2 community books. There is also a section in that documentation topic, ``Restricting to Specific Directories and Books'', that provides an alternative to classic ACL2 `make'-based certification (as discussed in the present topic) for certifying specified sets of books.
We assume here a familiarity with Unix/Linux `make'. We also assume that
you are using GNU `make' rather than some other flavor of `make'. And
finally, we assume, as is typically the case by following the standard
installation instructions, that you install the ACL2 community books in the
books/ subdirectory of your ACL2 distribution. We will refer below to
that directory as
In summary: to use `make' to certify books under a given directory, you
may create a simple Makefile in that directory (as explained below) so that
when you stand in that directory, you can submit the command, `make', to
certify those books. If you have a multi-processor machine or the like, then
you can use the `
-j flag `make'-level parallelism by specifying the
number of concurrent processes. For example:
make -j 4For each book
foo.lisp, a file
foo.outin the same directory as
foo.lispwill contain the output from the corresponding certification attempt. If you have previously executed such a command, then you might first want to delete certificate files and other generated files by executing the following command.
Note that when you run `make', then by default, the first error will cause
the process to stop. You can use
make -i to force `make' to ignore
errors, thus continuing past them. Or, use
make -k to keep going, but
skipping certification for any book that includes another whose certification
By default, your acl2-customization file (see acl2-customization) is ignored
by such `make' commands. However, you can specify the use of an
acl2-customization file by setting the value of environment variable
ACL2_CUSTOMIZATION to the empty string, indicating a default such file,
or to the desired absolute pathname. For example:
make ACL2_CUSTOMIZATION='' make ACL2_CUSTOMIZATION='~/acl2-customization.lisp'
We now discuss how to create makefiles to support `make' commands as discussed above.
First we give five steps for creating a
Makefile to support certification
of a directory of books, without subdirectories. For examples of such
Makefiles you can look in community book directories (which, however, might
disappear in future versions of ACL2).
1. Include the file
books/subdirectory of your ACL2 sources directory, but first perhaps define the variable `
ACL2'. Consider the following example.ACL2 ?= /Users/john_doe/acl2/acl2-sources/saved_acl2 include /Users/john_doe/acl2/acl2-sources/books/Makefile-genericIn this example, you can omit the first line, because the default ACL2 executable is file
saved_acl2in the directory immediately above the directory of the specified
Makefile-genericfile. Indeed, that is the common case. Note the use of
:=, so that
ACL2can instead be defined by the environment or provided on the command line as part of the `make' command.
2. (Optional; usually skipped.) Set the
INHIBITvariable if you want to see more than the summary output. For example, if you want to see the same output as you would normally see at the terminal, put this line in your Makefile after the `
include' lines.INHIBIT = (assign inhibit-output-lst (list (quote proof-tree)))For other values to use for
INHIBIT, see set-inhibit-output-lst and see the original setting of
3. Specify the books to be certified. Normally, every file with extension
.lispwill be a book that you want to certify, in which case you can skip this step. Otherwise, put a line in your
Makefileafter the ones above that specifies the books to be certified. The following example, from an old version of community books file
books/finite-set-theory/osets/Makefile, should make this clear.BOOKS = computed-hints fast instance map membership outer primitives \ quantify set-order sets sortBut better yet, use the extension
.lspfor any Lisp or ACL2 files that are not to be certified, so that the definition of
BOOKScan be omitted.
.acl2files for books that are to be certified in other than the initial ACL2 world (see portcullis). For example, if you look in community books file
books/arithmetic/equalities.acl2you will see
defpkgforms followed by a
certify-bookcommand, because it was determined that
defpkgforms were necessary in the certification world in order to certify the
equalitiesbook. In general, for each
<book-name>.lispwhose certification requires a non-initial certification world, you will need a corresponding
<book-name>.acl2file that ends with the appropriate
You also have the option of creating a file
cert.acl2that has a special role. When file
<book-name>.lispis certified, if there is no file
<book-name>.acl2but there is a file
cert.acl2will be used as
<book-name>.acl2would have been used, as described in the preceding paragraph, except that the appropriate
certify-bookcommand will be generated automatically. Thus, no
certify-bookcommand should occur in
It is actually allowed to put raw lisp forms in a
.acl2file (presumably preceded by
(value :q)and followed by
(lp)). But this is not recommended; we make no guarantees about certification performed any time after raw Lisp has been entered in the ACL2 session.
5. Generally, the next step is to include the following line after the `
Makefile-generic(see the first step above).-include Makefile-depsThis will cause `make' to create and then include a file
Makefile-depsthat contains ``dependency'' lines needed by `make'. If those dependencies are somehow flawed, it may be because you have
include-bookforms that are not truly including books, for example in multi-line comments (
#|..|#). These will be ignored if preceded by a semicolon (
;), or if you add a line break after ``
include-book.'' But instead of adding the `
-include' line above, you can create dependency lines yourself by running the commandmake dependenciesand pasting the result into the end of your
Makefile, and editing as you see fit.
This concludes the basic instructions for creating a
Makefile in a
directory including books. Here are some other capabilities offered by
community books file
books/Makefile-subdirs. Not included below is a
discussion of how to increase parallelism by avoiding the need to certify
included books before certifying a given book;
There is support for using `make' to certify books in subdirectories. Consider the following example.
DIRS = pass1 bind-free floor-mod include ../Makefile-subdirsThis indicates that we are to run `make' in subdirectories
floor-mod/of the current directory.
You can combine this subdirectory support with the support already discussed
for certifying books in the top-level directory. Here is an example, which
as of this writing is in community books file
contains the following lines.
arith-top: top all all: top DIRS = pass1 bind-free floor-mod include ../Makefile-subdirs include ../Makefile-generic -include Makefile-depsThe `
top' target is defined in
../Makefile-subdirsto call `make' in each subdirectory specified in
DIRS. We have set the default target in the example above to a new name,
arith-top, that makes that
toptarget before making the `
all' target which, in turn, is the default target in any
Makefile-generic, and is responsible for certifying books in the current directory as discussed in the five steps displayed above.
Makefile-psubdirs instead of
Makefile-subdirs if certification of
a book in a subdirectory never depends on certification of a book in a
different subdirectory, because then the
-j option of `make' can allow
subdirectories to be processed in parallel.
We note that there is a
clean target. Thus,
make cleanwill remove generated files including
.outfiles, and compiled files.
An environment variable
ACL2_SYSTEM_BOOKS is generally set automatically,
so you can probably skip reading the following paragraph unless your attempt
to certify books fails to locate those books properly.
The environment variable
ACL2_SYSTEM_BOOKS can be set to the top-level
directory of the ACL2 community books. A Unix-style pathname, typically
books, is permissible. In most cases, your ACL2
executable is a small script in which you can set this environment variable
just above the line on which the actual ACL2 image is invoked, for example:
export ACL2_SYSTEM_BOOKS ACL2_SYSTEM_BOOKS=/home/acl2/v3-2/acl2-sources/booksHowever, you can also set
ACL2_SYSTEM_BOOKSas a `make' variable, by setting it in your
Makefilebefore the first target definition, e.g.:
ACL2_SYSTEM_BOOKS ?= /home/acl2/v3-2/acl2-sources/books
books/Makefile-generic provides support for compiling books that
are already certified (but see compilation for an exception). For example,
suppose that you have certified books using GCL as the host Lisp, resulting
in compiled files with the
.o extension. Now suppose you would like to
compile the books for Allegro Common Lisp, whose compiled files have the
.fasl extension. The following command will work if you have included
books/Makefile-generic in your
make faslIn general, the compiled file extension for a Lisp supported by ACL2 will be a target name for building compiled files for all your books (after certifying the books, if not already up-to-date on certification).
If you run into problems, you can get help by joining the
list (follow the link from the ACL2 home page) and sending a message to that
list. Also consider trying another version of GNU `make'; for example, we
have found that versions 3.81 and 3.82 sometimes cause errors on Linux where
version 3.80 does not.