Reading “Theorem Proving in Lean4” in VSCode

Stream: new members

[Paul Talma]

Hi all,

Total Lean novice here! The Theorem Proving in Lean4 book states that it can be read in VSCode. I’ve had no success setting that up so far. I’ve installed Rust and Cargo, and then Mdbook. I’ve also run the command install --git https://github.com/leanprover/mdBook mdbook. I’m not sure what should happen next. Any tips?

[Bulhwi Cha]

Hmm, it used to work well two years ago.