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