Support https://hub.docker.com/u/mathcomp and custom images

[erikmd]

Recap of a discussion with @Zimmi48:

• Add a key mathcomp_version that will pick the appropriate image (with OCaml 4.07.1+flambda)
• Add a key custom_image that overwrites the chosen Docker image (and thereby ignore all other keys coq_version, ocaml_version, mathcomp_version)

[Zimmi48]

I expected that custom_image would do the job of supporting the math-comp images, and that it would precisely be the example that would be documented.

[erikmd]

Hi @Zimmi48, indeed that would be a simpler solution and I'd also be fine with it.

I was just thinking about the following advantage of specifying an intermediate configuration (i.e., no custom_image set but a mathcomp_version value set):

it will be easier to specify that a given development depends on coq_version ∈ {8.11, dev} and mathcomp_version ∈ {1.10.0, dev} rather than writing:

custom_image ∈ {
mathcomp/mathcomp:1.10.0-coq-8.11,
mathcomp/mathcomp:1.10.0-coq-dev,
mathcomp/mathcomp-dev:coq-8.11,
mathcomp/mathcomp-dev:coq-dev}

WDYT?

[erikmd]

I was thinking of this extra layer also because I believe @ejgallego had suggested once in the ssreflect mailing list to simplify the syntax of the mathcomp images (: vs. -) to be able to do more easily a "build matrix" specification...

Anyway, if you think this is not really necessary, we'll be able to implement this extra "layer" of mathcomp_version later on just as well if we want, to keep the code of the action simpler for now.

[Zimmi48]

I'm fine with both solutions. But what to give was an example if not Math-Comp?

[erikmd]

I'm fine with both solutions. But what to give as an example if not Math-Comp?

Indeed...

on the one hand, the "build matrix" feature is convenient to test the "product" of several configurations in a concise way;

but on the other hand, sometimes we wouldn't want to take "the exact product" of all coq / mathcomp versions (e.g. two different mathcomp versions don't necessarily support the same coq versions, and we may also want to remove some configurations by hand to have a more lightweight CI), and finally changing the ocaml_version in this context will be a no-op as math-comp images will ultimately have only one switch, cf. https://github.com/coq-community/docker-coq/issues/4#issue-588093947

so all in all, even if both solutions are interesting, let's stick to the mere custom_image solution for the time being, with mathcomp as a documentation example ((and if later on we get some feature request for a mathcomp_version property, we'll be able to reconsider this choice anyway))