Major Section: BOOKS
For background on the ACL2 community books, see community-books. Here we
explain how to certify those books, or some of those books, with ACL2. We
thank Bishop Brock, Jared Davis, and Sol Swords for their substantial
contributions to this methodology. See
books/Makefile, in the community
books, for more about ``Credits and History'', and for additional technical
details not covered in this topic (for example, how to build a local copy of
the xdoc manual for those who may wish to do that).
For more information about installing ACL2, see the installation instructions, either by following a link from the ACL2 home page or by going directly to the page http://www.cs.utexas.edu/users/moore/acl2/current/installation/installation.html. For information about so-called ``classic ACL2 `make'-based certification'', which provides support for certifying directories of books but may disappear in a future ACL2 release, see books-certification-classic.
We make the following assumptions.
o Gnu `make' is available on your system via the `make' command (rather than some other flavor of `make'). (Execute `
make --versionto verify this.)
o You have built or obtained an ACL2 executable.
o The ACL2 community books are installed in the
books/subdirectory of your ACL2 distribution, as is the case when you have followed the standard installation instructions.
o All commands shown below are issued in the top-level (ACL2 sources) directory of your ACL2 distribution.
By default the ACL2 executable is file
saved_acl2 in your ACL2 sources
directory, and you can issue the following command to the shell in order to
do a ``regression run'' that certifies all of the community books using that
make regressionBetter yet, save a log file in case there are problems, for example as follows.
(make regression) >& make-regression.logor perhaps better yet:
(time nice make regression) >& make-regression.logFor the sake of brevity, below we'll skip mentioning any of `
nice', or `
>& make-regression.log'. But saving a log file, in particular, is useful in case you encounter problems to report.
If you fetched the community books using svn, then you will have a directory
books/workshops/ that is not necessary for certifying the other books.
If you want to skip certification of the books under
use target `
certify-books' instead of target `
example as follows.
(time nice make certify-books) >& make-certify-books.log
Whether you use target `
regression' or target `
for each book
foo.lisp whose certification is attempted, a file
foo.cert.out in the same directory will contain the output from the
book's certification attempt.
A regression run may take a few hours, but if you have a multiprocessing
computer, you can speed it up by certifying some books in parallel, by
providing a value for `make' option
-j. For example, if you have 8
hardware threads then you might want to issue the following command.
make regression -j 8
Specifying the ACL2 Executable
If your ACL2 executable is not file
saved_acl2 in the ACL2 sources
directory, then you will need to specify that executable. You can do that by
ACL2, either as an environment variable or, as displayed
below, as a `make' variable. Either way, you will need to avoid relative
pathnames. For example, the first two forms below are legal, but the third
is not, assuming that
my-acl2 is on your
PATH in a Unix-like
environment (e.g., linux or MacOS) and that
my-saved_acl2 is just a
pathname relative to your ACL2 sources directory, which is not on your path.
make regression -j 8 ACL2=my-acl2 make regression -j 8 ACL2=/u/smith/bin/acl2 # The following only works if my-saved_acl2 is on your path (see above). make regression -j 8 ACL2=my-saved_acl2
You can delete files generated by book certification (including
.out files, compiled files, and more) by issuing the following
command (again, in your ACL2 sources directory).
make clean-booksIf you want to cause such deletion and then do a regression, simply replace the `
regression' or `
certify-books' target by `
regression-fresh' or `
certify-books-fresh', respectively, for example as follows. follows.
make -j 4 regression-fresh make -j 4 certify-books-fresh
If however you only want to clean up generated files residing under a given
directory (or its subdirectories, and recursively), you can issue the
following command while standing in that directory, where
DIR is a
pathname of your
DIR/clean.plFor example, to clean up generated files under
books/arithmetic, you could do the following.
cd books/arithmetic ../clean.pl cd - # to return to the ACL2 sources directory, if you wish to do so
Restricting to Specific Directories and Books
You can specify which books you want certified by using any or all of the
First, the set of desired
.cert files is restricted to those that do not
start with any string that is one of the words in the value of
supplied, specify which books should be certified, as illustrated by the
make -j 8 regression-fresh \ ACL2_BOOK_DIRS="symbolic paco" \ ACL2_BOOK_CERTS=" \ workshops/2006/cowles-gamboa-euclid/Euclid/ed6a.cert \ workshops/2006/cowles-gamboa-euclid/Euclid/ed4bb.cert \ "Then all book in directories
pacowill be certified, as will the books
workshops/2006/cowles-gamboa-euclid/Euclid/ed4bb.lisp. Note that all pathnames should be relative to your community books directory; in particular, they should not be absolute pathnames. Also notice the
.certextension used in files supplied for
Alternatively, you may wish to invoke
books/cert.pl while standing in a
directory under which you want to certify books. This will certify not only
those books, but all supporting books -- even those not under the current
directory -- that do not have up-to-date
.cert files. The following is
a simple command to invoke that will certify all books in the current
directory, where if the
books/ directory is not on your path, you will
need to provide a suitable filename, e.g.
cert.pl -j 4 *.lispHere is a more complex command, which illustrates a way to certify books in subdirectories (as well as the current directory), the use of provisional certification (see provisional-certification), and `make'-level parallelism (in this case specifying four parallel processes).
ACL2_PCERT=t cert.pl -j 4 `find . -name '*.lisp'`Note that with this approach, unlike classic ACL2 `make'-based certification (see books-certification-classic, out-of-date
.certfiles that are not under the current directory will also be built. For documentation of
cert.pl -hSee the top of
cert.plfor authorship and copyright information.
Finally, we give a brief summary of how to use so-called ``classic ACL2
`make'-based certification'' for community books;
see books-certification-classic for details. Note that support for this
approach might be eliminated in a future ACL2 release. We welcome comments
from the ACL2 community about whether or not that would be a good thing to
do. See the discussion above about
ACL2_BOOK_DIRS for the ``modern'' way
to accomplish the same thing.
Many community book directories have a
Makefile. If you modify books
only in such a directory, you can recertify by standing in that directory and
issuing a `make' command. This command can optionally specify an ACL2
executable as well as parallelism, for example as follows, where the first
make clean) is optional.
make clean (time nice make -j 8 ACL2=my-acl2)
ACL2 Customization Files
By default, your acl2-customization file (see acl2-customization) is ignored
by all flavors of ``
make regression''. 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 regression ACL2_CUSTOMIZATION='' make regression ACL2_CUSTOMIZATION='~/acl2-customization.lisp'
Regressions for Experimental Extensions of ACL2
The instructions are unchanged if you are using ACL2(h)
(see hons-and-memoization). However, note that the default executable (when
ACL2 is not specified) remains
saved_acl2 in your ACL2 sources
saved_acl2h as one might expect for ACL2(h)(p),
respectively. So probably you'll want to supply ``
explicitly with your `make' command.
The comments above also pertain pertain to using ACL2(p) (see parallel); the
saved_acl2 rather than
saved_acl2p. However, we recommend
that you use ACL2, not ACL2(p), for your regression. Then you can use
ACL2(p) for your own proof developments. (The analogous comment applies to
ACL2(hp), which combines capabilities of ACL2(h) and ACL2(p), i.e., we
recommend that you use ACl2(h) for your regression in that case.) However,
if you want to use ACL2(p) or ACL2(hp) for your regression,
If you intend to certify books in the
nonstd subdirectory of the
community books, you will want to use ACL2(r) (see real). In that case,
regression-nonstd for target
default executable (when
ACL2 is not specified) will be file
saved_acl2r in your ACL2 sources directory, rather than
To use provisional certification (see provisional-certification), supply
ACL2_PCERT=t with your `make' command. Here is an example.
time nice make regression -j 4 ACL2_BOOK_DIRS=deduction ACL2_PCERT=t
Other control of the certification process may be found by perusing community
books/make_cert. In particular, the
may be set to a call of
set-inhibit-output-lst, for example as
follows to obtain the output one would get by default in an (interactive)
time nice make regression -j 4 ACL2_BOOK_DIRS=arithmetic \ INHIBIT='(set-inhibit-output-lst proof-tree)'
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. Note however that Version 3.80 does not print certain
informational messages that are printed by later versions.