From bcf5c77d921fd4944b72283861d6ff8e2ca742c8 Mon Sep 17 00:00:00 2001
From: Rob Simmons <robsimmons@gmail.com>
Date: Thu, 6 Aug 2026 10:42:29 -0400
Subject: [PATCH] chore: sbx-friendly docker updates

---
 .dockerignore         |  1 +
 Dockerfile            |  7 ++++++-
 doc/DEVELOPMENT.md    | 16 ++++++++++++----
 scripts/hmr-nudge.mjs | 33 +++++++++++++++++++++++++++++++++
 4 files changed, 52 insertions(+), 5 deletions(-)
 create mode 100644 scripts/hmr-nudge.mjs

diff --git a/.dockerignore b/.dockerignore
index 377c356e..de79d128 100644
--- a/.dockerignore
+++ b/.dockerignore
@@ -13,6 +13,7 @@
 
 # Collaboration server
 !collab-server/dist
+!collab-server/package.json
 
 # Pre-built workbench extension
 !vscode-workbench.vsix
diff --git a/Dockerfile b/Dockerfile
index cda3cd0a..4450b9b8 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -166,9 +166,14 @@ RUN unzip -q /tmp/ext.vsix "extension/*" -d /tmp \
     && mv /tmp/extension /app/vscode-server/lib/vscode/extensions/leanprover.workbench-universal \
     && rm -rf /tmp/ext.vsix
 
+# Install and cache NPM dependencies
+COPY --parents package.json package-lock.json */package.json /app/workbench/
+RUN --mount=type=cache,target=/root/.npm cd /app/workbench && npm clean-install --ignore-scripts
+
+# Build workbench frontend
 COPY . /app/workbench
 RUN cd /app/workbench \
-    && npm clean-install \
+    && npm rebuild && npx next typegen && npx prisma generate \
     && mkdir -p /tmp/build-dummy \
     && LEAN_WORKBENCH_DATA_DIR=/tmp/build-dummy \
        npx next build \
diff --git a/doc/DEVELOPMENT.md b/doc/DEVELOPMENT.md
index 9cc1ece5..5a7a6ce9 100644
--- a/doc/DEVELOPMENT.md
+++ b/doc/DEVELOPMENT.md
@@ -5,7 +5,10 @@ It describes how to locally run and test the workbench software.
 
 ## Prerequisites
 
-- Docker installed and running.
+- Docker installed and running,
+  with at least 16GB memory allocated
+  (in Docker Desktop, go to Settings -> Resources -> Memory).
+- Node v24 or later is needed for `make` to work
 
 ## Running the workbench server
 
@@ -45,7 +48,7 @@ The sandbox can be started by running
 sbx run --name workbench
 ```
 
-Before running the usual dev setup in the sandbox, you'll need to run the following commands inside the sandbox.
+Before running the usual dev setup, you'll need to run the following commands *inside* the sandbox.
 The `WORKBENCH_PUBLISH_IP` setting is necessary to access workbench outside the sandbox,
 and the `DOCKER_CACHE_DIR` ensures that the docker cache doesn't have to cross the an inefficient VM boundary.
 
@@ -56,13 +59,18 @@ source ~/.bashrc
 ```
 
 To access the sandboxed website from your computer,
-you'll also need to run the following command outside the sandbox.
+you'll also need to run the following command *outside* the sandbox.
 
 ```
 sbx ports workbench --publish 43000:3000
 ```
 
-The sandboxed server will then be available at <http://localhost:43000>
+After running the makefile targets insidethe sandbox (i.e. `make dev`),
+the sandboxed server will be available on the host machine at <http://localhost:43000>
+
+Hot module reloading won't work correctly if you're making edits outside of the VM.
+Run `node scripts/hmr-nudge.mjs` in a separate `sbx` session
+in order to get hot module reloading working correctly.
 
 ## Makefile targets
 
diff --git a/scripts/hmr-nudge.mjs b/scripts/hmr-nudge.mjs
new file mode 100644
index 00000000..33c06a16
--- /dev/null
+++ b/scripts/hmr-nudge.mjs
@@ -0,0 +1,33 @@
+// In sandboxed development, changes in a text editor running outside the sandbox
+// will not always be correctly reflected inside the sandbox.
+// This script polls and nudges modified files as a workaround for this issue.
+// (See DEVELOPMENT.md)
+
+import { createHash } from 'node:crypto'
+import { readFile, utimes } from 'node:fs/promises'
+import chokidar from 'chokidar'
+
+const paths = process.argv.length < 3 ? ['src'] : process.argv.slice(2)
+const hashes = new Map()
+const nudge = async file => {
+  const hash = createHash('sha256')
+    .update(await readFile(file))
+    .digest('hex')
+  if (hashes.get(file) === hash) return
+  hashes.set(file, hash)
+  const now = new Date()
+  await utimes(file, now, now)
+  console.log(`[hmr-nudge] ${file}`)
+}
+
+chokidar
+  .watch(paths, {
+    usePolling: true,
+    interval: 400,
+    ignoreInitial: true,
+    ignored: /node_modules|lean-workbench-data|(^|\/)\./,
+  })
+  .on('all', (event, file) => {
+    if (event === 'unlink' || event === 'unlinkDir' || event === 'addDir') return
+    nudge(file).catch(err => console.error(`[hmr-nudge] ${file}: ${err.message}`))
+  })