Server sharing in live share

Stream: general

[Jason Rute]

I’m not quite sure what server sharing is, but I believe Gabriel said that one can’t make two concurrent calls to the info command in the lean server. If one does so the first call is cancelled or something when you make a second. Is this an issue with this feature?

[Gabriel Ebner]

This is fixed since 3.16, I believe?

[Reid Barton]

Oh dang I gotta upgrade then.

[Reid Barton]

This is really annoying in emacs because it means autocompletion doesn't work when the goal window is open (for example).

[Yury G. Kudryashov]

BTW, is there any Emacs package for collaborative editing?

[Adam Topaz]

You can always run a single emacs server remotely and connect with a client

[Scott Morrison]

@Bryan Gin-ge Chen, when you wrote

"excludeFiles":[
        "!*.olean",
        "*!leanpkg.path"
    ],

above, is the * in "*!leanpkg.path" a typo?

[Scott Morrison]

When I connect a guest session I get the error message

You are running Lean in a directory without a leanpkg.toml file, this is NOT supported. Please open the directoy containing the leanpkg.toml file instead.

even though I can see the leanpkg.toml file.

[Scott Morrison]

Presumably this is going to be essential to fix.

[Scott Morrison]

The very top issue at https://docs.microsoft.com/en-us/visualstudio/liveshare/reference/extensions#known-issues seems to be about this. We are using the fs API to look for configuration files.

[Gabriel Ebner]

Reading the live share documentation, they say that there are two kinds of extensions: project-specific extension (which are run on the host), and user-specific extension (which are also run on the guest). Project-specific extensions can be "shared", so that they are only run on the host. The lean extension would need to be a project-specific extension that is shared. But I have no idea how to configure that.

[Johan Commelin]

Should we ask someone from VScode on how to fix this / what we need to do to make this work?

[Johan Commelin]

We want Lean to show up in this list: https://docs.microsoft.com/en-us/visualstudio/liveshare/reference/platform-support

[Johan Commelin]

[ And since Lean is an MS product... ]

[Mario Carneiro]

I also don't see F* in the list, which is also an MS product and a lot more programmy than lean

[Mario Carneiro]

or Agda, Idris, Coq, etc

[Mario Carneiro]

the whole field is probably a rounding error to them

[Johan Commelin]

I can't even get the "Sign in" from Live Share to work...

[Johan Commelin]

I'm trying to Sign in with Github, and it's simply not working

[Scott Morrison]

works for me

[Scott Morrison]

Unless we can work out this "project-specific extension" thing that only runs on the host, I think we're doomed.

[Scott Morrison]

You can only access files on the host through the workspace.findFiles and workspace.openTextDocument API, it seems, and of course there is no way that our server can arrange to load *.olean files via that API.

[Johan Commelin]

I agree. But maybe they want to help

[Scott Morrison]

(unless we rewrite the server in javascript?!)

[Scott Morrison]

@Gabriel Ebner where did you find this documentation about the two kinds of extensions?

[Gabriel Ebner]

https://docs.microsoft.com/en-us/visualstudio/liveshare/reference/extensions

[Johan Commelin]

Whenever I try to login via Github (I don't have any microsoft accounts) I get redirected to a page that shows me:
image.png

[Scott Morrison]

I see.

[Scott Morrison]

I wonder if we could hack something whereby the guest's Lean server reads oleans from a local copy of mathlib (i.e. not provided via live share)

[Scott Morrison]

but still gets sent the text of shared documents

[Scott Morrison]

so before collaborating with someone you'd both have to checkout the same branch or whatever

[Scott Morrison]

It seems from Bryan's experiment (that I have confirmed) that it works reasonably well out of the box --- as long as you don't need any imports!

[Bhavik Mehta]

Johan Commelin said:

I can't even get the "Sign in" from Live Share to work...

I had this too - I think I just removed and put the extension back and maybe restarted my browser and vscode and it worked eventually

[Johan Commelin]

Wow... that sounds like a microsoft solution

[Johan Commelin]

Do I also need to reboot :grinning_face_with_smiling_eyes: :rofl:

[Bhavik Mehta]

Yeah, also turn your computer's wifi off and on again, and also your router

[Bryan Gin-ge Chen]

Scott Morrison said:

Bryan Gin-ge Chen, when you wrote

"excludeFiles":[
        "!*.olean",
        "*!leanpkg.path"
    ],

above, is the * in "*!leanpkg.path" a typo?

I can't test right this moment, but yes, that does look like a typo. I'm now no longer sure whether fooling around with that will be necessary.

[Johan Commelin]

@Bhavik Mehta I've tried 13 permutations of your instructions... but it's still br0xen

[Bryan Gin-ge Chen]

I had some very vague thoughts on how to proceed. First, I'd like to check this further, but from my brief tests, it seemed like all the behavior on the guest's side in the editor window (that is, decorations, hovers, code actions etc.) seem to work fine, presumably because these commands are sent to the host's computer, processed there and then transmitted back somehow. (This may be using some "project-specific extension" functionality.)

Assuming that's true, then the question becomes how to handle the info view. Again, here I'd like to understand better what's going on in the current state of the extension, but I believe the infoview on the guest's computer is working with a "copy" of the edited file in the Lean server launched on their side. This Lean server seems to not be picking up any leanpkg.path, so it's probably defaulting to the global one.

If that's the case, then my thought was that we could pop up a prompt for guests to specify a path to a Lean project on their computer to give to their Lean server. We could use leanproject to allow guests just to specify a github link too.

Lots of ifs and open questions here, but those were my thoughts. If anyone wants to do testing along these lines, that'd be greatly appreciated. I was just going to put lots of console.log in the extension source and then build a .vsix and try to run both guest and host on my laptop.

[Bryan Gin-ge Chen]

Johan Commelin said:

Whenever I try to login via Github (I don't have any microsoft accounts) I get redirected to a page that shows me:
image.png

Might you be using some browser extension that deletes unwanted cookies? I had to whitelist some new microsoft sites to keep my cookies from getting removed before I could log in properly.

[Johan Commelin]

Aaah, that might be the issue.

[Johan Commelin]

I'll try it tonight

[Scott Morrison]

Oh... I was pretty sure that no Lean specific information was passing back on forth between the computers.

[Scott Morrison]

Isn't what you see compatible with all the decorations, hovers, etc, just being run locally, based on just the current file?

[Scott Morrison]

I guess a good experiment would be to create a session, then kill the server on the host side.

[Scott Morrison]

I predict that in the guest session nothing will change.

[Bryan Gin-ge Chen]

Scott Morrison said:

Isn't what you see compatible with all the decorations, hovers, etc, just being run locally, based on just the current file?

I read that the hovers are run on the host somewhere (probably in a live share github issue?) and now I can't find it. I think the Known Issues doc hint at this though:

Guests receive the language service results from both their local extensions, and the host, and therefore, if both participants have the same language service extension installed, guests will see duplicate entries for certain things (e.g. auto-completion, code actions)