How do I read "Theorem Proving in Lean 4" inside vscode?

Stream: new members

[Paul Crowley]

You can open this book on VS Code by using the command "Lean 4: Open Documentation View". say the instructions. However, there's no such command. There's Show documentation resources, but that seems to open a browser window in vscode, and following the links doesn't result in a view that includes a try it! button

[Derek Rhodes]

Hi Paul, in VS Code, if you type Ctrl-Shift-p, then a text input box (command palette) will pop up at the top of the editor. If you start typing: "Lean 4: Open ..." options should start popping up that look like this:
image.png.

[Paul Crowley]

Screenshot 2024-10-12 at 20.18.46.png
This is what I see

[Paul Crowley]

As I said, I tried "Show documentation resources" but it just opened a browser-like window in VSCode; it led to a view of the manual that didn't have "try it" buttons

[Derek Rhodes]

oh sorry, my mistake I somehow managed to miss the last part of your post!

[Derek Rhodes]

By the way, where are you reading: "You can open this book on VS Code by using the command ..." ? Is that from within the book Theorem Proving in Lean 4 ?

[Derek Rhodes]

It sounds like a web version of the book?

[Derek Rhodes]

I don't see the "try it!" buttons from within VS code either.

[Paul Crowley]

https://lean-lang.org/theorem_proving_in_lean4/introduction.html
Screenshot 2024-10-12 at 20.34.48.png

[Derek Rhodes]

looks like there is a similar issue reported 2 years ago on github:
https://github.com/leanprover/theorem_proving_in_lean4/issues/30

[Paul Crowley]

This issue is closed though. It looks like "Open documentation view" used to work for this, but that command no longer exists.

[Marc Huisinga]

theorem_proving_in_lean4#124 has been open for a while now

[Paul Crowley]

aha thank you! Is this a temporary workaround, or is the idea of opening the book in vscode no longer something Lean wants to do?

[Marc Huisinga]

You can open the book in VS Code using the adjusted instructions in the link above - the only meaningful differences are that you now need an internet connection to navigate the book from within VS Code and that the "try it" button is gone and you have to copy things over instead of pressing a single "try it" button.

I may pick up working on better documentation integration in the Lean 4 VS Code extension again for Verso at some point in the future, but the old DocView in the Lean 4 VS Code extension is definitely gone for now.

The reason was that the old DocView had trouble with displaying most content, so I replaced it with VS Code's integrated Simple Browser, which doesn't struggle with displaying most content and is much nicer to use.

[Paul Crowley]

Got it! Sounds like just using a standard browser will work just as well. Thanks!