I would like to set up a global counter to be used in some custom tactic I'm working on to get UIDs. I thought I could simply do the usual dance of declaring a
Summary.ref and using
Libobject, but I'm having some trouble making it work. Basically, the counter is incremented correctly within a single proof, but then if I switch to a subsequent proof then the counter starts again at 0.
Is there anything weird going on with
Libobject and proofs?
@Rodolphe Lepigre libobject has little to do with proofs, but with persistance to .vo files
what do you mean by "a single proof"
A summary.ref keeps a value _by sentence_
What I mean is that if I do:
Goal True. Proof. getuid. (* gives 0 *) getuid. (* gives 1 *) auto. Qed. Goal True. Proof. getuid. (* gives 0, I expected 2. *) Abort.
However, I get what I expect with:
Definition xxx : True := ltac:(getuid; auto). (* Gives 0 *) Definition xxx : True := ltac:(getuid; auto). (* Gives 1 *)
It seems that whatever effect happens in a proof is undone (in terms of
Qed time. Maybe that's expected?
Is there any other way I can set up a counter that is automatically roll-backed when retracting?
What's funny is that if I do:
Definition xxx : True := ltac:(getuid; auto). (* Gives 0 *) Definition xxx : True := ltac:(getuid; auto). (* Gives 1 *) Goal True. Proof. getuid. (* Gives 2. *) auto. Qed. Goal True. Proof. getuid. (* Gives 2. *) auto. Qed.
So it seems that the effects in the definitions persist.
This exact semantics seems reasonable for vos/vok/async builds.
And if you want those to work well (and overall, we probably do), vo builds should match their semantics as closely as possible.
Of course, most things don't work like that, and some can't... So all this tells me is that this might be an STM feature?
the summary is reset at the end of the proof
I think the libjobjects are also reset
commands that want their effects to persist need to be classified as side effect, they will then get run again at the end of the proof (this is kinda hacky though)
tactics are not supposed to have side effects btw
I believe the https://github.com/coq-tactician/coq-tactician devs know this problem well and have some hacks to get around it (cc @Lasse Blaauwbroek ?) but in general this is not something that we care about making possible so those hacks should be considered unstable
We have been discussing (due to tactician) having an API to allow tactics to persist state better, but indeed as Gaëtan points out today, the situation is bit a hacky.
You can use a normal ref (instead of Summary.ref) and things will work for you, but indeed that's not stable enough.
The STM choses to reset the state at
Qed, but some other document managers may choose not to.
Coq's API itself is not clear here.
OK makes sense, thanks for your answers, that explains what I was seeing. Is this behaviour documented somewhere?
And yeah, in my case I can use a normal ref, but that suboptimal (although perfectly sound) for my application.
I think the Ltac profiler also persists profiliing information across proofs?
Does it really?
Everything lives in an unsynchronized ref so that info persists across Qed: https://github.com/coq/coq/blob/9368fc24242871d95bb64c6616e4905dad525303/plugins/ltac/profile_ltac.ml#L397
Last updated: Dec 05 2023 at 11:01 UTC