		Search-engine friendly clone of the ACL2 documentation.

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

Currently there are two supported methods of managing image creation. Both currently only allow images to be stored in one user-configured directory. In the first method, cert.pl can manage the building of images and their dependencies seamlessly, but requires the source files used for building the images to be all placed in one user-configured directory, and places some restrictions on the forms of the source files used to build the images. In the second method, cert.pl doesn't manage the building of images; instead, you need to wrap the cert.pl call inside a Makefile and add extra dependencies there.

Method 1 -- cert.pl native

In this method you must designate a directory where extended ACL2 images should be placed, given by the --bin command-line option or the ACL2_IMAGES environment variable; and additionally a directory for the source files used for building such images, given by the --image-sources option or ACL2_IMAGE_SRC_DIR environment variable. For each image file 'myimage' to be created, there must be a file 'myimage.lsp' in the image source file directory which contains the ACL2 commands to issue before saving the image. The last form in the file should be a local defconst of acl2::*acl2-image-message* giving a "modification notice" message to be printed when the image starts.

Here is an example such .lsp file:

(include-book "centaur/fgl/portcullis" :dir :system)
(include-book "centaur/aignet/portcullis" :dir :system)
(local (include-book "centaur/fgl/top" :dir :system))
(local (include-book "centaur/aignet/transforms" :dir :system))

(local (defconst *acl2-image-message*
         "This includes FGL books.  You'll need to include the ipasir-backend book separately."))

The items in the file don't always need to all be local events. Calls of LD and non embedded-event forms are allowed. Any nonlocal events will be in the portcullis of any books certified with the image. The file (and any others read using LD, etc.) will be scanned by the build system to determine the dependencies of the saved image.

The build system additionally defines another local constant in each image, acl2::*acl2-image-name*. It is a good idea to put an assert-event at the top each book that uses an extended image to make sure that when run interactively, the book is loaded into the right starting image:

(assert-event (equal acl2::*acl2-image-name* "my-extended-image"))

Method 2 -- makefile integrated

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.")

In method 2, instead of letting cert.pl handle the dependencies and creation of saved images, we instead create a Makefile that wraps around the one cert.pl will create. 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 scans for comments such as:

; cert-param: (acl2-image=myfancyimage)

Such a comment can either be in the book itself, its .acl2 file, or the directory's cert.acl2 file.

Alternatively, cert.pl will also look for files named foo.image for a book named foo, or cert.image for any book in the given directory. 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