PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS

re-defining undone 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.