## Stream: general

### Topic: Lean stuck for no reason

#### 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

#### Kenny Lau (Jun 14 2020 at 10:18):

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

#### Kenny Lau (Jun 14 2020 at 10:22):

this has something to do with using #check

#### Kenny Lau (Jun 18 2020 at 08:05):

has anyone else come across this error?

#### 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.

#### 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

#### Kenny Lau (Jun 18 2020 at 08:33):

now #check is also evil for some reason

#### Kenny Lau (Jun 18 2020 at 10:29):

update: it seems that the # is causing this issue

#### 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)

@Mario Carneiro

#### Mario Carneiro (Jun 24 2020 at 10:22):

what am I supposed to contribute to this discussion?

#### Mario Carneiro (Jun 24 2020 at 10:22):

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

#### 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)

It was a lean PR

#### Rob Lewis (Jun 24 2020 at 10:24):

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

#### 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

#### 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

#### Kenny Lau (Jun 24 2020 at 10:26):

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

#### Kenny Lau (Jun 24 2020 at 10:26):

I didn't realize that using tactics is the key

#### Kevin Buzzard (Jun 24 2020 at 10:30):

I realised that three years ago :P

Last updated: May 08 2021 at 19:11 UTC