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)