Karl Palmskog (Jun 22 2023 at 00:48): 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.
Karl Palmskog (Jun 22 2023 at 00:49):is this a bug, or just something to live with?
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.
Ali Caglayan (Jun 22 2023 at 11:27):However we could try to normalize the path in dune before sending it to coqdep.
Ali Caglayan (Jun 22 2023 at 11:27):https://github.com/ocaml/dune/issues/8026#issuecomment-1602471652
Ali Caglayan (Jun 22 2023 at 11:27):Was reported today :)
Ali Caglayan (Jun 22 2023 at 11:28):Apparently this might be fixed in a newer Coq version, but I haven't checked.
Ali Caglayan (Jun 22 2023 at 11:29):@Emilio Jesús Gallego Arias probably can say more.
Emilio Jesús Gallego Arias (Jun 23 2023 at 09:20):See my comment in the bug report.
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: Oct 13 2024 at 01:02 UTC