		Search-engine friendly clone of the ACL2 documentation.

Raw-lisp-error

Live-stobj-in-proof

Error messages about “live” stobjs during proofs

It is possible to see an error like the following. (This error is probably very rare, and perhaps can only occur during a proof.)

***********************************************
************ ABORTING from raw Lisp ***********
********** (see :DOC raw-lisp-error) **********
Error:  A live stobj (for stobj ST) was unexpectedly encountered
        when evaluating a call of the function, ST-INIT.
        See :DOC live-stobj-in-proof.
***********************************************

The solution is generally to disable the executable-counterpart of the offending function. It may well be that the only way to get an unexpected “live” stobj is by the use of swap-stobjs, as suggested by the example shown below (essentially provided by Sol Swords) — which results in a different error message, shown below, than the one above.

First introduce a pair of congruent stobjs.

(defstobj st (fld))
(defstobj st1 (fld1) :congruent-to st)

Now define a function that “initializes” the stobj st by creating a new stobj st1 and swapping the two (see swap-stobjs).

(defun st-init (st)
  (declare (xargs :stobjs (st)))
  (with-local-stobj st1
    (mv-let (st1 st)
      (swap-stobjs st1 st)
      st)))

Here is a proof attempt that results in a raw Lisp error due to a live stobj being introduced by swap-stobjs.

ACL2 !>(thm (not (equal (st-init '(1)) '(nil))))

***********************************************
Note:  SWAP-STOBJS has been called on stobjs named ST1 and ST,
where the value of ST1 is a live stobj but the value of ST is not.
This is an error, as such calls are unsupported; see :DOC swap-stobjs.
Advanced users may find it helpful to evaluate the form
(set-debugger-enable :bt)
to see a backtrace of calls leading to this error;
see :DOC set-debugger-enable.
  Will attempt to exit the proof in progress;
  otherwise, the next interrupt will abort the proof.
  For an immediate abort see :DOC abort-soft.
***********************************************

The message above might explain the error.  If not, and
if you didn't cause an explicit interrupt (Control-C),
then it may help to see :DOC raw-lisp-error.

To enable breaks into the debugger (also see :DOC acl2-customization):
(SET-DEBUGGER-ENABLE T)

Summary
Form:  ( THM ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

*** Note: No checkpoints to print. ***

ACL2 Error [Failure] in ( THM ...):  See :DOC failure.

******** FAILED ********
ACL2 !>

In fact, that formula is not a theorem! Through Version 8.6, ACL2 mistakenly proved this alleged theorem by evaluating the indicated call of st-init to obtain an actual Lisp array, because of how ACL2 handles stobjs in Lisp. But now ACL2 produces the error displayed just above.

The error is avoided if we disable the executable-counterpart of the offending function, st-init. Indeed, the following theorem, which contradicts the false claim above and disables the offending executable-counterpart, shows that the logical value of (st-init '(1)) is indeed '(nil).

(thm (equal (st-init '(1)) '(nil))
     :hints(("Goal" :in-theory (disable (:e st-init)))))