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.
opam _can_ do sth about OS-level packages — see all the
conf-* stuff and opam-depext
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
conf-* packages are not enough for https://github.com/bedrocksystems/BRiCk (despite what the dune-project file says)
I guess you have to edit that file: https://github.com/coq/coq/blob/master/dev/ci/docker/bionic_coq/Dockerfile
FWIW @Janno, the Docker images for Coq's CI will be updated soon to newer Ubuntu versions: https://github.com/coq/coq/pull/17785
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.
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.
I see. It's good to see the image(s) being updated.
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?
wouldn't it make sense to submit the "missing"
conf-* packages to opam-repository?
@Janno the key packages are on https://apt.llvm.org/, and that supports tons of Debian and Ubuntu versions, even bionic
@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?
the alternative would make the build slower and require
sudo, dunno if that's fine
Doubling the size of the Dockerfile itself is probably acceptable, doublign the size of the resulting Docker image I don't know.
Is the code requiring these dependencies worth testing in Coq's CI? or could alighter target without them be enough?
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.
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.
@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