BOOK-MAKEFILES

makefile support provided with the ACL2 community books 
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. And finally, we generally assume, as is typically the case by following the standard installation instructions, that you install the ACL2 community books in the books/ subdirectory of your ACL2 distribution.

See the end of this topic for a list of troubleshooting notes. Please feel free to suggest additions to that list!

The basic idea is to stand in the ACL2 sources directory and submit the following command, in order to certify all the books. 

make regression
For each book foo.lisp, a file foo.out in the same directory will contain the output from the corresponding certification attempt. If you have previous executed such a command, then you will first want to delete certificate files and other generated files, either by first executing make clean-books or simply by submitting the following command. 
make regression-fresh

By default, the ACL2 executable used is the file saved_acl2 in the ACL2 sources directory. But you can specify another instead; indeed, you must do so if you are using an experimental extension (see real, see hons-and-memoization, and see parallelism): 

make regression ACL2=<your_favorite_acl2_executable>

If you have a multi-processor machine or the like, then you can use the ACL2_JOBS variable to obtain make-level parallelism by specifying the number of concurrent processes. The following example shows how to specify 8 concurrent processes. Note that we avoid using the customary `make' option for concurrent processes, in this case `-j 8', because part of the regression (under the centaur/ community books directory) would fail to take advantage of that directive. 

make ACL2_JOBS=8 regression
Note that while other environment and `make' variables discussed here are also appropriate for use by suitable calls of `make' in the community books directory, ACL2_JOBS is only suitable for use with the regression target (and similar targets, such as regression-fresh) in the ACL2 sources directory).

You can also specify just the directories you want, among those offered in Makefile. For example: 

make ACL2_JOBS=8 regression ACL2_BOOK_DIRS='symbolic paco'

By default, your acl2-customization file (see acl2-customization) is ignored by all such 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'

The `make' commands displayed above all use the makefile, GNUmakefile, that resides in the ACL2 sources directory.

We now discuss how to create suitable makefiles in individual directories that contain certifiable books.

ACL2's regression suite is typically run on the community books, using Makefiles that include community books file books/Makefile-generic. You can look at existing Makefiles to understand how to create your own Makefiles. Here are the six 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. It is most common to use an ACL2 executable named saved_acl2 that resides in the parent directory of the books/ directory. In this case, unless you are using a very old version of GNU make (version 3.80, at least, works fine), you should be able to skip the following sentence, because the ACL2 `make' variable will be set automatically. Otherwise, define the ACL2 variable using ?= to point to your ACL2 executable (though this may be omitted for directories directly under the books/ directory), for example: 

ACL2 ?= ../../../saved_acl2
(For Makefile experts: we use ?= instead of = or := because of the protocol used by the ACL2 make system: command-line values are passed explicitly with recursive calls of make to override the Makefile values of ACL2, which in turn need to be able to override the environment value of ACL2 from books/Makefile-generic).

Also include the file Makefile-generic in the books/ directory. For example, community books file books/arithmetic-3/pass1/Makefile starts as follows. 

include ../../Makefile-generic
If you also have a line defining ACL2 as explained above, put that line just above this include line.

2. (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 `ACL2 ?=' and ~c[include]' lines. 

INHIBIT = (assign inhibit-output-lst (list (quote proof-tree)))
For other values to use for INHIBIT, see set-inhibit-output-lst and see the original setting of INHIBIT in books/Makefile-generic.

3. 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 an old version of community books file books/finite-set-theory/osets/Makefile, should make this clear. 

BOOKS = computed-hints fast instance map membership outer primitives \
        quantify set-order sets sort
But better yet, use the extension .lsp for any Lisp or ACL2 files that are not to be certified, so that the definition of BOOKS can be omitted.

4. 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 community books file 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.

5. Generally, the next step is to include the following line after the `include' of Makefile-generic (see the first step above). 

-include Makefile-deps
This will cause `make' to create and then include a file Makefile-deps that contains ``dependency'' lines needed by make. If those dependencies are somehow flawed, it may be because you have include-book forms that are not truly including books, for example in multi-line comments (#|..|#). These will be ignored if preceded by a semicolon (;), or if you add a line break after ``include-book.'' But instead, you can create dependency lines yourself by running the command 
make dependencies
and pasting the result into the end of your Makefile, and editing as you see fit.

6. 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, e.g., make -j 8 in a book directory or, if in the ACL2 sources directory, make ACL2_JOBS=8 regression.

This concludes the basic instructions for creating a Makefile in a directory including books. Here are some other capabilities offered by community books file books/Makefile-subdirs. Not included below is a discussion of how to increase parallelism by avoiding the need to certify included books before certifying a given book; see provisional-certification.

Subdirectory support. There is support for subdirectories. For example, community books file books/arithmetic-3/Makefile formerly had the following contents. 

DIRS = pass1 bind-free floor-mod
include ../Makefile-subdirs
This indicated that we are to run make in subdirectories pass1/, bind-free/, and floor-mod of the current directory (namely, community books directory books/arithmetic-3/).

However, there is also subdirectory support when the current directory has books as well. Community books file books/arithmetic-3/Makefile contains the following lines (at least as of ACL2 Version_3.6). 

arith-top: top all
all: top

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

-include Makefile-deps
The first line is optional because ../../saved_acl2 is the default and the directory is a sub-sub-directory of the distribution directory; but it is harmless to include this line. The other additional lines support certifying books in the subdirectories before certifying the books in the present directory, in the customary make style.

Specifically, the top target is defined in ../Makefile-subdirs to call make in each subdirectory in DIRS. We have set the default target in the example above to a new name, arith-top, that makes that top target before making the all target. The all target, in turn, is the top (default) target in ../Makefile-generic, and is responsible for certifying books in the current directory.

Use Makefile-psubdirs instead of Makefile-subdirs if certification of a book in a subdirectory never depends on certification of a book in a different subdirectory, because then make's -j option can allow subdirectories to be processed in parallel.

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

make clean
will remove generated files including .cert files, .port files (see uncertified-books), .acl2x files (if any), files resulting from compilation, and other ``junk''; see the full list under ``clean:'' in books/Makefile-generic.

System books. An environment variable ACL2_SYSTEM_BOOKS is generally set automatically (at least in GNU make versions 3.80 and 3.81), so you can probably skip reading the following paragraph unless your attempt to certify books fails to locate those books properly.

The environment variable ACL2_SYSTEM_BOOKS can be set to the books/ directory under which the books reside, typically the ACL2 community books. A Unix-style pathname, typically ending in books/ or books, is permissible. In most cases, your ACL2 executable is a small script in which you can set this environment variable just above the line on which the actual ACL2 image is invoked, for example: 

export ACL2_SYSTEM_BOOKS
ACL2_SYSTEM_BOOKS=/home/acl2/v3-2/acl2-sources/books
However, you can also set ACL2_SYSTEM_BOOKS as a make variable, by setting it in your Makefile before the first target definition, e.g.: 
ACL2_SYSTEM_BOOKS = /home/acl2/v3-2/acl2-sources/books

Compilation support. The file books/Makefile-generic provides support for compiling books that are already certified (but see compilation for an exception). 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
In general, the compiled file extension for a Lisp supported by ACL2 will be a target name for building compiled files for all your books (after certifying the books, if not already up-to-date on certification).

Troubleshooting notes. Please feel free to suggest additions and changes!

(1) PROBLEM: Regression fails early for community books, perhaps because of Perl. (For example, a Windows system has encountered such difficulty even after installing Perl.)

Solution: Skip certification of the centaur/ books by including ACL2_CENTAUR=skip with your `make' command. For example: 

make regression-fresh ACL2_CENTAUR=skip

(2) PROBLEM: The first part of the regression doesn't seem to be going in parallel, even though I supplied a -j option in my `make' command.

Solution: Set ACL2_JOBS to the number of jobs instead of using -j. For example: 

make ACL2_JOBS=8 regression-fresh