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!)
