Classic ACL2 `make'-based certification of books
This documentation topic explains an approach to certifying directories of books, which we call ``classic ACL2 `make'-based certification''.
Warning: The capability described in this section might be replaced at any time by a capability based on corresponding support for community books (see books-certification). If you think that would be a hardship, please contact the ACL2 implementors.
This topic discusses a way to certify a directory of books other than the ACL2 community books. See books-certification for how to certify the set of ACL2 community books. There is also a section in that documentation topic, ``Restricting to Specific Directories and Books'', that provides an alternative to classic ACL2 `make'-based certification (as discussed in the present topic) for certifying specified sets of 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 assume, as is typically the case by following the standard
installation instructions, that you install the ACL2 community books in the
In summary: to use `make' to certify books under a given directory,
you may create a simple Makefile in that directory (as explained below) so
that when you stand in that directory, you can submit the command, `make', to
certify those books. If you have a multi-processor machine or the like, then
you can use the `
make -j 4
For each book
Note that when you run `make', then by default, the first error will cause
the process to stop. You can use
By default, your acl2-customization file (see ACL2-customization) is
ignored by such `make' commands. However, you can specify the use of an
acl2-customization file by setting the value of environment variable
make ACL2_CUSTOMIZATION='' make ACL2_CUSTOMIZATION='~/acl2-customization.lisp'
We now discuss how to create makefiles to support `make' commands as discussed above.
First we give five steps for creating a
1. Include the file
Makefile-genericfrom the books/subdirectory of your ACL2 sources directory, but first perhaps define the variable ` ACL2'. Consider the following example.ACL2 ?= /Users/john_doe/acl2/acl2-sources/saved_acl2 include /Users/john_doe/acl2/acl2-sources/books/Makefile-generic
In this example, you can omit the first line, because the default ACL2 executable is file
saved_acl2in the directory immediately above the directory of the specified Makefile-genericfile. Indeed, that is the common case. Note the use of ?=instead of =or :=, so that ACL2can instead be defined by the environment or provided on the command line as part of the `make' command.
2. (Optional; usually skipped.) Set the
INHIBITvariable 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' lines.
For other values to use for
INHIBIT, see set-inhibit-output-lst and see the original setting of INHIBITin books/Makefile-generic.
3. Specify the books to be certified. Normally, every file with extension
.lispwill be a book that you want to certify, in which case you can skip this step. Otherwise, put a line in your Makefileafter 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
.lspfor any Lisp or ACL2 files that are not to be certified, so that the definition of BOOKScan be omitted.
.acl2files 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.acl2you 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 equalitiesbook. In general, for each <book-name>.lispwhose certification requires a non-initial certification world, you will need a corresponding <book-name>.acl2file that ends with the appropriate certify-book command.
You also have the option of creating a file
cert.acl2that has a special role. When file <book-name>.lispis certified, if there is no file <book-name>.acl2but there is a file cert.acl2, then cert.acl2will be used as <book-name>.acl2would have been used, as described in the preceding paragraph, except that the appropriate certify-book command will be generated automatically. Thus, no certify-bookcommand should occur in cert.acl2.
It is actually allowed to put raw lisp forms in a
.acl2file (presumably preceded by :qor (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-depsthat 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 of adding the ` -include' line above, you can create dependency lines yourself by running the commandmake dependencies
and pasting the result into the end of your
Makefile, and editing as you see fit.
This concludes the basic instructions for creating a
There is support for using `make' to certify books in subdirectories. Consider the following example.
DIRS = pass1 bind-free floor-mod include ../Makefile-subdirs
This indicates that we are to run `make' in subdirectories
You can combine this subdirectory support with the support already
discussed for certifying books in the top-level directory. Here is an
example, which as of this writing is in community books file
arith-top: top all all: top DIRS = pass1 bind-free floor-mod include ../Makefile-subdirs include ../Makefile-generic -include Makefile-deps
We note that there is a
will remove generated files including
An environment variable
The environment variable
export ACL2_SYSTEM_BOOKS ACL2_SYSTEM_BOOKS=/home/acl2/v3-2/acl2-sources/books
However, you can also set
ACL2_SYSTEM_BOOKS ?= /home/acl2/v3-2/acl2-sources/books
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).
If you run into problems, you can get help by joining the