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
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 !>
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
In order to prevent unsoundness, then, ACL2 maintains the following
invariant. Let us say that a
(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!)