Crash/slowdown when asynchronously stepping to point in large files

[MevenBertrand]

When stepping through large files (those of MetaCoq) using the asynchronous interpret to point feature, I often get first a slowdown/freeze of my system, then recover from the slowdown but with a greyed out proof goal window.
Using the synchronous interpret to point seems to work, and stepping manually in smaller steps also mitigates the issue.

I guess this means that something, somewhere, chokes on my file then crashes, but not sure what, nor how I can debug this further – I don’t know much about VsCode.

[gares]

Probably the Coq state (memory usage of a single coq instace) is too large to be duplicated via not-fork. Then the kernel kills the worker. You should see that in the dmesg log.

The new LSP thing we are working on should work better, since it uses fork on unix (copy on windows), while the old STM copies on all systems.

[MevenBertrand]

Using dmesg I get

[ 4920.969314] oom-kill:constraint=CONSTRAINT_NONE,nodemask=(null),cpuset=/,mems_allowed=0,global_oom,task_memcg=/user.slice/user-1000.slice/[email protected],task=coqidetop.opt,pid=10508,uid=1000
[ 4920.969334] Out of memory: Killed process 10508 (coqidetop.opt) total-vm:2993924kB, anon-rss:2111052kB, file-rss:0kB, shmem-rss:0kB, UID:1000 pgtables:4432kB oom_score_adj:0

so indeed it is looks like it.

[gares]

It seems it is using 2G, so 4G with 2 processes. Is your PC under some other load?

[MevenBertrand]

Nothing heavy, no – probably a browser with a few open tabs, maybe another Electron-based application.