Zulip Chat Archive

Stream: new members

Topic: VS Code issues

Dominique Danco (Sep 21 2022 at 14:35):

I've been having some sketchy behavior with the VS code extension. Sometimes when I open my project, the Lean server will fail to start, and I am occasionally told to install Lean (which is already installed). If I close and restart the folder a few times, it usually eventually starts working properly.

Has anyone seen behavior like this before, or know how to fix it? Thanks

Xiyu Zhai (Sep 21 2022 at 16:03):

I had this on windows.

Last updated: Dec 20 2023 at 11:08 UTC