Zulip Chat Archive

Stream: lean4

Topic: VS Code extension on WSL double spawns lean server

Yongyi Chen (Dec 09 2023 at 20:23):

The VS code lean4 extension on WSL on Windows 11 double spawns the lean server in the following case:

  1. Have a lean project open, then close all the files so that the editor has no files open.
  2. Close VS Code.
  3. Open VS Code, then select a lean file and open it.
    image.png

Yongyi Chen (Dec 09 2023 at 20:24):

A related issue while we're at it: Lean with Mathlib on WSL uses 6 GB of RAM, when it only uses 1 GB on Windows and less than 1 GB on dual-booted Linux.

Yongyi Chen (Dec 09 2023 at 20:25):

I guess this kind of thing belongs on https://github.com/leanprover/vscode-lean4/issues

Eric Wieser (Dec 10 2023 at 01:24):

I've seen this behavior occasionally on gitpod too, though I didn't investigate if there were truly two servers or just a double notification

Yongyi Chen (Dec 10 2023 at 01:29):

I have checked, it's 2 servers. One way you can tell is by noticing that there are 2 of each message in the problems panel.

Marc Huisinga (Dec 11 2023 at 11:28):

Yes, please create an issue in the vscode-lean4 repo for this.

Last updated: Dec 20 2023 at 11:08 UTC