feat: collab support in vscode-workbench extension

.dockerignore

@@ -12,8 +12,7 @@
 !tsconfig.json
 
 # Collaboration server
-!collab-server/package.json
-!collab-server/server.ts
+!collab-server/dist
 
 # Pre-built workbench extension
 !vscode-workbench.vsix

.gitignore

@@ -14,9 +14,10 @@ node_modules/
 # next.js
 /.next/
 /out/
+.docker-cache
 
 # prisma
-*/prisma/generated
+**/prisma/generated
 
 # production
 /build

DEVELOPMENT.md

@@ -25,13 +25,6 @@ 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 |
@@ -52,6 +45,7 @@ the first VSCode server to start up will have its [extension host](https://code.
 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

@@ -46,6 +46,7 @@ dev: container-dev
 		'npm run watch' \
  		'$(DOCKER_RUN) -p 127.0.0.1:3000:3000 \
 			-p 127.0.0.1:9229:9229 \
+			-v $(CURDIR)/.docker-cache:/root/.cache \
 			-v $(CURDIR):/app/workbench:ro \
 			-v $(CURDIR)/vscode-workbench:/app/openvscode-server/extensions/leanprover.workbench-universal:ro \
 			$(IMAGE_NAME):$(IMAGE_DEV_TAG)'

collab-server/esbuild.mjs

@@ -0,0 +1,22 @@
+import esbuild from 'esbuild'
+
+const isProd = process.argv.includes('--production')
+const watch = process.argv.includes('--watch')
+
+const ctx = await esbuild.context({
+  entryPoints: ['src/server.ts'],
+  bundle: true,
+  format: 'esm',
+  outfile: 'dist/server.js',
+  minify: isProd,
+  sourcemap: !isProd,
+  platform: 'node',
+  target: 'node24',
+})
+
+if (watch) {
+  await ctx.watch()
+} else {
+  await ctx.rebuild()
+  await ctx.dispose()
+}

collab-server/package.json

@@ -4,10 +4,15 @@
   "private": true,
   "type": "module",
   "scripts": {
-    "watch": "tsc --watch --preserveWatchOutput",
-    "tsc": "tsc"
+    "watch": "concurrently --names esbuild,tsc 'npm run watch:esbuild' 'npm run watch:tsc'",
+    "watch:esbuild": "node esbuild.mjs --watch",
+    "watch:tsc": "tsc --watch --preserveWatchOutput",
+    "tsc": "tsc",
+    "build": "tsc --noEmit && node esbuild.mjs --production"
   },
   "dependencies": {
-    "@hocuspocus/server": "^4.0.0"
+    "@hocuspocus/extension-database": "^4.0.0",
+    "@hocuspocus/server": "^4.0.0",
+    "esbuild": "^0.28"
   }
 }

collab-server/src/server.ts

@@ -0,0 +1,96 @@
+import { Database } from '@hocuspocus/extension-database'
+import { Server } from '@hocuspocus/server'
+import { once } from 'node:events'
+import fs from 'node:fs/promises'
+import path from 'node:path'
+import { DatabaseSync } from 'node:sqlite'
+import * as Y from 'yjs'
+
+// -- CLI --
+if (process.argv.length !== 3) {
+  console.error('Usage: node server.js <projectDir>')
+  process.exit(1)
+}
+
+const projectDir = process.argv[2]
+const socketPath = path.join(process.cwd(), 'collab.sock')
+const dbPath = path.join(process.cwd(), 'collab.db')
+
+// -- DB --
+const db = new DatabaseSync(dbPath)
+db.exec('CREATE TABLE IF NOT EXISTS document (path TEXT PRIMARY KEY NOT NULL, data BLOB NOT NULL)')
+
+const selectDocumentStatement = db.prepare('SELECT data FROM document WHERE path = ?')
+const selectDocument = (path: string): Uint8Array | undefined =>
+  (selectDocumentStatement.get(path) as { data: Uint8Array } | undefined)?.data
+const upsertDocumentStatement = db.prepare(
+  'INSERT INTO document (path, data) VALUES (?, ?) ON CONFLICT(path) DO UPDATE SET data = excluded.data',
+)
+const upsertDocument = (path: string, data: Uint8Array): void => {
+  upsertDocumentStatement.run(path, data)
+}
+
+// -- YJS FILE MANAGEMENT --
+// TODO: use const imported from single-source-of-truth module
+const YTEXT_KEY = 'content'
+
+function checkedToDiskPath(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({
+  extensions: [
+    // Note: we can't use the SQLite extension.
+    // Its onLoadDocument would be called after ours,
+    // but we want to try it *before* trying the filesystem.
+    new Database({
+      async fetch({ documentName }) {
+        const data = selectDocument(documentName)
+        if (data) return data
+        let content: string
+        try {
+          content = await fs.readFile(checkedToDiskPath(documentName), 'utf-8')
+        } catch {
+          return null
+        }
+        const doc = new Y.Doc()
+        doc.getText(YTEXT_KEY).insert(0, content)
+        return Y.encodeStateAsUpdate(doc)
+      },
+      async store({ documentName, state }) {
+        upsertDocument(documentName, state)
+      },
+    }),
+  ],
+})
+
+// TODO: listen for fs events to avoid lost writes.
+// VSCs could inform the server about which saves came from them,
+// as opposed to other processes (e.g. CLI tools).
+// Non-VSC edits could be applied to the Y.Doc as whole-file replacements.
+
+// `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()
+db.close()
+
+// TODO: ensure writes are flushed to disk.

collab-server/tsconfig.json

@@ -1,4 +1,4 @@
 {
   "extends": "../tsconfig.json",
-  "include": ["server.ts"]
+  "include": ["src/**/*.ts"]
 }