feat: sandboxed dev documentation, less telemetry

DEVELOPMENT.md

@@ -17,14 +17,53 @@ make dev # build and run the container in development mode
 Open `http://localhost:3000`. You'll see the setup page.
 
 1. - **Skip the OAuth section** — it's optional in dev mode.
-     This is the fastest way to get a running instance
+     This is the fastest way to get a running instance.
+     The UI forces you to put *something* for "Client ID" and "Client Secret",
+     but if you put in something invalid (and then "Save Configuration")
+     the only consequence is that GitHub OAuth won't work.
    - **Or** [create a GitHub OAuth App](https://github.com/settings/developers)
      with callback URL `http://localhost:3000/api/auth/github/callback`.
      Enter the resulting credentials on the setup page.
 2. Click **Start Setup** to seed the data volume (downloads Mathlib,
    takes 5--30 min on first run).
 3. When seeding finishes, you're redirected to the landing page.
 
+### Sandboxed development
+
+Development can be done inside of Docker Sandbox (which lets one avoid installing Docker Desktop on OSX).
+The following commands inside the `lean-workbench` directory will create a virtual machine
+and allow sufficient network access:
+
+```
+sbx create shell --name workbench .
+sbx policy allow network --sandbox workbench '*.docker.com:443,production.cloudfront.docker.com:443,*.docker.io:443,openvsx.eclipsecontent.org:443,electronjs.org:443,*.electronjs.org:443,fonts.googleapis.com:443,github-cloud.githubusercontent.com:443,raw.githubusercontent.com:443,release-assets.githubusercontent.com:443,github.com:443,*.github.com:443,fonts.gstatic.com:443,*.lean-lang.org:443,playwright.download.prss.microsoft.com:443,nodejs.org:443,*.nodejs.com:443,deb.nodesource.com:443,*.npmjs.org:443,open-vsx.org:443,*.playwright.dev:443,checkpoint.prisma.io:443,binaries.prisma.sh:443,www.schemastore.org:443,ports.ubuntu.com:80,ports.ubuntu.com:443'
+```
+
+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.
+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.
+
+```
+echo 'export WORKBENCH_PUBLISH_IP=0.0.0.0' >> ~/.bashrc
+echo 'export DOCKER_CACHE_DIR=lean-workbench-cache' >> ~/.bashrc
+source ~/.bashrc
+```
+
+To access the sandboxed website from your computer,
+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>
+
 ## Makefile targets
 
 | Target | What it does |

Makefile

@@ -4,6 +4,12 @@ IMAGE_TAG = latest
 IMAGE_DEV_TAG = latest-dev
 # Extra flags for `docker build`, e.g. --cache-from/--cache-to in CI.
 DOCKER_BUILD_FLAGS ?=
+# VSCode's build process opens thousands of files
+DOCKER_BUILD_ULIMIT = --ulimit nofile=65536
+# IP Address where the HTTP server publishes to port 3000 (needs to be 0.0.0.0 in some situations)
+WORKBENCH_PUBLISH_IP ?= 127.0.0.1
+# Where the Docker's container ~/.cache lives, used mostly for Lean's download cache
+DOCKER_CACHE_DIR ?= $(CURDIR)/.docker-cache
 
 .DEFAULT_GOAL := container
 .PHONY: clean container container-dev test clean-install serve dev enter
@@ -21,16 +27,16 @@ collab-server/dist/server.js: $(shell find collab-server/src -type f) collab-ser
 	npm --workspace collab-server run build
 
 container: vscode-workbench.vsix collab-server/dist/server.js
-	docker build $(DOCKER_BUILD_FLAGS) --tag $(IMAGE_NAME):$(IMAGE_TAG) --target runner-prod .
+	docker build $(DOCKER_BUILD_FLAGS) $(DOCKER_BUILD_ULIMIT) --tag $(IMAGE_NAME):$(IMAGE_TAG) --target runner-prod .
 
 container-dev:
-	docker build $(DOCKER_BUILD_FLAGS) --tag $(IMAGE_NAME):$(IMAGE_DEV_TAG) --target runner-dev .
+	docker build $(DOCKER_BUILD_FLAGS) $(DOCKER_BUILD_ULIMIT) --tag $(IMAGE_NAME):$(IMAGE_DEV_TAG) --target runner-dev .
 
 test:
 # Test vscode-workbench using VS Code with our patches applied.
 # `--output type=cacheonly` skips the expensive image export at the end.
 # `--progress=plain` displays RUN step output (notably the testing step).
-	docker build $(DOCKER_BUILD_FLAGS) --target tester-vscode-workbench --output type=cacheonly --progress=plain .
+	docker build $(DOCKER_BUILD_FLAGS) $(DOCKER_BUILD_ULIMIT) --target tester-vscode-workbench --output type=cacheonly --progress=plain .
 
 DOCKER_RUN = docker run --rm --init --tty \
 	--cap-add SYS_ADMIN \
@@ -42,7 +48,7 @@ DOCKER_RUN = docker run --rm --init --tty \
 
 serve: container
 	mkdir -p $(WORKBENCH_ROOT)
-	$(DOCKER_RUN) -p 127.0.0.1:3000:3000 $(IMAGE_NAME):$(IMAGE_TAG)
+	$(DOCKER_RUN) -p $(WORKBENCH_PUBLISH_IP):3000:3000 $(IMAGE_NAME):$(IMAGE_TAG)
 
 enter: container
 	mkdir -p $(WORKBENCH_ROOT)
@@ -55,9 +61,9 @@ dev: container-dev
 # 9229: Node.js debugger
 	npx concurrently --names host,docker \
 		'npm run watch' \
- 		'$(DOCKER_RUN) -p 127.0.0.1:3000:3000 \
+		'$(DOCKER_RUN) -p $(WORKBENCH_PUBLISH_IP):3000:3000 \
 			-p 127.0.0.1:9229:9229 \
-			-v $(CURDIR)/.docker-cache:/root/.cache \
+			-v $(DOCKER_CACHE_DIR):/root/.cache \
 			-v $(CURDIR):/app/workbench:ro \
 			-v $(CURDIR)/vscode-workbench:/app/vscode-server/lib/vscode/extensions/leanprover.workbench-universal:ro \
 			$(IMAGE_NAME):$(IMAGE_DEV_TAG)'

scripts/seed-volume.sh

@@ -164,12 +164,12 @@ else
     echo "[seed-volume] WARNING: hello template source not found, skipping."
   else
     mkdir -p "$HELLO_DIR"
-    cp "$HELLO_SRC/lean-toolchain" "$HELLO_DIR/"
+    echo "$TOOLCHAIN" > "$HELLO_DIR/lean-toolchain"
     cp "$HELLO_SRC/lakefile.toml" "$HELLO_DIR/"
     cp "$HELLO_SRC/Main.lean" "$HELLO_DIR/"
-    cat > "$HELLO_DIR/metadata.json" <<'ENDJSON'
-{ "name": "Hello World", "description": "Minimal Lean project" }
-ENDJSON
+    cat > "$HELLO_DIR/metadata.json" <<EOF
+{ "name": "Lean $LEAN_VERSION", "description": "Minimal Lean project" }
+EOF
     echo "[seed-volume] hello template installed."
   fi
 fi

src/lib/server/vscodeServer.ts

@@ -45,6 +45,33 @@ async function ensureMachineSettings(serverDataDir: string): Promise<void> {
   }
 }
 
+async function ensureUserSettings(serverDataDir: string): Promise<void> {
+  const userSettingsDir = path.join(serverDataDir, 'User')
+  const userSettingsFile = path.join(userSettingsDir, 'settings.json')
+  try {
+    await fs.access(userSettingsDir)
+  } catch {
+    await fs.mkdir(userSettingsDir, { recursive: true })
+    await fs.writeFile(
+      userSettingsFile,
+      JSON.stringify(
+        {
+          // Disable telemetry for vscode and well-behaved extensions
+          'telemetry.telemetryLevel': 'off',
+          'workbench.enableExperiments': false,
+          // Don't show vscode "what's new" content or release notes
+          'update.mode': 'none',
+          'update.showReleaseNotes': false,
+          // Hide the secondary sidebar (copilot chat) by default
+          'workbench.secondarySideBar.defaultVisibility': 'hidden',
+        },
+        null,
+        2,
+      ) + '\n',
+    )
+  }
+}
+
 async function waitForSocket(socketPath: string, timeoutMs = 10_000): Promise<void> {
   const deadline = Date.now() + timeoutMs
   let status = null
@@ -142,6 +169,7 @@ export class VscodeServerHandle implements AsyncDisposable {
       const homeDir = getUserHomeDir(this.viewer.name)
       const vscUserDataDir = path.join(homeDir, '.local', 'share', 'code-server')
       await ensureMachineSettings(vscUserDataDir)
+      await ensureUserSettings(vscUserDataDir)
 
       const sandboxHomeDir = bwrapHomeDir(this.viewer.name)
       const sandboxProjectDir = bwrapProjectDir(this.project.name)
@@ -184,6 +212,10 @@ export class VscodeServerHandle implements AsyncDisposable {
           '--auth', 'none',
           // Disable 'Do you trust this workspace?' modals.
           '--disable-workspace-trust',
+          // Disable code-server telemetry
+          '--disable-telemetry',
+          // Don't tell people they should be updating software they can't update
+          '--disable-update-check',
           // Reduce how long the extension host process waits for a web client to reconnect (default 3h).
           '--reconnection-grace-time', '60',
           sandboxProjectDir,