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

client/package.json

@@ -26,7 +26,10 @@
     "react-split": "^2.0.14",
     "react": "^19.2.0",
     "tailwindcss": "^4.1.18",
-    "vscode-ws-jsonrpc": "^3.5.0"
+    "vscode-ws-jsonrpc": "^3.5.0",
+    "y-monaco": "^0.1.6",
+    "y-webrtc": "^10.3.0",
+    "yjs": "^13.6.30"
   },
   "devDependencies": {
     "@codingame/esbuild-import-meta-url-plugin": "^1.0.3",

client/src/App.tsx

@@ -1,4 +1,5 @@
 import './css/App.css'
+import './css/Collab.css'
 import './css/Editor.css'
 
 import { faCode } from '@fortawesome/free-solid-svg-icons'
@@ -8,14 +9,26 @@ import { useAtom } from 'jotai/react'
 import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco'
 import * as monaco from 'monaco-editor'
 import * as path from 'path'
-import { useCallback, useEffect, useRef, useState } from 'react'
+import { useCallback, useEffect, useMemo, useRef, useState } from 'react'
 import Split from 'react-split'
+import { MonacoBinding } from 'y-monaco'
+import { WebrtcProvider } from 'y-webrtc'
+import * as Y from 'yjs'
 
 import LeanLogo from './assets/logo.svg'
 import { codeAtom } from './editor/code-atoms'
+import { NavButton } from './navigation/NavButton'
 import { Menu } from './navigation/Navigation'
+import RotatingGlobe from './navigation/RotatingGlobe'
+import LeaveCollaborationPopup from './Popups/LeaveCollaboration'
 import { mobileAtom, settingsAtom } from './settings/settings-atoms'
 import { lightThemes } from './settings/settings-types'
+import {
+  collabDisplayNameAtom,
+  collabPasswordAtom,
+  collabRoomAtom,
+  isCollaboratingAtom,
+} from './store/collaboration-atoms'
 import { importedCodeAtom } from './store/import-atoms'
 import { currentProjectAtom } from './store/project-atoms'
 import { screenWidthAtom } from './store/window-atoms'
@@ -37,8 +50,18 @@ function App() {
   const [, setScreenWidth] = useAtom(screenWidthAtom)
   const [project] = useAtom(currentProjectAtom)
   const [code, setCode] = useAtom(codeAtom)
+  const ydoc = useMemo(() => new Y.Doc(), [])
+  const [provider, setProvider] = useState<WebrtcProvider | null>(null)
+  const [binding, setBinding] = useState<MonacoBinding | null>(null)
+  const [collabRoom] = useAtom(collabRoomAtom)
+  const [collabDisplayName] = useAtom(collabDisplayNameAtom)
+  const [collabPassword] = useAtom(collabPasswordAtom)
+  const [usersInCollab, setUsersInCollab] = useState(0)
+  const [isCollaborating] = useAtom(isCollaboratingAtom)
   const [importedCode] = useAtom(importedCodeAtom)
 
+  const [leaveCollabOpen, setLeaveCollabOpen] = useState(false)
+
   const model = editor?.getModel()
 
   // Lean4monaco options
@@ -66,6 +89,59 @@ function App() {
     return () => window.removeEventListener('resize', handleResize)
   }, [setScreenWidth])
 
+  // clean up ydoc on unmount
+  useEffect(() => {
+    return () => ydoc.destroy()
+  }, [ydoc])
+
+  // this effect manages the lifetime of the Yjs document and the provider
+  useEffect(() => {
+    // const provider = new WebsocketProvider('wss://demos.yjs.dev/ws', roomname, ydoc)
+    // See https://github.com/yjs/y-webrtc for options
+    if (!isCollaborating || !collabRoom) {
+      setProvider(null)
+      return
+    }
+
+    const signalingUrl =
+      (window.location.protocol === 'https:' ? 'wss://' : 'ws://') +
+      window.location.host +
+      '/yjs-signaling'
+    console.log('[Lean4web] collab signaling url:', signalingUrl)
+
+    const provider = new WebrtcProvider(collabRoom, ydoc, {
+      maxConns: 50,
+      password: collabPassword,
+      signaling: [signalingUrl],
+      filterBcConns: true,
+    })
+    if (collabDisplayName) {
+      provider.awareness.setLocalStateField('user', { name: collabDisplayName })
+    }
+    setProvider(provider)
+    return () => {
+      provider?.destroy()
+    }
+  }, [ydoc, isCollaborating, collabRoom, collabDisplayName, collabPassword])
+
+  // this effect manages the lifetime of the editor binding
+  useEffect(() => {
+    if (provider == null || editor == null) {
+      return
+    }
+    console.log('reached', provider)
+    const binding = new MonacoBinding(
+      ydoc.getText(),
+      editor.getModel()!,
+      new Set([editor]),
+      provider?.awareness,
+    )
+    setBinding(binding)
+    return () => {
+      binding.destroy()
+    }
+  }, [ydoc, provider, editor])
+
   // Update LeanMonaco options when preferences are loaded or change
   useEffect(() => {
     if (!project) return
@@ -259,10 +335,33 @@ function App() {
     }
   }, [handleKeyDown, handleKeyUp])
 
+  // keep the number of people in the room updated
+  useEffect(() => {
+    if (!provider) return
+    const update = () => {
+      setUsersInCollab(provider.awareness.getStates().size)
+    }
+    provider.awareness.on('change', update)
+    update()
+    return () => {
+      provider.awareness.off('change', update)
+    }
+  }, [provider])
+
   return (
     <div className="app monaco-editor">
       <nav>
         <LeanLogo />
+        {isCollaborating && (
+          <NavButton
+            iconElement={<RotatingGlobe />}
+            text={`${collabDisplayName} ∈ ${collabRoom} (${usersInCollab})`}
+            className="leave-collab-button"
+            onClick={() => {
+              setLeaveCollabOpen(true)
+            }}
+          />
+        )}
         <Menu
           setContent={setContent}
           restart={leanMonaco?.restart}
@@ -322,6 +421,12 @@ function App() {
           </p>
         </div>
       </Split>
+      <LeaveCollaborationPopup
+        open={leaveCollabOpen}
+        handleClose={() => {
+          setLeaveCollabOpen(false)
+        }}
+      />
     </div>
   )
 }

client/src/Popups/Collaboration.tsx

@@ -0,0 +1,103 @@
+import { useAtom } from 'jotai'
+import { FormEvent, useState } from 'react'
+
+import { Popup } from '../navigation/Popup'
+import {
+  collabDisplayNameAtom,
+  collabPasswordAtom,
+  collabRoomAtom,
+  isCollaboratingAtom,
+} from '../store/collaboration-atoms'
+
+/** The popup to join a collaboration room. */
+function CollaborationPopup({ open, handleClose }: { open: boolean; handleClose: () => void }) {
+  const [collabRoom, setCollabRoom] = useAtom(collabRoomAtom)
+  const [collabDisplayName, setCollabDisplayName] = useAtom(collabDisplayNameAtom)
+  const [collabPassword, setCollabPassword] = useAtom(collabPasswordAtom)
+  const [, setIsCollaborating] = useAtom(isCollaboratingAtom)
+  const [collabError, setCollabError] = useState('')
+
+  function onSubmit(ev: FormEvent) {
+    ev.preventDefault()
+    const isValid = /^[\w\d]{3,20}$/
+    const isValidPwd = /^[\w\d]{1,20}$/
+    if (!isValid.test(collabRoom)) {
+      setCollabError('Room name must be 3-20 alphanumeric characters.')
+      return
+    }
+    if (collabPassword != undefined && !isValidPwd.test(collabPassword)) {
+      setCollabError('The password must be up to 20 alphanumeric characters.')
+      return
+    }
+    if (!isValid.test(collabDisplayName)) {
+      setCollabError('Display name must be 3-20 alphanumeric characters.')
+      return
+    }
+    setCollabError('')
+    if (collabRoom) {
+      setIsCollaborating(true)
+      handleClose()
+    }
+  }
+
+  return (
+    <Popup open={open} handleClose={handleClose}>
+      <h2>Start or join collaboration</h2>
+      <form onSubmit={onSubmit}>
+        <div>
+          <p>
+            Others can join the collaboration by using the same "room name". The "display name" can
+            be chosen freely.
+          </p>
+          <p>
+            An optional password can be provided to restrict room access. Note that supplying a
+            different password will not result in an error. Instead each combination of room name
+            and password will have its own room.
+          </p>
+        </div>
+        <label>Room name:</label>
+        <input
+          required
+          autoFocus
+          type="text"
+          placeholder="Room name"
+          value={collabRoom}
+          onChange={(e) => {
+            setCollabRoom(e.target.value)
+            setCollabError('')
+          }}
+        />
+        <label>Display name:</label>
+        <input
+          required
+          type="text"
+          placeholder="Your display name"
+          value={collabDisplayName}
+          onChange={(e) => {
+            setCollabDisplayName(e.target.value)
+            setCollabError('')
+          }}
+        />
+        <label>Password (optional):</label>
+        <input
+          type="password"
+          placeholder="room password"
+          value={collabPassword}
+          onChange={(e) => {
+            const pwd = e.target.value
+            if (pwd.length == 0) {
+              setCollabPassword(undefined)
+            } else {
+              setCollabPassword(pwd)
+            }
+            setCollabError('')
+          }}
+        />
+        {collabError && <p className="form-error">{collabError}</p>}
+        <input type="submit" value="Join" />
+      </form>
+    </Popup>
+  )
+}
+
+export default CollaborationPopup

client/src/Popups/LeaveCollaboration.tsx

@@ -0,0 +1,44 @@
+import { useAtom } from 'jotai'
+import { FormEvent } from 'react'
+
+import { Popup } from '../navigation/Popup'
+import { collabRoomAtom, isCollaboratingAtom } from '../store/collaboration-atoms'
+
+/** The popup to join a collaboration room. */
+function LeaveCollaborationPopup({
+  open,
+  handleClose,
+}: {
+  open: boolean
+  handleClose: () => void
+}) {
+  const [, setIsCollaborating] = useAtom(isCollaboratingAtom)
+  const [collabRoom] = useAtom(collabRoomAtom)
+
+  function onSubmit(ev: FormEvent) {
+    ev.preventDefault()
+    setIsCollaborating(false)
+    handleClose()
+  }
+
+  return (
+    <Popup open={open} handleClose={handleClose}>
+      <h2>{`Leave collaboration '${collabRoom}'?`}</h2>
+      <form onSubmit={onSubmit}>
+        <div className="button-row">
+          <button
+            onClick={(ev) => {
+              ev.preventDefault()
+              handleClose()
+            }}
+          >
+            Stay
+          </button>
+          <input type="submit" value="Leave" />
+        </div>
+      </form>
+    </Popup>
+  )
+}
+
+export default LeaveCollaborationPopup

client/src/Popups/LoadZulip.tsx

@@ -50,7 +50,7 @@ function LoadZulipPopup({
         Copy paste a zulip message here to extract code-blocks.{' '}
         <i>(mobile: "copy to clipboard", web: "view message source")</i>
       </p>
-      {error ? <p className="form-error">{error}</p> : null}
+      {error && <p className="form-error">{error}</p>}
       <form onSubmit={handleLoad}>
         <textarea
           name="Zulip message input"

client/src/Popups/PrivacyPolicy.tsx

@@ -8,13 +8,16 @@ function PrivacyPopup({ open, handleClose }: { open: boolean; handleClose: () =>
       <h2>Privacy Policy</h2>
 
       <p>
-        Our server collects metadata (such as IP address, browser, operating system) and the data
-        that the user enters into the editor. The data is used to compute the Lean output and
+        Our server collects metadata (such as IP address, browser, operating system) and the content
+        which the user enters into the editor. The data is used to compute the Lean output and
         display it to the user. The information will be stored as long as the user stays on our
         website and will be deleted immediately afterwards. We keep logs to improve our software,
-        but the contained data is anonymised.
+        but the contained data is anonymised and does not contain user code.
+      </p>
+      <p>
+        The collaboration feature keeps an in-memory list of active rooms. The content is then
+        shared directly peer-to-peer and therefore not stored on the server.
       </p>
-
       <p>
         We don't use cookies but you can choose to save the settings in the browser store by
         activating the option in the settings.

client/src/css/Collab.css

@@ -0,0 +1,22 @@
+.yRemoteSelection {
+  background-color: color-mix(in srgb, var(--vscode-symbolIcon-eventForeground) 25%, transparent);
+  border: 1px solid var(--vscode-contrastActiveBorder); /* for high-contrast theme */
+}
+
+.yRemoteSelectionHead {
+  position: absolute;
+  border-left: var(--vscode-symbolIcon-eventForeground) solid 2px;
+  border-top: var(--vscode-symbolIcon-eventForeground) solid 2px;
+  border-bottom: var(--vscode-symbolIcon-eventForeground) solid 2px;
+  height: 100%;
+  box-sizing: border-box;
+}
+
+.yRemoteSelectionHead::after {
+  position: absolute;
+  content: ' ';
+  border: 3px solid var(--vscode-symbolIcon-eventForeground);
+  border-radius: 4px;
+  left: -4px;
+  top: -5px;
+}