Stream: Coq devs & plugin devs

Topic: Libobject and proofs


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 09:45):

what do you mean by "a single proof"

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 09:46):

A summary.ref keeps a value _by sentence_

view this post on Zulip 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.

view this post on Zulip Rodolphe Lepigre (Apr 21 2023 at 09:48):

However, I get what I expect with:

Definition xxx : True := ltac:(getuid; auto). (* Gives 0 *)
Definition xxx : True := ltac:(getuid; auto). (* Gives 1 *)

view this post on Zulip Rodolphe Lepigre (Apr 21 2023 at 09:50):

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?

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Apr 21 2023 at 10:12):

This exact semantics seems reasonable for vos/vok/async builds.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 10:29):

Coq's API itself is not clear here.

view this post on Zulip 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.

view this post on Zulip Jason Gross (Apr 22 2023 at 04:43):

I think the Ltac profiler also persists profiliing information across proofs?

view this post on Zulip Gaëtan Gilbert (Apr 22 2023 at 06:55):

Does it really?

view this post on Zulip Gaëtan Gilbert (Apr 22 2023 at 06:55):

what info?

view this post on Zulip 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: Jun 17 2024 at 22:01 UTC