VSCode Live Share

Stream: general

[Kenny Lau]

I think I was just made aware of the extension Live Share in VSCode which allows collaboration

[Kenny Lau]

now we can have remote Lean hackathons!

[Scott Morrison]

Unfortunately it doesn't actually work. The remote person just gets random squiggles, because Lean is not actually running on their end.

[Scott Morrison]

Perhaps it is possible to modify the VS Code extension so that the output from the Lean server on the host's computer is actually propagated back to the client's.

[Scott Morrison]

(Similar with the LaTeX plugin. The client can't compile or even view the latest PDF from the host's end.)

[Kevin Buzzard]

@Scott Morrison I thought you and I got it working at some point?

[Kenny Lau]

It works better if you disable your own checking (i.e. on the bottom navigational bar (coloured blue by default) click (checking visible files) and select nothing), since the host's Lean is still fully functional and you can see the error transmitted from the host; however sometimes the errors go out of sync and it seems that the only way to resolve this issue is to quit and rejoin the session.