Multiplayer Lean

Stream: general

[Kevin Buzzard]

I remember one particularly crazy day at Xena in 2019 or so, when about 6 people were simultaneously editing a file formalizing the basics of dihedral groups D_n, with different people developing API at the same time. Everyone had working infoviews, we were all sitting around the same table, and when someone refactored the definition of D_n everyone started yelling at the same time. This was all being done using William Stein's CoCalc, which had support for Lean 3 and mathlib and was the first one-click solution for Lean, but which could not keep up with the frantic pace of development so was not practical for mathlib development.

Later on VS Code started to offer a multiplayer option, but it was never anywhere near as good because everyone could see the same infoview and in particular it would report on the state at someone else's cursor. However Stein's experiment is a proof that true multiplayer Lean can certainly be achieved and indeed it was achieved 5 years ago.

The other day I was surprised and pleased to run into an old friend, who was one of the other players in the dihedral group mission, and one of the first questions they asked me was whether multiplayer Lean was a thing yet. Given the general amazingness of this community, I was quite surprised to have to tell him that the answer was still "no, at least not that I am aware of". In other parts of the computery-maths ecosystem (e.g. overleaf) this is is commonplace. Is the problem that people don't generally want this or that there are technical difficulties which nobody realises that Stein must have solved 5 years ago?

[Andrew Yang]

Is gitpod not good enough for this purpose?

[Kevin Buzzard]

Oh lol I see that my memory can be refreshed by scrolling up this thread :-)

[Kevin Buzzard]

I don't know if Yael's thumbs up means "yes use gitpod" or "yes it's not good enough". Does it solve the "everyone can see the same infoview" problem?

[Kevin Buzzard]

I also thought that gitpod had ceased to exist in April?

[Shreyas Srinivas]

Andrew Yang said:

Is gitpod not good enough for this purpose?

No it’s not. I tried it last week and it only works if the people collaborating explicitly pass a token amongst themselves.

[Shreyas Srinivas]

Otherwise you get a message about conflicting edits and if you choose to overwrite your version instead of accepting incoming changes, gitpod stops sharing your edits with the others.

[Shreyas Srinivas]

And @Kevin Buzzard : they extended the gitpod classic plan till October. Gitpod will still exist but you will have to run it locally, or ask your university to set up a server for its members and students.

[Alex Kontorovich]

We recently had the same conversation at ICERM. Such a thing would be very cool!

[Alex Kontorovich]

Possibly related: when the DeepMind people were here (at IAS), they showed how they run AlphaProof on a sorry, and it doesn't stop you from continuing to edit elsewhere. Then if it finds a proof, it just replaces the sorry automatically, you don't even notice it. It would be quite cool if, e.g., exact? worked that way!... Imagine you have a bunch of have statements and want to keep working elsewhere but want to let exact? run in the background, and if it's able to close the have, put the code there but not interrupt your flow... ???

[Eric Wieser]

We're still exploring what the right interface is there, but certainly "try this" is not a great option for actions that run for more than a few seconds

[Eric Wieser]

Maybe incremental compilation is getting so good that this will soon no longer be the case though!

[Chase Norman]

I wanted to have Canonical do this. Let me know when the interface is decided on!

[Marc Huisinga]

As for "Lean multiplayer" in VS Code, I investigated support for LiveShare here.
The crux of the issue is that Microsoft appears to have mostly de-prioritized LiveShare (at least for now), and that proper support for LiveShare in the VS Code extension requires our extension to be whitelisted by Microsoft. Since the issue tracker of LiveShare has been abandoned for years, it's pretty unlikely that we would be whitelisted even if we invested the effort necessary to make the VS Code extension compatible with LiveShare.