Books-certification-alt
Alternate instructions for certifying the community-books,
from the perspective of the acl2-sources directory.
WARNING: Parts of this documentation are probably obsolete, but parts
are still relevant. See books-certification as the primary source of
information on how to certify the community-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/GNUmakefile, in the
community books, for more about ``Credits and History'', and for additional
technical details not covered in this topic.
For more information about installing ACL2, see the ACL2 installation instructions. 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.
- Gnu `make' is available on your system via the `make' command
(rather than some other flavor of `make'). (Execute `make --version to
verify this.)
- You have built or obtained an ACL2 executable.
- 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.
Note: 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 git, then you will have a
directories such books/workshops/ that is not necessary for certifying
the most widely-included books. You can certify just such books as
follows.
(time nice make basic) >& make-basic.log
Whether you use target `regression' or target `basic', 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
Alternatively, if you want to cause such deletion and then do a regression,
simply replace the `regression' target by `regression-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).
cert.pl --pcert-all -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 Variants of ACL2
The discussion above also pertains to using ACL2(p) (see parallel)
or ACL2(r) (see real), in which case the default is saved_acl2p or
saved_acl2r respectively, rather than saved_acl2. However, we
recommend that you use ACL2, not ACL2(p), for your regression. Then you can
use ACL2(p) for your own proof developments. However, if you want to use
ACL2(p) or for your regression, see waterfall-parallelism-for-book-certification.
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.
