Zulip Chat Archive

Stream: general

Topic: VScode extension hangs

Patrick Massot (Apr 16 2018 at 20:48):

Tonight VScode refuses to let me use lean. I have code that compiles fine using the command line lean, but in VScode orange side bars stay for a very long time before having excessive memory consumption

Patrick Massot (Apr 16 2018 at 20:48):

I'm using 04-06 nighly

Patrick Massot (Apr 16 2018 at 20:48):

which the one recommended by current mathlib head

Patrick Massot (Apr 16 2018 at 20:49):

Is there any way one can check Lean version from VScode?

Patrick Massot (Apr 16 2018 at 20:52):

Hum, I removed lean from my old before-elan place and VScode doesn't find it anymore

Patrick Massot (Apr 16 2018 at 20:53):

Damnit. I had a Lean path hardcoded in VScode

Kevin Buzzard (Apr 16 2018 at 20:54):

:-)

Kevin Buzzard (Apr 16 2018 at 20:54):

elan changed my .profile

Patrick Massot (Apr 16 2018 at 20:54):

Now it's all working

Kevin Buzzard (Apr 16 2018 at 20:54):

so I have to be careful now

Last updated: Dec 20 2023 at 11:08 UTC