Docker for mathcomp 1.8.0

[CohenCyril]

@erikmd I do not know how to produce stable mathcomp 1.8.0 + coq-* images. I created the branches but then dockerhub does not refresh. I compiled one image at home (tag mathcomp/mathcomp:1.8.0-coq-8.7) but I am not sure I did the right thing. Could you explain what to do?

[erikmd]

Hi @CohenCyril, the workflow I have used to prepare the coqorg/org & mathcomp/mathcomp:1.7.0-* stable images has three steps:

1. Create Git branches locally with the proper version as you did. (This can be automated, see below.)
2. Open Docker Hub's build settings to explicitly add the name of the branches to be built. The URL is https://cloud.docker.com/u/erikmd/repository/docker/mathcomp/mathcomp/builds/edit but (1) the link between Docker Hub and GitHub is specific to one user token, so I believe you won't be able to see the list of branches constituting the configuration… and (2) there is a bug with the current version of the Docker Hub web interface, which prevents me from modifying that build configuration... so I will report this bug which seems related to docker/hub-feedback#1776.
3. Push all Git branches to the docker-mathcomp repo, but not simultaneously, ideally with a sleep 2s between each branch. (This can also be automated, see below.)
   This last step triggers the automated build of the Docker images, so no need to build them locally.

Steps 1. and 3. have been fully automated (I have written a dedicated tool to this aim, so no need to do git checkout -b ... etc. by hand, cf. https://github.com/erikmd/docker-hub-helper#examples)

But the step 2 is currently blocking for us…

[erikmd]

@CohenCyril, I reported this in the GitHub issue docker/hub-feedback#1789

[erikmd]

Hi @CohenCyril, I've seen you have workarounded the issue regarding https://hub.docker.com/r/mathcomp/mathcomp by directly pushing images for mathcomp/mathcomp:1.8.0-* :+1:

But it will anyway be useful to setup the automated build rules so the images are automatically rebuild for upcoming updates of the stable images (on the OS / opam / docker-coq side)

As suggested in docker/hub-feedback#1789, one needs to configure the link between the mathcomp Docker Hub namespace and the math-comp GitHub organization, and to do so it is advised to use a "service user", see the screenshot below:

I'll have to do this at the same time for coqorg and mathcomp namespaces.

To this aim, I can use the Github service user @proofbot I had created some time ago (for migrating issues in ProofGeneral at that time), hopefully this will work for both Docker Hub namespaces... If not (according to the screenshot above), let's say we could use @proofbot for the communication between https://github.com/coq-community and coqorg, and we could create another Github service user for the communication between https://github.com/math-comp/docker-mathcomp and mathcomp.

Agenda

• [x] To sum up, @Zimmi48, I would like to add @proofbot as a collaborator of the repos https://github.com/coq-community/docker-base and https://github.com/coq-community/docker-coq (…that permission should be enough IINM, i.e. no need to give the service user owner permissions to the entire coq-community organization). OK for you?

• [x] Then I'll reconfigure the Docker Hub coqorg namespace to anticipate the configuration for the upcoming coqorg/coq:8.10-beta1 image.

• [x] Finally I'll do the same with the mathcomp namespace if it is possible to reuse @proofbot (otherwise we'll know we need another service user that e.g. @CohenCyril could create).

Cc @ejgallego FYI

[Zimmi48]

OK for me. If you only need proofbot as a collaborator, then you don't need any action from my part.

[erikmd]

Thanks @Zimmi48, I've started looking at this, indeed I was able to add proofbot as collaborator for the three repos I had mentioned. However Docker Hub still requires an approval from the owners to be able to configure automated builds. More precisely, I've clicked on the two Request buttons in the screenshot below and @CohenCyril and you will probably receive an automatic e-mail notification.

[CohenCyril]

@erikmd granted!

[erikmd]

Hi,

The three quick steps I had mentioned in my previous comment are now done; to sum up it appears it is unneeded to create yet another service user: Docker Hub autobuilds rules can now be added again, via to the service user proofbot that has minimal permissions in the coq-community and math-comp GitHub organizations.

I've updated the autobuild rules for mathcomp/mathcomp:1.8.0-* so further commits in the proper branches will trigger a recompilation of the image.

Also @CohenCyril, the issue I had mentioned earlier seems resolved, so you should now be able to display the list of autobuild rules in the shared URL: https://cloud.docker.com/u/mathcomp/repository/docker/mathcomp/mathcomp/builds/edit This list has to be updated at each release of a stable version of math-comp (this is the only step that can't be automated (but there is a related, open issue at docker/hub-feedback#1783)). − Anyway, I plan to document these steps in the issue you opened recently (math-comp/math-comp#327), after I've finished upgrading the coqorg images with the latest opam 2.0.4… and addressing the two PRs math-comp/math-comp#306 and math-comp/math-comp#307

For now, I guess this issue #2 can be closed if I am not missing anything.

Best, Erik

[CohenCyril]

Thank you so much @erikmd!