REGRESSION

Major Section:  BOOKS

Here we provide a concise summary of how to certify the ACL2 community books when you install ACL2. 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 more information about the ACL2 community books and how to certify them, see community-books and see book-makefiles.

The Basics

We assume that you have built or obtained an ACL2 executable, that the ACL2 community books are in subdirectory books/, and that you are standing in the ACL2 sources directory. If you built that executable, then by default its name is saved_acl2, and you can issue the following command to the shell.

  make regression

  (make regression) >& make-regression.log

  (time nice make regression) >& make-regression.log

Such a certification run may take a few hours, but if you have a multiprocessing computer, you can speed it up by specifying a value for ACL2_JOBS. For example, if you have 8 hardware threads then you might want to issue the following command.

  make regression ACL2_JOBS=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 ACL2_JOBS=8 ACL2=my-acl2
  make regression ACL2_JOBS=8 ACL2=/u/smith/bin/acl2
  # The following is unlikely to work (see above).
  make regression ACL2_JOBS=8 ACL2=my-saved_acl2

Regressions for Experimental Extensions of ACL2

The instructions are similar if you are using ACL2(h), the experimental extension supporting hash-cons, function memoization, and fast alists (see hons-and-memoization). However, in that case you should use target regression-hons in place of target regression, which will include directories that depend on ACL2(h) features not present in ACL2, and which will use saved_acl2h instead of saved_acl2 as the default executable name. So for example:

  make ACL2_JOBS=8 regression-hons

If you wish to use ACL2(p), the extension of ACL2 that supports parallel proof and execution (see parallelism), then we recommend that you use ACL2 for your regression as discussed above. Then you can use ACL2(p) for your own proof developments. (The analogous comment applies to ACL2(hp) and ACL2(h), i.e., to the use of parallelism on top of ACL2(h).)

See real for a discussion of how to certify books in subdirectory books/nonstd using ACL2(r).

Troubleshooting

If your system has difficulty certifying the books in the centaur/ directory, say because of issues with Perl, you can skip them by specifying ACL2_CENTAUR=skip, for example as follows.

  make regression ACL2_CENTAUR=skip

If you run into other 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.