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.
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.
If you are using only packages from existing libraries, these should be
dealt with automatically by the build system, which loads the portcullis
The most basic way to tell
$ 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
$ 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
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
Here is how
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