Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] Docker images of coq-mathcomp-character

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Docker images of coq-mathcomp-character


Chronological Thread 
  • From: Erik Martin-Dorel <>
  • To: , , Cyril Cohen <>
  • Subject: Re: [ssreflect] Docker images of coq-mathcomp-character
  • Date: Fri, 8 Feb 2019 19:40:28 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Pass ; spf=None
  • Ironport-phdr: 9a23:7aBKRBXddhhzc9u56/hyMHTQHcPV8LGtZVwlr6E/grcLSJyIuqrYbRCOt8tkgFKBZ4jH8fUM07OQ7/iwHzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9xIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlDkIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94VQnZPUMZPWiBYG4+xcpEAAPcdMOlFqYnzu0cBrQWjCgWyGejjzj9FimLz0aA8zu8vExzJ3BY4EtwAsHrassj7OqQcUe+60KbH0DrNYPFY1jrm9IjFcQosre2QUb9qc8fcz1QkGQPfjlWXrIzoJzyb1v4Ms2iY8uFuUvigi3Q7qwFwpDij38kiio7Tho0LzlDP6CJ0z5gvJd25S053e9ukH4FKtyGGNot2RNouTHxvuCYg1LIGvYW2fCkQyJQm2x7TcfKHc5KR7x/lSe2fLzB4hHd/d7K+gRa/6VWvyurgWcm3zllKtDBJncXLtnAIzxDT5cmHSud9/ke8wjmDzRzc6uZBIUwslKrbMZ8hwqIqmpodq0TOGDL9lkbujKKOa0kp9fWk5/76brn7ppKQLZF4hw7kPqgwnMG0HP42PRIUX2eB/OSxzL3j8lP9QLVNlvA2iazZsIzCJcgGvKK5AhVV0oc/6xqlATemyswUnXgBLF1bZBKKl5XlNl7TLPziEPuznlShnC11y/3JJLHtHI3BLn3Zn7fgebZ95VRcyA02zd1H+Z1UELABIPHpVk/0rtPYFAM5Mw2yw+r+Fdp90ZkeVnyLAqKCMaPSq16I5v41L+mCfo8ZoCz9JOQ95/7ykX85nkcQfbKy3ZsNdn+4EPBmLFuFbnrwmdoBCmcLvg8mTOPwklGCUDhTZ2yzX60m/D07BpimXs//QdW2m6aM0iO2FYF+Y3tcT1GKC3bhMYSCQfYFLiyIZodkmyAEXr+kU8ot2A+GtQngyrMhIPCQsgYJr5PnnPNy5+DV3UU55CZ1C4KW1GGASUl1mHkJTnk4xvYsj1Z6zwKuy6l7y9lRD8BS4bZlVR03MdaIwvZ7CJb3Uxjdf9HMRFG8T9GOACswUpQ/2YldMA5GB9y+g0WbjGKRCLgPmunOWM1to/DsmkPpLsM48E7okawojl0oWMxKZD+nnK9jsQbJVdeQzxep0p2yfKFZ5xbjsX+ZxDvcvVtZTEh+S/edBC1NVg7ttd38o3j6YfquBLAga1YT0sueMvIMa8fokRNIXqW7NQ==
Dear Emilio, [sorry for late reply]

Le vendredi 8 février 2019 à 10:52 +0100, Emilio Jesus Gallego Arias a écrit :
> Porting some travis scripts I was wondering about the naming scheme:
>
> > * mathcomp/mathcomp:1.7.0-coq-8.9 (opam switches: 4.05.0,
> > 4.07.0+flambda)
>
> vs
>
> > * mathcomp/mathcomp-dev:coq-8.6 (opam switch: 4.02.3)
>
> so indeed wouldn't it be more convenient this to be named:
>
> mathcomp/mathcomp:dev-coq-8.6 ?
>
> The thing is that I'd like to have a matrix with
>
> COQ_VERSION=xxx
> MATHCOMP_VERSION=yyy
>
> and use a substitution such as
> "mathcomp/mathcomp:$MATHCOMP_VERSION-coq-$COQ_VERSION"

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/

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?

Kind regards,

Erik

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


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

Archive powered by MHonArc 2.6.18.

Top of Page