GitHub [Codespaces](https://docs.github.com/en/codespaces/overview) are a feature I've found useful for Lean development. A Codespace is a virtual machine that you can spin up for a GitHub repository. The repository is automatically checked out and the Codespace can be configured to have the necessary tooling installed upon creation. On this page, I'll walk through how to set up a Codespace for Lean 4 development.
## Why use Codespaces?
The biggest advantage to using a Codespace for development in Lean that I've found is performance and disk space.
In my experience, type-checking in Lean is quite slow and I often had difficulty typechecking proofs in my [Generating Functions](https://github.com/kcaze/generating-functions) project when I used my Thinkpad T420 laptop, a 10+ years old machine. If your primary computing device is relatively low-specs, then Codespaces provides an environment that is sufficiently powerful for development in Lean.
Another advantage of using Codespaces for development is that it frees up valuable disk space. If your Lean project uses mathlib, then the precompiled `.olean` files take up nearly 4 gigabytes. Furthermore, each Lean project requires its own copy of mathlib in its `.lake` folder; there currently is no analogue to Yarn's Plug'n'Play or Conda environments that let you reuse packages across multiple Lean projects. As a result, a handful of Lean projects can easily take up to 10 or 20 gigabytes on your device. Codespaces enables you to offload that disk space requirement.
## How to configure the dev container
The environment inside a Codespace is called a [Development Container](https://containers.dev/). At a minimum, a base Docker image is included, but you can add "Features" that help install tools and configure your environment when it's being created. You will need to set up your development container for each repository that you plan to use Codespaces with. Fortunately, it's relatively easy to set up.
**Step 1:** Navigate to your repository and click on the green "Code" dropdown. Select "Codespaces", click on the three dots icon, and click on "Configure dev container".
![[Screenshot 2024-11-19 at 9.58.40 AM.png]]
**Step 2:** An editor will open up for a new `devcontainer.json` file in your repository. The contents of this file are used as the default development container settings for any Codespaces you create in this repository. Copy and paste the following configuration into your `devcontainer.json`:
```
{
"image": "mcr.microsoft.com/devcontainers/universal:2",
"customizations": {
"vscode": {
"extensions": [
"leanprover.lean4"
]
}
},
"features": {
"ghcr.io/kcaze/lean4-devcontainer-feature/lean4:1.0.6": {}
}
}
```
This configuration instructs VS Code to install the Lean 4 extension and selects the `lean4` dev container feature, which automatically installs `elan` and `lake` upon Codespace creation. Hit the "Commit changes..." button and you're ready to create a Codespace!
## Using a codespace
Once you've configured your `devcontainer.json` file, you can click on "Create codespace on main" in the "Code" dropdown of your repository. Doing so will create a new Codespace and connect to it in a browser-based VS Code. You can select a different editor by navigating to the "Codespaces" section of your GitHub settings and configuring the "Editor Preference" setting.
![[Screenshot 2024-11-19 at 10.26.58 AM.png]]
When you first create a Codespace, a terminal will pop up informing you that `elan` is being installed. Make sure that you wait for the installation to finish before you open up any Lean files. If you need to use mathlib, you will have to also run `lake exe cache get` from the terminal. All of this set up only happens once when your Codespace is created.
If you are done working with a Codespace, you can simply close the relevant VS Code window. By default, the Codespace will spin down when it's been idle for 30 minutes, but you can configure this timer to be shorter on longer in your GitHub settings. When you want to resume development, you can connect back to the same Codespace instance and the virtual machine will spin back up, with all your configuration and files intact.