Stream: Coq devs & plugin devs

Topic: Reachable evarmaps


view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 10:24):

As a side-product of https://github.com/coq/coq/issues/12487, I discovered that there is proof-specific data that survives proof closure.

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 10:24):

Does anybody know whether the STM keeps a pointer to evarmaps after proof closure in some way?

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 10:25):

That's currently my suspect number 1, but it's very hard to tell from the code.

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 10:26):

FTR, the incriminated data is evar instances, which doesn't exist anymore in the proof term after Qed / Defined.

view this post on Zulip Enrico Tassi (Jun 12 2020 at 12:08):

yes, each system state includes an evar map if there was an open proof. In order to jump back to that state you keep the evar map at that point (I'm talking of interactive mode)

view this post on Zulip Enrico Tassi (Jun 12 2020 at 12:08):

It is not the case if you are in coqc mode, there only the last (current) state is kept

view this post on Zulip Enrico Tassi (Jun 12 2020 at 12:09):

it is not really "the STM", but rather the caching strategy you use in the STM

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:42):

Well, I definitely observe those dangling evarmaps in coqc mode.

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:42):

So I suspect we're keeping more stuff still.

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:43):

e.g. just opening a proof mode is enough to leak evars

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:44):

I've just posted this example on the issue:

Definition sigT_eta {A P} (p : @sigT A P)
  : p = existT _ (projT1 p) (projT2 p).
Proof. Admitted.

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:44):

typechecking the type of the lemma generates an evar instance that leaks when calling coqc

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:45):

replacing Definition with Axiom still generates the instance but it's garbage collected at the end of the definition

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:48):

what does Admitted do precisely?

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:49):

I think there's some machinery to refine the admitted statement from the partial proof term

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:49):

maybe that's where the leak occurs?

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:49):

No, it also leaks with Qed / Defined

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:50):

then it must be something in the proof saving code, no?

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:50):

I believe so

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:50):

the STM blocks your path

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:50):

I don't think the VM distinguishes Axiom and Proof. Qed.

view this post on Zulip Maxime Dénès (Jun 12 2020 at 12:51):

(mentioning it since it was on your suspect list)

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:51):

there might be several sources of leaks...

view this post on Zulip Enrico Tassi (Jun 12 2020 at 13:24):

I may recall that the cache saves always the state at the beginning of proofs. It is easy to change, but I'd need a bit more context to understand what the problem is. (it is like that since 8.4 in interactive mode). See the ~cache argument https://github.com/coq/coq/blob/master/stm/stm.ml#L830 and this is where I force to save the state at the beginning of proofs https://github.com/coq/coq/blob/master/stm/stm.ml#L2439 (one could do as in here https://github.com/coq/coq/blob/master/stm/stm.ml#L2752 if the problem is in batch mode)

view this post on Zulip Enrico Tassi (Jun 12 2020 at 13:26):

I don't have the time to read/understand the issue you link @Pierre-Marie Pédrot , if you need more help please give me a brief explanation of what the problem is.

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 14:42):

Cross-posting with the issue, the problem is that the STM keeps a pointer to the summary for every proof opening, even in batch mode

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 14:43):

I tried to tweak by changing the cache boolean, but it explodes in the first Init file

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 14:51):

@Enrico Tassi the problem is fairly easy: introducing memory leaks is bad for your memory consumption...

view this post on Zulip Enrico Tassi (Jun 12 2020 at 14:54):

What was the invariant of the tactic monad again?
More seriously, here we talk about the evar map at the beginning of the proof, just after Lemma which has 1 evar in it. How can this be a visible leak?

view this post on Zulip Enrico Tassi (Jun 12 2020 at 14:55):

IIRC it is purely functional, so the one pointed from there cannot grow a posteriori

view this post on Zulip Enrico Tassi (Jun 12 2020 at 14:56):

I can help removing that entry from the cache, but I'm afraid we are looking at the wrong cause

view this post on Zulip Gaëtan Gilbert (Jun 12 2020 at 14:56):

It has all the evars from the type too
Maybe we could run Optimise Proof when starting it?

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 14:58):

How much of the global state are we keeping in the proof data?

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 15:01):

It does seem like a bad idea to introduce memory leaks just to support Undo

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 15:01):

in batch mode

view this post on Zulip Gaëtan Gilbert (Jun 12 2020 at 15:10):

Is it really for Undo?

view this post on Zulip Maxime Dénès (Jun 12 2020 at 15:11):

it may be for something else too, but at least it is used by Undo

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 15:12):

I don't understand why we would get backward references if it were not for backtracking...

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 15:13):

The fiat-crypto example is still fishy, because it seems that the evars are generated during the proof.

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 15:13):

could it be that abstract triggers such a caching?

view this post on Zulip Maxime Dénès (Jun 12 2020 at 15:15):

Is it an abstract in Defined or in Qed?

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 15:16):

in Defined

view this post on Zulip Enrico Tassi (Jun 12 2020 at 15:22):

Now that I look at the code, it seems that also the Qed node is cached in batch

view this post on Zulip Enrico Tassi (Jun 12 2020 at 15:23):

For both Defined and Qed. Let me check if we save the evar map (even if it is not needed at all)

view this post on Zulip Enrico Tassi (Jun 12 2020 at 15:28):

It should not, https://github.com/coq/coq/blob/master/stm/stm.ml#L2547

These states are mostly for Undo (in interactive mode). In batch mode they should all be droppable at some point (eg at Qed time you should be able to drop the one saved at proof opening time, but I never wrote the code).

view this post on Zulip Enrico Tassi (Jun 12 2020 at 15:29):

I don't think abstract does anything special.

view this post on Zulip Enrico Tassi (Jun 12 2020 at 15:29):

(for once)


Last updated: Oct 16 2021 at 03:02 UTC