DEFPKG

define a new symbol package 
Major Section:  EVENTS


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





General Form:
(defpkg "name" term doc-string)
where "name" is a (case-sensitive) string other than "" 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.

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 imports list 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 imports. That is, it is permissible to execute ``redundant'' defpkg commands. The redundancy test is based on the values of the two import forms, not on the forms themselves.