Big mutual can crash VSCode

Stream: lean4

[Mac Malone]

Today I learned that a big, slow mutual declaration can crash not just the server, but VSCode itself! :rofl: I sadly do not have MWE (as the big mutual is essentially my whole project), but I thought it might be a possibility worth noting.

[Mario Carneiro]

Compiling mathlib often kills vscode for me. Anything that uses too much memory could potentially wake up the oom killer