Package-reincarnation-import-restrictions
Re-defining undone defpkgs
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 was a theorem because
pkg::sym was read as a::sym because of the old imports.
