codespaces

Stream: Lean for teaching

[Matthew Ballard]

As Eric pointed out https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Basic.20Analysis.20hangup.20in.20Lean/near/288842411, GitHub Codespaces is free for educational use (currently).

We are getting to the point our intro to proofs course to start lean. I had previously planned on going with GitPod but it seems that Codespaces is easier to interact with for students. (Mainly due to the integration into the GH web UI. Plus it is actually free vs almost effectively free for GitPod.)

I put together a working Lean 4 Codespaces setup here.

[Matthew Ballard]

TLDR for codespaces setup: make a folder .devcontainer folder and put in a Dockerfile and devcontainer.json.

The ones here are based on the GitPod files for the class at KIT. The only complications were where to point the FROM in the Dockerfile (a good idea is to ask VS Code to make it for you start) and how to modify PATH for elan.

I am sure my setup is far from elegant so welcome any input!

[Gihan Marasingha]

Ah, I've just found out about codespaces. As I understand it, it's a way for students to do Lean in GitHub Classrooms using VS Code in the browser. The only problem is the installation of Lean + the VS Code extensions required each time one creates a codespace.

Is the codespace set up you mention a way of automating the installation or does it do something in addition to that? I assume the GitPod stuff isn't necessary if I'm using GitHub Classroom Is that correct?

[Matthew Ballard]

For my current class, Codepsaces provides a consistent development environment for all the students. They should not have setup problems if they use Codespaces (but they are free to use their own machines still). GitPod serves the same role here.

[Eric Wieser]

You can definitely configure codespaces to preinstall everything, just like we already do for gitpod

[Kevin Buzzard]

How does one do this?

[Matthew Ballard]

Make a folder .devcontainer and put a Dockerfile and devcontainer.json. The mathlib Dockerfile should work but you will need to point the FROM to a standard Microsoft image like

ARG VARIANT="buster"
FROM mcr.microsoft.com/vscode/devcontainers/base:0-${VARIANT}

For a sample devcontainer.JSON and an overall good example for setup is the Lean 4 samples repo.

You can also see the my json file for another example

[Eric Wieser]

I think we should probably commit such a configuration to the mathlib repo, and possibly publish a codespace docker image alongside the existing gitpod one.

[Sebastian Ullrich]

Codespaces is now free for everyone for 120 "core hours" per month image.png
What's even more interesting: organizations can pay for usage by memebers and outside collaborators

[Gihan Marasingha]

Anyone having memory problems with running the Lean 3 server in vscode in GitHub Codespaces?

I've given my (~260) first-year students at the University of Exeter 4 summative assessments in Lean 3 using a variant of @Matthew Ballard's GH autograder. So far (with reference to @Kevin Buzzard's earlier comment on this stream), I haven't been fired!

For my next assessment, GitHub Codespaces falls over if the file contains even just import data.set.basic.

It looks like (according to htop) my codespace is using 1.23Gb of the available 3.84Gb even before starting lean in server mode. When the lean server starts, it slowly uses all available memory then crashes.

However, if I run Lean from the terminal, it runs fine. For example, running /usr/bin/time -v lean .test/test.lean shows that 'maximum resident set size' is only about 430Mb.

Any suggestions on how to address this issue?

[Gihan Marasingha]

Addendum: I say that lean in the terminal 'works fine', but it takes 149s to run the above in the GitHub codepsaces terminal as opposed to 0.17s on my computer.

[Alex J. Best]

Do you have the mathlib oleans downloaded to the workspace? E.g. with leanproject get-mathlib-cache in the project

[Gihan Marasingha]

No, I don't have the oleans and I don't have leanproject installed in my codepsace either. Thanks. I'll try this out.

[Gihan Marasingha]

Thanks @Alex J. Best - that worked. Now I just need to figure out how to install leanproject automatically for all my student codespaces.

[Martin Dvořák]

Regarding setting up Lean 4 for students, how would you compare https://lean.math.hhu.de/ with Codespaces?

[Eric Wieser]

codespaces / gitpod lets you work in multiple files and save your work

[Martin Dvořák]

Matthew Ballard said:

I put together a working Lean 4 Codespaces setup here.

Is it OK if I open your Codespaces and see the following?
image.png

[Eric Wieser]

did you open the gitpod or the codespace?

[Eric Wieser]

(the two are basically the same, but getting a gitpod message from codespaces is weird)

[Martin Dvořák]

Oh sorry! It is GitPod.

[Martin Dvořák]

Is https://github.com/UofSC-Fall-2022-Math-300-H01/homework0 a setup for both Codespaces and GitPod?

[Eric Wieser]

It looks like it, yes

[Eric Wieser]

Note that you get a free codespace quota for students in a class, which I don't think is the case for gitpod

[Martin Dvořák]

What counts as a class? Can it be an online course for high school students who compete in mathematical olympiads?

[Eric Wieser]

https://education.github.com/teachers

[Eric Wieser]

https://docs.github.com/en/education/manage-coursework-with-github-classroom/integrate-github-classroom-with-an-ide/using-github-codespaces-with-github-classroom

[Eric Wieser]

I ran my supervisor's assignment using it as a TA last year

[Martin Dvořák]

Matthew Ballard said:

I put together a working Lean 4 Codespaces setup here.

How can I open it as a Codespace, as opposed to GitPod?
Would I have to be registered as a student somewhere?

[Eric Wieser]

image.png

[Martin Dvořák]

Ah thanks! I can open it and it works for me!

How is it done that I didn't have to prove that I am a student, nor did @Matthew Ballard have to prove that I am enrolled in his course? Can anyone with GitHub account go there and have their Codespace? Can any number of people just join and play with it as if they were students?

[Sebastian Ullrich]

In that case you're using the free limit I posted about above available to anyone

[Sebastian Ullrich]

I suppose it's different if you use GitHub Classroom

[Martin Dvořák]

You mean a free limit of my GitHub account? Nothing to do with Matthew Ballard's course?

[Martin Dvořák]

Sebastian Ullrich said:

I suppose it's different if you use GitHub Classroom

I think I got it now! If I wanted to use the GitHub Classroom, I wouldn't be required to prove that I am a student; instead, @Matthew Ballard would have to approve my account, right?

[Matthew Ballard]

I think the free allocation is only for use for assignments with GH Classroom.

[Matthew Ballard]

Note: the system chokes pretty fast building Mathlib (in case you forgot lake exe cache get) so I suspect you will have a bad time with the GH Classroom free level also

[Martin Dvořák]

I am not sure I am on the same line.

I opened Codespaces via the link you posted (i.e., https://github.com/UofSC-Fall-2022-Math-300-H01/homework0 and then < > Code -> Codespaces). Was I in the GH Classroom?

[Martin Dvořák]

And if I open your repository in GitPod (using the button behind your link), do I use my free limit as well?

[Matthew Ballard]

You can check your codespaces in settings to see if it under your account

[Martin Dvořák]

I can access this page under my GitHub settings:
image.png

[Martin Dvořák]

It says something about Codespaces, but I don't see any personal limit, nor can I see anything named "GitHub Classroom".

[Martin Dvořák]

Do I understand it correctly that; students don't have to prove they are students; I have to be a verified teacher and add my students' GitHub accounts to a GitHub Classroom, so that they will have an access to the Codespace with an increased CPU limit?

[Eric Wieser]

That sounds right to me

[Eric Wieser]

Though when I got my students to sign up I encouraged them to verify their student status anyway for their own benefit

[Martin Dvořák]

My students will come from many different high schools, so it would be probably too difficult to verify their student status.

[Eric Wieser]

I would recommend just verifying your teacher status and making a dummy student account to see how it behaves

[Martin Dvořák]

OK! I hope our legal department will allow me to use GitHub in the first place...

[Eric Wieser]

If you're not using it with students do they care?

[Eric Wieser]

That is, if you verify in order to evaluate the offering

[Eric Wieser]

Obviously you should wait for their approval before actually using it in an official capacity

[Martin Dvořák]

However, if 60 hours per month is enough for every single student, they don't need to have a student account and I don't need to have a teacher account either, right?

[Eric Wieser]

Sure, but you might find classroom useful, and you're likely going to need legal approval anyway to ask the students to sign up for github if your university already asked for approval

[Martin Dvořák]

I attempted to setup Codespaces in my repository:
https://github.com/madvorak/lean-mam

Sometimes it works. Sometimes I get errors like
image.png
and
image.png
and then it works again.

Do you know how to avoid those errors?

[Martin Dvořák]

PS: The problem seems to have resolved itself with switching to a different base image.

[Flo (Florent Schaffhauser)]

Gihan Marasingha said:

Thanks Alex J. Best - that worked. Now I just need to figure out how to install leanproject automatically for all my student codespaces.

Hi @Gihan Marasingha . Sorry to bother you directly, but I am having the exact same string of problems you encountered here and I was wondering if you or somebody else could tell me:

1. How to install leanproject in Codespaces.
2. How to make sure that it is then installed automatically for the students.

Please note that I am still using Lean 3 in my course this semester. Thank you!

[Flo (Florent Schaffhauser)]

Alex J. Best said:

Do you have the mathlib oleans downloaded to the workspace? E.g. with leanproject get-mathlib-cache in the project

To be clear, I don't know how to run this in Codespaces. Should it work automatically? Is leanproject supposed to be there already?

[Flo (Florent Schaffhauser)]

OK, I installed leanproject via pip3 install mathlibtools, but I am still missing leanpkg.

[Errno 2] No such file or directory: 'leanpkg'

[Scott Morrison]

Which installation instructions are you trying to follow?

[Flo (Florent Schaffhauser)]

https://leanprover-community.github.io/lean3/install/windows.html

[Flo (Florent Schaffhauser)]

And it seems that the following sequence works on Codespaces as well:

1. curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
2. pip3 install mathlibtools
3. leanproject new

Edit Actually, I could not reproduce that. After installing mathlibtools, I get the same error as before:

[Errno 2] No such file or directory: 'leanpkg'

So now it's down to the issue of making this config load automatically with Codespaces when my students use it :thinking:

[Matthew Ballard]

Does copying the docker file and devcontainer.json from the Mathlib repo not “just work”?

[Flo (Florent Schaffhauser)]

Hmm, I could not make it work. But then again, I seem to be doing something wrong even setting up Lean 3 inside Codespaces.

[Sebastian Ullrich]

If you search for Codespaces on this Zulip, you can find (presumably) working setups such as this one by @Floris van Doorn: https://github.com/fpvandoorn/LogicColloquiumTutorial/tree/master/.devcontainer. Which in particular sets up the mathlib4 cache, but I just remembered you're using Lean 3...

[Sebastian Ullrich]

Note the ENV PATH setting in the Dockerfile that should ensure that leanpkg exists as a command

[Flo (Florent Schaffhauser)]

Thanks! Indeed I would have to adapt it for Lean 3, but I wonder if it is really worth it at this stage, given that the semester is over in three weeks :sweat_smile:

It's frustrating, though, that I am not able to give the students easy access to the Lean files! The good thing is that it has made most of them want to install Lean on their own machines :-) The others just use CoCalc.

Anyway, thanks everyone! The final word for today is: I can setup Lean 3 in a Codespace, but only for me and only for as long as that particular Codespace is active.

The setup I used was the following sequence of command lines (which works provided that my base repo contains a leanpkg.toml file).

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
source $HOME/.elan/env
pip3 install mathlibtools
source ~/.profile
leanproject new

Then install the Lean 3 extension in VS Code and go to a Lean file to check that it works.

I leave this here in case someone else is trying to make the same thing work :smiling_face: At first I thought it would be possible to tell Codespaces to create an image of that configuration (once it is all set up), so that it would load automatically every time after that, but I could not figure out if this is indeed doable.

[Sebastian Ullrich]

Prior art for Lean 3 is also easily found on GitHub: https://github.com/search?q=mathlibtools%20path%3A.devcontainer&type=code

[Flo (Florent Schaffhauser)]

Thank you for the link! I suppose that my problem is more basic: I don't know how to create such .devcontainer files and make them work :flushed:

[Gihan Marasingha]

@Flo (Florent Schaffhauser) Sorry I didn't see this message at the time: unfortunately I had a family emergency to deal with.
Have you sorted out your issue? If not, I'm happy to help.

[Flo (Florent Schaffhauser)]

Hi @Gihan Marasingha :wave: Thanks for getting back to me! I could never make it work properly and it was already late in the semester, so I did not insist :sweat_smile: I think I am limited by my understanding of how Codespaces work and how to set one up.

Next time, I will want to implement a Codespace for my students, though! And I will do it using Lean 4, so perhaps I can use more directly the various setups that have been mentioned in this thread (thanks to everyone for their help :pray:).

May I ask: are you still using Codespaces in your course? Do you recommend it as a tool to have students use Lean?

[Gihan Marasingha]

Yes, I am still using Codespaces, particularly for assessment. The principal advantage is that it's a 'no installation' approach. Roughly the way it works is that you create a GitHub template repository that contains either a devcontainer.json or Dockerfile (or both). These files instruct Codespaces how to create a 'docker container' (something like a virtual machine) from a base docker 'image'.

The following works for me:
Create a .devcontainer directory in the root of your repository. Create a devcontainer.json file in this directory containing the following text:

{
    "name": "Debian",
    "image": "mcr.microsoft.com/devcontainers/base:debian",
    "onCreateCommand": ".devcontainer/setup.sh",
    "customizations": {
        "vscode": {
            "extensions": [
                "leanprover.lean4"              // Lean 4 extension
            ]
        }
    },
    "remoteUser": "vscode",
    "remoteEnv": {
        "PATH" : "${containerEnv:PATH}:/home/vscode/.elan/bin:/home/vscode/.local/bin"
    }
}

This refers to another file setup.sh where I put the actual setup code. You could instead put the code directly into the onCreateCommand above instead. Here's my setup.sh file:

#!/usr/bin/env bash
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \
  | sh -s -- --default-toolchain none  -y # Install the elan Lean version manager
export PATH=$PATH:~/.elan/bin
lake exe cache get!

[Flo (Florent Schaffhauser)]

Thanks! This helps a lot, because I do not know how to create this files myself, and whenever I try to setup my own Codespaces environment and save it to a file like this, I run into trouble (it takes up a lot of memory space, or it simply does not work).

I will try it out soon, to make sure it also works for me. Thanks again!

[Flo (Florent Schaffhauser)]

Yes, the no installation part is an advantage, as not all students find it interesting to install Lean without trying it out first.

I wonder what you mean by assessment :thinking: Do you have an automatised grading procedure?

[Heather Macbeth]

@Flo (Florent Schaffhauser) Indeed, various people have set up automatic grading procedures. You can see
https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for-teaching/topic/Automatic.20grading.20of.20lean4.20codes
for a recent discussion.

[Flo (Florent Schaffhauser)]

Thanks, Heather! So far I have managed to avoid this because the number of students has been 20+ and actually they were asking for more personal attention and guidance, but once I get to the point of teaching massive courses using Lean, it will be very helpful to be able to use this :blush: