Zulip Chat Archive

Stream: general

Topic: LiveShare


view this post on Zulip Kevin Buzzard (May 31 2019 at 11:05):

Has anyone got LiveShare working with Lean and mathlib? I just tried it with @Anca Ciobanu ; firstly she shared a session but had a .gitignore file containing things like _target, and when the session was shared her code compiled for her but not for me -- all the imports failed. We renamed her .gitignore and tried again, and this time I see her _target and also her leanpkg.path, all of which looks perfect (coincidentally, she is on a different OS so it couild have been random) but still my VS Code cannot pick up the imports. What are we doing wrong?

view this post on Zulip Kevin Buzzard (May 31 2019 at 11:05):

The sharing is working, it's just that her code compiles for her and not for me.

view this post on Zulip Scott Morrison (May 31 2019 at 14:46):

@Kevin Buzzard, LiveShare doesn't work.

view this post on Zulip Scott Morrison (May 31 2019 at 14:46):

I mean, you can both edit the same file, but the client will not see any meaningful feedback from the server

view this post on Zulip Scott Morrison (May 31 2019 at 14:47):

The problem is just that in VS Code, it shows you those files that exist on the hosts machine

view this post on Zulip Scott Morrison (May 31 2019 at 14:47):

but they do not actually exist on your computer anywhere in the filesystem

view this post on Zulip Scott Morrison (May 31 2019 at 14:47):

so the external Lean command has nothing to work on


Last updated: May 14 2021 at 04:22 UTC