Zulip Chat Archive

Stream: general

Topic: VSCode Live Share


view this post on Zulip 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

view this post on Zulip Kenny Lau (May 29 2019 at 16:04):

now we can have remote Lean hackathons!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Kevin Buzzard (May 29 2019 at 17:52):

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

view this post on Zulip 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: May 14 2021 at 21:11 UTC