		Search-engine friendly clone of the ACL2 documentation.

Packages

Package-reincarnation-import-restrictions

Re-defining undone defpkgs

ACL2 imposes the following restriction on redefining packages. Note that for the notion of a package definition being “undone”, the undoing might have been by use of :ubt, or it might have been because the defpkg form was evaluated by a local event that disappeared during the second pass of an encapsulate or include-book event.

Suppose (defpkg "pkg" imports) has been evaluated successfully and then has been undone. Then any future attempt in the same session to define "pkg" as a package must specify an identical imports list.

Reasons for the restriction

We will see below that the restriction above is necessary for avoiding unsoundness. But first consider the following simple example, which shows that the package doesn't entirely disappear when undone.

ACL2 !>(defpkg "FOO" nil)

Summary
Form:  ( DEFPKG "FOO" ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 "FOO"
ACL2 !>(assign x 'foo::a)
 FOO::A
ACL2 !>(u) ; undoes the defpkg event
           0:x(EXIT-BOOT-STRAP-MODE)
ACL2 !>(@ x)
FOO::A
ACL2 !>(eq (@ x) 'acl2::a)
NIL
ACL2 !>

Suppose that (without the restriction) the package "FOO" can now be introduced as (defpkg "FOO" '(a)). Then will (eq (@ x) 'acl2::a) evaluate to nil as before, since we didn't make another assignment to x? Or would that equality evaluate to t since the only symbol in package "FOO" whose symbol-name is "A" is acl2::a? Each result is plausible so to avoid confusion, it might be best if (@ x) is now undefined. But that would require somehow removing all symbols in the state whose package is "FOO" when undoing the defpkg event, which can be inefficient and — more importantly — may not make sense if there are stobjs that include such symbols. What a mess!

A more important reason for the restriction is that it prevents unsoundness. Consider the following two books.

;;; book1.lisp
;;; Portcullis command: (defpkg "FOO" '())
(in-package "ACL2")
(defthm thm1
  (equal (symbol-package-name (intern$ "A" "FOO"))
         "FOO"))

;;;;;;

;;; book2.lisp
;;; Portcullis command: (defpkg "FOO" '(a))
(in-package "ACL2")
(defthm thm2
  (equal (symbol-package-name (intern$ "A" "FOO"))
         "ACL2"))

After each of these two books is certifiable in a (separate) fresh ACL2 session, consider the following two events.

(encapsulate
  ()
  (local (include-book "book1"))
  (defthm thm1
    (equal (symbol-package-name (intern$ "A" "FOO"))
           "FOO")))

(encapsulate
  ()
  (local (include-book "book2"))
  (defthm thm1
    (equal (symbol-package-name (intern$ "A" "FOO"))
           "ACL2")))

Each is accepted in a separate, fresh ACL2 session. But if we could admit the first and then the second in the same session, we could of course prove nil. Fortunately, if we try that, then ACL2 implements the restriction by complaining about the second as follows, when encountering the (local (include-book "book2")) form in the second encapsulate.

ACL2 Error in ACL2-INTERFACE:
We cannot reincarnate the package "FOO" because it was previously defined
with a different list of imported symbols.

A final reason for the restriction stems from 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. So because of saved worlds, we do not clear out a package when it is undone.

A logical view of the restriction

The restriction on redefining packages is based on the following part of the logical foundation of ACL2.

Logical Persistence of Packages.
When a package is introduced by defpkg in an ACL2 session, its definition is considered to persist logically even if that defpkg event is undone.

That principle certainly rules out the new definition of an undone package with different imports. It also explains why package definitions from locally included books are included in a book's portcullis commands; see hidden-defpkg. Note that this is a logical principle; if you undo a defpkg event, then ACL2 will prevent you from referencing that package explicitly unless you first reintroduce it — with the same imports, because of the restriction.