gitpod or similar

Stream: lean4

[Kevin Buzzard]

With my Lean 3 projects for students now, I'm typically including a description in the README of how you can play along using gitpod and avoid having to install lean 3 and mathlib, because the simplest way to get mathlib3 oleans is via the command line, which is too much for my delicate mathematician audience (and involves having to install python).

Is there a way of doing a gitpod thing for lean 4 projects with mathlib as a dependency?

[Matthew Ballard]

I've had it set up for my class since the beginning of the semester but people almost universally use codespaces. Let me check if it works still.

[Kevin Buzzard]

This project doesn't depend on mathlib though, right?

[Matthew Ballard]

I use mathlib in it. But gitpod is not working atm

[Kevin Buzzard]

Where's the bit in your README which says "do make this work in codespaces, do X Y and Z"?

[Kevin Buzzard]

This is the one which is more complicated than gitpod because I have to do more than just commit some yaml file into the repo, right?

[Matthew Ballard]

You have to create a folder and then commit a json file

[Matthew Ballard]

Codespaces is only really an option if you are teaching through GitHub classroom where you get a reasonable free allotment.

[Matthew Ballard]

I am sure others are currently enjoying a working repo with GitPod and Mathlib4

[Adam Topaz]

@Kevin Buzzard we just recently set up codespaces on mathlib4. You could very easily copy that into some lean4 project to set it up

[Kevin Buzzard]

I am giving two one-off lectures to undergraduates, I just want to say to them "here's the repo, if you want to play along click here".

Are we yet at the point where I can say "install VS Code, install the Lean 4 extension, clone the repo, open the repo folder in VS Code, click "yes" five times and you have a fully working set-up with lean downloaded and all mathlib oleans"? That's what I really want, I guess.

[Kevin Buzzard]

With gitpod and lean 3 / mathlib 3 I can do "if you have an account on github then click here on this gitpod link, wait 2 minutes, and you're all set with everything running in your browser". This is what I want to emulate. I absolutely want to avoid the command line.

[Adam Topaz]

Let me make a video showing how this works with codespces.

[Matthew Ballard]

Click here

[Kevin Buzzard]

Thanks. I got to a VS Code with no Lean 4 extension. I've installed the Lean 4 extension, clicked "yes" twice (once to install Lean and once to restart Lean), and now I'm in orange bar hell.

[Adam Topaz]

you need to do this in a repo that has the right files.

[Matthew Ballard]

Uh oh. On my class notes repo?

[Adam Topaz]

it's the .devcontainer folder from the mathlib4 repo

[Matthew Ballard]

That I tested and it seems to be ok still.

[Kevin Buzzard]

No, in the repo which I'm working on.

[Matthew Ballard]

If you want Gitpod, try copying https://github.com/leanprover-community/mathlib4/blob/master/.docker/gitpod/Dockerfile into a .docker/gitpod folder on your repo and then add mathlib4 gitpod.yml to root. It should work the same

[Adam Topaz]

Kevin if your project depends on mathlib4 then you should be able to copy/paste the .devcontainer folder from mathlib4 into the root of your repo, and after that, clicking the "+" in the screenshot that Matt posted should open up a fresh vscode with lean4 installed + oleans

[Kevin Buzzard]

Yeah, I can confirm that this works :D Thanks both! So codespaces is up and running.

[Matthew Ballard]

I am not sure how accessible sin charges codespaces is currently

[Matthew Ballard]

I use it for my class since GitHub classroom comes with a free allotment.

[Kevin Buzzard]

Is it likely that a randomer will be able to use codespaces for 1 hour for free?

[Adam Topaz]

I think the default container should stay within the free tier. If you need more power, you can customize the json file, but we just set it up as the default.

[Matthew Ballard]

Is there a free tier?

[Adam Topaz]

with 2 cores (the default) it seems like you get 60 hours free per month

[Matej Penciak]

I actually just set up a Gitpod for a presentation I gave in @Heather Macbeth 's class (by basically just copying her template): https://github.com/mpenciak/FordhamSp2023
I'm not 100% sure it works, but I'd be interested in feedback if it works for other people

[Kevin Buzzard]

I see to be using it for free right now, and I'm not in orange bar hell any more

[Adam Topaz]

https://github.com/features/codespaces see pricing section after scrolling down a bit

[Matthew Ballard]

Great! That is a more robust free tier than I remember

[Matej Penciak]

Matej Penciak said:

I actually just set up a Gitpod for a presentation I gave in Heather Macbeth 's class (by basically just copying her template): https://github.com/mpenciak/FordhamSp2023
I'm not 100% sure it works, but I'd be interested in feedback if it works for other people

I think the only infrastructure needed to get it to work is the .gitpod.yml file, and the .docker/gitpod/Dockerfile file.

[Adam Topaz]

Yeah gitpod works great as well, but I think the fact that codespaces is build in to github has some benefits.

[Matthew Ballard]

Matej Penciak said:

I actually just set up a Gitpod for a presentation I gave in Heather Macbeth 's class (by basically just copying her template): https://github.com/mpenciak/FordhamSp2023
I'm not 100% sure it works, but I'd be interested in feedback if it works for other people

Testing it out

[Matthew Ballard]

It looks like it only had to build and link the Yatima files. Nice!

[Matthew Ballard]

Codespaces requires one less system to make an account in and integrates right into the GitHub flow but it seems underpowered relative to GitPod.

[Matthew Ballard]

Is this Standard: up to 4 cores, up to 8GB RAM, 30GB storage used on the free tier for GitPod?

[Kevin Buzzard]

Gitpod looks like it works on the Yatima file. Thanks.

One thing I don't understand: how come my mathlib3 github repos which support gitpod have a .gitpod.yml file but this lean 4 repo has a .docker/gitpod/Dockerfile file?

[Adam Topaz]

https://github.com/leanprover-community/mathlib4/blob/f85368f49bea5a60679f40625f31177479d7f732/.gitpod.yml#L2

[Adam Topaz]

it's just a choice

[Kevin Buzzard]

Wait what? Matt's gitpod setup has a notes/gitpod.yml file?

[Kevin Buzzard]

Aah, got it. Thanks Adam! Hopefully I now have all the info I need.

[Matthew Ballard]

I think yours point to that same image https://github.com/ImperialCollegeLondon/formalising-mathematics-2022/blob/af5f176b3b881b7bc0ae89b55befe48c9d4ab790/.gitpod.yml#L1

[Kevin Buzzard]

We still need command line for a local installation of a project which depends on mathlib4, right?

[Matthew Ballard]

Kevin Buzzard said:

Wait what? Matt's gitpod setup has a notes/gitpod.yml file?

Matt's repo should not be trusted for GitPod use :)

[Adam Topaz]

Kevin Buzzard said:

We still need command line for a local installation of a project which depends on mathlib4, right?

yeah I think you will need to run lake exe cache get at some point

[Matthew Ballard]

I also haven't seen any solution that avoids dropping into a terminal

[Matthew Ballard]

Can you avoid it with mathlib3?

[Adam Topaz]

not as far as I know.

[Matthew Ballard]

I am guessing Kevin wants the extension to do all the heavy lifting?

[Adam Topaz]

Oh, I think we do have some package for lean/mathlib3 that includes vscode/lean3/mathlib3/oleans in one bundle.

[Patrick Massot]

With Lean 3 and gitpod it was definitely possible to avoid dropping into a terminal.

[Kevin Buzzard]

Oh yeah I don't really want to do that because downloading 1.7 gigs kind of stinks. Also I think lean 4 oleans might be platform-dependent.

[Patrick Massot]

With https://github.com/PatrickMassot/MDD154/blob/master/.gitpod.yml gitpod was fetching olean on its own

[Adam Topaz]

Patrick Massot said:

With Lean 3 and gitpod it was definitely possible to avoid dropping into a terminal.

The same is true with lean4 (with either gitpod or codespaces). But I think Kevin wants something locally.

[Kevin Buzzard]

Yeah, with both gitpod and codespaces it looks like it's just a one-click install (or maybe few-click) for a repo depending on mathlib, thanks to the great work of the community here and the helpful answers above. But for a local installation with a repo depending on mathlib you still need a command line as far as I can see. It looks to me like this is now a job the lean 4 extension could do, because the only missing step is lake exe cache get. Is it worth opening an issue for this? I worry about these web-based solutions for longer-term courses such as the one I teach Jan-Mar to final year students; I fear that somehow something will time out and they'll lose all their work.

[Kevin Buzzard]

This year I had someone with several variants of python installed on their system who had problems getting leanproject working, and I had someone with one of these new macs having some nightmare, although the vast majority of the students had no problem, so I feel like the huge effort that people went into to making those instructions as idiot-proof as possible did really pay off.

[Matthew Ballard]

Do vs code extensions for other languages have this functionality?

[Adam Topaz]

Not sure. But the extension for lean4 can already download elan, so getting the oleans seems quite natural

[Ruben Van de Velde]

I guess most other programming languages are marketed at programmers :)

[Matthew Ballard]

From my memory, Go does.

[Matthew Ballard]

I think it makes sense to make the ask.

[Kevin Buzzard]

I summarised both what I had to do to make codespaces and gitpod work, and also what a user has to do to use them, in the README here: https://github.com/kbuzzard/IISc-experiments/blob/main/README.md

[Kevin Buzzard]

If anyone can be bothered to test them and let me know if it doesn't work, that would be great. I think it would also be nice to add some times in (e.g. "click here, wait about 2.5 minutes, and then you should be ready") but I didn't time these and actually I should probably worry about the lecture I'm giving in 11 hours' time (8 or so of which I intend to spend sleeping)

[Adam Topaz]

@Kevin Buzzard you may want to use the up-to-date version of the devcontainer stuff, that can be found here: https://github.com/leanprover-community/mathlib4/tree/master/.devcontainer

The "feature" that the older variant you're using is based on is unmaintained (I should probably just delete that repo)

[Adam Topaz]

you need both the .json file and the dockerfile

[Kevin Buzzard]

@Adam Topaz does it look OK now?

[Matthew Ballard]

GitPod works smoothly for me. Codespaces has a hiccup but I think Adam has diagnosed it

[Adam Topaz]

Kevin Buzzard said:

Adam Topaz does it look OK now?

Yup! I think that should work.

[Matthew Ballard]

Yeah, I can see cache firing now in the log

[Adam Topaz]

right. The old version did run the cache getter, but only after the container was created, so you had to wait a little while for it to work. This new version does it as part of the container creation.

[Matthew Ballard]

I think the folder structure changed from last time because import IIScExperiments.GroupTheorySolutions doesn't exist now

[Matthew Ballard]

Fixing that, it looks like the cache is there and things load quickly

[Matthew Ballard]

I think there some way you can auto-hide the terminal on startup if you are interested

[Adam Topaz]

oh yeah! What's the config option for that?

[Adam Topaz]

I would also vote for getting rid of the minimap + installing vim bindings by default, but those might be too opinionated :)

[Matthew Ballard]

https://marketplace.visualstudio.com/items?itemName=sirmspencer.vscode-autohide looks like an extension

[Kevin Buzzard]

Removing minimap by default would be wonderful. Does installing vim bindings break anything, or does it just add stuff?

[Matthew Ballard]

I am not sure there is much of an audience in the intersection of "I love vim bindings" and "I have never seen a terminal"

[Matthew Ballard]

It will default to using vim bindings to edit