Images for ocaml 4.09 have disappeared

[LasseBlaauwbroek]

I was using the *-ocaml-4.09-flambda series of images, but they seem to have disappeared. Is this intentional or unintentional? I guess I can upgrade to 4.10 but I would rather use the lowest-supported ocaml compiler of my plugin (this is actually 4 08, but those images have never been available, which is okay to me).

Should I upgrade, or can the 4.09 series be restored?

[tchajed]

I was also surprised when this happened. The wiki (https://github.com/coq-community/docker-coq/wiki) explains the policy for which versions to use, and basically 4.09 was dropped in favor of supporting the last two OCaml versions 4.10 and 4.11 (but there are still older versions of OCaml; check the wiki for the full policy and list of versions).

I'm not developing or using plugins so it was a straightforward choice for me to just bump OCaml all the way to 4.11 so I wouldn't have to worry about this for a while.

If you could make your plugin compatible with OCaml 4.07 then you could test on that. You could also perhaps just create the switch for 4.09 in the script; it would be slow but then you could test on whatever version you wanted.

[LasseBlaauwbroek]

Ah, I was not up-to-date with the policies here... Thanks for the info, I'll upgrade to 4.10.

Sorry for the noise. Closing.

[Zimmi48]

Hey, don't worry. I didn't answer yet because I was expecting @erikmd would write a more thorough answer but basically the change in policy should have been announced as soon as it happened but it didn't get announced yet because of some related discussion regarding coq-native in Docker images that is still not fully settled.

The policy changes can still be discussed if you want.

[LasseBlaauwbroek]

Not having the right version is not a huge problem for me. I cannot downgrade to 4.07 because I've got large pieces of code that use the monadic syntax introduced in 4.08 (and I'm not willing to remove that, the syntax is too nice).
Testing on the lowest supported OCaml version is useful because it allows you to verify that the version ranges in your opam files are correct. However, I wasn't really doing that anyway because only 4.09 was available. In order to really support that properly, you would have to provide the full matrix of compiler versions between OCaml 4.05-4.12 and Coq. I can imagine that would be too expensive. (And like @tchajed says, I can always compile OCaml myself during CI.)

One reasonable compromise could be to support the full matrix of OCaml versions for non-development Coq versions. Since those only have to be built once, that is pretty cheap. And at least for me, it would get me 90% of the way, because my plugin not only supports Coq dev but also older Coq versions.

[Zimmi48]

One reasonable compromise could be to support the full matrix of OCaml versions for non-development Coq versions. Since those only have to be built once, that is pretty cheap. And at least for me, it would get me 90% of the way, because my plugin not only supports Coq dev but also older Coq versions.

That does sound like a reasonable compromise indeed. However, most Coq plugins are developed on a model where there's one branch tracking each branch or released version of Coq, so it's not clear how many plugin developers would really benefit from this.

[erikmd]

Hi @LasseBlaauwbroek, thanks for opening this issue.
I wasn't able to reply earlier, so thanks @tchajed for having directed Lasse to the wiki! and @Zimmi48 for your comments.

So the change mentioned in this issue was intended, it was the result of the discussion in issue #12 and has been documented in the wiki but we wasn't able to widely announce that change (which basically consisted in switching from 3 available ocaml versions to 4 ocaml versions for each release of coq, including the two most recent ocaml versions, each in a "single-switch image").

This delay was indeed due to the tricky discussion that resulted from the packaging of the coq-native package in docker-coq.
However, I hope that we'll be able to do this announce later this week.

On the one hand as mentioned by @Zimmi48, as this policy has not yet been announced, it may be discussed further!
but on the other hand, I'd be wary to directly commit to support all the supported ocaml versions from 4.05.0 to the latest version of ocaml if applicable, for all the coq stable releases… notably as we currently have 45 images in docker-coq, which are intended to be compatible with a whole rebuild from a single GitLab CI pipeline, in particular you said:

Since those only have to be built once, that is pretty cheap.

but regularly, we happen to rebuild some images (or even all images) to take into account upstream changes, typically for instance, when a new version of Debian or opam is released.

To sum up I agree that the following point, documented in the wiki:

"Docker-Coq thus tracks the last two compatible versions of OCaml for each Coq version, so the ante-penultimate compatible OCaml won't be available anymore if a new OCaml is released and compatible with this Coq version."

is a limitation as a plugin developer if one can't test the plugin's minimal-supported version of OCaml. But to overcome this, the solution to support "the full matrix" does not look that cheap…

[LasseBlaauwbroek]

@Zimmi48 : However, most Coq plugins are developed on a model where there's one branch tracking each branch or released version of Coq

Perhaps my phrasing was not clear, this is what I do as well. But given that the code in these branches overlap 99%, it would be quite okay to only test OCaml versions on the non-dev-coq-version branches of the plugin, and just assume that it will also work on the dev branches.

@erikmd : but regularly, we happen to rebuild some images (or even all images) to take into account upstream changes, typically for instance, when a new version of Debian or opam is released.

Regarding the notion of cost: Does "cost" mean that someone is actually paying for this service and does not want to rack up a huge bill, or is it more in an abstract sense that we don't want to be too frivolous in wasting compute cycles? In the first case, I fully understand and I'm already quite happy that this service exists :-) In the second case, I also fully understand, but at some point, it might be interesting to check how many plugins are building their own versions of OCaml on every CI cycle. If there are many, it might still end up cheaper to do it centrally.

But again, this is by no means a deal breaker for me, and I'm quite happy to be using docker-coq at all 👍

[Zimmi48]

It's the latter. And you are right that this kind of things would deserve to be assessed better (but it's also difficult to do).