Zulip Chat Archive

Stream: general

Topic: Sever sharing in live share

Kenny Lau (Jun 25 2020 at 20:17):

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 (Jun 25 2020 at 20:18):

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

Bhavik Mehta (Jun 25 2020 at 20:18):

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

Patrick Massot (Jun 25 2020 at 20:18):

There is no obstruction, but it needs work.

Patrick Massot (Jun 25 2020 at 20:19):

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

Johan Commelin (Jun 26 2020 at 03:22):

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 (Jun 26 2020 at 04:42):

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

Johan Commelin (Jun 26 2020 at 05:19):

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

Kenny Lau (Jun 26 2020 at 05:44):


Kevin Buzzard (Jun 26 2020 at 05:52):

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 (Jun 26 2020 at 06:23):

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",
    "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:

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 (Jun 26 2020 at 06:25):

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


Johan Commelin (Jun 26 2020 at 06:26):

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

Johan Commelin (Jun 26 2020 at 06:26):

Because it seems that I should start preparing...

Kevin Buzzard (Jun 26 2020 at 07:01):

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

Bryan Gin-ge Chen (Jun 26 2020 at 07:24):

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 (Jun 26 2020 at 09:11):

Oh! Sorry, I must have made a slip.

Last updated: Aug 03 2023 at 10:10 UTC