Major Section: SWITCHES-PARAMETERS-AND-MODES
This documentation topic assumes familiarity with abstract stobjs. See defabsstobj.
Below we explain what is meant by an error message such as the following.
ACL2 Error in CHK-ABSSTOBJ-INVARIANTS: Possible invariance violation for an abstract stobj! See :DOC set-absstobj-debug, and PROCEED AT YOUR OWN RISK.
The use of
(set-absstobj-debug t) will make this error message more
informative, as follows, at the cost of slower execution -- but in
practice, the slowdown may be negligible (more on that below).
ACL2 Error in CHK-ABSSTOBJ-INVARIANTS: Possible invariance violation for an abstract stobj! See :DOC set-absstobj-debug, and PROCEED AT YOUR OWN RISK. Evaluation was aborted under a call of abstract stobj export UPDATE-FLD-NIL-BAD.
You may be best off starting a new ACL2 session if you see one of the errors
above. But you can continue at your own risk. With a trust tag
(see defttag), you can even fool ACL2 into thinking nothing is wrong, and
perhaps you can fix up the abstract stobj so that indeed, nothing really is
wrong. See the community book
how to do that. That book also documents the
:always keyword and a
special value for the first argument,
Examples: (set-absstobj-debug t) ; obtain extra debug info, as above (set-absstobj-debug t :event-p t) ; same as above (set-absstobj-debug t :on-skip-proofs t) ; as above, but even in include-book (set-absstobj-debug t :event-p nil) ; returns one value, not error triple (set-absstobj-debug nil) ; avoid extra debug info (default) General Form: (set-absstobj-debug val :event-p event-p ; default t :always always ; default nil :on-skip-proofs on-skip-proofs ; default nil )where the keyword arguments are optional with defaults as indicated above, and all supplied arguments are evaluated except for
on-skip-proofsp, which must be Boolean (if supplied). Keyword arguments are discussed at the end of this topic.
Recall (see defabsstobj) that for any exported function whose
function might (according to ACL2's heuristics) modify the concrete stobj
non-atomically, one must specify
:PROTECT t. This results in extra code
generated for the exported function, which provides a check that atomicity
was not actually violated by a call of the exported function. The extra code
might slow down execution, but perhaps only negligibly in typical cases. If
you can tolerate a bit extra slow-down, then evaluate the form
(set-absstobj-debug t). Subsequent such errors will provide additional
information, as in the example displayed earlier in this documentation topic.
Finally we document the keyword arguments, other than
:ALWAYS, which is
discussed in a book as mentioned above. When the value of
true, which it is by default, the call of
set-absstobj-debug will expand
to an event. That event is a call of
value-triple. In that case,
:ON-SKIP-PROOFS is passed to that call so that
an effect even when proofs are being skipped, as during
That behavior is the default; that is,
default. Also see value-triple. The value of keyword
must always be either
nil, but other than that, it is ignored