Zulip Chat Archive

Stream: new members

Topic: vscode lean installation issue


Jia Li (Jun 19 2022 at 17:07):

Hi ! I am new to lean, I run into a problem of installation (please tell me if i am posting the message at a wrong place)
I have followed this installation guide https://leanprover-community.github.io/install/debian_details.html
Then when I try to run "#eval 1+1", i got

Watchdog error: Cannot read LSP request: Invalid header field: "{\"command\":\"sync\",\"file_name\":\"/home/jia/workspace/lean_scripts/blublu.lean\",\"content\":\"#eval 1+1\\nopen nat\",\"seq_num\":0}\n"

and a pop up

Server has stopped with error code 1

My OS is Ubuntu 20.04.4 LTS and the vscode version is 1.68.1

Do you have an idea what the problem is?


Last updated: Dec 20 2023 at 11:08 UTC