Sever sharing in live share

Stream: general

[Kenny Lau]

Is it possible to tweak the Lean extension in VS Code to enable server sharing (so as to view the goals)? @Bhavik Mehta told me that for server sharing to work, the server needs to be TCP port or URL and Lean is not either of those.

[Bhavik Mehta]

As far as I know, Lean isn't either of those

[Bhavik Mehta]

Plus if this works then it might make collaboration easier for LFCM

[Patrick Massot]

There is no obstruction, but it needs work.

[Patrick Massot]

Basically you need to be very nice to Bryan or Gabriel.

[Johan Commelin]

Oh, I'll by anyone 3 good Belgian beers (or something with the same value, if you don't like beers or Belgians...) if they can make this work smoothly before LFTCM!

[Scott Morrison]

You're talking about working with https://visualstudio.microsoft.com/services/live-share/?

[Johan Commelin]

Yep, at least that's whay I was thinking of

[Kenny Lau]

Yes.

[Kevin Buzzard]

Yes. Currently it's extremely inconvenient. I will be working with summer students this summer and would donate three more. Currently what you can do is that one person uses Lean and the others can also type but they can't see the errors or goal state because if they run a local server then the imports fail

[Bryan Gin-ge Chen]

Wow, I'm playing around with it now (with my laptop on macOS and my desktop on Windows) and it works much better than I thought it would. Some observations:

• There's a useless "leanpkg.toml" message when the extension on the guest's side opens.
• The cursor of the guest doesn't track the host's automatically, but as a guest, if I put my cursor inside a tactic the goal window (sometimes) works and I can see the goal locally, as long as the file doesn't rely on any imports.
• Underlines and hovers seem to work only if the host has the same file in view.
• To get files with imports working properly, I think at a minimum the host will need to set up a .vsls.json file. I tried using the following, which at least gets _target/deps/mathlib to show up on the guest side:

{
    "$schema": "http://json.schemastore.org/vsls",
    "gitignore":"none",
    "excludeFiles":[
        "!*.olean",
        "*!leanpkg.path"
    ],
    "hideFiles": [
    ]
}

• I wonder if we need to take a look at the code that hides the oleans from view. Maybe if we show them, we can get live share to transfer them to the guests' computers?
• The goal window seems to work very inconsistently. As a guest, the goal view is often just stuck in a blank state, but if I start editing the file then that causes stuff to appear. (Unfortunately, it still complains about not being able to find the imports in the path).
• Here's a weird state I got in:
  Screenshot-2020-06-26-02.19.59.png
  

I typed in library_search on the guest's side and got two suggestions. Neither of them work, but I get different errors. Also note the problems panel showing two different open versions of blah.lean, which I don't understand.

I think I need to read up more on how live share actually works in order to work more on this, but the only info I could find about getting extensions to work with live share was this list of random issues and suggestions, which doesn't give enough of an explanation for me.

[Bryan Gin-ge Chen]

I think there's hope to get things working, but most likely only after the current info view refactor (with widgets) settles down.

leanprover/vscode-lean#191

[Johan Commelin]

@Bryan Gin-ge Chen Is there a particular brand of Belgian beer that you are fond of?

[Johan Commelin]

Because it seems that I should start preparing...

[Kevin Buzzard]

@Bryan Gin-ge Chen data.real.basic does not import library_search, I don't think!

[Bryan Gin-ge Chen]

Are you sure? This seems to work in a recent mathlib:

import data.real.basic

example : ℕ := by library_search

It also seems to work in the web editor.

[Kevin Buzzard]

Oh! Sorry, I must have made a slip.