Zulip Chat Archive

Stream: general

Topic: auto-recompiling

Kenny Lau (May 25 2019 at 07:28):

Is it possible to disable auto-recompiling in VSCode and manually recompile whenever I press Ctrl+Alt+R?

Mario Carneiro (May 25 2019 at 07:33):

ooh that sounds nice

Mario Carneiro (May 25 2019 at 07:33):

I hate being afraid to open a file because it will trigger a recompile

Koundinya Vajjha (May 25 2019 at 14:02):

Or if I accidentally change a character in core.lean and it recompiles everything and my laptop hangs.

Kenny Lau (May 27 2019 at 08:01):

@Gabriel Ebner

Kevin Buzzard (May 27 2019 at 08:12):

I have completely fixed computer-hanging issues with command line lean compilations by always passing an -M4000 flag to lean. Is this sort of thing possible with VS Code? Is it possible to tell VS Code to always use this flag?

The other thing I did (in Ubuntu) was set up some swap space on my desktop, to give me advanced warning of a potential problem. I also have some swap set up on my laptop, just in case, even though it's SSD. Does Windows work in the same way?

Keeley Hoek (May 27 2019 at 09:42):

Yes, there is a vscode extension option to set the memory limit. It has a default value of 4096 I think.

Last updated: Dec 20 2023 at 11:08 UTC