BOOK-MAKEFILES

Major Section:  BOOKS

This topic describes the ACL2 methodology for using makefiles to assist in the automation of the certification of collections of ACL2 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.

ACL2's regression suite is run using Makefiles that include books/Makefile-generic. You can look at existing Makefiles to understand how to create your own Makefiles. Here are the seven steps to follow to create a Makefile for a directory that contains books to be certified, and certify them using that Makefile. Below these steps we conclude with discussion of other capabilties provided by books/Makefile-generic.

1. Include the file books/Makefile-generic. For example, if you look at books/misc/Makefile then you'll see that it starts with this line:

include ../Makefile-generic

2. Define the ACL2 variable. For example, file books/arithmetic-3/pass1/Makefile starts as follows.

include ../../Makefile-generic
ACL2 = ../../../saved_acl2

3. (Optional; usually skipped.) Set the INHIBIT variable 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 and ACL2 lines.

INHIBIT = (assign inhibit-output-lst (list (quote proof-tree)))

4. Specify the books to be certified. If every file with extension .lisp is a book that you want to certify, you can skip this step. Otherwise, put a line in your Makefile after the ones above that specifies the books to be certified. The following example, from books/finite-set-theory/osets/Makefile, should make this clear.

BOOKS = computed-hints fast instance map membership outer primitives \
        quantify set-order sets sort

5. Create .acl2 files for books that are to be certified in other than the initial ACL2 world (see portcullis). For example, if you look in books/arithmetic/equalities.acl2 you will see defpkg forms followed by a certify-book command, because it was determined that defpkg forms were necessary in the certification world in order to certify the equalities book. In general, for each <book-name>.lisp whose certification requires a non-initial certification world, you will need a corresponding <book-name>.acl2 file that ends with the appropriate certify-book command. Of course, you can also use .acl2 files with initial certification worlds, for example if you want to pass optional arguments to certify-book.

You also have the option of creating a file cert.acl2 that has a special role. When file <book-name>.lisp is certified, if there is no file <book-name>.acl2 but there is a file cert.acl2, then cert.acl2 will be used as <book-name>.acl2 would have been used, as described in the preceding paragraph, except that the appropriate certify-book command will be generated automatically -- no certify-book command should occur in cert.acl2.

It is actually allowed to put raw lisp forms in a .acl2 file (presumably preceded by :q or (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.

6. Run the following command:

make dependencies

7. Run make. This will generate a <book-name>.out file for each <book-name>.lisp file being certified, which is the result of redirecting ACL2's standard output. Note that make will stop at the first failure, but you can use make -i to force make to continue past failures. You can also use the -j option to speed things up if you have a multi-core machine.

That concludes the basic instructions for creating a Makefile in a directory including books. Here are some other capabilities offered by books/Makefile-subdirs.

Subdirectory support. There is support for the case that there are no books in the current directory, but there are subdirectories that include books (or themselves have no books but contain subdirectories with books, etc.) For example, file books/arithmetic-3/Makefile has the following contents.

DIRS = pass1 bind-free floor-mod
include ../Makefile-subdirs

Cleaning up. We note that there is a clean target. Thus,

make clean

Compilation support. Finally, books/Makefile-generic provides support for compiling books that are already certified. For example, suppose that you have certified books in GCL, 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 Makefile.

make fasl