Zulip Chat Archive

Stream: new members

Topic: telling lean not to compile


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

view this post on Zulip Johan Commelin (Dec 02 2020 at 11:54):

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

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

view this post on Zulip Johan Commelin (Dec 02 2020 at 11:55):

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

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

view this post on Zulip jachym simon (Dec 02 2020 at 11:58):

Awsome, thanks!

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

view this post on Zulip Marc Huisinga (Dec 02 2020 at 12:17):

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?

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

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