Stream: coq-community devs & users

Topic: Coq dependencies in docker-base


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jun 12 2020 at 11:32):

Using it for other systems would create more maintenance demand.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jun 12 2020 at 11:36):

Choice of version is one.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jun 12 2020 at 11:36):

but it has the inconvenience of being heavier because each image includes many switches

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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: Feb 04 2023 at 02:03 UTC