When keeping too many files opened, coqide fills up all memory and stop responding

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4074
From: @charguer
Reported version: 8.5
CC: @gares, @silene, @ppedrot

[coqbot]

Comment author: @charguer

Hi,

Would it be possible to limit the number of buffers in CoqIDE for which coqtop is running? Else one can crash the system with less than a dozen buffer opened.
Maybe a limit that can be modified in the preferences, with a default value of 3 or 4.

Thanks,
Arthur

[coqbot]

Comment author: @charguer

Another approach would be to interrupt all threads when the free memory falls below 100Mb. Indeed, when coq starts swapping, it becomes pretty much useless.

Best,
Arthur

[coqbot]

Comment author: @gares

I guess the simplest thing is to have CoqIDE garbage collect (i.e. kill coqtop) of the oldest tab when a threshold is passed (user configurable).

[coqbot]

Comment author: @ppedrot

Why can't we share the coqtop processes between CoqIDE tabs?

[coqbot]

Comment author: @gares

We could. It would require changing XML the protocol (since each message has to contain the buffer identifier) and supporting that in Coq. The STM state can be backed up and restored, you could hot swap it.

But:

• a few things are not really first class. for example the OCaml C runtime for vm_compute. You have only one of these
• it is not clear we would save memory. How much of the states would be shared? If the answer is very little, then there is no gain in having only 1 coq process.

BTW, What I propose is what browsers do to solve the very same problem.

[coqbot]

Comment author: @silene

Could you elaborate on the issue with vm_compute? I don't remember it having any global state.

By sharing the coqtop process, we should be able to share the libraries, since the various tabs presumably rely on the same libraries. What we would lose is that, if coqtop is busy in one tab (e.g. goto-end), the other tabs become unresponsive.

[coqbot]

Comment author: @ppedrot

Isn't there a way to make Coq dump parts of the state graph to the disk? Just like a sleep-on-disk feature. This would probably greatly reduce the memory use of Coq.

[coqbot]

Comment author: @silene

Yes, we could use the input/output state feature for that purpose. It is deprecated, but last time I checked, it worked mostly well.

[coqbot]

Comment author: @gares

The C runtime has a state, all functions translated to byte code site there.

If you run "ocaml" and you type "let f x = .... ;;" you get an extra entry
f in the runtime. It is more complex than that in Coq, but you have the same problem: you can mask f, not remove it, as far as I know. Also, there is 1 runtime, where all byte code would enter (not 1 runtime per proof, or per tactic...).
Also, the context in the env data structure sometimes holds pointers to the C side to "already evaluated" bytecode (a cache).

I'm not saying that it is a bad idea to share the same coqtop, I'm just saying
that it is orders of magnitude more complex (and also complementary) to the very pedestrian solution browsers adopt.

[coqbot]

Comment author: @charguer

Shall this bug be closed as "won't fix"? If so, please go ahead.

[coqbot]

Comment author: @ppedrot

I don't think it deserves a WONTFIX. The issue is real, and I'm pretty sure I'll try to come up with a mitigating patch when I have more time. I know that's typically the kind of statement people will look up 10 years from now and laugh at, but I'm genuinely willing to reduce this problem. In the meantime, I don't think it hurts to leave the bug report open.