VSCode Getting Started

Stream: new members

[Fouad Mardini]

I'm trying to get started with lean. Setup elan and installed lean4 stable and things seem to be working. I can't figure out how to Get the info view in VsCode. I can see with ps aux that lean server is running when I start VSCode

[Patrick Massot]

There is no infoview in Lean 4 yet. Are you sure you want to use Lean 4 instead of Lean 3? Lean 4 is very much work in progress which is not ready for beginners yet.

[Fouad Mardini]

Thanks Patrick! I will switch to 3 then!

[Patrick Massot]

You should have a look at https://leanprover-community.github.io/