Stream: Coq devs & plugin devs

Topic: dpdgraph


view this post on Zulip Ali Caglayan (Mar 03 2023 at 14:34):

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.

view this post on Zulip Ali Caglayan (Mar 03 2023 at 14:35):

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.

view this post on Zulip Ali Caglayan (Mar 03 2023 at 14:35):

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.

view this post on Zulip Ali Caglayan (Mar 03 2023 at 14:36):

What is the current version of Dune in the CI?

view this post on Zulip Gaëtan Gilbert (Mar 03 2023 at 14:36):

https://github.com/coq/coq/blob/master/dev/ci/docker/bionic_coq/Dockerfile

view this post on Zulip Ali Caglayan (Mar 03 2023 at 14:39):

OK so it seems we are running the dpdgraph job on the BASE_OPAM version?

view this post on Zulip Ali Caglayan (Mar 03 2023 at 14:39):

Is that normally how we build plugins?

view this post on Zulip Karl Palmskog (Mar 03 2023 at 14:41):

the opam version is pretty ancient too (2.0.6)

view this post on Zulip Ali Caglayan (Mar 03 2023 at 14:43):

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

view this post on Zulip Gaëtan Gilbert (Mar 03 2023 at 14:48):

which plugins use base or edge is basically picked randomly
feel free to change dpdgraph

view this post on Zulip Gaëtan Gilbert (Mar 03 2023 at 14:49):

although note that when I tried @runtest locally it still failed and I have dune 3.6.1

view this post on Zulip Ali Caglayan (Mar 03 2023 at 15:12):

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