Stream: Coq devs & plugin devs

Topic: coq-core and coq, duplicate libs


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Oct 21 2021 at 21:03 UTC