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
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.
(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.
( ((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
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
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
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)
(local (defthm my-natp-cr
(equal (my-natp x)
(and (integerp x)
(<= 0 x)))
(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