LOCAL-INCOMPATIBILITY

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.