BOOKS-CERTIFICATION

certifying ACL2 community books 
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.

The Basics

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 --version to 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 executable. 

make regression
Better yet, save a log file in case there are problems, for example as follows. 
(make regression) >& make-regression.log
or perhaps better yet: 
(time nice make regression) >& make-regression.log
For the sake of brevity, below we'll skip mentioning any of `time', `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 books/workshops/, use target `certify-books' instead of target `regression', for example as follows. 

(time nice make certify-books) >& make-certify-books.log

Whether you use target `regression' or target `certify-books', then 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 setting variable 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

Cleaning

You can delete files generated by book certification (including .cert files, .out files, compiled files, and more) by issuing the following command (again, in your ACL2 sources directory). 

make clean-books
If 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 books directory. 

DIR/clean.pl
For 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 variables EXCLUDED_PREFIXES, ACL2_BOOK_CERTS, or ACL2_BOOK_DIRS. 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 EXCLUDED_PREFIXES. Then ACL2_BOOK_CERTS and ACL2_BOOK_DIRS, if supplied, specify which books should be certified, as illustrated by the following example. 

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 symbolic and paco will be certified, as will the books workshops/2006/cowles-gamboa-euclid/Euclid/ed6a.lisp and 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 .cert extension used in files supplied for ACL2_BOOK_CERTS.

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 or ~/acl2/books/cert.pl. 

cert.pl -j 4 *.lisp
Here 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 .cert files that are not under the current directory will also be built. For documentation of cert.pl invoke: 
cert.pl -h
See the top of cert.pl for 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 line (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 directory, not saved_acl2h as one might expect for ACL2(h)(p), respectively. So probably you'll want to supply ``ACL2=<your_acl2>'' explicitly with your `make' command.

The comments above also pertain pertain to using ACL2(p) (see parallel); the default is 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, see waterfall-parallelism-for-book-certification.

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, substitute target regression-nonstd for target regression. The default executable (when ACL2 is not specified) will be file saved_acl2r in your ACL2 sources directory, rather than saved_acl2.

Provisional Certification

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

Miscellany

Other control of the certification process may be found by perusing community books file books/make_cert. In particular, the INHIBIT variable 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) ACL2 session. 

time nice make regression -j 4 ACL2_BOOK_DIRS=arithmetic \
  INHIBIT='(set-inhibit-output-lst proof-tree)'

Troubleshooting

If you run into problems, you can get help by joining the acl2-help email 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.