		Search-engine friendly clone of the ACL2 documentation.

Cert.pl

Pre-certify-book-commands

How to add commands to be executed before calling certify-book. You'll need this to use ACL2 features like defpkg and add-include-book-dir.

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
(in-package "MY-PACKAGE")
(defun f (x) (+ x 1))

$ acl2
ACL2 !> (defpkg "MY-PACKAGE"
          (union-eq *acl2-exports*
                    *common-lisp-symbols-from-main-lisp-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, named mybook.acl2:

$ cat mybook.acl2
(in-package "ACL2")
(defpkg "MY-PACKAGE"
  (union-eq *acl2-exports*
            *common-lisp-symbols-from-main-lisp-package*))
;; 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:
(in-package "ACL2")
(defpkg "MY-PACKAGE"
  (union-eq *acl2-exports*
            *common-lisp-symbols-from-main-lisp-package*))
...

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 ACL2::working-with-packages instead.

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.