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
defpkg by the user.
When printing symbols, the package prefix is displayed if it is not
current-package and may be optionally displayed otherwise.
"ACL2" then the symbol
be printed as
'MY-PKG::SYMB must be
MY-PKG::SYMB. But if
the former symbol must be printed as
ACL2::SYMB while the latter may
be printed as
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
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
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
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.