When non-local events won't replay in isolation
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. (But see the Remark at the end of this topic about a related issue with guard-checking.)
Local incompatibilities may be detected while trying to execute the
strictly non-local events of an encapsulate or certify-book call. For example,
How can a sequence of events admitted with ld-skip-proofsp
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 a local definition of
(encapsulate () (local (defun f (x) x)) (defun g (x) x) (defthm f-is-g (equal (f x) (g x))) )
In this case, either the defthm should be made local or, if
we want to export the
An example of mistake (2) would be to include
(encapsulate ( ((fn *) => *) ) (defun fn (x) x) )
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 inclusion of a fully certified book. Certification ensures against it. Therefore, if include-book reports an incompatibility, we claim 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 the ACL2 implementors.
When a local incompatibility is detected during the second pass of an encapsulate or certify-book, the logical world is restored to what it was immediately before that call was evaluated.
Note that for
See fast-cert for a way to skip the local incompatibility check, although that may compromise soundness.
Here is a subtle example of local incompatibility. The problem is
that in order for
(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)))))
Remark. We conclude by remarking that for ``local incompatibility''
in the case of
The example above may be helpful while reading the following general
explanation of how local incompatibility incorporates the setting of
guard-checking. Suppose you are evaluating commands directly in the
top-level read-eval-print loop. One of those commands might be a call of
set-guard-checking that weakens guard-checking from its default