telling lean not to compile

Stream: new members

[jachym simon]

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]

You can write #exit and lean will ignore everything that comes after it

[Bhavik Mehta]

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]

Also, if you use VScode, you can select a bunch of code and hit Ctrl-/, and it will (un)comment the entire selection.

[Johan Commelin]

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]

Awsome, thanks!

I am using vscode, but the shortcut doesnt work. But the #exit thing is perfect

[Marc Huisinga]

Bhavik Mehta said:

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

is the latter commonly used?

[Kevin Buzzard]

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]

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)