Zulip Chat Archive
Stream: general
Topic: vscode
Kenny Lau (Jul 14 2020 at 19:30):
I notice that Lean has been recompiling everything more frequently recently
Kenny Lau (Jul 14 2020 at 19:31):
(my workaround is to restart Lean as always)
Kenny Lau (Jul 15 2020 at 04:53):
am I the only one getting this error?
Kenny Lau (Jul 15 2020 at 04:53):
@Johan Commelin
Johan Commelin (Jul 15 2020 at 04:55):
Unfortunately, I've been spending very little time actually writing lean code in the last couple of weeks... so I can't really confirm anything.
Scott Morrison (Jul 15 2020 at 05:06):
No problems in VSCode recently for me.
Floris van Doorn (Jul 15 2020 at 05:11):
Yeah, I'm noticing in the last couple of weeks that sometimes Lean recompiles a file from the start for no apparent reason. Sometimes when it's done, a single keystroke later it starts from scratch again. (even when lean --make just completes quickly and after restarting VSCode). Couldn't consistently reproduce it though.
Bryan Gin-ge Chen (Jul 15 2020 at 07:34):
Is this the same issue as the one in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/random.20recompiling ?
I don't think there have been any changes that have affected that.
Kenny Lau (Jul 15 2020 at 07:38):
that's when I opened a file or performed #check or #print
Kenny Lau (Jul 15 2020 at 07:38):
now I don't even need to do those
Kenny Lau (Jul 15 2020 at 07:39):
Lean just recompiles everything randomly
Bryan Gin-ge Chen (Jul 15 2020 at 07:43):
Does it happen when you might be triggering an info request from the server? E.g. hovering over some text or clicking a widget in the info view?
Kenny Lau (Jul 15 2020 at 07:44):
perhaps
Bryan Gin-ge Chen (Jul 15 2020 at 07:45):
Just as with Lean issues, it would be good to get a kind of #mwe for this. In the other thread there was some toy example I came up with, but I don't think I ever figured out why it behaved differently on Windows vs macOS vs Linux.
Edward Ayers (Jul 15 2020 at 20:56):
I also sometimes get something like this but I can't repro reliably. It seems to depend on what editor windows I have open.
Edward Ayers (Jul 15 2020 at 20:56):
I made a github issue a while ago but its not useful because I can't get it to repro https://github.com/leanprover-community/lean/issues/379
Edward Ayers (Jul 15 2020 at 21:00):
My guess is that every time a file changes, lean spawns a task and in some cases they are not being cancelled properly and so you get vast numbers of tasks all checking the same thing.
Kenny Lau (Jul 28 2020 at 09:26):
98% of @Kevin Buzzard's stream: "oh great Lean is recompiling again"
Kevin Buzzard (Jul 28 2020 at 11:16):
It was the combination of the recompiling and the autoparams and the fact that I didn't know any definitions so was forever looking at source files
Last updated: Dec 20 2023 at 11:08 UTC