HIDDEN-DEATH-PACKAGE

handling defpkg events that are local 
Major Section:  DEFPKG

This documentation topic explains a little bit about certain errors users may see when attempting to evaluate a defpkg event. In brief, if you see an error that refers you to this topic, you are probably trying to admit a defpkg event, and you should change the name of the package to be introduced by that event.

Recall that defpkg events introduce axioms, for example as follows. 

ACL2 !>(defpkg "PKG0" '(a b))


Summary
Form:  ( DEFPKG "PKG0" ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 "PKG0"
ACL2 !>:pr! "PKG0"


Rune:       (:REWRITE PKG0-PACKAGE)
Status:     Enabled
Lhs:        (SYMBOL-PACKAGE-NAME (INTERN-IN-PACKAGE-OF-SYMBOL X Y))
Rhs:        "PKG0"
Hyps:       (AND (STRINGP X)
                 (NOT (MEMBER-SYMBOL-NAME X '(A B)))
                 (SYMBOLP Y)
                 (EQUAL (SYMBOL-PACKAGE-NAME Y) "PKG0"))
Equiv:      EQUAL
Backchain-limit-lst:    NIL
Subclass:   BACKCHAIN
Loop-stopper: NIL
ACL2 !>
Now, a defpkg event may be executed underneath an encapsulate or include-book form that is marked local. In that case, traces of the added axiom will disappear after the surrounding encapsulate or include-book form is admitted. This can cause inconsistencies. (You can take our word for it, or you can look at the example shown in the ``Essay on Hidden Packages'' in source file axioms.lisp.)

In order to prevent unsoundness, then, ACL2 maintains the following invariant. Let us say that a defpkg event is ``hidden'' if it is in support of the current logical world but is not present in that world as an event, because it is local as indicated above. We maintain the invariant that all defpkg events, even if ``hidden'', are tracked under-the-hood in the current logical world. Sometimes this property causes defpkg events to be written to the portcullis of a book's certificate (see books). At any rate, if you then try to define the package in a manner inconsistent with the earlier such definition, that is, with a different imports list, you will see an error because of the above-mentioned tracking.

(By the way, this topic's name comes from Holly Bell, who heard "hidden death package" instead of "hidden defpkg". The description seemed to fit. Thanks, Holly!)