After closing the buffer coq-lsp should reduce memory consumption

[Alizter]

Here is a common situation:

1. open Pff.v
2. Let it eat lots of memory
3. close Pff.v
4. Observe that coq-lsp is still eating lots of memory.

Can we somehow invoke the OCaml GC to come and cleanup our memory usage when we close a document?

edit:

• [memo] Cache control and eviction improvements #662 implements a rudimentary "Trim cache" request, that can help with this
• we still want to have more automatic memory management

[ejgallego]

This is because Pff.v entries in the memo table are still cached, but indeed it is not clear what to do.

GC will do nothing in this case; you wanna trim the memo hashtbl.

Maybe the user would reopen the doc, and in that case it'd be very useful for the cache to work (this doesn't work today, but we could make it work tho).

Note that I don't think it is a good idea for the cache to be per-file, even if that doesn't matter a lot as of today.

I guess caching-wise, ideally we'd like the user just to set the memory consumption of the cache, and then coq-lsp can try to do its best.

Unfortunately the keys we have for Coq states are not stable, which doesn't allow us to have a sound saving strategy for the disk; it'd be great to improve that, but it is not easy.