Setting up codespaces for a class

Stream: mathlib4

[Trevor Hyde]

I'm teaching a Lean class this semester. I'm concerned not all my students will have computers that are able to run Lean. I was advised to have an option to use Github Codespaces. I just need some help setting this up. I copied a .devcontainer folder into my project from someone else's repo, but I'm not sure what comes next. Is there anything else I need to do? What do the students need to do to open/create a codespace based on my repo?

[Riccardo Brasca]

If the .devcontainer is OK just go to https://codespaces.new/yourname/yourrepo to create it

[Riccardo Brasca]

Each student has to create it

[Trevor Hyde]

Hey Riccardo, I'm trying to setup codespaces for my Lean class using the dev container from your repo. When I open my repo in codespaces and try to build the container, I'm getting errors. I suspect I probably didn't make the right changes in the dev container.

This seems to be the relevant error:

====================================== ERROR ====================================
2025-01-21 15:56:01.208Z: Failed to create container.
=================================================================================
2025-01-21 15:56:01.208Z: Error: Command failed: /bin/sh -c lake exe cache get! && lake build
2025-01-21 15:56:01.209Z: Error code: 1302 (UnifiedContainersErrorFatalCreatingContainer)

Here is my devcontainer.json

{
  "name": "math301spring2025 dev container",

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

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

  "hostRequirements": {
     "cpus": 4
  },

  "customizations": {
    "vscode" : {
      "extensions" : [ "leanprover.lean4" ]
    }
  }
}

All I changed was the name and removed the Libraryafter lake build since my project doesn't have a Library.

[Riccardo Brasca]

Hmm, I am not sure. Is your repo public?

[Trevor Hyde]

Yes
https://github.com/tghyde/math301spring2025

[Riccardo Brasca]

I also get an error doing lake build locally (probably because there is no file called math301spring2025.lean)

[Trevor Hyde]

I see. The repo seems to work fine for me locally. There is a file, but it looks like it was created with a capital M. I'll try changing the name of the file.

[Riccardo Brasca]

That is the file that is compiled when you do lake build. You can erase it and never doing lake build if you don't need it (if each file only depends on mathlib and NOT on other files of your project for example)

[Riccardo Brasca]

Or you can keep it empty, or with just #eval 2+2 to check that everything works.

[Riccardo Brasca]

change the M to m and it should work

[Trevor Hyde]

I see. I didn't understand what the lake build command was doing, I thought it was needed whenever starting a Lean project.

[Riccardo Brasca]

It compiles the file specified in lakefile.lean at the @[default_targer] line. Currently you have

@[default_target]
lean_lib «math301spring2025» {

that is why it is looking for math301spring2025.lean.

[Riccardo Brasca]

You can of course put Math301spring2025 there

[Riccardo Brasca]

the idea is that that file imports everything in your project (or maybe it contains the final theorem), so compiling it checks that everything is ok.

[Trevor Hyde]

Got it. I was naively copying files from another repo and changing the names of things that seemed like they needed to change. So if I had custom libraries of definitions and theorems that I wanted the class to use, I could put them all in this file and they'd be available for students to use in this project? Of in the case of your project, we can have a folder full of different Lean files to be imported?

[Riccardo Brasca]

if you have prerequisites written by yourself just put them in a folder whatevername and import them in any file you need (I suggest to hide this in VS Code so students don't play with it). In this case importing those in math301spring2025.lean and doing lake build (only once) it is necessary.

[Riccardo Brasca]

Note that with code space students have to create the codespace only once, then they are supposed to go to https://github.com/codespaces/ and reopen it.

[Riccardo Brasca]

anyway now your repo works on codespace for me

[Trevor Hyde]

Thanks @Riccardo, I appreciate the help

[Riccardo Brasca]

I just did the installation with students today and I have to say everything went pretty well.

Of course you have to deal with trivial things like "I didn't register to github even if you asked us to do so" or "I forgot the password and it is sending the code to my other phone" but well, that's life

[Damiano Testa]

Riccardo Brasca said:

Of course you have to deal with trivial things like "I didn't register to github even if you asked us to do so" or "I forgot the password and it is sending the code to my other phone" but well, that's life

These kind of things make me think that AI can be more successful than humans at everything.

[Ruben Van de Velde]

Can AI register a github account?

[Riccardo Brasca]

The captcha is really hard, with a finger pointing left (say) and you have to rotate a cat (say) to same direction of the finger

[Ruben Van de Velde]

Can AI guess the password of an existing github account?

(Sorry, really going off topic here)

[Riccardo Brasca]

More to the point, my strategy for the first class was the following: getting codespace ready asap, explaining that this part is like a pre-introduction to be done once. Once everyone has clicked on "create codespace" I asked to not touch the computer and listen to me doing the actual introduction to the class.

[Rob Lewis]

Something I just discovered the other day, of interest to people teaching with codespaces: GitHub is willing to prebuild codespace images for a very small fee. (In your repository, Settings -> Codespaces.) For me it'll cost about $1 to keep the image available this whole semester, and save each student minutes every time they create a codespace. Well worth it.