Zulip Chat Archive
Stream: general
Topic: checking nothing
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?
Kenny Lau (Jun 27 2020 at 14:05):
and, following that, how to disable Lean completely?
Johan Commelin (Jun 27 2020 at 14:06):
Why would you want to disable Lean? Might as well turn off your laptop completely :wink:
Mario Carneiro (Jun 27 2020 at 14:06):
You get out of date information
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
Mario Carneiro (Jun 27 2020 at 14:07):
unless you deliberately crash the server and avoid the restart button
Mario Carneiro (Jun 27 2020 at 14:08):
but it will continue to receive change notifications internally I believe
Kenny Lau (Jun 27 2020 at 14:08):
where is the information coming from?
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
Mario Carneiro (Jun 27 2020 at 14:08):
from the last valid check
Kenny Lau (Jun 27 2020 at 14:08):
so I don't want to run the Lean compiler twice
Mario Carneiro (Jun 27 2020 at 14:08):
I've done that before
Mario Carneiro (Jun 27 2020 at 14:09):
there is no "kill server" button in vscode
Kenny Lau (Jun 27 2020 at 14:09):
can we write a code that will crash the server?
Kenny Lau (Jun 27 2020 at 14:09):
(or just write a code that will kill the server and add the button)
Mario Carneiro (Jun 27 2020 at 14:09):
kill -9 lean or somesuch
Mario Carneiro (Jun 27 2020 at 14:10):
I usually use the process manager if I see two competing lean processes
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: Dec 20 2023 at 11:08 UTC