Lean stuck for no reason

Stream: general

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

this has something to do with using #check

[Kenny Lau]

has anyone else come across this error?

[Yakov Pechersky]

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.

[Kenny Lau]

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

[Kenny Lau]

now #check is also evil for some reason

[Kenny Lau]

update: it seems that the # is causing this issue

[Kenny Lau]

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)

[Kenny Lau]

@Mario Carneiro

[Mario Carneiro]

what am I supposed to contribute to this discussion?

[Mario Carneiro]

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

[Kenny Lau]

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

[Kevin Buzzard]

It was a lean PR

[Rob Lewis]

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

[Mario Carneiro]

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

[Gabriel Ebner]

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

[Kenny Lau]

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

[Kenny Lau]

I didn't realize that using tactics is the key

[Kevin Buzzard]

I realised that three years ago :P