Opening batteries fork in gitpod

Stream: batteries

[Shreyas Srinivas]

Currently it is trival to open mathlib or a fork of it in gitpod. There is a link in the README.md file. Is there a way to do the same for forks of batteries?

[Yaël Dillies]

https://gitpod.io/#https://github.com/leanprover-community/batteries

[Shreyas Srinivas]

Well that's the two step way. I am looking for a gitpod link in PRs and README

[Yaël Dillies]

I guess that depends on what "trivial" means, but the gitpod.io/# trick (if that's really a trick, arguably it's one of the most prominent features of Gitpod) applies to literally all repos, so I don't really see how that doesn't fit the bill.

[Yaël Dillies]

Note that the Gitpod badge in the README is simply an hyperlink to what I wrote above

[Shreyas Srinivas]

I imagine teaching is much simpler if there is a single repository that students can spin gitpod instances from.

[Shreyas Srinivas]

and for demos too

[Yaël Dillies]

Don't students know how to click a link?

[Shreyas Srinivas]

sure. I am just suggesting we put one in the batteries README.md

[Shreyas Srinivas]

One thing about that link is, it isn't adaptive. If I fork a repo X as fork_X, and if X has a gitpod link. then the gitpod link of fork_X will set up X. If one opens the fork by handcrafting the the link, one automatically gets two git remotes setup.

[Eric Wieser]

Install the gitpod chrome extension, to get that link everywhere?

[Shreyas Srinivas]

firefox user here

[Eric Wieser]

s/chrome/your browser of choice/

[Shreyas Srinivas]

that's neat. thanks.

[Shreyas Srinivas]

maybe this is slightly off topic. But I have another project (math dependent) for which I want to set up gitpod that work as out of the box as it does for mathlib. I understand that I need some Dockerfiles and a gitpod.yml file. Could some tell me exactly how to do this?

[Yaël Dillies]

You just need .gitpod.yml. This file will do

[Yaël Dillies]

It points to a dockerfile, and that dockerfile is the one provided by mathlib, so you don't even have to worry about maintaining the dockerfile yourself

[Shreyas Srinivas]

ooh this is even better than I thought. Thanks :)

[Eric Wieser]

Yaël Dillies said:

It points to a dockerfile, and that dockerfile is the one provided by mathlib

I have no idea where this docker image comes from

[Eric Wieser]

Unless @Kim Morrison knows better, I don't think anything updates that image any more

[Shreyas Srinivas]

I just tested it on my project repo and so far it works.

[Shreyas Srinivas]

My repo was on toolchain 4.10.0

[Yaël Dillies]

Eric Wieser said:

Yaël Dillies said:

It points to a dockerfile, and that dockerfile is the one provided by mathlib

I have no idea where this docker image comes from

Actually, me neither. And I haven't managed to get gitpod to update it

[Kim Morrison]

No, nothing is updating that docker image at present.

[Yaël Dillies]

Could it be updated? Every time I open gitpod, I must update elan from 1.4.3 to 3.1.1

[Kim Morrison]

What happens if you just modify the Dockerfile? e.g. add some whitespace if nothing else? As far as I'm aware gitpod is not pulling images from anywhere, and just building itself.

[Yaël Dillies]

Already modified the dockerfile in less trivial ways and it still opens with elan 1.4.3

[Shreyas Srinivas]

I think the docker file that is fetched is from docker hub?

[Yaël Dillies]

Sorry, no, I meant I modified .gitpop.yml

[Yaël Dillies]

The dockerfile I don't have access to, because as Shreyas says it's hosted on dockerhub

[Shreyas Srinivas]

In any case, updates to the dockerfile have to be propagated to docker hub somehow.

[Shreyas Srinivas]

Otherwise they don't have any effect

[Kim Morrison]

That's not how it used to work on gitpod... They were building their own images direct from the the Dockerfile in the repository.

[Shreyas Srinivas]

I can double check what's happening per these instructions: https://www.gitpod.io/docs/references/gitpod-yml#image

But apparently GitHub is down

[Kim Morrison]

But it does seem to be what happens now.

[Kim Morrison]

At least someone pulled the image from docker hub 16 hours ago.

[Shreyas Srinivas]

I did

[Shreyas Srinivas]

16 hours ago sounds about right

[Kim Morrison]

Oh, so that is no evidence that gitpod is pulling from it.

[Shreyas Srinivas]

No I did it from gitpod

[Kim Morrison]

The image at docker hub contains mathlib3 from 2 years ago.

[Shreyas Srinivas]

I mean I opened gitpod

[Kim Morrison]

I doubt this is what is affecting Yael?

[Shreyas Srinivas]

What Yael says also happens to me. Elan self update is the first instruction that runs after the image is ready

[Kim Morrison]

https://hub.docker.com/layers/leanprovercommunity/mathlib/gitpod/images/sha256-2a9254b40ef9b316d6d429335137095953e060f7c0a927005f92203d09e5dc65?context=repo

[Kim Morrison]

is all that exists at docker hub.

[Shreyas Srinivas]

My bad. The image is specified in .gitpod.yml as .docker/gitpod/Dockerfile. That's the local file

[Kim Morrison]

@Yaël Dillies, in the setup you usually use, can you distinguish between the Dockerfile in the mathlib repo (e.g. which installs nvim) and the Dockerfiler that was pushed to docker hub 2 years ago (e.g. which doesn't).

I'm very skeptical that docker hub has anything to do with this.

[Kim Morrison]

Has anyone tried https://www.gitpod.io/docs/configure/workspaces/workspace-image#manually-rebuild-a-workspace-image

[Shreyas Srinivas]

Dockerhub has nothing to do with it. I am sorry.

[Shreyas Srinivas]

The docker file in mathlib is installing elan as follows:

install elan
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh

[Shreyas Srinivas]

Is this correct?

[Shreyas Srinivas]

I misread that image spec line which is why I thought it was picking the image from dockerhub. Sincere apologies. The file that is being used is the one in mathlib4 repo which is installing elan as described above.

[Kim Morrison]

Shreyas Srinivas said:

The docker file in mathlib is installing elan as follows:

install elan
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh

No, it's not?

[Kim Morrison]

https://github.com/leanprover-community/mathlib4/blob/master/.docker/gitpod/Dockerfile#L23

[Shreyas Srinivas]

I truncated the copy since I am on my phone

[Shreyas Srinivas]

But it's the same line.

[Shreyas Srinivas]

@Kim Morrison : the following is my .gitpod.yml : https://github.com/Shreyas4991/DGAlgorithms/blob/main/.gitpod.yml

[Shreyas Srinivas]

I copied it from the LeanAPAP one that Yael linked to in this chat

[Shreyas Srinivas]

Fwiw, it worked after the elan update. I think the mathlib gitpod.yml is different. Whence all the above confusion about hub and installation practices

[Shreyas Srinivas]

I assumed these files must have come from mathlib

[Shreyas Srinivas]

Until a minute ago

[Shreyas Srinivas]

It seems both @Yaël Dillies and I are using a .gitpod.yml file that fetches the mathlib3 docker image from docker hub. How it works with mathlib4 projects perfectly is a mystery to me.

[Kim Morrison]

elan just works

[Shreyas Srinivas]

Kim Morrison said:

https://hub.docker.com/layers/leanprovercommunity/mathlib/gitpod/images/sha256-2a9254b40ef9b316d6d429335137095953e060f7c0a927005f92203d09e5dc65?context=repo

This one to be precise

[Kim Morrison]

Okay, now I understand!

[Kim Morrison]

Because Mathlib wasn't using that image, I assumed no one else was.

[Kim Morrison]

Ideally, we would have no dependency on docker hub, and no ongoing maintenance job to update images there.

[Kim Morrison]

Can you solve this problem simply by copying the Dockerfile from Mathlib into your repo (@Yaël Dillies too)?

[Kim Morrison]

I'd prefer to pursue that first.

[Shreyas Srinivas]

I sorta assumed that because my mathlib4 based project worked perfectly fine, Yael must be using the same file as mathlib, and I think they were under the same assumption

[Kim Morrison]

(Ideally, we can delete the images on docker hub, but I guess at this point it's hard to be sure no one is relying on them :sad: )

[Shreyas Srinivas]

Taking a look at that docker file, I think it can be standardised with no updates required. Only the parts downloading mathlib3tools needs to be deleted

[Shreyas Srinivas]

as along as elan _just works_ which is almost always, we don't need to rely on the parts of the docker file after the elan based toolchain install.

[Shreyas Srinivas]

In the mathlib4 file the mathlib3 parts are not there and instead a neovim install is offered (but I guess that's for a general container, not needed for gitpod). The remaining parts of the file can stay unchanged.

[Shreyas Srinivas]

No updates needed

[Shreyas Srinivas]

@Kim Morrison : I tried remotely linking to the mathlib4 Dockerfile. This fails. Maintaining my own copy means tracking changes to the Dockerfile in the main mathlib4 repository. Is this the only viable way. Ideally we should be able to link to a standard image that mathlib4 specifies.

[Shreyas Srinivas]

Screenshot-from-2024-08-15-02-24-48.png

This is what I get when trying to link directly to the mathlib4 docker file

[Shreyas Srinivas]

Also, I am not sure how the "maintain our own copy of the dockerfile" approach scales. If there are substantial changes to setup, then I suspect anybody who uses gitpod will start facing issues.

[Eric Wieser]

I think "maintain a standard docker image" is something we should start doing at the point where the setup becomes complicated, not at the point where we start theorizing about how it might in future become complicated

[Yakov Pechersky]

Would it make sense to host docker images on ghcr, since we're so GitHub based?

[Yaël Dillies]

Kim Morrison said:

Can you solve this problem simply by copying the Dockerfile from Mathlib into your repo (Yaël Dillies too)?

Oh sure, but I thought it was preferred for everyone to use the same image by pulling it from dockerhub, as then that's less maintenance work: If the dockerfile needs updating, some mathlib maintainer updates it and all people downstream immediately see the changes

[Shreyas Srinivas]

It is complicated for all downstream users as soon as people have to maintain their own image.

[Shreyas Srinivas]

Docker images are not easy to debug unless someone knows docker and understands these files. So essentially projects which would like to use gitpod would need one docker expert to make keep pace with changes.

[Kim Morrison]

Okay, I persuaded that if someone is willing to take on this job, it would be a good idea to update regularly at docker hub.

[Shreyas Srinivas]

Happy to volunteer

[Kim Morrison]

It requires credentials for the account, so I would prefer to find a maintainer or (official) reviewer to take this.

[Yaël Dillies]

I am willing to do it, as I use it in at least 5 different projects

[Kim Morrison]

Great. Docker Hub credentials incoming via DM!

[Yaël Dillies]

Just so that we agree, we do not want to continue the docker image associated to the mathlib repo, but instead want a new one associated to the mathlib4 repo?

[Shreyas Srinivas]

yes. A similar one for batteries alone would be nice.

[Shreyas Srinivas]

for the moment I suspect you will find it easy to use the gitpod dockerfile of mathlib minus the nvim parts.

[Yaël Dillies]

Something I'm not very clear about is why there is a notion of repositories at all in dockerhub, as opposed to, you know, just containers

[Shreyas Srinivas]

Docker has a notion of images created by repositories. Because sometimes you need many images. Containers are running instances of images.

[Yakov Pechersky]

My comment about GHCR was to make it simpler with regards to credentials and linking images with code repositories.

[Yakov Pechersky]

Where we could have a GitHub workflow that builds and pushes an image on every master push or what have you. The workflow would look quite similar to the same one that would push to Dockerhub, other than how the credentials are passed

[Shreyas Srinivas]

In this case, it needs to be tested with gitpod.yml config. I don't see any obvious way to specify third party sources

[Yakov Pechersky]

image: ghcr.io/leanprover-community/mathlib4 in gitpod.yml

[Yakov Pechersky]

https://www.gitpod.io/docs/configure/workspaces/workspace-image#configuring-a-workspace-image

[Eric Wieser]

One warning about using an un-versioned community image: downstream projects with a Dockerfile are currently pinned to a set of install requirements, but this isn't the case if your dockerfile says ghcr.io/leanprover-community/mathlib4

[Eric Wieser]

This means if polyrith ever is rewritten to not use python, then your old repos on old mathlib versions pointing to the image will find themselves unable to use polyrith because you'll get the new image for old code.

[Yaël Dillies]

Does that apply to dockerhub also?

[Eric Wieser]

Yes, this applies to publishing any image anywhere without versioning it

[Yaël Dillies]

I guess my question is: "Does either of GHCR or DockerHub let you publish versioned images?"

[Eric Wieser]

I think all such registries do, but we never used the feature before

[Shreyas Srinivas]

Yes, but like git, each version has a different hash. You need to make sure that the gitpod tag matches the latest

[Yakov Pechersky]

Yes, of course one can publish tagged images. I would imagine we always publish a latest, and also publish a tag matching a lean version release on version bumps

[Yakov Pechersky]

Without a tag specified, docker pulls the image with the "latest" tag

[Shreyas Srinivas]

As it exists the image doesn't come with a toolchain. Elan is installed without a toolchain. Then when the project is opened, lake does the honours.

[Shreyas Srinivas]

Keeps things simple

[Eric Wieser]

Sure, but you still need to decide which python packages to install in the container, which elan doesn't manage

[Eric Wieser]

If your container is literally just elan then managing a docker image seems like too much overhead

[Yakov Pechersky]

While it doesn't come with a toolchain, the image tagged with some lean release is really from a mathlib4 commit where the lakefile points to that particular lean release.

[Shreyas Srinivas]

Yes and that's what lake uses to do the honours

[Shreyas Srinivas]

It doesn't affect the building of the image per se. Just what's loaded into the project folder and guides lake

[Shreyas Srinivas]

I think it installs some toolchain but doesn't pick a default to be more precise. But that's semantics

[Shreyas Srinivas]

Anyway that's a moot point. The question is whether the docker image should do what elan and lake can manage as long as a standard Linux + FS is provided