Stream: new members
Topic: telling lean not to compile
jachym simon (Dec 02 2020 at 11:53):
Hi! Is there some easy way to tell lean not to compile the code from some line onwards? Or to ignore all proofs except the one i am working on?
I tried to use commenting the rest of the code, but since its full of comment blocks i would have to do it on a lot of places, which is annoying... Cheers, Jachym
Johan Commelin (Dec 02 2020 at 11:54):
You can write
#exit and lean will ignore everything that comes after it
Bhavik Mehta (Dec 02 2020 at 11:55):
You can use
#exit on the line you want Lean to stop trying on, or alternatively in VSCode you can set Lean to only check visible lines
Johan Commelin (Dec 02 2020 at 11:55):
Also, if you use VScode, you can select a bunch of code and hit
/, and it will (un)comment the entire selection.
Johan Commelin (Dec 02 2020 at 11:56):
If you don't use VScode, then you are using an editor that also has this feature, but I don't know how tell butterfly this intended effect.
jachym simon (Dec 02 2020 at 11:58):
I am using vscode, but the shortcut doesnt work. But the
#exit thing is perfect
Marc Huisinga (Dec 02 2020 at 12:17):
Bhavik Mehta said:
You can use
#exiton the line you want Lean to stop trying on, or alternatively in VSCode you can set Lean to only check visible lines
is the latter commonly used?
Kevin Buzzard (Dec 02 2020 at 16:53):
If I am switching between branches and want to change a bunch of olean files, I used to switch the check to "checking nothing", do command line leanproject stuff and then switch back and restart Lean -- I had had issues with Lean getting super-confused about olean files randomly changing and then filling up memory compiling stuff when things were in a temporary broken state. Now I tend to just exit VS Code and then restart it though.
Reid Barton (Dec 02 2020 at 16:55):
I think I use it in emacs but just because it is the default (or perhaps I thought it sounded like a good idea long ago)
Last updated: May 09 2021 at 19:11 UTC