Hidden-death-package
Handling defpkg events that are local
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)
Enabled: T
Hyps: T
Equiv: EQUAL
Lhs: (PKG-IMPORTS "PKG0")
Rhs: '(A B)
Backchain-limit-lst: NIL
Subclass: ABBREVIATION
ACL2 !>
Consider a defpkg event that is introduced during evaluation of an
include-book event, where that include-book event occurs locally inside a surrounding encapsulate event or another
include-book event. In that case, traces of the axiom added by the
defpkg event will disappear after the surrounding event is admitted. If
ACL2 were to allow the same package name to be defined subsequently with a
different set of imports, that could cause inconsistencies. See package-reincarnation-import-restrictions for relevant discussion, or see the
“Essay on Hidden Packages” in source file axioms.lisp..
In order to prevent unsoundness, 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). This invariant guarantees that
if you then try to define a package in a manner inconsistent with its earlier
definition — specifically, with a different imports list — you
will see an error because of the tracking discussed above.
(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!)
