Stream: Coq devs & plugin devs

Topic: Proofview monad snapshot


view this post on Zulip Rodolphe Lepigre (Oct 20 2022 at 16:04):

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

view this post on Zulip Rodolphe Lepigre (Oct 20 2022 at 16:05):

(For context: this is for logging debug messages.)

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2022 at 16:06):

I guess we could implement that, but this is playing with fire as we also have some pieces of the state that are imperative.

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2022 at 16:07):

You can have a look at the Logic_monad module, there is a low-level API to expose the internal details of the monad.

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2022 at 16:07):

basically a glorified state

view this post on Zulip Rodolphe Lepigre (Oct 20 2022 at 16:09):

I don't mind fire. :wink: Thanks, I'll have a look at the low-level API.


Last updated: Feb 06 2023 at 00:03 UTC