I'm trying to do something a bit silly as part of a plugin, where I would like to keep a thunk of some (pure, never failing, but expensive) Ltac2 computation to be forced much later, after we left the tactic monad from which the computation arose, but in ideally the same state (environment, evar map, I don't care so much about goals).
Basically, what I'm asking is: is there a way to implement something like the following? Even in an imperfect way.
type snapshot (* "state" of the tactic monad at some point *) val save : snapshot tactic val restore : snapshot -> unit tactic
(For context: this is for logging debug messages.)
I guess we could implement that, but this is playing with fire as we also have some pieces of the state that are imperative.
You can have a look at the Logic_monad module, there is a low-level API to expose the internal details of the monad.
basically a glorified state
I don't mind fire. :wink: Thanks, I'll have a look at the low-level API.
Last updated: Jun 09 2023 at 07:01 UTC