Zulip Chat Archive

Stream: general

Topic: VSCode Live Share

Kenny Lau (May 29 2019 at 15:44):

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

Kenny Lau (May 29 2019 at 16:04):

now we can have remote Lean hackathons!

Scott Morrison (May 29 2019 at 16:59):

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

Scott Morrison (May 29 2019 at 17:00):

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 (May 29 2019 at 17:01):

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

Kevin Buzzard (May 29 2019 at 17:52):

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

Kenny Lau (Jun 07 2019 at 22:00):

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.

Last updated: Dec 20 2023 at 11:08 UTC