The switch to Dune for dpdgraph was actually fine on the maintiners end. Everything was running against coq-master including the tests. The issue was that we required Dune 3.3 which was not present in CI. Since Dune is currently 3.7, it would be great to bump the version of Dune available in the Coq CI.
We have since reverted the Dune commit but I opened another PR adding it back in. This time I want to coordinate better with the CI team here.
The only difference is that we no longer need ./configure and autoconfi in the CI. And I guess if you want to have the correct install prefixes you can just do the dune build commands in the CI too.
What is the current version of Dune in the CI?
https://github.com/coq/coq/blob/master/dev/ci/docker/bionic_coq/Dockerfile
OK so it seems we are running the dpdgraph job on the BASE_OPAM version?
Is that normally how we build plugins?
the opam version is pretty ancient too (2.0.6)
I think it is fine to test the lower supported bound of Dune for Coq, however building all the plugins this way seems kind of suspect
which plugins use base or edge is basically picked randomly
feel free to change dpdgraph
although note that when I tried @runtest
locally it still failed and I have dune 3.6.1
Yeah I see the failures now when I compose with Coq. Its failing because it can't find coqlib...
Last updated: Oct 13 2024 at 01:02 UTC