Ssreflect Users Discussion List

[Erik Martin-Dorel <>]

Hi Emilio,

Le samedi 9 février 2019 à 18:03 +0100, Emilio Jesus Gallego Arias a écrit :
> Dear Erik,
> 
> Thank you very much for your prompt answer!
> 
> Erik Martin-Dorel 
> <>
>  writes:
> > Your use case seems very sensible.
> >
> > Technically speaking, this was not possible at the time the Docker Hub
> > organization https://hub.docker.com/u/mathcomp/ was created, because
> > stable releases of math-comp (in mathcomp/mathcomp) are built using
> > the automated build feature of Docker Hub, which has always been
> > incompatible with the "docker push" command (currently used from
> > GitLab CI to mathcomp/mathcomp-dev).
> >
> > Still, since 2018-12-13 [1] and according to the main documentation
> > page of automated builds [2], it seems that this separation in two
> > different repos is not needed anymore (but I have not tested it yet).
> >
> > [1] https://blog.docker.com/2018/12/the-new-docker-hub/
> > [2] https://docs.docker.com/docker-hub/builds/
> 
> Thanks a lot for the detailed explanation, after writing the mail indeed
> I realized that the split would have indeed been due to some technical
> restriction.
> 
> > Emilio, if you think one such refactoring of the current Docker Hub
> > repos is worth it in terms of naming convention, I could do the
> > following:
> >
> > * Update the GitLab CI protected variables and open a PR in
> >   https://github.com/math-comp/math-comp to push master builds to
> >   mathcomp/mathcomp:dev-coq-* instead of mathcomp/mathcomp-dev:coq-*
> >
> > If this is successful after this PR has been merged:
> >
> > * Remove the https://hub.docker.com/r/mathcomp/mathcomp-dev repo
> > * Update the https://hub.docker.com/r/mathcomp/mathcomp documentation,
> >   before doing another announce.
> >
> > What do you think?
> 
> I'd be great to have this slightly more uniform naming, and the plan
> looks good.
> 
> On the hand the current scheme is not so bad to work with [just need a
> bit of ugly vars],

OK :)

> so I'd say I am not sure I'd be worth the effort.

Beyond the naming convention, it seems to me that keeping stable and
development images of MathComp apart brings maybe a bit more clarity,
given that both kinds of images don't have the same build chain
(Docker Hub automated build vs. GitLab CI), and don't have the same
number of opam switches (2 vs. 1)…

But I am willing to do the refactoring if there is a consensus that
it's better to have a single repo with a uniform naming convention…
To sum up:

(Choice 1) => currently implemented:

- mathcomp/mathcomp:1.7.0-coq-8.9
- mathcomp/mathcomp-dev:coq-8.9

(Choice 2) => requiring a non-trivial refactoring:

- mathcomp/mathcomp:1.7.0-coq-8.9
- mathcomp/mathcomp:dev-coq-8.9

Do the math-comp devs have an opinion on this choice? Cyril?

Kind regards,

Erik

-- 
Érik Martin-Dorel, PhD
Maître de Conférences, Lab. IRIT, Univ. Toulouse 3


https://www.irit.fr/~Erik.Martin-Dorel