Outdated docker image

Stream: lean4

[Yaël Dillies]

Annoyingly, the update to elan 3.1.0 is transitive on gitpod, so I get asked whether I want to update elan every time I open a workspace

[Eric Wieser]

I think that means a docker image needs rebuilding / invalidating

[Yaël Dillies]

I agree, but I don't know which one, where, nor how

[Yaël Dillies]

I've been poking around for an hour but I literally cannot even figure where the docker image is stored :frowning:

[Eric Wieser]

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

[Eric Wieser]

Based on https://stackoverflow.com/a/72971216/102441, the error is that we used RUN and not ADD there

[Eric Wieser]

The former caches the url, the latter caches the result pointed to by the url

[Eric Wieser]

Or alternatively, we should hard-code a version, to avoid rebuilding an image for every elan update

[Eric Wieser]

I guess the release cadence is low enough for it to not matter

[Eric Wieser]

The easiest option is to add some no-op command to the docker file before the elan installation, to cause a one-off cache invalidation

[Yaël Dillies]

Eric Wieser said:

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

That's not the image. That's the dockerfile.

[Yaël Dillies]

Sky answered my question: Apparently the image is hidden in some gitpod server and there's a way to ask for a regeneration, which I'm going to try now

[Eric Wieser]

I think we would do better to change the dockerfile to bust their (and anyone else's) cache

[Yaël Dillies]

Yaël Dillies said:

there's a way to ask for a regeneration, which I'm going to try now

It did regenerate the image but I ended up with elan 3.0.0 again :frowning: Are we pinning the version of elan somehow?

[Yaël Dillies]

I just found https://hub.docker.com/r/leanprovercommunity/mathlib... which hasn't been updated in a year and is Lean 3?

[Yaël Dillies]

Original problem fixed in #13439

[Sky Wilshaw]

I think it's inadvisable to update the Docker image, as then it'll need to be rebuilt after every elan update. Since elan self-updates really fast (<1s), I just added a step to gitpod.yml to do the update on workspace initialisation.

[Sky Wilshaw]

(At least for gitpod's Dockerfile - if anyone's using the Dockerfile for other things maybe it's worth changing.)