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?
IIRC @Emilio Jesús Gallego Arias you said that you made some symbolic links to be backward compatible. Is it the problem here?
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.
Indeed they are just a workaround, https://github.com/coq/coq/pull/13617 removes the symlinks and provides the overlays
They help in quite a few cases but they also create problems so I hope we can move forward with #13617
Note that we could keep the packages
coq.* but IMHO as we don't have ML-level compat I don't think there is a point of introducing the full compat layer
I did keep the symlink until #13617 is implemented due to technical / time-saving reasons.
otherwise it would need a lot of work in the makefiles, just for them to be removed in #13617
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: Nov 29 2023 at 05:01 UTC