		Search-engine friendly clone of the ACL2 documentation.

Community-books

Books-certification

Instructions for certifying the ACL2 community-books.

The Community Books provides a make system, which is recommended for certifying a specified subset of those books from the books/ directory of your ACL2 distribution. Alternate instructions are however available for certifying from the top-level directory (see books-certification-alt).

Below are instructions for certifying various sets of books. They all have the following form in common. Note: If there is a suitable "acl2" executable on your Unix PATH — for example, if the bin subdirectory of the main ACL2 directory is on your PATH, so that bin/acl2 may be your executable — then you can omit "ACL2=..." below.

cd /path/to/acl2-sources/books
make ACL2=/path/to/acl2-sources/saved_acl2 ...

For example, the section ``A Full Build'', below, says to do the following if you would like to make a change to the community-books (where the -j argument is optional).

$ cd /path/to/acl2-sources/books
$ make ACL2=/path/to/acl2-sources/saved_acl2 -j 2 all

Success is indicated by a Linux exit status of 0. Equivalently, there should be no failures in the log. Failures may be found by searching for **; for example, if output is redirected to a log file make-regression.log, then the following should provide no output.

fgrep -a '**' make-regression.log

Unusual books that create output in the log file should not produce the string ** except upon failure.

By default, make commands for certifying books take advantage of files *@useless-runes.lsp. See useless-runes.

Prerequisites

We assume that you have already downloaded and installed ACL2 as per the ACL2 installation instructions on the ACL2 home page.

We assume you know the path to your ACL2 executable. Typically this is a script named saved_acl2 in your acl2-sources directory.

We assume the ACL2 community-books are installed in the books/ subdirectory of your ACL2 distribution, as is the case when you have followed the ACL2 installation instructions above.

The instructions below are suitable for ACL2 and all of its experimental extensions, e.g., ACL2(p) and ACL2(r).

It may be preferable to avoid being logged in as root, since developers do not test as root and at least one community book (books/oslib/tests/copy.lisp) has failed to certify when logged in as root.

A Basic Build

Before ACL2 Version 6.4, building the Community Books could take several hours. Now, the default make target in books/GNUmakefile, called basic, is much faster — it excludes many books and certifies only books listed below, which tend to be widely used. WARNING: the basic target of books/GNUmakefile is insufficient for validating changes that will go into the community-books; for that, use the all target.

arithmetic
arithmetic-3
arithmetic-5
ihs
misc
tools (mostly)
std
xdoc (in part)
data-structures

To certify these books, you should be able to run make as follows. The -j 2 part of this command is suitable for a computer with two cores. If you have, e.g., a quad-core computer, you should probably use -j 4 instead, and so on.

$ cd /path/to/acl2-sources/books
$ make ACL2=/path/to/acl2-sources/saved_acl2 -j 2 basic

If you configure your PATH so that you can launch ACL2 by typing acl2, then you may omit the ACL2=... part.

Certifying Additional Books

We expect that most ACL2 users will want to certify at least the basic books described above. But what if you also need other books? One option is to do a full build (see below). But it is usually much faster to simply tell make to build the books you actually want to use.

There are make targets corresponding to most directory names. For instance, to build the books under coi and rtl and cgen, you can run:

$ cd /path/to/acl2-sources/books
$ make ACL2=/path/to/acl2-sources/saved_acl2 coi rtl cgen -j 2

For finer grained control, you can name individual books. This works particularly well for libraries that have top books. For instance, if you want the rtl/rel9 library, you could run:

$ cd /path/to/acl2-sources/books
$ make ACL2=/path/to/acl2-sources/saved_acl2 rtl/rel9/lib/top.cert -j 2

Books that Require ACL2 Extensions

Some books require experimental extensions to ACL2, such as ACL2(p) (see parallelism) or ACL2(r) (see real). Other books require certain additional software.

The build system will automatically determine which kind of ACL2 you are running (ACL2, ACL2(p), or ACL2(r)) and, based on this, may prevent incompatible books from being certified. The output of make should explain which books are being excluded and why.

These kinds of book requirements are controlled by special build::cert_param comments.

Books that Require Quicklisp

Some books, especially interfacing-tools like oslib and the ACL2 bridge, require certain Common Lisp libraries.

These libraries are now bundled with ACL2 via quicklisp, so you should not need to download anything extra to use them. They are enabled by default for all host Lisps except GCL, but you can avoid books that depend on Quicklisp libraries by setting USE_QUICKLISP=0 in your make command.

Using Quicklisp should definitely work if the host Lisp is CCL or SBCL. (Note however that certification of books that use Quicklisp may require openssl to be installed if it is not already on your system.) There is some chance it will work with Allegro CL, LispWorks, and CMUCL. It will almost certainly not work for GCL (at least as of 2018).

Books that Require Additional Software

Some other books based on satlink and gl require a SAT solver, typically Glucose, to be installed; see satlink::sat-solver-options for installation options. The build system should automatically determine if Glucose is installed on your system, and will avoid trying to certify these books unless Glucose is present.

Building the manual

If you just want to get a copy of the ACL2+Books manual for local viewing, you probably don't need to build it yourself because you can just download a copy. If for some reason you do want to build the manual yourself, you should be able to do so as follows, provided you have installed glucose. (That requirement might be eliminated in the future.)

$ cd /path/to/acl2-sources/books
$ make manual -j 4

Building the manual should work on at least CCL and SBCL on Linux and Mac OS X. It may not work for some other OS/Lisp combinations. In particular, building the manual requires some features from oslib and quicklisp that may not be available on some other Lisps.

The resulting web-based manual may be found in:

acl2-sources/books/doc/manual/index.html

See also ACL2-doc for details about how to build your own Emacs-based manual, and xdoc::save for general information about how to build and distribute custom XDOC manuals, e.g., manuals that additionally include your own unreleased books.

A Full Build

Building all of the books can take hours and is usually unnecessary. That said, it is easy to do: just run make all, for example as follows. (But as noted above, you may omit "ACL2=..." if a suitable executable named acl2 is on your Unix PATH, such as bin/acl2.)

$ cd /path/to/acl2-sources/books
$ make ACL2=/path/to/acl2-sources/saved_acl2 -j 2 all

This includes a few books that are quite slow to certify. You can exclude those by replacing ``all'' by ``regression'' in the command above.

Cleaning Up

If you want to delete generated files, you can run make clean to remove certificates, compiled files, and build logs.

If you just want to remove the files in a particular subdirectory (and its subdirectories), you can go into that directory and then run the build/clean.pl script. This will delete, starting from your current directory, recursively, all certificates, logs, compiled files, etc.

Note that make clean doesn't remove some files, e.g., xdoc manuals. To remove everything, try make moreclean.

Debugging Failed Certifications

If a book fails to certify, you may want to try certifying it in an interactive session. The most reliable way to do this is to replicate the environment and commands that the build system used. This information can be found at the top of the [bookname].cert.out file. For instance:

;; foo.cert.out
-*- Mode: auto-revert -*-
...
Environment variables:
ACL2_CUSTOMIZATION=NONE                 ;; <-- first configure your
ACL2_SYSTEM_BOOKS=/path/to/acl2/books   ;;     environment to match
ACL2=/path/to/saved_acl2                ;;     these settings
...
Temp lisp file:
(acl2::value :q)                 ;; <--- then submit these commands to
(acl2::in-package "ACL2")      ;;      $ACL2 to debug the failure
...                              ;;      interactively
--- End temp lisp file ---

Some other notes/tips:

Make sure the ACL2 image you run is the same as the one listed as ACL2 in those environment variables!
You may wish to set the environment variables for only the duration of your ACL2 session by using the "env" command.
You may wish to edit some of the commands for better debugging purposes; e.g. you may modify the set-inhibit-output-lst command, or insert a set-debugger-enable command, etc.
If you don't want your session to exit after a successful certification, replace the last form (er-progn (time$ (certify-book ... with just the (time$ (certify-book ...)) part.

Further Resources

The build system is largely based on build::cert.pl. There is considerable documentation about cert.pl, and we highly recommend using it to manage your own ACL2 projects.

The main build script is books/GNUmakefile. There are many comments at the start of this file, and you can also inspect it to see what targets are available.

Please feel absolutely free to contact the ACL2-help mailing list with any questions about building the community books.

Subtopics

Books-certification-classic: Classic ACL2 `make'-based certification of books
Provisional-certification: Certify a book in stages for improved book-level parallelism
Books-certification-alt: Alternate instructions for certifying the community-books, from the perspective of the acl2-sources directory.
Using-extended-ACL2-images: (Advanced) how to get cert.pl to use save-exec images to certify parts of your project.