feat: collab support in vscode-workbench extension

.dockerignore

@@ -1,11 +1,25 @@
-.git
-.github
-.husky
-.next
-.vscode
-branch-*
-node_modules
-plans
-.env*
-.eslintcache
-vscode-workbench/
+# Ignore everything by default, then allow only what the Dockerfile build needs.
+*
+
+# Next.js server
+!public
+!src
+!next-env.d.ts
+!next.config.ts
+!package-lock.json
+!package.json
+!prisma.config.ts
+!tsconfig.json
+
+# Collaboration server
+!collab-server/package.json
+!collab-server/server.ts
+
+# Pre-built workbench extension
+!vscode-workbench.vsix
+
+# Scripts, data, etc.
+!scripts
+!templates
+!nginx.conf.template
+!start.sh

.gitignore

@@ -1,6 +1,6 @@
 # dependencies
-/node_modules
-/.pnp
+node_modules/
+.pnp
 .pnp.*
 .yarn/*
 !.yarn/patches

DEVELOPMENT.md

@@ -10,7 +10,7 @@ It describes how to locally run and test the workbench software.
 ## Running the workbench server
 
 ```bash
-npm install # install dependencies and generate types
+npm clean-install # install dependencies and generate types
 make dev # build and run the container in development mode
 ```
 
@@ -25,6 +25,13 @@ Open `http://localhost:3000`. You'll see the setup page.
    takes 5--30 min on first run).
 3. When seeding finishes, you're redirected to the landing page.
 
+## Updating NPM packages
+
+Make sure to pass `--install-strategy=nested` to `npm install`.
+This ensures that `package-lock.json` places `node_modules` in package folders
+as opposed to hoisting them out to the root directory;
+we rely on this in the dev container.
+
 ## Makefile targets
 
 | Target | What it does |
@@ -41,11 +48,11 @@ Set the `WORKBENCH_ROOT` Makefile argument to customize this.
 ## Debugging
 
 In dev mode (`make dev`),
-each editor session in the admin panel has an "Enable debugger" button.
-Clicking it causes the [extension host](https://code.visualstudio.com/api/advanced-topics/extension-host) of that VSCode server
-to start a debugger on port 9229.
-Use the "Attach to vscode-workbench" launch target configured in this workspace to attach.
-You can set breakpoints in the vscode-workbench/ extension.
+the first VSCode server to start up will have its [extension host](https://code.visualstudio.com/api/advanced-topics/extension-host)
+start a debugger on port 9229.
+Use the "Attach to vscode-workbench" VSCode launch target to attach.
+You can set breakpoints in the `vscode-workbench/` extension.
+Note that `console.log` in the extension goes to the _renderer_, i.e., the web client.
 
 ## Resetting the data volume
 

Makefile

@@ -12,7 +12,7 @@ clean:
 	@test "$(realpath $(WORKBENCH_ROOT) 2>/dev/null)" != "/" || { echo "ERROR: WORKBENCH_ROOT resolves to /"; exit 1; }
 	rm -rf $(WORKBENCH_ROOT)
 
-vscode-workbench.vsix:
+vscode-workbench.vsix: $(shell find vscode-workbench/src -type f) vscode-workbench/.vscodeignore vscode-workbench/esbuild.mjs vscode-workbench/package.json vscode-workbench/tsconfig.json
 	cd vscode-workbench && npx vsce package --out ../vscode-workbench.vsix
 
 container: vscode-workbench.vsix

collab-server/package.json

@@ -0,0 +1,9 @@
+{
+  "name": "@leanprover/workbench-collab-server",
+  "version": "0.1.0",
+  "private": true,
+  "type": "module",
+  "dependencies": {
+    "@hocuspocus/server": "^4.0.0"
+  }
+}

collab-server/server.ts

@@ -0,0 +1,75 @@
+import { Server } from '@hocuspocus/server'
+import { once } from 'node:events'
+import fs from 'node:fs/promises'
+import path from 'node:path'
+
+// -- CLI --
+if (process.argv.length !== 4) {
+  console.error('Usage: node server.ts <socketPath> <projectDir>')
+  process.exit(1)
+}
+
+const socketPath = process.argv[2]
+const projectDir = process.argv[3]
+
+// -- YJS FILE MANAGEMENT --
+// TODO: import vscode-workbench/util
+const YTEXT_KEY = 'content'
+
+function toDiskPath(documentName: string): string {
+  const file = path.normalize(documentName)
+  if (!file.startsWith(projectDir)) {
+    throw new Error(`Path traversal in document name: '${documentName}' escapes '${projectDir}'`)
+  }
+  return file
+}
+
+// -- HTTPS/WS SERVER --
+const server = new Server({
+  async onLoadDocument(data) {
+    const ytext = data.document.getText(YTEXT_KEY)
+    if (ytext.length > 0) return
+    try {
+      const content = await fs.readFile(toDiskPath(data.documentName), 'utf-8')
+      ytext.insert(0, content)
+    } catch (e) {
+      if ((e as NodeJS.ErrnoException).code !== 'ENOENT') throw e
+    }
+  },
+  async onStoreDocument(data) {
+    console.log('onstore', data.documentName, data.clientsCount)
+    // TODO: this runs more or less whenever someone edits something.
+    // - We want better saving semantics:
+    //   when *any user* saves, the file is persisted to disk,
+    //   but not otherwise.
+    // - Dirty state should be reflected for all users:
+    //   a boolean in Y.Doc is one option,
+    //   whereas Claude recommends storing mtime (or such) in Y.Doc
+    //   and computing dirty state from that.
+    // - We should persist Y.Docs to a (in-memory or on-disk) database; not the project dir.
+    const file = toDiskPath(data.documentName)
+    const ytext = data.document.getText(YTEXT_KEY)
+    await fs.mkdir(path.dirname(file), { recursive: true })
+    await fs.writeFile(file, ytext.toString(), 'utf-8')
+  },
+})
+
+// `server.listen` exposes a port. We use a socket which needs direct `httpServer` access.
+server.httpServer.listen(socketPath, () => {
+  // Cosmetic monkey-patches to display the correct start screen. Server works regardless of these.
+  Object.defineProperty(server, 'webSocketURL', {
+    get: () => `ws+unix:${socketPath}`,
+  })
+  Object.defineProperty(server, 'httpURL', {
+    get: () => `http+unix:${socketPath}`,
+  })
+  server['showStartScreen']()
+
+  // No need to call `onListen` hooks here since we don't register any.
+})
+
+await Promise.race([once(process, 'SIGINT'), once(process, 'SIGQUIT'), once(process, 'SIGTERM')])
+console.log('Hocuspocus shutting down..')
+await server.destroy()
+
+// TODO: ensure writes are flushed to disk.