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

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

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

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

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)

It is not the case if you are in `coqc`

mode, there only the last (current) state is kept

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

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

So I suspect we're keeping more stuff still.

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

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

replacing `Definition`

with `Axiom`

still generates the instance but it's garbage collected at the end of the definition

what does `Admitted`

do precisely?

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

maybe that's where the leak occurs?

No, it also leaks with Qed / Defined

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

I believe so

*the STM blocks your path*

I don't think the VM distinguishes `Axiom`

and `Proof. Qed.`

(mentioning it since it was on your suspect list)

there might be several sources of leaks...

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)

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.

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

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

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

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?

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

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

It has all the evars from the type too

Maybe we could run Optimise Proof when starting it?

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

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

in *batch* mode

Is it really for Undo?

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

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

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

could it be that `abstract`

triggers such a caching?

Is it an `abstract`

in `Defined`

or in `Qed`

?

in Defined

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

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

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).

I don't think abstract does anything special.

(for once)

Last updated: Aug 02 2024 at 23:01 UTC