vscode with remote repositories failing to find toolchain

Stream: mathlib4

[Thomas Murrills]

If I try to look at my branch of mathlib4 as a remote repository in VS code, I can't seem to start the lean server. I get told I have "no default "lean-toolchain" in this folder or any parent folder", and if I try to select the toolchain via command palette > Lean 4: Select Toolchain, I see "Error: elan toolchain list returned no output". If I further try to specify the path exactly by using the root directory of the nightly in .elan/toolchains/, I get the same errors as before.

Does anyone else have this issue or know how to fix it?

[Scott Morrison]

Works fine for me. Can you run elan in an ssh shell on the remote host?

[Thomas Murrills]

hmm, I'm not on a remote host—I'm using github remote repositories in VS code (it might be an extension? not sure if it's integrated into VS code or not)

[Scott Morrison]

Oh, sorry, I misunderstood. I haven't used that.

[Alex J. Best]

I think most vscode extensions that do nontrivial things have to be explicitly rewritten to support remote repositories.
Just looking at https://code.visualstudio.com/api/extension-guides/virtual-workspaces#review-that-the-extension-code-is-ready-for-virtual-resources and the current extension it seems this would be nontrivial, if possible at all!