Zulip Chat Archive

Stream: general

Topic: Accidentally editing core files causing large recompile


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?

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.

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: Dec 20 2023 at 11:08 UTC