Jason Gross (Sep 17 2020 at 22:42): Jason Gross (Sep 17 2020 at 22:42):What's the policy on being able to build Coq after installing ocaml & dependencies from system packages? I was under the impression that Coq is supposed to be build-able with packages from the latest Debian stable and Ubuntu LTS versions, but the recent switch to zarith seems to have broken this. Also, if my impression is correct, should we add a job to the CI that tests this property?
Erik Martin-Dorel (Sep 17 2020 at 22:50):@Jason Gross This probably doesn't directly answers your question, but beyond Coq's own CI, the docker-coq nightly-build also checks regression with building coq+bignums on Debian stable + latest opam 2.0; and it precisely failed yesterday due to the recent zarith version bump (cf. GitLab CI pipeline log)
anyway, this should be fixed tonight thanks to the commit I pushed: https://github.com/coq-community/docker-base/commit/a731a37e92925473d6a26607295173da3bf74467
Jason Gross (Sep 17 2020 at 22:51):This tests the build with opam, though, rather than the system packages, no?
Erik Martin-Dorel (Sep 17 2020 at 22:57):exactly, with the zarith opam package, but with the APT package for gmp.
anyway, I'm not aware of the OCaml team's policy w.r.t. the maintenance of Debian OCaml packages (the versions that can go in stable/testing, etc.), so I can't really comment on that.
Bas Spitters (Sep 18 2020 at 06:51):I had a similar experience on a Mac. The issue seems to be with installing opam from the package manager. Everything needs to be done using opam.
I believe it was this one:
https://github.com/ocaml/opam/issues/3968
Théo Zimmermann (Sep 18 2020 at 07:25):I guess there used to be such an informal policy. However, we already parted from this policy when we bumped the required OCaml version to 4.05 before Debian stable included it, hoping that the next Debian stable release would occur before the next Coq release. Then, porting CoqIDE to gtk3 (in reaction to Debian kicking gtk2 out) also required a new "edge" dependency (lablgtk3). And the hope that the build system would be switched to Dune also implied using a version that would be too recent for Debian stable. All I can say regarding the latest zarith release is that hopefully it will soon be included in Debian experimental and maybe even in Debian testing (I can talk to Ralf Treinen about this if that helps).
Last updated: Oct 13 2024 at 01:02 UTC