Major Section: EVENTS
Example:
(defpkg "MY-PKG"
(union-eq *acl2-exports*
*common-lisp-symbols-from-main-lisp-package*))
Some Related Topics
defpkg events that are local
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)returns a symbol whose
symbol-name is "XYZ" and whose
symbol-package-name is "MY-PKG". On the other hand, if
the imports to the defpkg does include a symbol with the name
"XYZ", say in the package "LISP", then
(intern-in-package-of-symbol "XYZ" 'my-pkg::abc)returns that symbol (which is uniquely determined by the restriction on the imports list above). See intern-in-package-of-symbol.
Upon admission of a defpkg event, the function pkg-imports is
extended to compute a list of all symbols imported into the given package,
without duplicates.
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. A more general form of that function is also provided:
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.
NOTE: Also see managing-acl2-packages for contributed documentation on managing ACL2 packages.
