feat: debug extension host in workbench

.vscode/launch.json

@@ -0,0 +1,21 @@
+{
+  "version": "0.2.0",
+  "configurations": [
+    {
+      "type": "node",
+      "request": "attach",
+      "name": "Attach to extension host",
+      "address": "localhost",
+      "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:////*": "/*"
+      }
+    }
+  ]
+}

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
 

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
 ```
 
@@ -37,6 +38,15 @@ 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`),
+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
 
 The data volume is preserved on the host across development sessions,

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" \
@@ -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
 

Makefile

@@ -28,12 +28,18 @@ 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)
 	$(DOCKER_RUN) --entrypoint bash $(IMAGE_NAME):$(IMAGE_TAG)
 
 dev: container-dev
 	mkdir -p $(WORKBENCH_ROOT)
-	$(DOCKER_RUN) -p 3000:3000 -v $(CURDIR):/app/workbench:ro $(IMAGE_NAME):$(IMAGE_DEV_TAG)
+# 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 \
+		-v $(CURDIR)/vscode-lean4/vscode-lean4:/app/openvscode-server/extensions/leanprover.lean4-universal:ro \
+		$(IMAGE_NAME):$(IMAGE_DEV_TAG)

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<ActionResponse> {
   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<ActionResponse> {
+  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<string, number> {

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 (
     <li>
       <div className='info'>
@@ -24,9 +31,14 @@ export function SessionRow({ info }: { info: EditorSessionInfo }) {
       </div>
       <div className='actions'>
         <span style={{ fontSize: '0.8rem', color: '#90a4ae' }}>port {info.port}</span>
-        <button className='delete' disabled={pending} onClick={() => startTransition(killAction)}>
+        <button className='delete' disabled={killPending} onClick={() => startTransition(killAction)}>
           Kill
         </button>
+        {cfg.isDevMode && (
+          <button disabled={debugPending} onClick={() => startTransition(debugAction)}>
+            [DEV] Enable debugger
+          </button>
+        )}
       </div>
       {error && <div style={{ color: '#dc2626', fontSize: 13 }}>{error}</div>}
     </li>

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<EditorSessionInfo[]> {
     const result: EditorSessionInfo[] = []
     for (const [projectId, sessions] of this.editorSessions) {

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<number, ProcessInfo> {
+  const procs = new Map<number, ProcessInfo>()
+  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
+}

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