Using the extension with remote-ssh

[nano-o]

Hello, it seems that the extension does not work when accessing a remote folder using SSH (with the SSH extension from Microsoft). VSCode says the extension is defined to run in the remote host and that it is not installed in the remote host; but it is installed on the remote host. Am I missing something, or is this just not supposed to work?

[lemmy]

I've never tried this and don't know how this is supposed to work, but the extension simply spawns a TLC process https://github.com/tlaplus/vscode-tlaplus/blob/4a0d7233df210ebada17ba2252da7a6b14560c3d/src/tla2tools.ts#L132C24-L146

[achamayou]

@nano-o for what it's worth, I have used the TLA+ extension with SSH remote many times with success:. Just now:

If you need to change some of the settings, you have to be a bit careful to do it under the Remote tab, but that's true for all extensions when using remote, it otherwise behaves as one would hope.