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.
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.
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.
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
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,
(assert-event (equal acl2::*acl2-image-name* "my-extended-image"))
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
extended-acl2: support.cert make-extended-acl2.lsp @rm -f extended-acl2 $(ACL2) < make-extended-acl2.lsp &> extended-acl2.out ls -l extended-acl2
To decide what image to use to certify
; 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