I plan to switch the HoTT library to start using Dune when installing using opam. https://github.com/HoTT/Coq-HoTT/pull/1687
Will this cause issues in the Coq CI?
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.
mathcomp-word and stalmarck are already using Dune in the CI
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.
by default, I think the assumption is that it's synchronized with coq-core required Dune version (currently 2.9), right?
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.
We might build Coq with the lowest bound Dune, but that should not necesserily be the case for running the CI.
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).
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.
That's why I didn't think the CI script would have an issue.
It's just the bench I am assuming will need a bump, and I don't think that will be a problem.
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/
In that case there will be no problem.
I plan to bump dune to 3.6 in the edge version see PR for docker update deps
It is important we test both upper bounds IMHO
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: Nov 29 2023 at 18:01 UTC