From 0ff490df0f52535d9dfe0dca423e60ad7d56dd58 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 1 Jul 2026 17:00:51 -0400 Subject: [PATCH 1/2] feat: sandboxed dev documentation, less telemetry --- DEVELOPMENT.md | 44 +++++++++++++++++++++++++++++++++- Makefile | 15 ++++++++---- scripts/seed-volume.sh | 8 +++---- src/lib/server/vscodeServer.ts | 32 +++++++++++++++++++++++++ templates/hello/lean-toolchain | 1 - 5 files changed, 89 insertions(+), 11 deletions(-) delete mode 100644 templates/hello/lean-toolchain diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md index 00e206a..438f64f 100644 --- a/DEVELOPMENT.md +++ b/DEVELOPMENT.md @@ -17,7 +17,10 @@ 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. @@ -25,6 +28,45 @@ Open `http://localhost:3000`. You'll see the setup page. 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 +cnetwork 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_DEV_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_DEV_IP=0.0.0.0' >> ~/.bashrc +echo 'export DOCKER_CACHE_DIR=lean-workbench-cache' >> ~/.bashrc +source ~/.bashrc +``` + +You'll also need to run the following command outside the sandbox in order to +access the sandboxed website from your computer. + +``` +sbx ports workbench --publish 43000:3000 +``` + +The sandboxed server will then be available at + ## Makefile targets | Target | What it does | diff --git a/Makefile b/Makefile index 06dcc84..4ef689e 100644 --- a/Makefile +++ b/Makefile @@ -4,6 +4,8 @@ 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 .DEFAULT_GOAL := container .PHONY: clean container container-dev test clean-install serve dev enter @@ -21,16 +23,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 \ @@ -48,6 +50,9 @@ enter: container mkdir -p $(WORKBENCH_ROOT) $(DOCKER_RUN) --interactive --entrypoint bash $(IMAGE_NAME):$(IMAGE_TAG) +WORKBENCH_DEV_IP ?= 127.0.0.1 +DOCKER_CACHE_DIR ?= $(CURDIR)/.docker-cache + dev: container-dev mkdir -p $(WORKBENCH_ROOT) # Ports bound on localhost by the container: @@ -55,9 +60,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_DEV_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)' \ No newline at end of file diff --git a/scripts/seed-volume.sh b/scripts/seed-volume.sh index 8b99a1b..05c00c4 100755 --- a/scripts/seed-volume.sh +++ b/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" < { } } +async function ensureUserSettings(serverDataDir: string): Promise { + 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 { 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, diff --git a/templates/hello/lean-toolchain b/templates/hello/lean-toolchain deleted file mode 100644 index 7638861..0000000 --- a/templates/hello/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:stable From 53c7a1a5aff8b8d2ea8b2288c844f4f95f0c81c8 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 1 Jul 2026 20:38:08 -0400 Subject: [PATCH 2/2] Cleanup --- DEVELOPMENT.md | 29 +++++++++++++---------------- Makefile | 11 ++++++----- 2 files changed, 19 insertions(+), 21 deletions(-) diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md index 438f64f..da41745 100644 --- a/DEVELOPMENT.md +++ b/DEVELOPMENT.md @@ -17,10 +17,10 @@ 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. 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. + 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. @@ -30,10 +30,9 @@ Open `http://localhost:3000`. You'll see the setup 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 -cnetwork access: +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 . @@ -46,20 +45,18 @@ 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_DEV_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. +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_DEV_IP=0.0.0.0' >> ~/.bashrc +echo 'export WORKBENCH_PUBLISH_IP=0.0.0.0' >> ~/.bashrc echo 'export DOCKER_CACHE_DIR=lean-workbench-cache' >> ~/.bashrc source ~/.bashrc ``` -You'll also need to run the following command outside the sandbox in order to -access the sandboxed website from your computer. +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 diff --git a/Makefile b/Makefile index 4ef689e..0a2bd07 100644 --- a/Makefile +++ b/Makefile @@ -6,6 +6,10 @@ IMAGE_DEV_TAG = latest-dev 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 @@ -44,15 +48,12 @@ 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) $(DOCKER_RUN) --interactive --entrypoint bash $(IMAGE_NAME):$(IMAGE_TAG) -WORKBENCH_DEV_IP ?= 127.0.0.1 -DOCKER_CACHE_DIR ?= $(CURDIR)/.docker-cache - dev: container-dev mkdir -p $(WORKBENCH_ROOT) # Ports bound on localhost by the container: @@ -60,7 +61,7 @@ dev: container-dev # 9229: Node.js debugger npx concurrently --names host,docker \ 'npm run watch' \ - '$(DOCKER_RUN) -p $(WORKBENCH_DEV_IP):3000:3000 \ + '$(DOCKER_RUN) -p $(WORKBENCH_PUBLISH_IP):3000:3000 \ -p 127.0.0.1:9229:9229 \ -v $(DOCKER_CACHE_DIR):/root/.cache \ -v $(CURDIR):/app/workbench:ro \