Zulip Chat Archive

Stream: general

Topic: auto-recompiling


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 25 2019 at 07:33):

ooh that sounds nice

view this post on Zulip Mario Carneiro (May 25 2019 at 07:33):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (May 27 2019 at 08:01):

@Gabriel Ebner

view this post on Zulip 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?

view this post on Zulip 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: May 14 2021 at 12:18 UTC