How to view Theorem Proving in Lean 4 in VSCode?

Stream: lean4

[Ziyuan]

I understand the book can be viewed in VSCode:

If you are reading the book inside of VS Code, you will see a button that reads "try it!" Pressing the button copies the example to your editor with enough surrounding context to make the code compile correctly...You can open this book on VS Code by using the command "Lean 4: Open Documentation View".

The problem is that I cannot find the command "Lean 4: Open Documentation View" (after installing the extension and git-clone-ing the book repository):
Screenshot 2024-10-14 123506.png

I can also run "Lean 4: Docs: Show Documentation Resources" and show the book in VSCode, but that just shows the book in an embedded browser without interactivity:
Screenshot 2024-10-14 123711.png

So what am I missing here?

[Marc Huisinga]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/How.20do.20I.20read.20.22Theorem.20Proving.20in.20Lean.204.22.20inside.20vscode.3F/near/476566886

[Ziyuan]

Marc Huisinga said:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/How.20do.20I.20read.20.22Theorem.20Proving.20in.20Lean.204.22.20inside.20vscode.3F/near/476566886

Good. So I searched in the wrong channel.