Karl Palmskog (Jun 12 2020 at 10:54): Karl Palmskog (Jun 12 2020 at 10:54):@Erik Martin-Dorel it seems to me that there isn't a whole lot that restricts docker-base to Coq. Do you see any obvious reasons why one couldn't or shouldn't use docker-base to build other Dockerfiles that need access to the OCaml ecosystem? The most obvious one is HOL Light, but also HOL4 has several tools key tools like Ott and Lem that are in OCaml/OPAM.
Karl Palmskog (Jun 12 2020 at 10:58):the most obvious Coq tie-ins I see are: (1) coq user on the system, and (2) adding the released Coq opam repo, but that's pretty much it, right?
Théo Zimmermann (Jun 12 2020 at 11:32):Docker base is really thought specifically for the use case of Coq CI, in particular with respect to the set of chosen versions.
Théo Zimmermann (Jun 12 2020 at 11:32):Using it for other systems would create more maintenance demand.
Théo Zimmermann (Jun 12 2020 at 11:33):Given that the Dockerfile is very simple, it should be easy to fork it to create something that is suited for another OCaml-based project.
Karl Palmskog (Jun 12 2020 at 11:34):yes, I'm not asking it for it to be accommodated/changed, just what the current ties to Coq are
Théo Zimmermann (Jun 12 2020 at 11:36):Choice of version is one.
Théo Zimmermann (Jun 12 2020 at 11:36):Note that there also exist the ocaml/opam2 images that may be generally useful: https://github.com/ocaml/infrastructure/wiki/Containers
Théo Zimmermann (Jun 12 2020 at 11:36):but it has the inconvenience of being heavier because each image includes many switches
Karl Palmskog (Jun 12 2020 at 11:37):Théo Zimmermann said:
Choice of version is one.
but as per above, there is no Coq version choice in docker-base, no?
Théo Zimmermann (Jun 12 2020 at 11:39):No Coq version choice indeed, I meant the choice of OCaml versions is strongly dependent on the needs of Coq
Erik Martin-Dorel (Jun 19 2020 at 22:14):@Karl Palmskog yes, beyond the two specificities you mention, I confirm what said @Théo Zimmermann, one of the main reasons for not using the ocaml/opam2 images was indeed their large size due to the many switches provided (while coqorg/base:latest has only two switches… and I precisly plan to further switch to single-switches images in a couple of days :)
Last updated: Apr 19 2024 at 13:02 UTC