The docker hub images are not updated

Stream: lean4

[Chiung-Yi Tseng]

I've posted this to leanprover/lean4 on github: https://github.com/leanprover/lean4/issues/6996 but was advised to reach out to the community. Paste here:

The images in the docker hub is outdated. https://hub.docker.com/u/leanprovercommunity
Although the hub is hosted by leanprovercommunity, but the official lean4 repository is here.

Can we create a new official leanprover identity in docker hub and main the images? I will help many users to install and use lean4 quickly and let developers be able to switch between different versions of lean4 easily. Users can easily add more tools and build their images on top of lean4 easily.

I could help on this. I already hosted my own docker image release pipeline and build images nightly. https://github.com/ctseng777/docker-lean4/tree/main

Mainly, I want to run lean-gym and various projects on top of lean4 in a cleaner and flexible way. Building/installing several lean4 from scratch locally isn't fun.

[Kim Morrison]

@Yaël Dillies, I know you were interested in this. Do you know what the status is? Can we add some CI that keeps these updated, so humans don't have to?

[Yaël Dillies]

The status is that you should ping me every time we need to update the images. I don't know anything about automating with dockerhub

[Chiung-Yi Tseng]

@Yaël Dillies I've built my own docker pipeline which builds nightly images.
https://github.com/ctseng777/docker-lean4/tree/main
You may refer to it, or I could help.

[Yaël Dillies]

We already have scripts/docker_build.sh and scripts/docker_push.sh that automate most of the work. Sadly, it's hard for me to run these scripts because I am not Unix-proficient :sweat:

[Kim Morrison]

@Chiung-Yi Tseng, if we could run the scripts @Yaël Dillies refers to regularly, would this solve your use case? If not, are you able to PR additions to those scripts that would?

[Chiung-Yi Tseng]

The challenge is, even with the script, someone needs to run it. We need to have some ci workflow to fully automate the work.
In fact, @leodemoura has a repo:lean4-nightly for it, but the repo has nothing.

[Kim Morrison]

No, you're misunderstanding the purpose of the lean4-nightly repo.

[Kim Morrison]

Yes, we can run a script every day/week/month as appropriate, and I can populate the credentials appropriately. The missing work is someone writing and testing and documenting a script, not running it.

[Chiung-Yi Tseng]

Ah, see. I'd like to help writing/testing/documenting the script.
@Yaël Dillies I can't find scripts/docker_build.sh and scripts/docker_push.sh. Which repo are they located? Can you share the links?

[Yaël Dillies]

They are both in the mathlib4 repo: https://github.com/leanprover-community/mathlib4/tree/master/scripts

[Yaël Dillies]

Okay, @Sky Wilshaw and I tracked down scripts/docker_build.sh not working to the addition of the following two lines in the dockerfile:

RUN curl -s -L https://github.com/neovim/neovim/releases/download/stable/nvim-linux64.tar.gz | tar xzf - && sudo mv nvim-linux64 /opt/nvim
ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:/opt/nvim/bin:${PATH}"

[Yaël Dillies]

They come from #9024, which @Julian Berman authored.

[Yaël Dillies]

Is there any way to achieve the same result without hardcoding the download link, which in this case seems to no longer be valid?

[Julian Berman]

https://github.com/leanprover-community/mathlib4/pull/21653

It looks like neovim now builds separately for x86-64 and arm64 on Linux. So I've just mirrored that assuming we also may want multi-arch builds (e.g. if someone bundles a toolchain into an image). (If that's not the case then in theory we could just hardcode something there rather than using TARGETARCH). But this seems to work here.

Jammy's version is ancient, so another way to get the same result would be updating the base image, presumably newer ubuntu has newer neovim (though not sure if newest ubuntu is even up to date honestly).

[Yaël Dillies]

Ah yes, I am happy to update the base image

[Julian Berman]

It looks like even oracular is still old https://packages.ubuntu.com/oracular/neovim (0.9, which is like 2 years or so, and not supported upstream). So probably still this way is reasonable at least as far as nvim is concerned.