Ssreflect Users Discussion List

[Emilio Jesús Gallego Arias <>]

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], so I'd say I am not sure I'd be worth the effort.

Best regards,
E.