Integrate Dockerfile (or similar) into this repository?

[fingolfin]

Right now, we have Dockerfiles in various separate repositories, e.g. https://github.com/gap-system/gap-docker/blob/master/Dockerfile

But we could also have one (or multiple) in this repository. That would be quite natural in some sense. I am not completely sure about the relative merits, but I think we should at least review the options.

[wilfwilson]

I think it would be a great idea to have all of the Dockerfiles in one repository (and combined into a small handful of files). This makes it much easier to raise issues on the Docker containers, and it reduces code duplication. It also increases the visibility of all of the containers (since they will be located, and documented, in the same place). Multiple similar repositories are annoying to deal with, anyway.

But which repository should that be? For now, I think gap-system/containers is fine for it; see gap-system/containers#1.

With my current understanding of Docker containers, the only advantage that I see for hosting it in this repository is that it would be really easy to rebuild a container when there is, e.g., a push to a master or stable branch. But it is not even clear that that is something that we even want to do; building the containers for these branches once per day would probably be sufficient.

On the other hand, it might be somehow 'cleaner' to have the Docker files, and their issues and pull requests, in a separate repository.

In any case, the focus should be on developing gap-system/containers; once it is mature, it would be very little effort to merge it into this repository, if that is what we decided to do.