Waiting for Lean server to start...

[vithar1]

I am using distribution manjaro linux.

vscode https://aur.archlinux.org/packages/visual-studio-code-bin

lean 4 plugin.

I get the following error when trying to get the result of interpreting the proof on lean:

`Waiting for Lean server to start...

I did about the following steps in order to work with lean:

1. Install elan https://leanprover-community.github.io/install/linux.html
2. run command source $HOME/.elan/env
3. install vscode and plugin for vscode lean4
4. create enviroment for python
5. pip isntall mathlibtools
6. create project with leanproject new project
7. cd project
8. code .

[PatrickMassot]

This description mixes Lean 3 and Lean 4 so it cannot work. You should decide which version you want to use. mathlibtools and leanproject are Lean 3 only, and you opened this issue for Lean 3 vscode extension.

[vithar1]

Thanks for the advice. Installing the Lean 3 plugin helped me.