Enrico Tassi (Mar 08 2021 at 17:55): Enrico Tassi (Mar 08 2021 at 17:55):I'm getting in CI using the docker image:
# Error: Files /home/coq/.opam/4.07.1+flambda/lib/coq/tactics/tactics.cmxa
# and /home/coq/.opam/4.07.1+flambda/lib/coq-core/tactics/tactics.cmxa
# both define a module named DeclareScheme
This is the dune file: https://github.com/gares/vscoq-language-server/blob/main/vscoqtop/dune
Am I doing something wrong?
Enrico Tassi (Mar 08 2021 at 18:19):IIRC @Emilio Jesús Gallego Arias you said that you made some symbolic links to be backward compatible. Is it the problem here?
Enrico Tassi (Mar 08 2021 at 18:25):OK, I've fixed my dune file by using coq-core.* instead of coq.*. But this also means that the backward compat symlinks don't work as expected.
Emilio Jesús Gallego Arias (Mar 08 2021 at 18:26):Indeed they are just a workaround, https://github.com/coq/coq/pull/13617 removes the symlinks and provides the overlays
Emilio Jesús Gallego Arias (Mar 08 2021 at 18:27):They help in quite a few cases but they also create problems so I hope we can move forward with #13617
Emilio Jesús Gallego Arias (Mar 08 2021 at 18:29):Note that we could keep the packagescoq.* but IMHO as we don't have ML-level compat I don't think there is a point of introducing the full compat layer
Emilio Jesús Gallego Arias (Mar 08 2021 at 18:29):I did keep the symlink until #13617 is implemented due to technical / time-saving reasons.
Emilio Jesús Gallego Arias (Mar 08 2021 at 18:30):otherwise it would need a lot of work in the makefiles, just for them to be removed in #13617
Emilio Jesús Gallego Arias (Mar 08 2021 at 18:31):note that actually after #13617, we could use dune's library deprecation mechanism if desired for free, tho I still think the advantage is pretty low as opposed to people just updating their dune files.
Last updated: Jun 09 2023 at 07:01 UTC