		Search-engine friendly clone of the ACL2 documentation.

Miscellaneous

Local-incompatibility

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, 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. Certify-book does something similar, so that when include-book assumes the non-local events in the book, we are confident that the previously successful certification has performed the necessary admissibility 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 a local definition of f and a non-local theorem about f, for example as follows.

(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 defthm, then the defun of f should be made non-local. Similar analysis holds if the events in the encapsulate call above are instead in a book.

An example of mistake (2) would be to include ((fn *) => *) among your signatures and then to write (defun fn (x) ...) in your events, instead of (local (defun fn ...)), as shown in the example below. In essence, this is an error because fn is exported twice: once by the signature and once by the defun.

(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 certify-book, local incompatibility could be caused by an event that is local either in the certification world (see portcullis) or in the book itself. ACL2 checks during certify-book for local incompatibility by rolling back the world — back through the first portcullis command that generates a local event, or if there is none, then back through the first local event in the book (with the general exception of those inside an encapsulate, but see final Remark below) — and then including the book. But all that is skipped in the absence of either kind of local event.

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

Remark. We conclude by remarking that for ``local incompatibility'' in the case of certify-book, the notion of ``local'' is a bit more comprehensive than the name suggests, in that it can involve guard-checking in the following situation. For example, in a fresh ACL2 session evaluate the command (set-guard-checking :none) followed by (table foo 0 (car 3)). Then any attempt to certify a book should fail, since subsequent inclusion of that book would fail with a guard violation; that's because the set-guard-checking call was not saved in the certificate file, hence was not evaluated when evaluating (car 3) while attempting to include the book.

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 behavior, i.e., (set-guard-checking VAL) where VAL is other than t, :nowarn, or :all. This command does not change the logical world, so it will not be part of the book's portcullis commands. In that sense, it is like a local portcullis command. ACL2 notices this case and insists that any portcullis event evaluated with guard-checking that is weaker than the default must be rolled back during the check for local incompatibilities.