Skip to content

Commit 905f46d

Browse files
authored
feat: collaboration server (#12)
* feat: set up workspace * perf: dev startup time * chore: ignore subfolders * feat: collab server * feat: start collab servers * feat: more robust server startup Removes several race conditions from openvscode-server and collab-server startup/shutdown. Fixes 404 on initial editor session startup. * feat: invert dockerignore * fix: various paths * feat: collab server * fix: use FS dir and write-mount * fix: oops
1 parent 69a1b9a commit 905f46d

16 files changed

Lines changed: 69575 additions & 6131 deletions

.dockerignore

Lines changed: 25 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,25 @@
1-
.git
2-
.github
3-
.husky
4-
.next
5-
.vscode
6-
branch-*
7-
node_modules
8-
plans
9-
.env*
10-
.eslintcache
11-
vscode-workbench/
1+
# Ignore everything by default, then allow only what the Dockerfile build needs.
2+
*
3+
4+
# Next.js server
5+
!public
6+
!src
7+
!next-env.d.ts
8+
!next.config.ts
9+
!package-lock.json
10+
!package.json
11+
!prisma.config.ts
12+
!tsconfig.json
13+
14+
# Collaboration server
15+
!collab-server/package.json
16+
!collab-server/server.ts
17+
18+
# Pre-built workbench extension
19+
!vscode-workbench.vsix
20+
21+
# Scripts, data, etc.
22+
!scripts
23+
!templates
24+
!nginx.conf.template
25+
!start.sh

.gitignore

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
# dependencies
2-
/node_modules
3-
/.pnp
2+
node_modules/
3+
.pnp
44
.pnp.*
55
.yarn/*
66
!.yarn/patches

DEVELOPMENT.md

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ It describes how to locally run and test the workbench software.
1010
## Running the workbench server
1111

1212
```bash
13-
npm install # install dependencies and generate types
13+
npm clean-install # install dependencies and generate types
1414
make dev # build and run the container in development mode
1515
```
1616

@@ -25,6 +25,13 @@ Open `http://localhost:3000`. You'll see the setup page.
2525
takes 5--30 min on first run).
2626
3. When seeding finishes, you're redirected to the landing page.
2727

28+
## Updating NPM packages
29+
30+
Make sure to pass `--install-strategy=nested` to `npm install`.
31+
This ensures that `package-lock.json` places `node_modules` in package folders
32+
as opposed to hoisting them out to the root directory;
33+
we rely on this in the dev container.
34+
2835
## Makefile targets
2936

3037
| Target | What it does |
@@ -41,11 +48,10 @@ Set the `WORKBENCH_ROOT` Makefile argument to customize this.
4148
## Debugging
4249

4350
In dev mode (`make dev`),
44-
each editor session in the admin panel has an "Enable debugger" button.
45-
Clicking it causes the [extension host](https://code.visualstudio.com/api/advanced-topics/extension-host) of that VSCode server
46-
to start a debugger on port 9229.
47-
Use the "Attach to vscode-workbench" launch target configured in this workspace to attach.
48-
You can set breakpoints in the vscode-workbench/ extension.
51+
the first VSCode server to start up will have its [extension host](https://code.visualstudio.com/api/advanced-topics/extension-host)
52+
start a debugger on port 9229.
53+
Use the "Attach to vscode-workbench" VSCode launch target to attach.
54+
You can set breakpoints in the `vscode-workbench/` extension.
4955

5056
## Resetting the data volume
5157

Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ clean:
1212
@test "$(realpath $(WORKBENCH_ROOT) 2>/dev/null)" != "/" || { echo "ERROR: WORKBENCH_ROOT resolves to /"; exit 1; }
1313
rm -rf $(WORKBENCH_ROOT)
1414

15-
vscode-workbench.vsix:
15+
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
1616
cd vscode-workbench && npx vsce package --out ../vscode-workbench.vsix
1717

1818
container: vscode-workbench.vsix

collab-server/package.json

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
{
2+
"name": "@leanprover/workbench-collab-server",
3+
"version": "0.1.0",
4+
"private": true,
5+
"type": "module",
6+
"dependencies": {
7+
"@hocuspocus/server": "^4.0.0"
8+
}
9+
}

collab-server/server.ts

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
import { Server } from '@hocuspocus/server'
2+
import { once } from 'node:events'
3+
import fs from 'node:fs/promises'
4+
import path from 'node:path'
5+
6+
// -- CLI --
7+
if (process.argv.length !== 4) {
8+
console.error('Usage: node server.ts <socketPath> <projectDir>')
9+
process.exit(1)
10+
}
11+
12+
const socketPath = process.argv[2]
13+
const projectDir = process.argv[3]
14+
15+
// -- YJS FILE MANAGEMENT --
16+
const YTEXT_KEY = 'content'
17+
18+
function toDiskPath(documentName: string): string {
19+
const joined = path.join(projectDir, documentName)
20+
if (!joined.startsWith(projectDir)) {
21+
throw new Error(`Path traversal in document name: ${documentName}`)
22+
}
23+
return joined
24+
}
25+
26+
// -- HTTPS/WS SERVER --
27+
const server = new Server({
28+
async onLoadDocument(data) {
29+
const ytext = data.document.getText(YTEXT_KEY)
30+
if (ytext.length > 0) return
31+
try {
32+
const content = await fs.readFile(toDiskPath(data.documentName), 'utf-8')
33+
ytext.insert(0, content)
34+
} catch (e) {
35+
if ((e as NodeJS.ErrnoException).code !== 'ENOENT') throw e
36+
}
37+
},
38+
async onStoreDocument(data) {
39+
console.log('onstore', data.documentName, data.clientsCount)
40+
// TODO: this runs more or less whenever someone edits something.
41+
// - We want better saving semantics:
42+
// when *any user* saves, the file is persisted to disk,
43+
// but not otherwise.
44+
// - Dirty state should be reflected for all users:
45+
// a boolean in Y.Doc is one option,
46+
// whereas Claude recommends storing mtime (or such) in Y.Doc
47+
// and computing dirty state from that.
48+
// - We should persist Y.Docs to a (in-memory or on-disk) database; not the project dir.
49+
const file = toDiskPath(data.documentName)
50+
const ytext = data.document.getText(YTEXT_KEY)
51+
await fs.mkdir(path.dirname(file), { recursive: true })
52+
await fs.writeFile(file, ytext.toString(), 'utf-8')
53+
},
54+
})
55+
56+
// `server.listen` exposes a port. We use a socket which needs direct `httpServer` access.
57+
server.httpServer.listen(socketPath, () => {
58+
// Cosmetic monkey-patches to display the correct start screen. Server works regardless of these.
59+
Object.defineProperty(server, 'webSocketURL', {
60+
get: () => `ws+unix:${socketPath}`,
61+
})
62+
Object.defineProperty(server, 'httpURL', {
63+
get: () => `http+unix:${socketPath}`,
64+
})
65+
server['showStartScreen']()
66+
67+
// No need to call `onListen` hooks here since we don't register any.
68+
})
69+
70+
await Promise.race([once(process, 'SIGINT'), once(process, 'SIGQUIT'), once(process, 'SIGTERM')])
71+
console.log('Hocuspocus shutting down..')
72+
await server.destroy()
73+
74+
// TODO: ensure writes are flushed to disk.

0 commit comments

Comments
 (0)