WITH-LIVE-STATE

allow a reference to state in raw Lisp
Major Section:  ACL2-BUILT-INS

The macro with-live-state is an advanced feature that very few users will need (basically, only system hackers). Indeed, it is untouchable; see remove-untouchable for how to enable calling with-live-state in the ACL2 loop.

Example Form:
(with-live-state (assign y 3))

General form:
(with-live-state form)
where form is an arbitrary form with a free reference to the variable state.

Logically, (with-live-state FORM) macroexpands to FORM. However, in raw Lisp it expands to:

(let ((state *the-live-state*))
  FORM)

If a form that mentions the variable state might be executed in raw Lisp -- that is, either outside the ACL2 loop or in raw mode (see set-raw-mode) -- then the surrounding the form with with-live-state as shown above can avoid potential warnings or (much less likely) errors. Note however that if state is lexically bound to a state other than the usual ``live'' state, surprising behavior may occur when evaluating a call of with-live-state in raw Lisp or raw mode (either directly by evaluation or at compile time), because with-live-state will override that lexical binding of state by a lexical binding of state to the usual ``live'' state.