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