Major Section: MISCELLANEOUS
Sometimes a ``local incompatibility'' is reported while attempting
to embed some events, as in an encapsulate or include-book. This is
generally due to the use of a locally defined name in a non-local
event or the failure to make a witnessing definition local.
local incompatibilities may be detected while trying to execute the
strictly non-local events of an embedding. For example, encapsulate
operates by first executing all the events (local and non-local)
with ld-skip-proofsp nil, to confirm that they are all admissible.
Then it attempts merely to assume the non-local ones to create the
desired theory, by executing the events with ld-skip-proofsp set to
'include-book. Similarly, include-book assumes the non-local ones,
with the understanding that a previously successful certify-book has
performed the admissiblity check.
How can a sequence of events admitted with ld-skip-proofsp nil fail
when ld-skip-proofsp is 'include-book? The key observation is that
in the latter case only the non-local events are processed. The
local ones are skipped and so the non-local ones must not depend
upon them.
Two typical mistakes are suggested by the detection of a local
incompatibility: (1) a locally defined function or macro was used in
a non-local event (and, in the case of encapsulate, was not included
among the signatures) and (2) the witnessing definition of a
function that was included among the signatures of an encapsulate
was not made local.
An example of mistake (1) would be to include among your
encapsulated events both (local (defun fn ...)) and
(defthm lemma (implies (fn ...) ...)). Observe that fn is
defined locally but a formula involving fn is defined
non-locally. In this case, either the defthm should be made
local or the defun should be made non-local.
An example of mistake (2) would be to include (fn (x) t) among your
signatures and then to write (defun fn (x) ...) in your events,
instead of (local (defun fn ...)).
One subtle aspect of encapsulate is that if you constrain any member
of a mutually recursive clique you must define the entire clique
locally and then you must constrain those members of it you want
axiomatized non-locally.
Errors due to local incompatibility should never occur in the
assumption of a fully certified book. Certification ensures against
it. Therefore, if include-book reports an incompatibility, we
assert that earlier in the processing of the include-book a warning
was printed advising you that some book was uncertified. If this is
not the case -- if include-book reports an incompatibility and there
has been no prior warning about lack of certification -- please
report it to us.
When a local incompatibility is detected, we roll-back to the world
in which we started the encapsulate or include-book. That is, we
discard the intermediate world created by trying to process the
events skipping proofs. This is clean, but we realize it is very
frustrating because the entire sequence of events must be processed
from scratch. Assuming that the embedded events were, once upon a
time, processed as top-level commands (after all, at some point you
managed to create this sequence of commands so that the local and
non-local ones together could survive a pass in which proofs were
done), it stands to reason that we could define a predicate that
would determine then, before you attempted to embed them, if local
incompatibilities exist. We hope to do that, eventually.
We conclude with a subtle example of local incompatibility. The problem
is that in order for foo-type-prescription to be admitted using the
specified :typed-term (foo x), the conclusion (my-natp (foo x))
depends on my-natp being a compound-recognizer. This is fine on the
first pass of the encapsulate, during which lemma my-natp-cr is
admitted. But my-natp-cr is skipped on the second pass because it is
marked local, and this causes foo-type-prescription to fail on the
second pass.
(defun my-natp (x)
(declare (xargs :guard t))
(and (integerp x)
(<= 0 x)))
(defun foo (x)
(nfix x))
(encapsulate
()
(local (defthm my-natp-cr
(equal (my-natp x)
(and (integerp x)
(<= 0 x)))
:rule-classes :compound-recognizer))
(defthm foo-type-prescription
(my-natp (foo x))
:hints (("Goal" :in-theory (enable foo)))
:rule-classes ((:type-prescription :typed-term (foo x)))))
