From fb96f938a5fd88af63fdbed3c6ec04a2fc1dadaa Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 27 Apr 2026 19:45:52 -0400 Subject: [PATCH 1/3] feat: debug extension host in workbench --- .vscode/launch.json | 12 ++++++++ AGENTS.md | 1 + DEVELOPMENT.md | 1 + Dockerfile | 6 ++-- Makefile | 9 ++++-- src/app/admin/actions.ts | 13 ++++++-- src/app/admin/components/SessionRow.tsx | 20 +++++++++--- src/lib/server/editorSessions.ts | 41 ++++++++++++++++++++++++- src/lib/server/util.ts | 31 +++++++++++++++++++ start.sh | 2 +- 10 files changed, 122 insertions(+), 14 deletions(-) create mode 100644 .vscode/launch.json create mode 100644 src/lib/server/util.ts diff --git a/.vscode/launch.json b/.vscode/launch.json new file mode 100644 index 0000000..935ced7 --- /dev/null +++ b/.vscode/launch.json @@ -0,0 +1,12 @@ +{ + "version": "0.2.0", + "configurations": [ + { + "type": "node", + "request": "attach", + "name": "Attach to Node process", + "address": "localhost", + "port": 9229 + } + ] +} diff --git a/AGENTS.md b/AGENTS.md index 2d43951..9cea0b7 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -42,6 +42,7 @@ over manually storing response/error state with `useState`. - Ignore `TODO`s and `FIXME`s in the codebase. - Don't set `NODE_ENV` to anything besides `production` (https://nodejs.org/learn/getting-started/nodejs-the-difference-between-development-and-production). +- Prefer full CLI flag and command names in scripts. More self-documenting. ## Refactoring diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md index 6ee8319..beef3ae 100644 --- a/DEVELOPMENT.md +++ b/DEVELOPMENT.md @@ -10,6 +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 make dev # build and run the container in development mode ``` diff --git a/Dockerfile b/Dockerfile index de16f70..7fc42f7 100644 --- a/Dockerfile +++ b/Dockerfile @@ -58,7 +58,7 @@ RUN install_vsix_as_builtin() { \ # Install open-collaboration-server from source (self-contained esbuild bundle) RUN git clone --depth 1 https://github.com/eclipse-oct/open-collaboration-tools.git /tmp/oct \ && cd /tmp/oct \ - && npm ci \ + && npm clean-install \ && npm run build \ && mv /tmp/oct/packages/open-collaboration-server /app/open-collaboration-server \ && rm -rf /tmp/oct @@ -80,11 +80,9 @@ FROM builder-base AS builder-prod WORKDIR /app/workbench COPY . . -RUN npm ci --ignore-scripts && npm rebuild better-sqlite3 \ +RUN npm clean-install \ && mkdir -p /tmp/build-dummy \ - && npx prisma generate \ && LEAN_WORKBENCH_DATA_DIR=/tmp/build-dummy \ - BETTER_AUTH_SECRET=build-dummy \ npx next build \ && npm prune --omit=dev diff --git a/Makefile b/Makefile index 0bae1db..7fded4f 100644 --- a/Makefile +++ b/Makefile @@ -28,7 +28,7 @@ DOCKER_RUN = docker run --rm --init --interactive --tty \ serve: container mkdir -p $(WORKBENCH_ROOT) - $(DOCKER_RUN) -p 3000:3000 $(IMAGE_NAME):$(IMAGE_TAG) + $(DOCKER_RUN) -p 127.0.0.1:3000:3000 $(IMAGE_NAME):$(IMAGE_TAG) enter: container mkdir -p $(WORKBENCH_ROOT) @@ -36,4 +36,9 @@ enter: container dev: container-dev mkdir -p $(WORKBENCH_ROOT) - $(DOCKER_RUN) -p 3000:3000 -v $(CURDIR):/app/workbench:ro $(IMAGE_NAME):$(IMAGE_DEV_TAG) \ No newline at end of file +# 3000: Nginx +# 9229: Node.js debugger + $(DOCKER_RUN) -p 127.0.0.1:3000:3000 \ + -p 127.0.0.1:9229:9229 \ + -v $(CURDIR):/app/workbench:ro \ + $(IMAGE_NAME):$(IMAGE_DEV_TAG) \ No newline at end of file diff --git a/src/app/admin/actions.ts b/src/app/admin/actions.ts index a95e26e..3f02a0f 100644 --- a/src/app/admin/actions.ts +++ b/src/app/admin/actions.ts @@ -114,20 +114,29 @@ export async function updateOAuthConfig(clientId: string, clientSecret: string | // --- Editor sessions --- -const zKillEditorSession = z.object({ +const zEditorSession = z.object({ viewerId: z.string().min(1), projectId: z.string().min(1), }) export async function killEditorSession(viewerId: string, projectId: string): Promise { await requireAdmin() - const parsed = zKillEditorSession.safeParse({ viewerId, projectId }) + const parsed = zEditorSession.safeParse({ viewerId, projectId }) if (!parsed.success) return { error: parsed.error.issues[0].message } const mgr = getEditorSessionManager() mgr.killSession(parsed.data.viewerId, parsed.data.projectId) return { ok: undefined } } +export async function debugEditorSession(viewerId: string, projectId: string): Promise { + await requireAdmin() + const parsed = zEditorSession.safeParse({ viewerId, projectId }) + if (!parsed.success) return { error: parsed.error.issues[0].message } + const mgr = getEditorSessionManager() + mgr.debugSession(parsed.data.viewerId, parsed.data.projectId) + return { ok: undefined } +} + // --- System health --- function parseMeminfo(): Record { diff --git a/src/app/admin/components/SessionRow.tsx b/src/app/admin/components/SessionRow.tsx index 2fcc0c6..438ad80 100644 --- a/src/app/admin/components/SessionRow.tsx +++ b/src/app/admin/components/SessionRow.tsx @@ -1,18 +1,25 @@ 'use client' +import { ConfigCtx } from '@/lib/contexts' import type { EditorSessionInfo } from '@/lib/server/editorSessions' import { useServerAction } from '@/lib/util' import { useRouter } from 'next/navigation' -import { startTransition } from 'react' -import { killEditorSession } from '../actions' +import { startTransition, use } from 'react' +import { debugEditorSession, killEditorSession } from '../actions' export function SessionRow({ info }: { info: EditorSessionInfo }) { const router = useRouter() - const [error, killAction, pending] = useServerAction( + const cfg = use(ConfigCtx) + const [killError, killAction, killPending] = useServerAction( () => killEditorSession(info.viewerId, info.projectId), () => router.refresh(), ) + const [debugError, debugAction, debugPending] = useServerAction( + () => debugEditorSession(info.viewerId, info.projectId), + () => router.refresh(), + ) + const error = killError && debugError return (
  • @@ -24,9 +31,14 @@ export function SessionRow({ info }: { info: EditorSessionInfo }) {
    port {info.port} - + {cfg.isDevMode && ( + + )}
    {error &&
    {error}
    }
    • diff --git a/src/lib/server/editorSessions.ts b/src/lib/server/editorSessions.ts index befd8c7..f9a6a57 100644 --- a/src/lib/server/editorSessions.ts +++ b/src/lib/server/editorSessions.ts @@ -6,8 +6,10 @@ import { getOpenVscodeServerDir, getPackageSetsDir, getWorkspacesDir, + isDevMode, } from '@/lib/server/config' import { getDb } from '@/lib/server/db' +import { readProcesses } from '@/lib/server/util' import { Project } from '@/prisma/generated/client' import { execSync, spawn } from 'node:child_process' import fs from 'node:fs' @@ -172,6 +174,17 @@ export class EditorSessionManager { : ['--overlay-src', projectDir, '--tmp-overlay', sandboxProjectDir] const overlayArgs = await buildOverlayArgs(project.id, projectDir, sandboxProjectDir) + const devArgs = isDevMode() + ? [ + // Instructs Node to bind its debugger to this address, when debugging is enabled. + // FIXME: VSC also passes --experimental-network-inspection to the extension host, + // but that is disallowed in NODE_OPTIONS. + '--setenv', + 'NODE_OPTIONS', + '--inspect-port=0.0.0.0:9229', + ] + : [] + const child = spawn( 'bwrap', // prettier-ignore @@ -200,6 +213,7 @@ export class EditorSessionManager { '--setenv', 'GIT_CONFIG_COUNT', '1', '--setenv', 'GIT_CONFIG_KEY_0', 'safe.directory', '--setenv', 'GIT_CONFIG_VALUE_0', '*', + ...devArgs, '--unshare-user', '--uid', '1000', '--gid', '1000', @@ -258,12 +272,37 @@ export class EditorSessionManager { killSession(viewerId: string, projectId: string): void { const projectSessions = this.editorSessions.get(projectId) ?? [] const session = projectSessions.find(s => s.viewerId === viewerId) - if (!session) return + if (!session) { + console.warn(`Tried to kill nonexistent session '${viewerId} editing ${projectId}'`) + return + } try { process.kill(session.pid) } catch {} } + /** Start a debugger in the extension host of the given VSCode session. */ + debugSession(viewerId: string, projectId: string) { + const projectSessions = this.editorSessions.get(projectId) ?? [] + const session = projectSessions.find(s => s.viewerId === viewerId) + if (!session) { + console.warn(`Tried to debug nonexistent session '${viewerId} editing ${projectId}'`) + return + } + // Send SIGUSR1 to the (assumed unique) extension host descendant of openvscode-server. + const root = readProcesses().get(session.pid) + const stack = root ? [root] : [] + while (stack.length > 0) { + const proc = stack.pop()! + if (proc.cmdline.includes('--type=extensionHost')) { + process.kill(proc.pid, 'SIGUSR1') + return + } + stack.push(...proc.children) + } + console.warn(`Extension host not found for session '${viewerId} editing ${projectId}'`) + } + async listSessions(): Promise { const result: EditorSessionInfo[] = [] for (const [projectId, sessions] of this.editorSessions) { diff --git a/src/lib/server/util.ts b/src/lib/server/util.ts new file mode 100644 index 0000000..7389f1f --- /dev/null +++ b/src/lib/server/util.ts @@ -0,0 +1,31 @@ +import fs from 'node:fs' +import 'server-only' + +export interface ProcessInfo { + pid: number + /** Parent PID. */ + ppid: number + cmdline: string[] + children: ProcessInfo[] +} + +/** Read the process table from `/proc`, + * returning a map from PID to process info with children linked. + * Linux-only. */ +export function readProcesses(): Map { + const procs = new Map() + for (const entry of fs.readdirSync('/proc')) { + const pid = Number(entry) + if (!Number.isInteger(pid)) continue + try { + const status = fs.readFileSync(`/proc/${pid}/status`, 'utf-8') + const ppid = Number(status.match(/^PPid:\s*(\d+)/m)![1]) + const cmdline = fs.readFileSync(`/proc/${pid}/cmdline`, 'utf-8').split('\0') + procs.set(pid, { pid, ppid, cmdline, children: [] }) + } catch {} + } + for (const proc of procs.values()) { + procs.get(proc.ppid)?.children.push(proc) + } + return procs +} diff --git a/start.sh b/start.sh index 27fd914..1fef21e 100755 --- a/start.sh +++ b/start.sh @@ -38,7 +38,7 @@ else mount --bind "/tmp/workbench.tmpfs/$f" "${SCRIPT_DIR}/$f" done - cd "${SCRIPT_DIR}" && npm install && npm run dev -- --port 3002 & + cd "${SCRIPT_DIR}" && npm clean-install && npm run dev -- --port 3002 & fi APP_PID=$! trap 'kill $APP_PID 2>/dev/null' EXIT From 52476dd99df8fd90aca6fdb90c69d29e80a7ff23 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 27 Apr 2026 19:52:29 -0400 Subject: [PATCH 2/3] doc: debug --- DEVELOPMENT.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md index beef3ae..0cec732 100644 --- a/DEVELOPMENT.md +++ b/DEVELOPMENT.md @@ -38,6 +38,14 @@ Open `http://localhost:3000`. You'll see the setup page. The data volume is stored in `/tmp/lean-workbench/` on the host by default. Set the `WORKBENCH_ROOT` Makefile argument to customize this. +## Debugging + +In dev mode (`make dev`), the admin panel displays a "Debug" button on each editor session. +This launches a debugger in the [extension host](https://code.visualstudio.com/api/advanced-topics/extension-host) +of that VSCode server. +Use the "Attach to Node process" VSCode launch target configured in this workspace +to attach to the debugger after launching it. + ## Resetting the data volume The data volume is preserved on the host across development sessions, From 2c30f85eb97e16328fccf5bd7787a5ba7635167c Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 27 Apr 2026 20:49:26 -0400 Subject: [PATCH 3/3] feat: attach to vscode-lean4 --- .vscode/launch.json | 13 +++++++++++-- DEVELOPMENT.md | 11 ++++++----- Dockerfile | 2 +- Makefile | 1 + src/app/admin/components/SessionRow.tsx | 2 +- 5 files changed, 20 insertions(+), 9 deletions(-) diff --git a/.vscode/launch.json b/.vscode/launch.json index 935ced7..b08f0a6 100644 --- a/.vscode/launch.json +++ b/.vscode/launch.json @@ -4,9 +4,18 @@ { "type": "node", "request": "attach", - "name": "Attach to Node process", + "name": "Attach to extension host", "address": "localhost", - "port": 9229 + "port": 9229, + "localRoot": "${workspaceFolder}/vscode-lean4/vscode-lean4/", + // The extension dir as seen by bubblewrap + "remoteRoot": "/workspace/.openvscode-server/extensions/leanprover.lean4-universal/", + "sourceMaps": true, + "outFiles": ["${workspaceFolder}/vscode-lean4/*/dist/**/*.js"], + "sourceMapPathOverrides": { + // Cursed. Caused by our webpack config. Maybe undo those hacks. + "file:////*": "/*" + } } ] } diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md index 0cec732..5f75e60 100644 --- a/DEVELOPMENT.md +++ b/DEVELOPMENT.md @@ -40,11 +40,12 @@ Set the `WORKBENCH_ROOT` Makefile argument to customize this. ## Debugging -In dev mode (`make dev`), the admin panel displays a "Debug" button on each editor session. -This launches a debugger in the [extension host](https://code.visualstudio.com/api/advanced-topics/extension-host) -of that VSCode server. -Use the "Attach to Node process" VSCode launch target configured in this workspace -to attach to the debugger after launching it. +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 extension host" launch target configured in this workspace to attach. +You can set breakpoints in the vscode-lean4 extension. ## Resetting the data volume diff --git a/Dockerfile b/Dockerfile index 7fc42f7..6a1f6ed 100644 --- a/Dockerfile +++ b/Dockerfile @@ -49,7 +49,7 @@ RUN arch=$(uname -m) && \ RUN install_vsix_as_builtin() { \ wget -q -O /tmp/ext.vsix "https://open-vsx.org/api/$1/$2/$3/file/$1.$2-$3.vsix" \ && unzip -q /tmp/ext.vsix "extension/*" -d /tmp \ - && mv /tmp/extension "/app/openvscode-server/extensions/$1.$2-$3-universal" \ + && mv /tmp/extension "/app/openvscode-server/extensions/$1.$2-universal" \ && rm -rf /tmp/ext.vsix; \ } \ && install_vsix_as_builtin "leanprover" "lean4" "0.0.234" \ diff --git a/Makefile b/Makefile index 7fded4f..00fbd9d 100644 --- a/Makefile +++ b/Makefile @@ -41,4 +41,5 @@ dev: container-dev $(DOCKER_RUN) -p 127.0.0.1:3000:3000 \ -p 127.0.0.1:9229:9229 \ -v $(CURDIR):/app/workbench:ro \ + -v $(CURDIR)/vscode-lean4/vscode-lean4:/app/openvscode-server/extensions/leanprover.lean4-universal:ro \ $(IMAGE_NAME):$(IMAGE_DEV_TAG) \ No newline at end of file diff --git a/src/app/admin/components/SessionRow.tsx b/src/app/admin/components/SessionRow.tsx index 438ad80..18c764d 100644 --- a/src/app/admin/components/SessionRow.tsx +++ b/src/app/admin/components/SessionRow.tsx @@ -36,7 +36,7 @@ export function SessionRow({ info }: { info: EditorSessionInfo }) { {cfg.isDevMode && ( )}