Zulip Chat Archive

Stream: general

Topic: checking nothing


view this post on Zulip Kenny Lau (Jun 27 2020 at 14:02):

What does "checking nothing" actually do? Why can I still hover my mouse over the declarations and get information?

view this post on Zulip Kenny Lau (Jun 27 2020 at 14:05):

and, following that, how to disable Lean completely?

view this post on Zulip Johan Commelin (Jun 27 2020 at 14:06):

Why would you want to disable Lean? Might as well turn off your laptop completely :wink:

view this post on Zulip Mario Carneiro (Jun 27 2020 at 14:06):

You get out of date information

view this post on Zulip Mario Carneiro (Jun 27 2020 at 14:07):

It's almost the same as having lean actually off, which I think there is no explicit option for in vscode

view this post on Zulip Mario Carneiro (Jun 27 2020 at 14:07):

unless you deliberately crash the server and avoid the restart button

view this post on Zulip Mario Carneiro (Jun 27 2020 at 14:08):

but it will continue to receive change notifications internally I believe

view this post on Zulip Kenny Lau (Jun 27 2020 at 14:08):

where is the information coming from?

view this post on Zulip Kenny Lau (Jun 27 2020 at 14:08):

Johan Commelin said:

Why would you want to disable Lean? Might as well turn off your laptop completely :wink:

because I'm also compiling it

view this post on Zulip Mario Carneiro (Jun 27 2020 at 14:08):

from the last valid check

view this post on Zulip Kenny Lau (Jun 27 2020 at 14:08):

so I don't want to run the Lean compiler twice

view this post on Zulip Mario Carneiro (Jun 27 2020 at 14:08):

I've done that before

view this post on Zulip Mario Carneiro (Jun 27 2020 at 14:09):

there is no "kill server" button in vscode

view this post on Zulip Kenny Lau (Jun 27 2020 at 14:09):

can we write a code that will crash the server?

view this post on Zulip Kenny Lau (Jun 27 2020 at 14:09):

(or just write a code that will kill the server and add the button)

view this post on Zulip Mario Carneiro (Jun 27 2020 at 14:09):

kill -9 lean or somesuch

view this post on Zulip Mario Carneiro (Jun 27 2020 at 14:10):

I usually use the process manager if I see two competing lean processes

view this post on Zulip Mario Carneiro (Jun 27 2020 at 14:11):

as long as the server isn't using resources there is no need to kill it


Last updated: May 08 2021 at 03:17 UTC