[wish] Support for building Docker images from Github action

[ejgallego]

Dear docker-coq-action devs,

would it make sense to update this action so users could deploy their own custom images resulting from the build of the opam package?

I was under the impression that this was an active subject, but I couldn't find the right issue / thread.

My use case is to generate a docker image with coq-lsp pre-build from coq-lsp CI so other people can pull it easily in AI clusters.

It could be very well that my request is outside the scope of this action, if that's the case please close.

[erikmd]

Hi @ejgallego, thanks for opening this thread.

would it make sense to update this action so users could deploy their own custom images resulting from the build of the opam package?

docker-coq-action can be viewed as an enhanced GitHub-Actions façade of the docker run command. Not docker build.
Still, what you suggest is technically feasible (using the docker commit command).

I was under the impression that this was an active subject, but I couldn't find the right issue / thread.

Nope: I guess you are the first dev to explicitly speak about this use case :)

Also AFAICT, docker-coq-action existed before GitHub includes it own Container Registry - which could be precisely to the point for hosting the generated image.

It could be very well that my request is outside the scope of this action, if that's the case please close.

No I think it's relevant!
Still, I can't tell about an ETA for this one, given the other feature request about "multiple-step support" has high-priority.

[ejgallego]

Thanks for the information @erikmd !

Still, what you suggest is technically feasible (using the docker commit command).

Interesting, I'll look into that command.

No I think it's relevant!

Indeed it is! On the other hand I was wondering if we shouldn't have two actions?

I am not expert on Docker, so I was assuming that the usual workflow for example for me to generate a coq-lsp Docker image my users can depend on would be to:

• provide a Dockerfile that starts from the right CoqOrg image
• use the github docker build action

So indeed, the above set of actions seems quite orthogonal to what the docker-coq-action does, because basically docker-coq-build be basically the github docker build action + a pre_script that generates the right Dockerfile.

On the other hand, we could use docker commit, which could indeed re-use the CI run.

Still, I can't tell about an ETA for this one, given the other feature request about "multiple-step support" has high-priority.

Indeed! Note that we now have sub-issues on github, so if there is some common issue we could reflect that. I'm happy to put some time to contribute to the action, once I understand the desired technical design.