chore: sbx-friendly docker updates

.dockerignore

@@ -13,6 +13,7 @@
 
 # Collaboration server
 !collab-server/dist
+!collab-server/package.json
 
 # Pre-built workbench extension
 !vscode-workbench.vsix

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 \

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
 

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}`))
+  })