LiveShare

Stream: general

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Scott Morrison]

@Kevin Buzzard, LiveShare doesn't work.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

so the external Lean command has nothing to work on