Reading documentation inside vscode

Stream: lean4

[Ken Sailor]

I'm new to lean and read in the documentation that I can read the documentation inside vscode. Are there any instructions in how to do this? I've got vscode installed on my ubuntu box and lean 4 running fine - I just don't know how to open the documentation inside vscode. Any help?

[Mario Carneiro]

where did you read this? It's possible it was copied from another iteration of the docs

[Mario Carneiro]

some of the tutorials / books / manuals also have a setup for doing this, usually specific to that particular book

[Ken Sailor]

I see. Now I can't find the reference. It seems to me I saw a button in the code snippets I was reading that was supposed to eval the code in lean. If it is not normal thing I can copy and paste. It sounded cool, however, like literate coding taken to the max.

[Mario Carneiro]

I'm not doubting that you saw it, but the setup to do so is context-dependent. It generally amounts to cloning a repo recommended by the doc and opening a markdown side-by-side view

[Ken Sailor]

Thanks. Clearly more complicated than I had hoped, and no instructions in the document as I remember it (just "if you're reading this inside of vscode you can press the button " or some such.

[Ken Sailor]

Actually, I got it finally.
Ctrl-Shift-P and type Lean 4 in the command prompt.
Select from the suggested list "Open Documentation View"
This gives you a choice of the usual texts (like Theorem Proving in Lean)
Choose the text you want, and you can read the book inside of VS Code and click on the Try Me buttons at will.