defpkgs
Major Section: MISCELLANEOUS
Suppose (defpkg "pkg" imports) is the most recently executed
successful definition of "pkg" in this ACL2 session and that it
has since been undone, as by :ubt. Any future attempt in this
session to define "pkg" as a package must specify an identical
imports list.
The restriction stems from the need to implement the reinstallation
of saved logical worlds as in error recovery and the :oops command.
Suppose that the new defpkg attempts to import some symbol, a::sym,
not imported by the previous definition of "pkg". Because it was
not imported in the original package, the symbol pkg::sym, different
from a::sym, may well have been created and may well be used in some
saved worlds. Those saved worlds are Common Lisp objects being held
for you ``behind the scenes.'' In order to import a::sym into
"pkg" now we would have to unintern pkg::sym, rendering those
saved worlds ill-formed. It is because of saved worlds that we do
not actually clear out a package when it is undone.
At one point we thought it was sound to allow the new defpkg to
import a subset of the old. But that is incorrect. Suppose the old
definition of "pkg" imported a::sym but the new one does not.
Suppose we allowed that and implemented it simply by setting the
imports of "pkg" to the new subset. Then consider the conjecture
(eq a::sym pkg::sym). This ought not be a theorem because we did
not import a::sym into "pkg". But in fact in AKCL it is a theorem
because pkg::sym is read as a::sym because of the old imports.
