Feature: Add collaborative text editing using Yjs, y-webrtc and y-monaco

[nileshtrivedi]

Since yjs provides an integration for Monaco editor, I was able to add this ability relatively easily.

Document opens with this button in the Nav:

Clicking on this prompts the user to pick a roomname and a displayname:

I wrote a simple signaling server to help peers find each other. But this is only used for peer discovery. Once peers are found, the document updates are sent over WebRTC (i.e. peer to peer).

The document then updates in real-time and remote cursors are shown in orange colors:

I wanted to show nametags on the cursors as well, but this seems a bit tricky and might need to be implemented in y-monaco first.

[joneugster]

This is a nice feature!

Unfortunately, it might be a while until I get around to review this carefully as we currently have some serious issues to fix.

[jcreedcmu]

Not to create undue pressure to review if you have other priorities, but I wanted to comment that I also had a small FRO-internal experiment I had scraped together along similar lines, and some brief testing showed it was pretty fun and useful to discuss lean4web-scale single page lean developments with it. It also used y-monaco, albeit instead of webrtc datachannel and a signalling server, it had just a straightforward monolithic copy of y-websocket-server running on the same host as the lean4web server. WebRTC is very cool but I've struggled to get it to work reliably in the past for all behind-NAT users unless there is a stable TURN server.

One downside of using y-monaco directly (assuming I'm not making a mistake in understanding you're making similar choices in having separate lean servers for each client) is that some ide features appear to (sensibly!) assume the document won't be changed except at the cursor, so for example autocomplete can be confused if a user other than the one that initiated autocomplete changes line/col positions of the text that's being autocompleted.

On the other hand, I think this might not be as bad a problem in practice as it is in theory. A big use-case for this kind of collaboration seemed to be where two people are on a video call and either one can make an edit at any time, but actually what happens may be that they naturally take turns editing as the conversation proceeds.

Anyway, would be happy dig up and share code and/or discuss further if it would be of any help!

[nileshtrivedi]

@jcreedcmu Thanks for that insightful comment.

Slightly off-topic: Another feature that I am currently exploring in the belief that it might make real-time collaboration more fun, is adding a live-updating dependency graph, in the style of LeanBlueprint.

A recent work, LeanArchitect, adds annotations in Lean source code on definitions and theorems, to derive this but it still relies on very heavy LaTeX tooling. I am trying to show the dependency graph below the Lean infoview, extracted these annotations but via JSON and therefore, do it in real-time with each character change. It seems possible to achieve this with Lean's User Widgets which can add interactive components to the InfoView. ProofWidgets, in particular, already has support for Penrose.

Update: I got it working!

[joneugster]

Hey Jason, cool to hear the FRO had played around with this idea, too. I do agree that it's definitely something cool to add! I have a few things which would need to be worked out

1. The webrtc server should probably be part of the lean4web installation, so that we don't call an external wide-robin-20.snowmountain.deno.net.
2. if that is true about not being able to edit simultaneously, we'd need some good handling of that. (e.g. disable the editor on shared instances)
3. I have some concerns about data security, so we'd need to think about what needs to be added to make this GDPR-conform. Maybe it's as simple as requesting the permission to share personal data and to implement something against brute-forcing room names (room name complexity, rate limits, manual approval to join, ...).

(Btw, concretely, with "serious problems" above I meant this lean4game issue for Windows users. I still haven't fully pin-pointed where that's coming from, but I'm meanwhile 95% certain that it does not affect lean4web)

Regarding the dependency graph widget, please consider contributing useful machinery in this regard to https://github.com/leanprover-community/import-graph ! Ideally lean4web can then simply allow this to be integrated through the sample projects (I'm thinking e.g. Projects/MathlibDemo/MathlibDemo.lean contains the setup to display the widget and lean4web would essentially read the preample from that file)

[nileshtrivedi]

I have now added the yjs signaling feature within this repo, so now there is no need for external signaling server. I also added validation for roomname and displayname, and pulled latest changes from main.

[joneugster]

Sorry for the slow reply here!

Overall I have to repeat, this is really cool and I'd like to integrate this certainly!

All comments are more about cleaning up the code and making it more closely aligned with existing code.

[joneugster]

What would be a good design to incorporate the other person's display name somehow?

[nileshtrivedi]

NameTags on the cursor could look like this:

But before that, I should implement distinct color cursors for distinct clients.

[joneugster]

IMO it's also fine to display the names without distict colors. The two feauters seem to be indepenent from antother

[joneugster]

@nileshtrivedi I've took the liberty to work on this a little and push the result to your branch :)

[joneugster]

So, I think what's left is:

• ideally display peoples names
• optionally use different colours
• update docs

I want to give you a chance to look at the changes in case you'd like to change/refine anything again! Afterwards I think we can start to think about merging this feature

[nileshtrivedi]

Thanks @joneugster

I want to spend some time testing that document updates do not confuse any existing features like autocomplete.