How to set up new package and portcullis files.
Here is a basic recipe to follow for creating new directories that make use of packages:
;; 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* ...)
;; 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")
(include-book "portcullis") ;; cert-flags: ? t [:ttags :all ...]
(ld "~/acl2-customization.lsp" :ld-missing-input-ok t) (ld "package.lsp") (in-package "FOO")
Using the same names for
The empty portcullis book is a useful trick. Including this book, rather
than directly ld'ing the package from
(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