Pierre-Marie Pédrot (Jun 12 2020 at 10:24): 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.
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?
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.
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.
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)
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
Enrico Tassi (Jun 12 2020 at 12:09):it is not really "the STM", but rather the caching strategy you use in the STM
Pierre-Marie Pédrot (Jun 12 2020 at 12:42):Well, I definitely observe those dangling evarmaps in coqc mode.
Pierre-Marie Pédrot (Jun 12 2020 at 12:42):So I suspect we're keeping more stuff still.
Pierre-Marie Pédrot (Jun 12 2020 at 12:43):e.g. just opening a proof mode is enough to leak evars
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.
typechecking the type of the lemma generates an evar instance that leaks when calling coqc
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
Maxime Dénès (Jun 12 2020 at 12:48):what does Admitted do precisely?
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
Maxime Dénès (Jun 12 2020 at 12:49):maybe that's where the leak occurs?
Pierre-Marie Pédrot (Jun 12 2020 at 12:49):No, it also leaks with Qed / Defined
Maxime Dénès (Jun 12 2020 at 12:50):then it must be something in the proof saving code, no?
Pierre-Marie Pédrot (Jun 12 2020 at 12:50):I believe so
Pierre-Marie Pédrot (Jun 12 2020 at 12:50):the STM blocks your path
Maxime Dénès (Jun 12 2020 at 12:50):I don't think the VM distinguishes Axiom and Proof. Qed.
Maxime Dénès (Jun 12 2020 at 12:51):(mentioning it since it was on your suspect list)
Pierre-Marie Pédrot (Jun 12 2020 at 12:51):there might be several sources of leaks...
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)
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.
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
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
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...
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?
Enrico Tassi (Jun 12 2020 at 14:55):IIRC it is purely functional, so the one pointed from there cannot grow a posteriori
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
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?
Pierre-Marie Pédrot (Jun 12 2020 at 14:58):How much of the global state are we keeping in the proof data?
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
Pierre-Marie Pédrot (Jun 12 2020 at 15:01):in batch mode
Gaëtan Gilbert (Jun 12 2020 at 15:10):Is it really for Undo?
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
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...
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.
Pierre-Marie Pédrot (Jun 12 2020 at 15:13):could it be that abstract triggers such a caching?
Maxime Dénès (Jun 12 2020 at 15:15):Is it an abstract in Defined or in Qed?
Pierre-Marie Pédrot (Jun 12 2020 at 15:16):in Defined
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
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)
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).
Enrico Tassi (Jun 12 2020 at 15:29):I don't think abstract does anything special.
Enrico Tassi (Jun 12 2020 at 15:29):(for once)
Last updated: Oct 13 2024 at 01:02 UTC