Stream: Coq devs & plugin devs

Topic: Files installed in strange location


view this post on Zulip Julien Puydt (Jan 24 2022 at 15:30):

While reviewing how Debian's packages are done and comparing with dune's packages, I saw that the whole /usr/lib/coq-core/tools directory is suspicious: it looks more like /usr/share material for the most part ; or perhaps the Python files should be in /usr/libexec...

Should I open an issue on github?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 24 2022 at 16:25):

Sure @Julien Puydt , but maybe it could be more interesting to open an issue in the dune repository for general Debian support; I think there may be already an issue by the way. This way, if dune is adapted to work well with debian, we just inherit that for Coq

view this post on Zulip Julien Puydt (Jan 24 2022 at 16:51):

Well, Debian isn't particular in that, I'm sure most linux distributions and all BSDs have very similar requirements... their maintainers might not be as diligent and picky though

view this post on Zulip Emilio Jesús Gallego Arias (Jan 24 2022 at 16:52):

Sure, but Debian is a good start

view this post on Zulip Emilio Jesús Gallego Arias (Jan 24 2022 at 16:52):

as Dune so far is mostly used in the OPAM world

view this post on Zulip Julien Puydt (Jan 24 2022 at 21:10):

I reported https://github.com/ocaml/dune/issues/5379 ; notice that it isn't just about Debian -- I'm just the pickier and noisier maintainer.

Most probably all maintainers just take what coq gives, and move things around with patches to fix matters -- and don't report.


Last updated: Oct 13 2024 at 01:02 UTC