feat: vscode-workbench extension

.dockerignore

@@ -8,3 +8,4 @@ node_modules
 plans
 .env*
 .eslintcache
+vscode-workbench/

.gitignore

@@ -43,4 +43,10 @@ next-env.d.ts
 .eslintcache
 
 # git
-branch-*
+branch-*
+
+# vscode extension
+dist/
+.vscode-test/
+out/
+*.vsix

.vscode/launch.json

@@ -0,0 +1,17 @@
+{
+  "version": "0.2.0",
+  "configurations": [
+    {
+      "type": "node",
+      "request": "attach",
+      "name": "Attach to vscode-workbench",
+      "address": "localhost",
+      "port": 9229,
+      "localRoot": "${workspaceFolder}/vscode-workbench/",
+      // The extension dir as seen by bubblewrap
+      "remoteRoot": "/workspace/.openvscode-server/extensions/leanprover.workbench-universal/",
+      "sourceMaps": true,
+      "outFiles": ["${workspaceFolder}/vscode-workbench/dist/**/*.js"]
+    }
+  ]
+}

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 vscode-workbench" launch target configured in this workspace to attach.
+You can set breakpoints in the vscode-workbench/ extension.
+
 ## Resetting the data volume
 
 The data volume is preserved on the host across development sessions,

Dockerfile

@@ -2,95 +2,100 @@
 
 # --- base image: Node.js installation shared between builders and runners ---
 FROM buildpack-deps:24.04-curl AS base
-RUN curl -fsSL https://deb.nodesource.com/setup_24.x | bash - \
+RUN curl -sSfL https://deb.nodesource.com/setup_24.x | bash - \
+    && apt-get update \
     && apt-get install -y --no-install-recommends nodejs \
     && rm -rf /var/lib/apt/lists/*
 
-# --- base builder image: build bubblewrap ---
+# --- base builder image: build and download prerequisites ---
 FROM base AS builder-base
 
-RUN apt-get update && apt-get install -y --no-install-recommends \
-        meson ninja-build pkg-config libcap-dev xz-utils gcc g++ libc6-dev make \
-    && rm -rf /var/lib/apt/lists/*
+RUN apt-get update \
+    && apt-get install -y --no-install-recommends \
+        meson ninja-build pkg-config libcap-dev xz-utils gcc g++ libc6-dev make unzip
+
+# Will be copied to runner images
+RUN mkdir /app
 
 # Build bubblewrap 0.11.1 from source (need --tmp-overlay support; Ubuntu 24.04 only has 0.9.0)
 ARG BUBBLEWRAP_VERSION="0.11.1"
 RUN curl -sSfL https://github.com/containers/bubblewrap/releases/download/v${BUBBLEWRAP_VERSION}/bubblewrap-${BUBBLEWRAP_VERSION}.tar.xz \
     | tar -xJ \
     && cd bubblewrap-${BUBBLEWRAP_VERSION} \
-    && meson setup _build --prefix=/usr \
+    && meson setup _build --prefix=/usr --buildtype=release \
     && ninja -C _build \
     && ninja -C _build install \
     && cd / && rm -rf /bubblewrap-${BUBBLEWRAP_VERSION}
 
-# --- base runner image: minimal runtime, no build tools ---
-FROM base AS runner-base
-
-RUN apt-get update && apt-get install -y --no-install-recommends \
-        nginx strace git libcap2 gettext-base unzip \
-    && rm -rf /var/lib/apt/lists/*
-
-WORKDIR /app/
-
 # Install openvscode-server
 ARG OPENVSCODE_SERVER_VERSION="1.109.5"
 RUN arch=$(uname -m) && \
     if [ "${arch}" = "x86_64" ]; then arch="x64"; \
     elif [ "${arch}" = "aarch64" ]; then arch="arm64"; \
+    else echo "unsupported architecture: ${arch}" >&2; exit 1; \
     fi && \
     ovsc_tag="openvscode-server-v${OPENVSCODE_SERVER_VERSION}" && \
-    wget https://github.com/gitpod-io/openvscode-server/releases/download/${ovsc_tag}/${ovsc_tag}-linux-${arch}.tar.gz && \
+    wget -q https://github.com/gitpod-io/openvscode-server/releases/download/${ovsc_tag}/${ovsc_tag}-linux-${arch}.tar.gz && \
     tar -xzf ${ovsc_tag}-linux-${arch}.tar.gz && \
     mv -f ${ovsc_tag}-linux-${arch} /app/openvscode-server && \
     rm -f ${ovsc_tag}-linux-${arch}.tar.gz
 
-# Install builtin VS Code extensions. Everyone uses the same on-disk copy of these.
-# Cannot use `--install-builtin-extension` which behaves identically to `--install-extension`.
+# Install builtin VS Code extensions. Workbench users get a read-only view of these.
+# Cannot use `--install-builtin-extension` as it does not store in the builtin directory
+# (behaves identically to `--install-extension`).
 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" \
     && install_vsix_as_builtin "tamasfe" "even-better-toml" "0.21.2"
 
-# 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 run build \
-    && mv /tmp/oct/packages/open-collaboration-server /app/open-collaboration-server \
-    && rm -rf /tmp/oct
+# --- base runner image: minimal runtime, no build tools ---
+FROM base AS runner-base
+
+RUN apt-get update \
+    && apt-get install -y --no-install-recommends \
+        nginx strace git libcap2 gettext-base \
+    && rm -rf /var/lib/apt/lists/*
+
+WORKDIR /app/
 
 # Create the user-routes dir for dynamic nginx includes
 RUN mkdir -p /etc/nginx/user-routes
 
+COPY --from=builder-base --parents /usr/bin/bwrap /
+
 EXPOSE 3000
 
 ENTRYPOINT ["/app/workbench/start.sh"]
 
-# --- dev runner image: /app/workbench is empty, expects host mount ---
+# --- dev runner image: /app/workbench and vscode-workbench are empty, expect host mounts ---
 FROM runner-base AS runner-dev
 
-COPY --from=builder-base --parents /usr/bin/bwrap /
+COPY --from=builder-base /app /app
 
-# --- prod builder image: bundle the Next.js server ---
+# --- prod builder image: bundle the extension and the Next.js server ---
 FROM builder-base AS builder-prod
 
-WORKDIR /app/workbench
-COPY . .
-RUN npm ci --ignore-scripts && npm rebuild better-sqlite3 \
+# Install production build of workbench extension
+COPY ./vscode-workbench.vsix /tmp/ext.vsix
+RUN unzip -q /tmp/ext.vsix "extension/*" -d /tmp \
+    && mv /tmp/extension /app/openvscode-server/extensions/leanprover.workbench-universal \
+    && rm -rf /tmp/ext.vsix
+
+COPY . /app/workbench
+RUN cd /app/workbench \
+    && 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
 
-# --- prod runner image: /app/workbench contains built server ---
+# --- prod runner image: /app/ contains built server and workbench extension ---
 FROM runner-base AS runner-prod
 
 ENV NODE_ENV=production
 
-COPY --from=builder-prod --parents /usr/bin/bwrap /app/workbench /
+COPY --from=builder-prod /app /app

Makefile

@@ -11,14 +11,17 @@ clean:
 	@test -n "$(WORKBENCH_ROOT)" || { echo "ERROR: WORKBENCH_ROOT is empty"; exit 1; }
 	@test "$(realpath $(WORKBENCH_ROOT) 2>/dev/null)" != "/" || { echo "ERROR: WORKBENCH_ROOT resolves to /"; exit 1; }
 	rm -rf $(WORKBENCH_ROOT)
+
+vscode-workbench.vsix:
+	cd vscode-workbench && npx vsce package --out ../vscode-workbench.vsix
 
-container:
+container: vscode-workbench.vsix
 	docker build --tag $(IMAGE_NAME):$(IMAGE_TAG) --target runner-prod .
 
 container-dev:
 	docker build --tag $(IMAGE_NAME):$(IMAGE_DEV_TAG) --target runner-dev .
 
-DOCKER_RUN = docker run --rm --init --interactive --tty \
+DOCKER_RUN = docker run --rm --init --tty \
 	--cap-add SYS_ADMIN \
 	--security-opt seccomp=unconfined \
 	--security-opt apparmor=unconfined \
@@ -28,12 +31,21 @@ 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)
+	$(DOCKER_RUN) --interactive --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)
+# Ports bound on localhost by the container:
+# 3000: Nginx
+# 9229: Node.js debugger
+	npx concurrently --names vscode-workbench,docker \
+		'npm run watch:vscode-workbench' \
+ 		'$(DOCKER_RUN) -p 127.0.0.1:3000:3000 \
+			-p 127.0.0.1:9229:9229 \
+			-v $(CURDIR):/app/workbench:ro \
+			-v $(CURDIR)/vscode-workbench:/app/openvscode-server/extensions/leanprover.workbench-universal:ro \
+			$(IMAGE_NAME):$(IMAGE_DEV_TAG)'

eslint.config.mjs

@@ -9,12 +9,15 @@ const eslintConfig = defineConfig([
   prettier,
   // Override default ignores of eslint-config-next.
   globalIgnores([
+    // vscode-workbench:
+    '*/dist/',
+    '*/.vscode-test/',
     // Default ignores of eslint-config-next:
-    '.next/**',
-    'out/**',
-    'build/**',
+    '.next/',
+    'out/',
+    'build/',
     'next-env.d.ts',
-    'branch-*',
+    'branch-*/',
   ]),
 ])