Cannot open infoview

[zao05]

May I ask how am I supposed to open infoview? I can't find it in the command palette. I have already installed elan.

[mhuisi]

The InfoView opens automatically when Lean starts up. From your screenshot, it looks like Lean isn't running.

1. How did you install Lean?
2. What output does the Troubleshooting: Show Setup Information command produce?
3. What output is contained in the panel opened by the Troubleshooting: Show Troubleshooting Output command?

[zao05]

1. I installed Lean using the VS Code extensions

2. Troubleshooting: Show Setup Information shows this

**Operating system**: Windows_NT (release: 10.0.26200)
**CPU architecture**: x64
**CPU model**: 12 x AMD Ryzen 5 5500U with Radeon Graphics         
**Available RAM**: 7.88 GB
**VS Code version**: Reasonably up-to-date (version: 1.119.0)
**Lean 4 extension version**: 0.0.236
**Curl installed**: false
**Git installed**: true
**Elan**: Reasonably up-to-date (version: 4.2.1)
**Lean**: Reasonably up-to-date (version: 4.21.0)
**Project**: Valid Lean project (path: c:\Users\User\mathematics_in_lean)
**Active Lean version**: leanprover/lean4:v4.21.0 (set by `file://%3F/c%3A/Users/User/mathematics_in_lean/lean-toolchain`)
**Installed Lean versions**: leanprover/lean4:v4.21.0, leanprover/lean4:v4.29.1, leanprover/lean4:v4.30.0-rc2

3. Troubleshooting: Show Troubleshooting Output shows

c:\Users\User\mathematics_in_lean> curl --version
c:\Users\User\mathematics_in_lean> git --version
=> Operation failed. Exit code: -4058.
git version 2.54.0.windows.1

> curl --version
> git --version
=> Operation failed. Exit code: -4058.
git version 2.54.0.windows.1

> winget --version
v1.28.240

[mhuisi]

Ah, so Curl is not installed. Curl usually ships by default on Windows 11.

I'm not sure why it is missing on your system (if you have an idea, please let me know - I'm eager to improve our installation procedure!), but here are some suggestions for how to install it: https://stackoverflow.com/a/16216825

After you installed curl, reboot your system and check whether curl --version from a command line works. Then everything should work as expected.

[zao05]

Thanks a lot. Curl was already installed, I just had to add it to PATH.

[mhuisi]

Thanks a lot. Curl was already installed, I just had to add it to PATH.

#780 also ensures that you now get a proper error message in this type of setup instead of things just failing silently. Sorry for that.

Do you understand why it wasn't on the PATH to begin with? If this is a common pattern on specific kinds of Windows machines, I'd like to understand it so that we can improve the installation for these kinds of machines.

[zao05]

I'm not sure. Sorry