How to make my Lean repo work in Github Codespaces?

This post tells you how to set up your Lean repo in Github Codespaces AND install Paperproof in that codespace by default. Remove the Paperproof lines if you'd like a vanilla project.

Suppose you already have a repo with Lean code, and you'd like to make it available on Github Codespaces, so that your users can play with it + Paperproof online, like this:

To achieve this, you would need to:

1. locally, in your repo, add require Paperproof from git "https://github.com/Paper-Proof/paperproof.git"@"main"/"lean" to lakefile.lean

2. locally, in your terminal, run lake update Paperproof

3. locally, in your repo,  add a .devcontainer folder to the root of your project, with two files inside:

• devcontainer.json

{
  "name": "Mathlib4 dev container",

  "build": {
    "dockerfile": "Dockerfile"
  },

  "onCreateCommand": "lake exe cache get!",

  "customizations": {
    "vscode" : {
      "extensions" : ["leanprover.lean4@0.0.176", "paperproof.paperproof"],
      "settings": {
        "editor.wordWrap": "on"
      }
    }
  }
}

• Dockerfile

USER vscode
WORKDIR /home/vscode

RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none

ENV PATH="/home/vscode/.elan/bin:${PATH}"

And push all of this to github.

Now, go to https://codespaces.new/.../..., where .../... is superseded with your repo name.
For exampe, for Paperproof that would be https://codespaces.new/Paper-Proof/paperproof.

This will open github codespaces for your Lean project, with Paperproof and all other dependencies automatically installed.

You're done 🎉🎉🎉

How to open some file automatically?

To your devcontainer.json, add "customizations": { "codespaces": { "openFiles": ["relative-path-to-my-file.lean"] } }.

How to add a nice "Open in Github Codespaces" button to Readme.md?

Just add [![Open in Codespaces](https://github.com/codespaces/badge.svg)](https://codespaces.new/.../...) to your .md file.
If you prefer html, add: <a href="https://codespaces.new/.../..."><img src="https://github.com/codespaces/badge.svg"/></a>.

Both of these will render the following button:

Is there some example project?

Absolutely, see https://github.com/Paper-Proof/DEMO-FormalisingMathematics, where we set up Paperproof + Kevin Buzzard's "Formalising Mathematics 2024" in Github codespaces.
All of the required changes can be seen in this commit: commit link.

Why do we need to fix the leanprover.lean version?

You could notice we write "leanprover.lean4@0.0.176" instead of writing "leanprover.lean4", which would automatically install the latest version of the lean4 vscode extension.

It's fine to write "leanprover.lean4" too, but specifying a version safeguards you against your codespace going stale because "leanprover.lean4" introduced a backwards-incompatible change and Paperproof didn't yet accommodate.