The 'Lean 4' extension is not available in Visual Studio Code for the Web.

[Louw123]

Description

The lean 4 extension is not supported in vscode.dev. When going to in

Context

So, I am working on a project that uses for lean4 game. I cant work offline, and gitpod takes too long to load. So I must use github codespaces/vscode for web. Unfortunately, the latest version listed '0.0201', does not support vscode.

Steps to Reproduce

1. go to github codespaces/vscode for web
2. go the extensions.
3. search "lean4"

Expected behavior: It is available for the web, without issue.

Actual behavior: "The 'Lean 4' extension is not available in Visual Studio Code for the Web."

Versions

lean extension version: 0.0201

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[mhuisi]

GitHub codespaces is not the same as vscode.dev. The Lean 4 extension works fine in the former, but it will not run in the latter.

When using GitHub codespaces, extensions and language servers (like the Lean one) run on the GitHub servers in a regular Linux environment. In vscode.dev, extensions run directly in the browser, which is an entirely different environment that the Lean language server can't run it (e.g. it relies on being able to spawn processes and being able to mmap memory into the process).