Stream: Dune devs & users

Topic: Warning for cmxs using different paths


view this post on Zulip Karl Palmskog (Jun 22 2023 at 00:48):

I was playing around with the Dune Plugin Template, and I get this warning during compilation (dune build of https://github.com/coq-community/coq-plugin-template/tree/v8.17%2B0.8), which makes little sense to me:

*** Warning: ltac_plugin.cmxs already found in
/home/palmskog/.opam/5.0.0+flambda+coq.8.17/lib/coq-core/plugins/ltac
(discarding /home/palmskog/.opam/5.0.0+flambda+coq.8.17/lib/coq/../coq-core/plugins/ltac/ltac_plugin.cmxs)

The second path appends /coq/.. in the middle, which leads to an identical filename at the OS level.

view this post on Zulip Karl Palmskog (Jun 22 2023 at 00:49):

is this a bug, or just something to live with?

view this post on Zulip Ali Caglayan (Jun 22 2023 at 11:27):

Bug on the coqdep side since it doesn't see the paths as the same. Coqdep is spitting out the warning.

view this post on Zulip Ali Caglayan (Jun 22 2023 at 11:27):

However we could try to normalize the path in dune before sending it to coqdep.

view this post on Zulip Ali Caglayan (Jun 22 2023 at 11:27):

https://github.com/ocaml/dune/issues/8026#issuecomment-1602471652

view this post on Zulip Ali Caglayan (Jun 22 2023 at 11:27):

Was reported today :)

view this post on Zulip Ali Caglayan (Jun 22 2023 at 11:28):

Apparently this might be fixed in a newer Coq version, but I haven't checked.

view this post on Zulip Ali Caglayan (Jun 22 2023 at 11:29):

@Emilio Jesús Gallego Arias probably can say more.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 09:20):

See my comment in the bug report.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 09:20):

We should try to fix coqc -config to report the true path


Last updated: May 25 2024 at 19:02 UTC