Paolo Giarrusso (Nov 29 2020 at 20:07): Paolo Giarrusso (Nov 29 2020 at 20:07):I thought-R was a universally agreed upon legacy setting. Emilio seems to disagree for dune.
Paolo Giarrusso (Nov 29 2020 at 20:08):What’s the best practice?
Théo Zimmermann (Dec 01 2020 at 10:49):I also thought that but what I understood of @Emilio Jesús Gallego Arias's position is that you should be able to load files in your own project without a From clause or a fully qualified module name, but once they get installed, then it's important that the modules are only accessible with a From clause or a fully qualified module name. Thus, -R within a project but -Q for making it available to the world. That being said, I don't know how technically feasible this setup actually is.
Théo Zimmermann (Dec 01 2020 at 10:55):Oh, I didn't realize that this followed an already extensive discussion with Emilio in the Dune stream!
Christian Doczkal (Dec 01 2020 at 11:22):@Théo Zimmermann What you describe does indeed sound like the best solution to me, it would avoid having to repeat the namespace of the project within the projects files.
Emilio Jesús Gallego Arias (Dec 01 2020 at 12:50):Indeed that was the idea when I chose -R ; it works OK for OCaml. I couldn't find any official guideline that says that -R is deprectaed, but indeed in coq_makefile it makes sense to avoid it as you don't have a notion of library, so imagine you use a few libraries in your tree, you'd have a mess.
But I insist that from the point of Dune, the semantics of (coq.theory ...) are to be understood independently from actual Coq low-level options. I'm sure we will implement new flags in Coq for example to make it compliant with the desired semantics from Dune.
Christian Doczkal (Dec 01 2020 at 13:43):Just to be sure, if I have a single-library source tree (probably the most common scenario out there) then it should be fine to use -R in the _CoqProject file, because the difference between locally using -Q and or -R is no longer visible after the library has been installed via OPAM, right? Or am I missing something?
Guillaume Melquiond (Dec 01 2020 at 15:16):That is right. That is what I am doing for all my libraries. And presumably a lot of other users do that just fine.
Paolo Giarrusso (Dec 01 2020 at 16:18):I never knew that was possible, and until today I considered all uses of -R clear bugs (like Theo). I’m still not sure that’s appropriate for all use-cases.
Paolo Giarrusso (Dec 01 2020 at 16:20):since I maintain multiple but tightly coupled libraries, I’m not sure that using -R would save me much (or anything) in case of a rename.
Pierre-Marie Pédrot (Dec 01 2020 at 16:20):FTR, once you have a v(i)o both -R and -Q are the same.
Paolo Giarrusso (Dec 01 2020 at 16:20):but it would make it more likely that a Require breaks, or changes meaning, when moving code across libraries
Paolo Giarrusso (Dec 01 2020 at 16:21):@Emilio Jesús Gallego Arias I don’t know the difference between “low-level” -Q/-R and the high-level behaviors, and I don’t want to know — but the latter don’t have names.
Pierre-Marie Pédrot (Dec 01 2020 at 16:22):There is a feature request by @Michael Soegtrop which is quite related: https://github.com/coq/coq/issues/12686
Paolo Giarrusso (Dec 01 2020 at 16:22):so, I must keep using -Q/-R for the high-level behavior of Require.
Paolo Giarrusso (Dec 01 2020 at 16:24):@Pierre-Marie Pédrot but a v(i)o does contain part of the library name, no? Does it only contain the last component?
Pierre-Marie Pédrot (Dec 01 2020 at 16:25):It does contain the library name, but it is in theory easy to relocate.
Paolo Giarrusso (Dec 01 2020 at 16:26):same question, now for “library name”
Pierre-Marie Pédrot (Dec 01 2020 at 16:26):WDYM?
Paolo Giarrusso (Dec 01 2020 at 16:26):does coq/theories/Lists/List.vo contain coq.Lists.List or List or sth in between?
Gaëtan Gilbert (Dec 01 2020 at 16:26):Coq.Lists.List
Pierre-Marie Pédrot (Dec 01 2020 at 16:26):it contains Coq.Lists.List.
Pierre-Marie Pédrot (Dec 01 2020 at 16:27):but due to the way we define its content, we can perform a substitution on the stuff that you can find in a vo
Paolo Giarrusso (Dec 01 2020 at 16:29):mystified: in which way is this fact relevant to the discussion? (Not suggesting that it isn’t, but I’m missing the link)
Pierre-Marie Pédrot (Dec 01 2020 at 16:29):It's relevant to the problem of having a library which relies on -R when you can have several relocated variants of that library.
Paolo Giarrusso (Dec 01 2020 at 16:30):so, to Michael’s feature request?
Paolo Giarrusso (Dec 01 2020 at 16:30):fair
Pierre-Marie Pédrot (Dec 01 2020 at 16:31):The use of -R allows to keep the name of the encompassing library implicit.
Paolo Giarrusso (Dec 01 2020 at 16:34):I don’t follow, but since this thread is not about -V, I guess that’s fine.
Paolo Giarrusso (Dec 01 2020 at 16:35):@Emilio Jesús Gallego Arias in any case, as @Christian Doczkal and @Guillaume Melquiond say, uses of the -Q semantics today are in no way workarounds for coq_makefile limitations. Today’s setup simply mandates -Q semantics for installed libraries; the Require semantics within the library are up to the library author.
Michael Soegtrop (Dec 01 2020 at 16:49):Maybe we can have a breakout chat on this tomorrow (or now if you want).
Last updated: Oct 03 2023 at 04:02 UTC