Working with lean/git installed in WSLv1 or WSLv2 instance

[vadimkantorov]

Could you please advise if vscode-lean4 can work with a WSLv1 (or WSLv2) instance

E.g. I have a VS Code running in Windows, code stored in NTFS home dir C:\Users\vadim (/mnt/c/Users/vadim), but would like to have git/lean/lean language server running in my WSLv1 instance?

It appears that this is supported when I connect to Remote Host in bottom-left

but it would be nice to have this explicitly explained in README - especially in README popping up when accidentally installing the vscode-lean4 extension when not connected to Remote Host

[mhuisi]

If I am understanding correctly, then the request of this issue is that the Lean VS Code extension should explain somewhere how to use the VS Code Remote Development extensions?

especially in README popping up when accidentally installing the vscode-lean4 extension when not connected to Remote Host

I'm not sure if I am understanding this correctly, but I don't think that this should be a popup. Using Lean on native Windows without WSL works just fine.

[vadimkantorov]

the request of this issue is that the Lean VS Code extension should explain somewhere how to use the VS Code Remote Development extensions

Or at least just mention that there are several ways of operation:

• native Windows
• local WSL via Remote Host Extension
• and maybe also Remote Host which runs the prover on a remote big linux server? (as laptops sometimes get quickly overheated when running lean locally)

[Tomodovodoo]

Could you please advise if vscode-lean4 can work with a WSLv1 (or WSLv2) instance

E.g. I have a VS Code running in Windows, code stored in NTFS home dir C:\Users\vadim (/mnt/c/Users/vadim), but would like to have git/lean/lean language server running in my WSLv1 instance?

It appears that this is supported when I connect to Remote Host in bottom-left

but it would be nice to have this explicitly explained in README - especially in README popping up when accidentally installing the vscode-lean4 extension when not connected to Remote Host

Thanks so much for this, I am also running lean inside WSL, and my lean server also kept repeating an error, this works perfectly for me.