CURRENT-PACKAGE

Major Section:  MISCELLANEOUS

Current-package is an ld special (see ld). The accessor is (current-package state) and the updater is (set-current-package val state), or more conventionally, (in-package val). The value of current-package is actually the string that names the package. (Common Lisp's ``package'' objects do not exist in ACL2.) The current package must be known to ACL2, i.e., it must be one of the initial packages or a package defined with defpkg by the user.

When printing symbols, the package prefix is displayed if it is not the current-package and may be optionally displayed otherwise. Thus, if current-package is "ACL2" then the symbol 'ACL2::SYMB may be printed as SYMB or ACL2::SYMB, while 'MY-PKG::SYMB must be printed as MY-PKG::SYMB. But if current-package is "MY-PKG" then the former symbol must be printed as ACL2::SYMB while the latter may be printed as SYMB.

In Common Lisp, current-package also affects how objects are read from character streams. Roughly speaking, read and print are inverses if the current-package is fixed, so reading from a stream produced by printing an object must produce an equal object.

In ACL2, the situation is more complicated because we never read objects from character streams, we only read them from object ``streams'' (channels). Logically speaking, the objects in such a channel are fixed regardless of the setting of current-package. However, our host file systems do not support the idea of Lisp object files and instead only support character files. So when you open an object input channel to a given (character file) we must somehow convert it to a list of ACL2 objects. This is done by a deus ex machina (``a person or thing that appears or is introduced suddenly and unexpectedly and provides a contrived solution to an apparently insoluble difficulty,'' Webster's Ninth New Collegiate Dictionary). Roughly speaking, the deus ex machina determines what sequence of calls to read-object will occur in the future and what the current-package will be during each of those calls, and then produces a channel containing the sequence of objects produced by an analogous sequence of Common Lisp reads with *current-package* bound appropriately for each.

A simple rule suffices to make sane file io possible: before you read an object from an object channel to a file created by printing to a character channel, make sure the current-package at read-time is the same as it was at print-time.