How to add commands to be executed before calling certify-book. You'll need this to use ACL2 features like defpkg and
Background: Pre certify-book Commands
ACL2 commands like defpkg can't be embedded within books. Instead,
when using raw ACL2 to certify books, you typically define the package before
issuing the certify-book command. The defpkg command then
becomes part of the book's ACL2::portcullis.
For example, here is how to successfully certify a book with its own
package, using raw ACL2:
$ cat mybook.lisp
(defun f (x) (+ x 1))
ACL2 !> (defpkg "MY-PACKAGE"
ACL2 !> (certify-book "mybook" ?)
If this doesn't make sense, please see the documentation for books,
especially see ACL2::book-example which explains something like the
above in far greater detail.
Individual .acl2 Files
For cert.pl to certify books with packages, it needs to be able to find
these extra defpkg commands that can't go directly into the book.
If you are using only packages from existing libraries, these should be
dealt with automatically by the build system, which loads the portcullis
(.port file) of each included book before certifying a book. (To defeat
this mechanism, add a comment containing "no_port" at the end of the line of
each include-book whose portculli you don't want.) However, if you are defining
a new package, you need to know how to put it in your book's portcullis.
The most basic way to tell cert.pl how to certify a file like
mybook.lisp is to put the defpkg form into a corresponding file,
$ cat mybook.acl2
;; no certify-book command, unlike in legacy files for Makefile-generic
At this point, we can simply run:
$ cert.pl mybook
ACL2 executable is ...
System books directory is ...
Making .../mybook.cert on 24-Oct-2013 09:25:03
Successfully built .../my-book.cert
-rw-rw-r-- 1 jared logic 513 Oct 24 09:25 mybook.cert
If you inspect the resulting mybook.cert.out output log, you'll see
that these instructions that were picked up from the .acl2 file:
$ cat mybook.cert.out
-*- Mode: auto-revert -*-
; instructions from .acl2 file mybook.acl2:
Furthermore, if you inspect mybook.cert, you'll see that defpkg form
replicated in the portcullis section of the certificate. In fact, all the
books that include your book (transitively) or that also load the same package
will also replicate this form in their portculli. This can be a problem
because including multiple books depending on this package requires checking
many times that this defpkg form is redundant, which can actually add up to a
significant performance problem. We suggest using the discipline described in
Directory-Wide cert.acl2 Files
It's very common for all of the books in a directory to want to use the same
packages. Instead of setting up a corresponding .acl2 file for every
single book, it is often much more convenient to use a special, directory-wide
.acl2 file, called cert.acl2.
Here is how cert.pl chooses the .acl2 file to use when you ask
it to certify foo.lisp:
- First, if a file named foo.acl2 exists, then it will be used.
- Else, if a file named cert.acl2 exists, then it will be used.
- Otherwise, no .acl2 files will be used; no pre certify-book
commands will be given.
In the typical case, then, where you have a whole directory of books that
are all supposed to be in some package, you just need a single cert.acl2
file that gets that defpkg form loaded.