Li-yao (May 25 2021 at 16:19): 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?
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...
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
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
Emilio Jesús Gallego Arias (May 25 2021 at 16:40):as it our "base" lib
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.
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
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.
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.
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)
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.
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
Emilio Jesús Gallego Arias (May 26 2021 at 14:58):so it helps a bit
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
Emilio Jesús Gallego Arias (May 26 2021 at 14:59):or make life easier
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: Jun 03 2023 at 17:29 UTC