How to make my Lean repo work in Github Codespaces?

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:

Paperproof in github codespaces screenshot

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.