Zulip Chat Archive

Stream: general

Topic: Accidentally editing core files causing large recompile


view this post on Zulip Keefer Rowan (Jun 02 2020 at 14:43):

How do I prevent myself from accidentally changing files like order/lattice.lean when I'm looking at them in VS Code. I'll be look through them and accidentally hit the wrong key. I quickly hit ctrl-z but that doesn't stop VS Code from recompile a whole bunch of stuff that then takes forever. Any suggestions?

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:45):

After the ctrl-z you can ctrl-shift-p : restart Lean. That will save you the recompilation.

view this post on Zulip Johan Commelin (Jun 02 2020 at 14:46):

Also, you can set the --old flag for the lean server, and it will ignore such changes and use old oleans anyway.


Last updated: May 08 2021 at 04:14 UTC