Janno (Jul 04 2023 at 10:52): Janno (Jul 04 2023 at 10:52):Is there any documentation on how to deal with OS-level (i.e. not opam-installable) dependencies for projects tracked by Coq CI? IIUC it is recommended to use https://hub.docker.com/r/coqorg/coq (through the github coq community action, for example) in CI for coq projects. These seem to be based on debian 11 ("bullseye", or "oldstable" at this point). Coq itself uses a ubuntu bionic beaver image (a release from 2018). This doesn't seem to be a problem with most user projects tracked in Coq CI because their dependencies can be installed via opam. But I am not sure how to deal with the discrepancy in a project that I am preparing for inclusion in Coq CI that requires specific (and not entirely outdated) OS-level dependencies (i.e. nothing opam can provide). I am already struggling to get them installed in the coqorg/coq images and it is going to be an even bigger pain in Coq's own CI docker image.
Paolo Giarrusso (Jul 04 2023 at 10:53):opam _can_ do sth about OS-level packages — see all the conf-* stuff and opam-depext
Janno (Jul 04 2023 at 10:53):The image that Coq CI uses isn't available on hub.docker.com, is it? How would I go about including it in my own project without copying the contents? If I could depend on it directly I could at least save some amount of work by figuring out how to install dependencies only once instead of twice
Janno (Jul 04 2023 at 10:54):conf-* packages are not enough for https://github.com/bedrocksystems/BRiCk (despite what the dune-project file says)
Pierre Roux (Jul 04 2023 at 10:56):I guess you have to edit that file: https://github.com/coq/coq/blob/master/dev/ci/docker/bionic_coq/Dockerfile
Théo Zimmermann (Jul 04 2023 at 10:57):FWIW @Janno, the Docker images for Coq's CI will be updated soon to newer Ubuntu versions: https://github.com/coq/coq/pull/17785
Théo Zimmermann (Jul 04 2023 at 10:57):Depending whether you decide to have you project tested in the base or edge switch, it will use Ubuntu 20.04 or Ubuntu 23.04.
Théo Zimmermann (Jul 04 2023 at 10:58):And yes indeed, those images are not available from DockerHub, may be cleaned from time to time, and I guess it is not reasonable to depend on them for anything outside Coq's own CI.
Janno (Jul 04 2023 at 11:04):I see. It's good to see the image(s) being updated.
Janno (Jul 04 2023 at 11:04):So what's the right choice here? Do I copy the upcoming version of, say, the edge switch for my own CI and then update it every now and then to keep it in sync? Or do I use coqorg/coq images for my own CI and maintain two different CI scripts to juggle the dependencies?
Karl Palmskog (Jul 04 2023 at 11:05):wouldn't it make sense to submit the "missing" conf-* packages to opam-repository?
Paolo Giarrusso (Jul 04 2023 at 11:08):@Janno the key packages are on https://apt.llvm.org/, and that supports tons of Debian and Ubuntu versions, even bionic
Janno (Jul 04 2023 at 11:18):@Pierre Roux I suspect adding the extra bits I need would roughly double the size of that Dockerfile. Is that a reasonable thing to do?
Paolo Giarrusso (Jul 04 2023 at 11:22):the alternative would make the build slower and require sudo, dunno if that's fine
Pierre Roux (Jul 04 2023 at 11:50):Doubling the size of the Dockerfile itself is probably acceptable, doublign the size of the resulting Docker image I don't know.
Pierre Roux (Jul 04 2023 at 11:51):Is the code requiring these dependencies worth testing in Coq's CI? or could alighter target without them be enough?
Paolo Giarrusso (Jul 04 2023 at 11:57):inside Bedrock, LLVM+clang+bunch of adds roughly 1GB — but that could be a specialized image built FROM Coq's image even if the latter is not in CI, given a reliable name for Coq's image.
Janno (Jul 04 2023 at 12:02):We could opt to remove the parts that depend on llvm. The hope is to eventually get another part of our development (our proof automation) into Coq CI and that depends on the files generated with the help of llvm. But even there we could rely on pre-computed outputs to avoid llvm entirely. Given the complexity of all these CI questions I am tempted to take that route.
Paolo Giarrusso (Jul 04 2023 at 12:23):@Karl Palmskog FWIW: packaging conf-clang-libs sounds more trouble than coqide, especially if one must do it up to opam-repository's standard. And different clang plugins might need different clang libs.
Last updated: Dec 05 2023 at 12:01 UTC