Using-extended-ACL2-images
(Advanced) how to get cert.pl to use save-exec images
to certify parts of your project.
In most ACL2 projects, each book uses include-book to load
all of its dependencies, and the same, "stock" ACL2 executable is used to
certify every book. This generally works well and certainly keeps things
simple.
By default, cert.pl will simply try to certify all books using whatever
ACL2 image is invoked with acl2, or else whatever image it is told to use
via the $ACL2 environment variable or the --acl2 option; see
Helping cert.pl find ACL2 of preliminaries for
details.
Unfortunately, this usual approach means that widely included books must be
loaded repeatedly. As your project grows, you may eventually find that you are
spending a lot of time waiting for include-book commands. One way to
combat this is to use save-exec to write out a new ACL2 image that has
your supporting books pre-loaded. These extended ACL2 images can be re-started
instantly. For interactive development, images can be a very convenient way to
quickly get back into a good starting place, with your supporting books already
loaded. Meanwhile, using images to re-certify books can significantly reduce
the time spent waiting for include-book commands to finish.
cert.pl supports using extended images for certain books. For this to
work, you will need to get a few pieces working together. The notes below
explain the basics of how to set this up. See also
projects/milawa/ACL2/Makefile for a working example of a project that uses
around a dozen images to certify various directories of files.
Image Creation
Suppose you want to use save-exec to create an extended ACL2 image
using the following script:
;; make-extended-acl2.lsp
(in-package "ACL2")
(include-book "support")
:q
(save-exec "extended-acl2" "Supporting libraries pre-loaded.")
While cert.pl does have good support for using the resulting image to
certify particular books, there is currently no way to directly tell
cert.pl that it needs to run this script to create the extended-acl2
image. Instead, if you want to use extended ACL2 images, you will probably
need to put together a Makefile. See static-makefiles for
information about how to use cert.pl to do the dependency scanning for
your Makefile.
In your Makefile, you can easily explain what the dependencies of
extended-acl2 are, and how to build it, e.g., as follows:
extended-acl2: support.cert make-extended-acl2.lsp
@rm -f extended-acl2
$(ACL2) < make-extended-acl2.lsp &> extended-acl2.out
ls -l extended-acl2
Helping cert.pl find your Images
For cert.pl to find extended-acl2, the easiest thing to do is make
sure that it is located somewhere in your $PATH, and we especially
recommend this option if you are going to be invoking cert.pl
interactively, i.e., not exclusively from your Makefile.
Alternately, cert.pl accepts a --bin option that can be used to
indicate which directory will contain images.
Specifying the Image for each Book
To decide what image to use to certify foo.lisp, cert.pl will
first look for a file named foo.image. This file should contain a single
line that just gives the name of the ACL2 image to use. For instance, if we
want to certify foo.lisp using extended-acl2, then foo.image
should simply contain:
extended-acl2
You can also write a cert.image file to indicate a directory-wide
default image to use. (This is exactly analogous to how cert.pl looks for
.acl2 files for pre-certify-book-commands.)
