VScode extension not showing infoview

Stream: lean4

[Eric Wieser]

When working with the "remote - SSH" extension, I seem to be getting into a weird state with the (preview release of the) vscode extension, where the .lean file shows all the various LSP annotations, but the \forall button for the lean extension does not expose a "restart server" or "open infoview" butotn

[Marc Huisinga]

I assume "Restart File" and "Project Actions" are not visible, either?

[Eric Wieser]

Yes, I have only
image.png

[Eric Wieser]

And the Ctrl+Shift+P menu is also absent those commands

[Marc Huisinga]

Does the InfoView show up at all when first launching the editor?

[Eric Wieser]

This error is in the logs:

Activating extension leanprover.lean4 failed due to an error:
2024-04-26 11:03:07.588 [error] Error: Got URI with unsupported scheme 'output': 'output:extension-output-ms-vscode-remote.remote-ssh-%231-Remote%20-%20SSH'
    at a (~/.vscode-server/extensions/leanprover.lean4-0.0.142/dist/extension.js:2:397407)
    at ~/.vscode-server/extensions/leanprover.lean4-0.0.142/dist/extension.js:2:391223
    at Array.forEach (<anonymous>)
    at new t.LeanConfigWatchService (~/.vscode-server/extensions/leanprover.lean4-0.0.142/dist/extension.js:2:391179)
    at ~/.vscode-server/extensions/leanprover.lean4-0.0.142/dist/extension.js:2:318743
    at Generator.next (<anonymous>)
    at ~/.vscode-server/extensions/leanprover.lean4-0.0.142/dist/extension.js:2:318019
    at new Promise (<anonymous>)
    at i (~/.vscode-server/extensions/leanprover.lean4-0.0.142/dist/extension.js:2:317764)
    at _ (~/.vscode-server/extensions/leanprover.lean4-0.0.142/dist/extension.js:2:318620)
    at ~/.vscode-server/extensions/leanprover.lean4-0.0.142/dist/extension.js:2:321802
    at Generator.next (<anonymous>)
    at s (~/.vscode-server/extensions/leanprover.lean4-0.0.142/dist/extension.js:2:317821)
    at process.processTicksAndRejections (node:internal/process/task_queues:95:5)

[Marc Huisinga]

Ah, that's extremely helpful!

[Eric Wieser]

(I'd seen that error a bunch before, but hadn't managed to find it alongside Activating extension leanprover.lean4 failed until now)

[Marc Huisinga]

Ok, I think I know what's going wrong here. Thanks for the report, I'll look into it.

[Marc Huisinga]

I've added a fix for this to a new pre-release (0.0.143). Please let me know if you still encounter the issue since I didn't have time to test the fix in detail.

[Eric Wieser]

It seems to work for me now