feat: sandboxed dev documentation, less telemetry

[robsimmons]

Several small improvements based on getting things running in a development sandbox:

• Clarify skip-github-auth workaround that flummoxed me
• Add my notes for actually using sbx sandboxing
• Add a --ulimit that was keeping VSCode from being able to build
• Make the WORKBENCH_DEV_IP configurable (necessary for running inside sbx)
• Make the DOCKER_CACHE_DIR configurable (important for efficiency running inside sbx)
• Create user settings that disable telemetry, hide update notifications, and hide the Codex sidebar
• Disable telemetry for code-server
• Move the "Hello world" project to be an empty "Lean $FIRST_INSTALLED_VERSION" project.

[jcreedcmu]

optional suggestion: if it is easy to make the production IP address configurable also, that would be be useful to accommodate different setups where the installer might or might not want to bind to 0.0.0.0 vs. 127.0.0.1 depending on whether they want to directly expose the service to the internet or, e.g. terminate SSL in a different way, have some other way of getting ingress.

[robsimmons]

@jcreedcmu should I just make it WORKBENCH_IP rather than WORKBENCH_DEV_IP that's configurable and have it connect to prod as well? Seems straightforward enough

[jcreedcmu]

That sounds good to me yeah

…

On Wed, Jul 1, 2026, 18:25 Robert J. Simmons ***@***.***> wrote: *robsimmons* left a comment (leanprover/lean-workbench#51) <#51 (comment)> @jcreedcmu <https://github.com/jcreedcmu> should I just make it WORKBENCH_IP rather than WORKBENCH_DEV_IP that's configurable and have it connect to prod as well? Seems straightforward enough — Reply to this email directly, view it on GitHub <#51?email_source=notifications&email_token=AALONFVXNBZNSZ7RY3NKRWL5CWFURA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTIOBWGA2TCNZSGI42M4TFMFZW63VHNVSW45DJN5XKKZLWMVXHJLDGN5XXIZLSL5RWY2LDNM#issuecomment-4860517229>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AALONFVKJ6CYVPKUAJJJJYT5CWFURAVCNFSNUABGKJSXA33TNF2G64TZHMYTCNZTG4ZTMNZRGQ5US43TOVSTWNBXHA4TEMJVGAYDNILWAI> . Triage notifications, keep track of coding agent tasks and review pull requests on the go with GitHub Mobile for iOS <https://github.com/notifications/mobile/ios/AALONFQND2NOSIFVHNOZ6JL5CWFURA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTIOBWGA2TCNZSGI42M4TFMFZW63VHNVSW45DJN5XKKZLWMVXHJKTGN5XXIZLSL5UW64Y> and Android <https://github.com/notifications/mobile/android/AALONFX5JKB5UMWC53I6ZBL5CWFURA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTIOBWGA2TCNZSGI42M4TFMFZW63VHNVSW45DJN5XKKZLWMVXHJLTGN5XXIZLSL5QW4ZDSN5UWI>. Download it today! You are receiving this because you were mentioned.Message ID: ***@***.***>

[Vtec234]

The prod IP should go into an option in install.sh, no? It's not currently defined in the Makefile or the Dockerfile. We set it here. (The make serve target is for testing the prod container, not actual deployments.)

[robsimmons]

Ok if the makefile setting is only for dev testing the prod server that makes even more sense for the setting to affect both places, but changing it in install.sh will be a different beast, sounds like, and a different PR.