DEFPKG

Major Section:  EVENTS

Example:
(defpkg "MY-PKG"
        (union-eq *acl2-exports*
                  *common-lisp-symbols-from-main-lisp-package*))


HIDDEN-DEATH-PACKAGE -- handling defpkg events that are local



HIDDEN-DEFPKG -- handling defpkg events that are local





General Form:
(defpkg "name" term doc-string)

where "name" is a non-empty string consisting of standard characters (see standard-char-p), none of which is lower case, that names the package to be created; term is a variable-free expression that evaluates to a list of symbols, where no two distinct symbols in the list may have the same symbol-name, to be imported into the newly created package; and doc-string is an optional documentation string; see doc-string. The name of the new package must be ``new'': the host lisp must not contain any package of that name. There are two exceptions to this newness rule, discussed at the end of this documentation.

(There is actually an additional argument, book-path, that is used for error reporting but has no logical content. Users should generally ignore this argument, as well as the rest of this sentence: a book-path will be specified for defpkg events added by ACL2 to the portcullis of a book's certificate; see hidden-death-package.)

Defpkg forms can be entered at the top-level of the ACL2 command loop. They should not occur in books (see certify-book).

After a successful defpkg it is possible to ``intern'' a string into the package using intern-in-package-of-symbol. The result is a symbol that is in the indicated package, provided the imports allow it. For example, suppose 'my-pkg::abc is a symbol whose symbol-package-name is "MY-PKG". Suppose further that the imports specified in the defpkg for "MY-PKG" do not include a symbol whose symbol-name is "XYZ". Then

(intern-in-package-of-symbol "XYZ" 'my-pkg::abc)

(intern-in-package-of-symbol "XYZ" 'my-pkg::abc)

Defpkg is the only means by which an ACL2 user can create a new package or specify what it imports. That is, ACL2 does not support the Common Lisp functions make-package or import. Currently, ACL2 does not support exporting at all.

The Common Lisp function intern is weakly supported by ACL2. See intern.

We now explain the two exceptions to the newness rule for package names. The careful experimenter will note that if a package is created with a defpkg that is subsequently undone, the host lisp system will contain the created package even after the undo. Because ACL2 hangs onto worlds after they have been undone, e.g., to implement :oops but, more importantly, to implement error recovery, we cannot actually destroy a package upon undoing it. Thus, the first exception to the newness rule is that name is allowed to be the name of an existing package if that package was created by an undone defpkg and the newly proposed set of imports is identical to the old one. See package-reincarnation-import-restrictions. This exception does not violate the spirit of the newness rule, since one is disinclined to believe in the existence of undone packages. The second exception is that name is allowed to be the name of an existing package if the package was created by a defpkg with identical set of imports. That is, it is permissible to execute ``redundant'' defpkg commands. The redundancy test is based on the values of the two import forms (comparing them after sorting and removing duplicates), not on the forms themselves.

Finally, we explain why we require the package name to contain standard characters, none of which is lower case. We have seen at least one implementation that handled lower-case package names incorrectly. Since we see no need for lower-case characters in package names, which can lead to confusion anyhow (note for example that foo::bar is a symbol whose symbol-package-name is "FOO", not "foo"), we simply disallow them. Since the notion of ``lower case'' is only well-specified in Common Lisp for standard characters, we restrict to these.