Ali Caglayan (Dec 31 2022 at 15:40): Ali Caglayan (Dec 31 2022 at 15:40):I plan to switch the HoTT library to start using Dune when installing using opam. https://github.com/HoTT/Coq-HoTT/pull/1687
Ali Caglayan (Dec 31 2022 at 15:41):Will this cause issues in the Coq CI?
Ali Caglayan (Dec 31 2022 at 15:41):AFAIK we use git directly in the CI currently, but it might cause issues in the bench. If so, if we could bump the Dune version in the bench to at least 3.5 that would be great.
Karl Palmskog (Dec 31 2022 at 15:51):mathcomp-word and stalmarck are already using Dune in the CI
Ali Caglayan (Dec 31 2022 at 16:24):mathcomp word needs Dune 2.8 and stalmarck uses 2.5 so my question is really about how high does the CI Dune version go.
Karl Palmskog (Dec 31 2022 at 16:37):by default, I think the assumption is that it's synchronized with coq-core required Dune version (currently 2.9), right?
Karl Palmskog (Dec 31 2022 at 16:44):I've tried to lobby in the past to raise min OCaml version when there was no specific breakage (just that 4.04/4.05 gave us tons of trouble/breakage in the Coq opam archive), didn't have much luck. Might be more efficient to write a manual opam that calls dune.
Ali Caglayan (Dec 31 2022 at 16:57):We might build Coq with the lowest bound Dune, but that should not necesserily be the case for running the CI.
Théo Zimmermann (Jan 02 2023 at 08:51):We only have two opam switches in the Coq CI Dockerfile, base and edge: https://github.com/coq/coq/blob/master/dev/ci/docker/bionic_coq/Dockerfile
Currently, Dune is set at 2.9.1 in BASE_ONLY_OPAM and 2.9.3 in BASE_OPAM_EDGE.
It is important that we keep testing the minimum required version somewhere, so BASE_ONLY_OPAM should stay at 2.9. But it would be fine to bump the version in BASE_OPAM_EDGE and switch ci-hott to be built with ci-template-flambda (i.e., with the edge switch).
Ali Caglayan (Jan 02 2023 at 14:14):I should make it clear that the old makefile still works for HoTT and should continue working. It's just that the opam package in the repoo uses Dune now.
Ali Caglayan (Jan 02 2023 at 14:15):That's why I didn't think the CI script would have an issue.
Ali Caglayan (Jan 02 2023 at 14:15):It's just the bench I am assuming will need a bump, and I don't think that will be a problem.
Gaëtan Gilbert (Jan 02 2023 at 14:19):the opam file in the repo is not used by the bench, the bench uses the opam file in https://github.com/coq/opam-coq-archive/
Ali Caglayan (Jan 02 2023 at 14:25):In that case there will be no problem.
Emilio Jesús Gallego Arias (Jan 02 2023 at 22:47):I plan to bump dune to 3.6 in the edge version see PR for docker update deps
Emilio Jesús Gallego Arias (Jan 02 2023 at 22:47):It is important we test both upper bounds IMHO
Paolo Giarrusso (Jan 03 2023 at 02:36):and with a recent enough dune like 3.6.x you could enable --reproducibility-check if you use caching (looking forward to it)
Last updated: Oct 12 2024 at 13:01 UTC