Add configurable limit to number of coq-lsp instances running

[Alizter]

When editing many .v files, opening them all quickly eats up memory. We should add a configuration option to limit the number of files coq-lsp can look at to a given number. This will prevent running LSP on too many files at once.

[ejgallego]

Mmm, how do you propose to implement that, I'm unsure we can do something like this and still remain LSP compliant?

Note that once #49 and #24 are implemented memory consumption for many docs should be much better.

Instead, maybe what we could implement is just a total memory limit for coq-lsp, in general we should have mem and thread limit. But that' s at least 0.2 material, for some technical reasons that's not so easy to do with the way Coq and OCaml work.

It is a pity we can't save the cache to disk tho :S that'd be so useful, but see todo.org file for current issues.

[Alizter]

I suppose the best way to handle this is a combination of lazy document checking and memprof limits.

[ejgallego]

memprof limits are geared more towards limiting single sentences, I think here, as we handle everything under one instance, it is really about #348 + better cache eviction.

[ejgallego]

Note that once I get the require from memory PR Coq upstream memory consumption for things like HoTT and multiple documents should be reduced dramatically (as requires may be shared)!

Do you have test cases that are eating too much memory?

[Alizter]

@ejgallego One stupid way to achieve this is to open every .v file in HoTT and run coq-lsp.

[ejgallego]

That's a great idea, I can try to automate that. Maybe every file is too much? What is a set of files where you start to have pain?

[Alizter]

You can try something heavy like everything in theories/Homotopy for instance. It can happen in development if you are tweaking lots of files at once in a name change or something.