Zulip Chat Archive

Stream: general

Topic: Lean stuck for no reason


view this post on Zulip Kenny Lau (Jun 14 2020 at 10:18):

I have not figured out how to reproduce this yet, but sometimes Lean gets stuck (i.e. freezes) for no reason and refuses to compile anything for like 10 seconds

view this post on Zulip Kenny Lau (Jun 14 2020 at 10:18):

this is a new error (i.e. should be caused by 3.16.0)

view this post on Zulip Kenny Lau (Jun 14 2020 at 10:22):

this has something to do with using #check

view this post on Zulip Kenny Lau (Jun 18 2020 at 08:05):

has anyone else come across this error?

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 08:07):

I had something similar hang my machine completely. Using a work-around by limiting memory accessible to Lean via VSCode preferences. I set mine to 1GB. Haven't have complete freezes since.

view this post on Zulip Kenny Lau (Jun 18 2020 at 08:32):

well my workaround is to restart Lean just like what I would do for the evil #print bug

view this post on Zulip Kenny Lau (Jun 18 2020 at 08:33):

now #check is also evil for some reason

view this post on Zulip Kenny Lau (Jun 18 2020 at 10:29):

update: it seems that the # is causing this issue

view this post on Zulip Kenny Lau (Jun 24 2020 at 10:21):

it might also be noteworthy that if it is allowed to compile, then eventually one runs into the replace bug (i.e. too much memory consumed)

view this post on Zulip Kenny Lau (Jun 24 2020 at 10:21):

@Mario Carneiro

view this post on Zulip Mario Carneiro (Jun 24 2020 at 10:22):

what am I supposed to contribute to this discussion?

view this post on Zulip Mario Carneiro (Jun 24 2020 at 10:22):

I think the by sorry # bug has been fixed in a recent PR

view this post on Zulip Kenny Lau (Jun 24 2020 at 10:23):

I don't know what that bug is, but this bug persists (my mathlib has just been updated)

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 10:23):

It was a lean PR

view this post on Zulip Rob Lewis (Jun 24 2020 at 10:24):

It was also like two hours ago so it hasn't landed anywhere yet.

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

it will be a while before it propagates to mathlib. Maybe just avoid writing that for now

view this post on Zulip Gabriel Ebner (Jun 24 2020 at 10:24):

This is the other thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/memory.20bug.3F

view this post on Zulip Kenny Lau (Jun 24 2020 at 10:26):

oh, so that is why I couldn't reproduce it

view this post on Zulip Kenny Lau (Jun 24 2020 at 10:26):

I didn't realize that using tactics is the key

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 10:30):

I realised that three years ago :P


Last updated: May 08 2021 at 19:11 UTC