Dockerhub

Stream: general

[Yaël Dillies]

Continuing from #batteries > Opening batteries fork in gitpod, I have now updated the leanprovercommunity/lean and leanprovercommunity/mathlib Docker images using the Dockerfiles from #15936 (thanks @Sky Wilshaw!).

[Yaël Dillies]

cc @Kim Morrison, @Shreyas Srinivas, @Eric Wieser

[Yaël Dillies]

It's probably not the end of the story, but it's a good start. I have self-proclaimed myself "image maintainer", by which I mean "Come annoy me with your image issues!".

[Eric Wieser]

I think it might still be a better idea to manage these via ghcr.io, since that way we don't have to keep track of dockerhub credentials

[Eric Wieser]

Yaël Dillies said:

I have now updated the leanprovercommunity/lean and leanprovercommunity/mathlib Docker images

I fear this will have broken any lean3 projects that were referring to the previous image without referencing a version. It would be better to create new 4 images I think, and rollback to the old versions of these.

[Eric Wieser]

Yeah, I can confirm that if I open one of my old lean3 repos in gitpod, leanproject is no longer installed.

[Eric Wieser]

So please can you put these images back to the ones generated from the mathlib3 repo, and choose new names (either mathlib4, or using ghcr) for the lean4 ones; while no one should be writing new lean3 code, that's no reason to break old archived code referenced by papers etc.

[Shreyas Srinivas]

I agree with Eric. Changing the image under a given name and tag breaks compatibility for existing work making it harder to reproduce the results of old projects. New lean4 and mathlib4 images would be better.

[Sky Wilshaw]

In general, it might be a good idea to version-tag the docker images we produce, e.g. leanprovercommunity/mathlib4:2024-08-19, for increased reproducibility. Dockerhub/ghcr don't have maximum tag limits, right?

[Shreyas Srinivas]

Don't know about tag limits. I think this was already discussed further up. The main point is existing images shouldn't be altered.

[Shreyas Srinivas]

A latest or gitpod or devcontainer tag would be a nice addition since those containers don't need a vscode install

[Eric Wieser]

Who is the target audience for latest?

[Sky Wilshaw]

Projects in active development, I presume? I used it on the Con(NF) project a while ago (until the port to Lean 4)

[Sky Wilshaw]

For CI, I mean

[Sky Wilshaw]

It's significantly easier to set up a docker container that you can test locally than to try to understand the arcane workings of GitHub Actions

[Shreyas Srinivas]

I think the CI we use would already be containerized

[Eric Wieser]

I think my claim is that even for that use-case a versioned image would be better

[Shreyas Srinivas]

I suspect there would be limits for how many images can be stored

[Shreyas Srinivas]

Images can easily reach a gigabyte

[Sky Wilshaw]

I should clarify that the images I've been working on with Yaël do not contain a version of mathlib, but (at least for now) I ask elan to download the latest stable lean just so that there's something there to use - so there aren't too many possible versions

[Sky Wilshaw]

This means that latest would work for any project that can be compiled with current lake

[Shreyas Srinivas]

that's more or less what the current image does

[Sky Wilshaw]

Yeah - the Lean 3 image for leanprovercommunity/mathlib also had a leanproject get call in it though, which I thought was the cause for concern about versioning

[Shreyas Srinivas]

that line can be safely removed for mathlib4 images

[Eric Wieser]

Sky Wilshaw said:

This means that latest would work for any project that can be compiled with current lake

Ah, but using latest is also saying "my project will continue to work with all futures versions of lake".

[Sky Wilshaw]

I instead interpret it as "my project is intended to follow current development of lake and I will regularly run lake update"

[Eric Wieser]

(probably this matters more for blueprint dependencies, indeed the lean-only dependencies are unlikely to have versioning issues)

[Sky Wilshaw]

When you freeze a project you would also fix that version

[Shreyas Srinivas]

you need the latest image to open actively maintained repositories like mathlib4 or dependents

[Eric Wieser]

I think a lot of projects are frozen by being abandoned

[Sky Wilshaw]

Yeah, that's true

[Sky Wilshaw]

The lean and mathlib images we've been working on will very very rarely need an update, only something that changes something fundamental in elan or adds a new binary will need people to update; conversely, the gitpod container (with leanblueprint etc) is liable to lots of updates

[Sky Wilshaw]

(This is all to say that I agree with the points above about reverting the original images, by the way! I'm just saying that we need a better solution than just making a single Lean 4 image.)

[Yaël Dillies]

Btw, by "reverting the original images" you actually mean "rerun the dockerfiles in the mathlib3 repo and push them to dockerhub, right?

[Shreyas Srinivas]

https://github.com/features/packages

[Eric Wieser]

Yaël Dillies said:

Btw, by "reverting the original images" you actually mean "rerun the dockerfiles in the mathlib3 repo and push them to dockerhub, right?

Yes, exactly

[Shreyas Srinivas]

Yaël Dillies said:

Btw, by "reverting the original images" you actually mean "rerun the dockerfiles in the mathlib3 repo and push them to dockerhub, right?

for that repo/name/tag.

[Yaël Dillies]

I'm asking because, importantly, if I do that the images will end up with elan 3.1.1 and not elan 1.4.3 as the original images did

[Yaël Dillies]

(I think that's an improvement)

[Sky Wilshaw]

And probably a newer leanproject

[Shreyas Srinivas]

Doesn't docker hub let you revert your change?

[Eric Wieser]

It's certainly better than having the lean4 image there!

[Shreyas Srinivas]

The answer is no apparently: https://stackoverflow.com/questions/55475080/how-can-i-revert-my-last-push-on-hub-docker-com

[Sky Wilshaw]

Shreyas Srinivas said:

Doesn't docker hub let you revert your change?

I don't think it does. I think that tags on Docker Hub are "supposed" to be immutable.

[Shreyas Srinivas]

The second answer in that link suggests a way to recover the old image

[Shreyas Srinivas]

the tag is just for human readability. there is an underlying digest for each image.

[Sky Wilshaw]

The Advanced Image Management feature was removed in 2023, apparently. https://github.com/docker/roadmap/issues/534

[Shreyas Srinivas]

okay. Strange decision on their part.

[Shreyas Srinivas]

@Yaël Dillies it is possible that you locally have the old image.

[Shreyas Srinivas]

docker image ls

[Shreyas Srinivas]

You can also look as the history of an image with a name and tag: https://docs.docker.com/reference/cli/docker/image/history/

[Shreyas Srinivas]

You might be able to locally revert the image to the previous digest by tagging it. It took me a short while but I found a gist that does this: https://gist.github.com/jclosure/b2bcf0686739ad6b79df

[Yaël Dillies]

I mean is it really that terrible if the lean3 and mathlib3 images have an updated elan/leanproject?

[Shreyas Srinivas]

Intuition suggests it shouldn't matter. But it is hard to predict in advance that nothing important is broken by these changes. There are all sorts of bureaucratic artefact reproducibility rules that require artefacts to be preserved for a decade or so.

[Shreyas Srinivas]

Honestly I expect the probability that something is affected to be smaller than almost any positive epsilon we can pick, and we do live in the "real" world, but as long as we have the option to not break things, I see no reason to break them. Then again, who benefits from up to date lean3 images?

[Eric Wieser]

I think it's probably ok for them to end up with updated elan / leanproject

[Yuri]

Yaël Dillies said:

It's probably not the end of the story, but it's a good start. I have self-proclaimed myself "image maintainer", by which I mean "Come annoy me with your image issues!".

@Yaël Dillies, let me know if you need to share the load. I am happy to help. I am no expert but worked for a few years with it.

[Yaël Dillies]

I am afraid

Kim Morrison said:

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

means I shouldn't share the load, at least for the "pushing images to Dockerhub" part

[Shreyas Srinivas]

I think we can work out a system where the community has a repository for maintaining the docker images and you push images to docker hub. Others make PRs through forks or non-main branches.

[Shreyas Srinivas]

There should be a CI setup for testing images before pushing them to registries anyway.

[Yaël Dillies]

We're not far off: The repository is mathlib4 and people can already open PRs to modify the dockerfiles (eg #15936). We just don't have the images themselves and CI to test them

[Sky Wilshaw]

Shreyas Srinivas said:

I think we can work out a system where the community has a repository for maintaining the docker images and you push images to docker hub. Others make PRs through forks or non-main branches.

There's really very little to maintain. The Dockerfiles are very small.

[Shreyas Srinivas]

Yes that I know. There just needs to be a proper CI that tests an image (by maybe doing the following: running the image with mathlib, building mathlib, testing mathlib, deleting the container etc.)

[Yuri]

Yes, in general maintenance is mostly upkeep with new versions, security updates, etc.

[Sky Wilshaw]

Yuri de Wit said:

Yes, in general maintenance is mostly upkeep with new versions, security updates, etc.

My point is that this isn't even done on the side of the Docker image. The image only contains a version of elan, not even lean or mathlib. The only dependency that will be frequently updated is leanblueprint.

[Sky Wilshaw]

(And that of course should have CI and testing!)

[Sky Wilshaw]

As far as I'm concerned, the main priority for now is to republish (versions of) the old images, and to get the new images up so that people can use them. I think that more complicated CI can wait until we're more frequently publishing images and don't want to manually test them.

[Shreyas Srinivas]

yes please. This is probably important to get right before someone finds that they are not able to open their old lean3 project.

[Yaël Dillies]

I have now pushed new Lean 3 images to leanprovercommunity/lean and leanprovercommunity/mathlib, and new Lean 4 images to leanprovercommunity/lean4, leanprovercommunity/gitpod4, leanprovercommunity/gitpod4-blueprint

[Shreyas Srinivas]

are the lean4 images with or withuot mathlib?

[Shreyas Srinivas]

Do we have a blueprint-free mathlib-containing gitpod image?

[Eric Wieser]

What would "with mathlib" mean?

[Eric Wieser]

Maybe "with the dependencies needed by polyrith"?

[Shreyas Srinivas]

I mean there is pure lean3 image and a lean3 image with mathlib. Similarly there could be a pure lean4 image, a lean4 image with batteries, and a lean4 image with mathlib

[Shreyas Srinivas]

Appropriately initialising the project folder. The update/build/fetch cache step can safely be run from the gitpod config file

[Shreyas Srinivas]

@Yaël Dillies : it fails with the error "leanproject not found". I'll revert flypitch to the docker image from the file for now. Ref: #general > Can't run lean 3 project