diff --git a/client/package.json b/client/package.json index 3bd4bc8b..b5e6952e 100644 --- a/client/package.json +++ b/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", diff --git a/client/src/App.tsx b/client/src/App.tsx index 153fb034..3fd64638 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -8,8 +8,11 @@ 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, useRef, useState, useMemo } from 'react' import Split from 'react-split' +import * as Y from 'yjs' +import { WebrtcProvider } from 'y-webrtc' +import { MonacoBinding } from 'y-monaco' import LeanLogo from './assets/logo.svg' import { codeAtom } from './editor/code-atoms' @@ -37,6 +40,14 @@ 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(null) + const [binding, setBinding] = useState(null) + const [collabDialogVisible, setCollabDialogVisible] = useState(false) + const [collabRoomName, setCollabRoomName] = useState('') + const [collabDisplayName, setCollabDisplayName] = useState('') + const [isCollaborating, setIsCollaborating] = useState(false) + const [collabError, setCollabError] = useState('') const [importedCode] = useAtom(importedCodeAtom) const model = editor?.getModel() @@ -66,6 +77,55 @@ 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 || !collabRoomName) { + setProvider(null) + return + } + + const signalingUrl = (window.location.protocol === 'https:' ? 'wss://' : 'ws://') + window.location.host.replace(':3000', ':8080') + '/yjs-signaling' + console.log('COLLAB: Signaling URL:', signalingUrl); + + const provider = new WebrtcProvider( + collabRoomName, // roomname + ydoc, + { + maxConns: 50, + password: undefined, + signaling: [signalingUrl], + filterBcConns: true, + } + ) + if (collabDisplayName) { + provider.awareness.setLocalStateField('user', { name: collabDisplayName }) + } + setProvider(provider) + return () => { + provider?.destroy() + } + }, [ydoc, isCollaborating, collabRoomName, collabDisplayName]) + + // 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 @@ -114,95 +174,95 @@ function App() { var leanMonacoEditor = new LeanMonacoEditor() _leanMonaco.setInfoviewElement(infoviewRef.current!) - ;(async () => { - await _leanMonaco.start(options) - await leanMonacoEditor.start( - editorRef.current!, - path.join(project.folder, `${project.folder}.lean`), - code ?? '', - ) - - setEditor(leanMonacoEditor.editor) - setLeanMonaco(_leanMonaco) - - // Add a `Paste` option to the context menu on mobile. - // Monaco does not support clipboard pasting as all browsers block it - // due to security reasons. Therefore we use a codeMirror editor overlay - // which features good mobile support (but no Lean support yet) - if (mobile) { - leanMonacoEditor.editor?.addAction({ - id: 'myPaste', - label: "Paste: open 'Plain Editor' for editing on mobile", - // keybindings: [monaco.KeyMod.CtrlCmd | monaco.KeyCode.KEY_V], - contextMenuGroupId: '9_cutcopypaste', - run: (_editor) => { - setCodeMirror(true) - }, - }) - } + ; (async () => { + await _leanMonaco.start(options) + await leanMonacoEditor.start( + editorRef.current!, + path.join(project.folder, `${project.folder}.lean`), + code ?? '', + ) + + setEditor(leanMonacoEditor.editor) + setLeanMonaco(_leanMonaco) + + // Add a `Paste` option to the context menu on mobile. + // Monaco does not support clipboard pasting as all browsers block it + // due to security reasons. Therefore we use a codeMirror editor overlay + // which features good mobile support (but no Lean support yet) + if (mobile) { + leanMonacoEditor.editor?.addAction({ + id: 'myPaste', + label: "Paste: open 'Plain Editor' for editing on mobile", + // keybindings: [monaco.KeyMod.CtrlCmd | monaco.KeyCode.KEY_V], + contextMenuGroupId: '9_cutcopypaste', + run: (_editor) => { + setCodeMirror(true) + }, + }) + } + + // // TODO: This was an approach to create a new definition provider, but it + // // wasn't that useful. I'll leave it here in connection with the TODO below for + // // reference. + // monaco.languages.registerDefinitionProvider('lean4', { + // provideDefinition(model, position) { + // const word = model.getWordAtPosition(position); + // if (word) { + // console.log(`[Lean4web] Providing definition for: ${word.word}`); + // // Return the location of the definition + // return [ + // { + // uri: model.uri, + // range: {startLineNumber: 0, startColumn: word.startColumn, endColumn: word.endColumn, endLineNumber: 0}, // Replace with actual definition range + // }, + // ]; + // } + // return null; + // }, + // }); - // // TODO: This was an approach to create a new definition provider, but it - // // wasn't that useful. I'll leave it here in connection with the TODO below for - // // reference. - // monaco.languages.registerDefinitionProvider('lean4', { - // provideDefinition(model, position) { - // const word = model.getWordAtPosition(position); - // if (word) { - // console.log(`[Lean4web] Providing definition for: ${word.word}`); - // // Return the location of the definition - // return [ - // { - // uri: model.uri, - // range: {startLineNumber: 0, startColumn: word.startColumn, endColumn: word.endColumn, endLineNumber: 0}, // Replace with actual definition range - // }, - // ]; - // } - // return null; - // }, - // }); - - // TODO: Implement Go-To-Definition better - // This approach only gives us the file on the server (plus line number) it wants - // to open, is there a better approach? - const editorService = (leanMonacoEditor.editor as any)?._codeEditorService - if (editorService) { - const openEditorBase = editorService.openCodeEditor.bind(editorService) - editorService.openCodeEditor = async (input: any, source: any) => { - const result = await openEditorBase(input, source) - if (result === null) { - // found this out with `console.debug(input)`: - // `resource.path` is the file go-to-def tries to open on the disk - // we try to create a doc-gen link from that. Could not extract the - // (fully-qualified) decalaration name... with that one could - // call `...${path}.html#${declaration}` - let path = input.resource.path - .replace(new RegExp('^.*/(?:lean|\.lake/packages/[^/]+/)'), '') - .replace(new RegExp('\.lean$'), '') - - if ( - window.confirm( - `Do you want to open the docs?\n\n${path} (line ${input.options.selection.startLineNumber})`, - ) - ) { - let newTab = window.open( - `https://leanprover-community.github.io/mathlib4_docs/${path}.html`, - '_blank', - ) - if (newTab) { - newTab.focus() + // TODO: Implement Go-To-Definition better + // This approach only gives us the file on the server (plus line number) it wants + // to open, is there a better approach? + const editorService = (leanMonacoEditor.editor as any)?._codeEditorService + if (editorService) { + const openEditorBase = editorService.openCodeEditor.bind(editorService) + editorService.openCodeEditor = async (input: any, source: any) => { + const result = await openEditorBase(input, source) + if (result === null) { + // found this out with `console.debug(input)`: + // `resource.path` is the file go-to-def tries to open on the disk + // we try to create a doc-gen link from that. Could not extract the + // (fully-qualified) decalaration name... with that one could + // call `...${path}.html#${declaration}` + let path = input.resource.path + .replace(new RegExp('^.*/(?:lean|\.lake/packages/[^/]+/)'), '') + .replace(new RegExp('\.lean$'), '') + + if ( + window.confirm( + `Do you want to open the docs?\n\n${path} (line ${input.options.selection.startLineNumber})`, + ) + ) { + let newTab = window.open( + `https://leanprover-community.github.io/mathlib4_docs/${path}.html`, + '_blank', + ) + if (newTab) { + newTab.focus() + } } } + return null + // return result // always return the base result } - return null - // return result // always return the base result } - } - // Keeping the `code` state up-to-date with the changes in the editor - leanMonacoEditor.editor?.onDidChangeModelContent(() => { - setCode(leanMonacoEditor.editor?.getModel()?.getValue()!) - }) - })() + // Keeping the `code` state up-to-date with the changes in the editor + leanMonacoEditor.editor?.onDidChangeModelContent(() => { + setCode(leanMonacoEditor.editor?.getModel()?.getValue()!) + }) + })() return () => { leanMonacoEditor.dispose() _leanMonaco.dispose() @@ -269,7 +329,58 @@ function App() { codeMirror={codeMirror} setCodeMirror={setCodeMirror} /> + + {collabDialogVisible && ( +
+
{ + e.preventDefault(); + const isValid = /^[a-z0-9]{3,20}$/; + if (!isValid.test(collabRoomName)) { + setCollabError("Room name must be 3-20 lowercase alphanumeric characters."); + return; + } + if (!isValid.test(collabDisplayName)) { + setCollabError("Display name must be 3-20 lowercase alphanumeric characters."); + return; + } + setCollabError(""); + if (collabRoomName) { + setIsCollaborating(true); + setCollabDialogVisible(false); + } + }} + > +

Join Collaboration

+ {collabError &&
{collabError}
} +
+ + { setCollabRoomName(e.target.value); setCollabError(''); }} style={{ padding: '6px', backgroundColor: 'var(--vscode-input-background, white)', color: 'var(--vscode-input-foreground, black)', border: '1px solid var(--vscode-input-border, #ccc)' }} /> +
+
+ + { setCollabDisplayName(e.target.value); setCollabError(''); }} style={{ padding: '6px', backgroundColor: 'var(--vscode-input-background, white)', color: 'var(--vscode-input-foreground, black)', border: '1px solid var(--vscode-input-border, #ccc)' }} /> +
+
+ + +
+
+
+ )} { diff --git a/client/src/css/index.css b/client/src/css/index.css index dceb0cc6..9eecaf2e 100644 --- a/client/src/css/index.css +++ b/client/src/css/index.css @@ -22,3 +22,23 @@ body { font-family: 'JuliaMono'; src: local('JuliaMono'), url('/fonts/JuliaMono-Regular.ttf'); } + +.yRemoteSelection { + background-color: rgb(250, 129, 0, .5) +} +.yRemoteSelectionHead { + position: absolute; + border-left: orange solid 2px; + border-top: orange solid 2px; + border-bottom: orange solid 2px; + height: 100%; + box-sizing: border-box; +} +.yRemoteSelectionHead::after { + position: absolute; + content: ' '; + border: 3px solid orange; + border-radius: 4px; + left: -4px; + top: -5px; +} \ No newline at end of file diff --git a/server/index.mjs b/server/index.mjs index 62d193ac..a44f6ecc 100755 --- a/server/index.mjs +++ b/server/index.mjs @@ -228,10 +228,117 @@ function FilenamesToUri(prefix, obj) { return obj; } +const enableCollab = process.argv.includes('--collab=yes'); +if (enableCollab) { + console.log("COLLAB: Enabling signaling server for collaboration."); +} + +const yjsTopics = new Map(); // roomName -> Set + +const sendYjs = (conn, message) => { + if (conn.readyState !== 0 && conn.readyState !== 1) { + conn.close(); + } + try { + conn.send(JSON.stringify(message)); + } catch (e) { + conn.close(); + } +}; + +const setupYjsConnection = (conn, req) => { + const ip = req ? (req.headers["x-forwarded-for"] || req.socket.remoteAddress) : "unknown"; + console.log(`COLLAB: New connection established from ${ip}`); + const subscribedTopics = new Set(); + let closed = false; + // Check if connection is still alive + let pongReceived = true; + const pingInterval = setInterval(() => { + if (!pongReceived) { + conn.close(); + clearInterval(pingInterval); + } else { + pongReceived = false; + try { + conn.ping(); + } catch (e) { + conn.close(); + } + } + }, 30000); + conn.on("pong", () => { + pongReceived = true; + }); + conn.on("close", () => { + console.log(`COLLAB: Connection closed from ${ip}`); + subscribedTopics.forEach((topicName) => { + const subs = yjsTopics.get(topicName) || new Set(); + subs.delete(conn); + if (subs.size === 0) { + yjsTopics.delete(topicName); + } + }); + subscribedTopics.clear(); + closed = true; + }); + conn.on("message", (message) => { + if (typeof message === "string" || message instanceof Buffer) { + try { + message = JSON.parse(message); + } catch (e) { + return; + } + } + if (message && message.type && !closed) { + switch (message.type) { + case "subscribe": + (message.topics || []).forEach((topicName) => { + if (typeof topicName === "string") { + let topic = yjsTopics.get(topicName); + if (!topic) { + topic = new Set(); + yjsTopics.set(topicName, topic); + } + topic.add(conn); + subscribedTopics.add(topicName); + console.log(`COLLAB: Client subscribed to topic: ${topicName}`); + } + }); + break; + case "unsubscribe": + (message.topics || []).forEach((topicName) => { + const subs = yjsTopics.get(topicName); + if (subs) { + subs.delete(conn); + console.log(`COLLAB: Client unsubscribed from topic: ${topicName}`); + } + }); + break; + case "publish": + if (message.topic) { + const receivers = yjsTopics.get(message.topic); + console.log(`COLLAB: Client published to topic ${message.topic} (receivers: ${receivers ? receivers.size : 0})`); + if (receivers) { + message.clients = receivers.size; + receivers.forEach((receiver) => sendYjs(receiver, message)); + } + } + break; + case "ping": + sendYjs(conn, { type: "pong" }); + } + } + }); +}; + wss.addListener("connection", async function (ws, req) { const urlRegEx = /^\/websocket\/([\w.-]+)$/; const reRes = urlRegEx.exec(req.url); if (!reRes) { + if (enableCollab && (req.url === "/yjs-signaling" || req.url === "/yjs-signaling/")) { + setupYjsConnection(ws, req); + return; + } console.error(`Connection refused because of invalid URL: ${req.url}`); return; } diff --git a/server/package.json b/server/package.json index 480d71e4..6d6641f1 100644 --- a/server/package.json +++ b/server/package.json @@ -6,8 +6,8 @@ "server": "index.mjs" }, "scripts": { - "dev": "NODE_ENV=development nodemon index.mjs", - "prod": "NODE_ENV=production nodemon index.mjs", + "dev": "NODE_ENV=development nodemon index.mjs --collab=yes", + "prod": "NODE_ENV=production nodemon index.mjs --collab=yes", "build": "./build.sh" }, "dependencies": {