Set-persistent-whs-and-ephemeral-whs
maintaining wormhole coherence
General Form:
(set-persistent-whs-and-ephemeral-whs name new-status state)
where name is the name of a wormhole other than one of the
built-in ACL2 system wormholes, and new-status is the desired status of
the wormhole. ACL2 insists that name be supplied as a quoted
constant. The constant *protected-system-wormhole-names* lists the
names of the built-in wormholes and includes brr (the break-rewrite wormhole name), accumulated-persistence, and
fc-wormhole (the name of the wormhole managing forward-chaining-reports), among others.
Set-persistent-whs-and-ephemeral-whs moves new-status into the
wormhole's persistent-whs (the status stored outside of the ACL2 state) and
then executes sync-ephemeral-whs-with-persistent-whs to re-establish
coherence. It returns a modified state.
See wormhole-programming-tips for some tips for using this
function.
