Stream: Dune devs & users

Topic: Conditional dependency


view this post on Zulip Li-yao (May 25 2021 at 16:19):

Apparently coq.lib has been renamed to coq-core.lib on dev, so what's the right way to specify either dependency, whether I have coq 8.13 or (what will be) 8.14?

view this post on Zulip Théo Zimmermann (May 25 2021 at 16:28):

I'm not sure what you mean exactly by your question, but the basic assumption was that plugin developers maintain compatibility for only one version of Coq in a given branch, and therefore that you should switch from coq.lib to coq-core.lib when switching from 8.13 to 8.14...

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2021 at 16:40):

Indeed we made that assumption @Li-yao , however note that Dune does provide a compat mode for renaming libs, so if you have a use case we could enable it in Coq

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2021 at 16:40):

If that's only for coq.libcan be done, note @Théo Zimmermann that this particular library happens to be quite stable

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2021 at 16:40):

as it our "base" lib

view this post on Zulip Li-yao (May 25 2021 at 16:51):

I see. It's good to know that's the assumption. I'm not fond of maintaining multiple branches though. Given how configurable dune is, I was hoping I could somehow write something like (libraries (coq.lib || coq-core.lib)) in a library stanza, without requiring any changes in Coq.

view this post on Zulip Li-yao (May 25 2021 at 17:15):

So, there's a hack that does that: https://github.com/Vertalo/tezos/blob/404b0728e4561d0f9617fad7b98d3b83e0ab207c/src/bin_node/dune

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2021 at 23:31):

Indeed there are hacks, but usually the approach is to enable the compat flag in the coq library code; another nice thing would be to expose %coq:version for use in rules, but didn't get to implement it yet.

view this post on Zulip Li-yao (May 26 2021 at 13:10):

Why would that be the better approach though? It seems to add maintenance burden to Coq when the alternative could be no burden.

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2021 at 14:40):

You mean the coq:version variable? This makes it very convenient for plugins to define their own small compat layer, then do a copy rule such as (cp compat_%{coq:version} compat.ml)

view this post on Zulip Li-yao (May 26 2021 at 14:55):

I meant

but usually the approach is to enable the compat flag in the coq library code

This seems contradictory with the aforementioned assumption of compatibility with one version of Coq at most.

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2021 at 14:58):

That flag just introduces a dummy coq.liblibrary that will depend on coq-core.lib , and emits a warning

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2021 at 14:58):

so it helps a bit

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2021 at 14:58):

we don't promise compatibility, but that doesn't mean we cannot try to lower the impact of change on plugin authors

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2021 at 14:59):

or make life easier

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2021 at 15:00):

for now we need to reserve the right to change the OCaml API as we know it is not good in a few places [I'm sure you know that :p ], but we wouldn't mind at all improving this and having a more stable setup in the future


Last updated: Oct 16 2021 at 09:07 UTC