Rodolphe Lepigre (Apr 21 2023 at 09:42): Rodolphe Lepigre (Apr 21 2023 at 09:42):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?
Emilio Jesús Gallego Arias (Apr 21 2023 at 09:45):@Rodolphe Lepigre libobject has little to do with proofs, but with persistance to .vo files
Emilio Jesús Gallego Arias (Apr 21 2023 at 09:45):what do you mean by "a single proof"
Emilio Jesús Gallego Arias (Apr 21 2023 at 09:46):A summary.ref keeps a value _by sentence_
Rodolphe Lepigre (Apr 21 2023 at 09:47):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 Libobject) at Qed time. Maybe that's expected?
Is there any other way I can set up a counter that is automatically roll-backed when retracting?
Rodolphe Lepigre (Apr 21 2023 at 09:54):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.
Paolo Giarrusso (Apr 21 2023 at 10:12):This exact semantics seems reasonable for vos/vok/async builds.
Paolo Giarrusso (Apr 21 2023 at 10:14):And if you want those to work well (and overall, we probably do), vo builds should match their semantics as closely as possible.
Paolo Giarrusso (Apr 21 2023 at 10:16):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?
Gaëtan Gilbert (Apr 21 2023 at 10:16):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
Emilio Jesús Gallego Arias (Apr 21 2023 at 10:27):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.
Emilio Jesús Gallego Arias (Apr 21 2023 at 10:29):The STM choses to reset the state at Qed, but some other document managers may choose not to.
Emilio Jesús Gallego Arias (Apr 21 2023 at 10:29):Coq's API itself is not clear here.
Rodolphe Lepigre (Apr 21 2023 at 10:52):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.
Jason Gross (Apr 22 2023 at 04:43):I think the Ltac profiler also persists profiliing information across proofs?
Gaëtan Gilbert (Apr 22 2023 at 06:55):Does it really?
Gaëtan Gilbert (Apr 22 2023 at 06:55):what info?
Jason Gross (Apr 22 2023 at 22:18):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