		Search-engine friendly clone of the ACL2 documentation.

Working-with-packages

How to set up new package and portcullis files.

Recommendations

Here is a basic recipe to follow for creating new directories that make use of packages:

foo/package.lsp — main package definitions

;; load other packages needed to define our new packages...
;; note that we only include portcullis files, that define
;; the packages, not the libraries which those files support
(include-book "lib1/portcullis" :dir :system)
(include-book "lib2/portcullis" :dir :system)

;; define our new packages
(defpkg "PKG1" ...)
(defpkg "PKG2" ...)

;; optionally set up useful exports lists
(defconst PKG1::*pkg1-exports* ...)
(defconst PKG2::*pkg2-exports* ...)

foo/portcullis.lisp — a nearly empty book

;; We need an "in-package" line to make this a valid book, but
;; which package doesn't matter since the rest of the book is empty.
(in-package "FOO")

foo/portcullis.acl2 — certification instructions for the portcullis book

(ld "package.lsp")

foo/cert.acl2 — certification instructions for the other books

(include-book "portcullis")
;; cert-flags: ? t [:ttags :all ...]

foo/acl2-customization.lsp — merely for convenience

(ld "~/acl2-customization.lsp" :ld-missing-input-ok t)
(ld "package.lsp")
(in-package "FOO")

Rationale

Using the same names for package.lsp and portcullis.lisp is a nice convention that improves consistency and discoverability.

The .lsp extension helps Emacs realize the package file is a Lisp file
It also helps build::cert.pl know it is not a certifiable book.

The empty portcullis book is a useful trick. Including this book, rather than directly ld'ing the package from cert.acl2, means that when several books from the same directory are loaded into the same session, each of their individual .cert files contain commands like:

(include-book "portcullis")

instead of:

(defpkg "FOO" (union-eq ...))

This is good because ACL2 can quickly realize that the include-book form is redundant and not do any work, instead of having to re-evaluate the package commands to see if it is indeed the same.

Having a customization file that starts ACL2 up in "the right package" is often very convenient while developing. Loading the user's customization file first, if one exists, is nice for users who have their own macros.

It can also be good to pre-load packages like std when your session starts. See books/std/std-customization.lsp for an ACL2-customization file that does this.