Remove document from state table when it is closed.

[rtetley]

Closes #751

• make the limit configurable
• what to do when tabs are invisible but not purged?

[gares]

We could use ocaml GC module to know the memory footprint and let the user declare a cap above which we purge closed tabs.

[gares]

@rtetley I did look at this PR implementing the memory reclaim when the memory footprint > 4G (should be configurable I guess).

There are two problems:

• I added a visible attribute to each tab, and there is a lot of code that is done on all tabs. Now we could only operate on visible tabs, but before this patch I really don't understand what the code was doing
• Removing tabs for the states table does not seem to help much in reclaiming memory, so either I'm misusing the Gc API or the state is also referenced by something else. Try to open a large file, like Pfff.v and close the tab. I now print how much memory was reclaimed.

[gares]

Thanks Gaetan, that clearly helped! Indeed the stack is a root. Kudos.

There is still something bad, I don't know if we should used some memory profiler.
If I open and close Pfff (and set the treshold to 0G, so that it always collects):

[lspManager          , 722507, 1719490340.485819] memory footprint 3967614976 -> 2680127488

(3.97G -> 2.68G)
while if I open a trivial file

[lspManager          , 722939, 1719490376.821685] memory footprint 93913088 -> 124223488

(93.9M -> 124M)
So clearly just parsing Pfff leaves a crapload of memory hanging

[gares]

Closing the trivial buffer actually increses the memory, I don't know how Gc.compact can result in that.

[SkySkimmer]

Closing the trivial buffer actually increses the memory, I don't know how Gc.compact can result in that.

Since you measure heap_words which is the major heap size, maybe something got promoted from minor to major?
Or it got resized but the live_words count decreased?

[gares]

update it is not reproducible, this time it went down to 500M, that is still huge, but 5 times smaller. So I guess the measure implemented in this PR is OKish.

The other question for @rtetley is still valid: why is the code doing something on invisible tabs? Is it wanted? Should I systematically skip working on invisible tabs (even if their state is not purged)?

[SkySkimmer]

What is the state of the installed summary (eg the parser state, Global.env, etc) when running the Gc.compact?

[gares]

Exactly, this is what could have changed, since this time I worked on the smaller tab before closing the huge one.

It means that calling compact without installing a minimal state may not work well. Looking into it.

[gares]

Bingo! it now goes to 100M without fiddling with other tabs

[SkySkimmer]

What's the reason for doing replace with visible = false then filtering instead of doing Hashtbl.remove?

[rtetley]

You don't necessarily want to remove the execution state of the document when you close it. For example you might close a document by mistake.

[gares]

The point is that, if memory allows for it, we want to keep the coq sessions alive.

It is not uncommon to close a tab and reopen it.
In VSCode you have the usual browser shortcut for it, ctrl-w to close and shift-ctrl-t to open the last closed tab.
In this scenario we want to be nice to the users and not lose their session.

[SkySkimmer]

Does reopening the tab get the saved state with the current code?

Also I guess the consider_purge should be delayed a bit since big sessions are the ones that are the worst to lose by mistake.

[rtetley]

Good question. Probably not at the moment.

For the consider_purge a reasonable alternative would be to send a popup message to the user when memory runs out asking him if he wants to purge ?

[rtetley]

I think we are good to go. @gares ?