Don't see Lean 4: Open Documentation View in command palette

Stream: new members

[the leanerrrrrrrrrrrrrrrrrrrrrrr]

image.png
image.png
For some reason, I'm not able to see the Lean 4: Open Documentation View command in the VS Code command palette.

Setup Information:
Operating system: Windows_NT (release: 10.0.19045)
CPU architecture: x64
CPU model: 8 x 11th Gen Intel(R) Core(TM) i7-1165G7 @ 2.80GHz
Available RAM: 16.89 GB

Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.8.0)
Project: No open project

---

Elan toolchains:

installed toolchains
--------------------

leanprover/lean4:stable (default)
leanprover/lean4:v4.8.0-rc2


active toolchain
----------------

leanprover/lean4:stable (default)

Lean (version 4.8.0, x86_64-w64-windows-gnu, commit df668f00e6c0, Release)

I have restarted VS Code and uninstalled/reinstalled lean4 from Extensions multiple times.

[Yaël Dillies]

Stupid question: Is the vscode Lean 4 extension running? I believe this influences what you see in the command palette

[the leanerrrrrrrrrrrrrrrrrrrrrrr]

Yes, it's running

[Marc Huisinga]

the leanerrrrrrrrrrrrrrrrrrrrrrr said:

image.png
image.png
For some reason, I'm not able to see the Lean 4: Open Documentation View command in the VS Code command palette.

Setup Information:
Operating system: Windows_NT (release: 10.0.19045)
CPU architecture: x64
CPU model: 8 x 11th Gen Intel(R) Core(TM) i7-1165G7 @ 2.80GHz
Available RAM: 16.89 GB

Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.8.0)
Project: No open project

---

Elan toolchains:

installed toolchains
--------------------

leanprover/lean4:stable (default)
leanprover/lean4:v4.8.0-rc2


active toolchain
----------------

leanprover/lean4:stable (default)

Lean (version 4.8.0, x86_64-w64-windows-gnu, commit df668f00e6c0, Release)

I have restarted VS Code and uninstalled/reinstalled lean4 from Extensions multiple times.

The command has been renamed to "Docs: Show Documentation Resources". Where did you read about the "DocView: Open DocView" command?

[the leanerrrrrrrrrrrrrrrrrrrrrrr]

It's mentioned at the beginning of both Mathematics in Lean and Theorem Proving in Lean, I can't use "Try it!" from the TPIL web mdbook or follow these steps for MIL
image.png
within the Simple Browser

[Michael Wu]

the leanerrrrrrrrrrrrrrrrrrrrrrr said:

image.png
image.png
For some reason, I'm not able to see the Lean 4: Open Documentation View command in the VS Code command palette.

Setup Information:
Operating system: Windows_NT (release: 10.0.19045)
CPU architecture: x64
CPU model: 8 x 11th Gen Intel(R) Core(TM) i7-1165G7 @ 2.80GHz
Available RAM: 16.89 GB

Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.8.0)
Project: No open project

---

Elan toolchains:

installed toolchains
--------------------

leanprover/lean4:stable (default)
leanprover/lean4:v4.8.0-rc2


active toolchain
----------------

leanprover/lean4:stable (default)

Lean (version 4.8.0, x86_64-w64-windows-gnu, commit df668f00e6c0, Release)

I have restarted VS Code and uninstalled/reinstalled lean4 from Extensions multiple times.

Getting the same issue. When I use the Lean 4 Docs: Show Documentation Resources as suggested by Marc Huisinga, VS Code opens a "Simple Browser" tab where I don't see a "Try it!" button.

[Marc Huisinga]

The "Try it!" button with VS Code integration is gone for now. You can still achieve the same behavior by clicking the "Show hidden lines" button and then copying code over to your editor. I'll see if I can submit PRs to update MiL and TPiL to reflect this fact next week.