diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md index 00e206a..da41745 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,42 @@ 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 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 + ## Makefile targets | Target | What it does | diff --git a/Makefile b/Makefile index 06dcc84..0a2bd07 100644 --- a/Makefile +++ b/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)' \ 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