I thought-R was a universally agreed upon legacy setting. Emilio seems to disagree for dune.
What’s the best practice?
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.
Oh, I didn't realize that this followed an already extensive discussion with Emilio in the Dune stream!
@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.
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.
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?
That is right. That is what I am doing for all my libraries. And presumably a lot of other users do that just fine.
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.
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.
FTR, once you have a v(i)o both -R and -Q are the same.
but it would make it more likely that a Require breaks, or changes meaning, when moving code across libraries
@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.
There is a feature request by @Michael Soegtrop which is quite related: https://github.com/coq/coq/issues/12686
so, I must keep using
-Q/-R for the high-level behavior of
@Pierre-Marie Pédrot but a
v(i)o does contain part of the library name, no? Does it only contain the last component?
It does contain the library name, but it is in theory easy to relocate.
same question, now for “library name”
List or sth in between?
it contains Coq.Lists.List.
but due to the way we define its content, we can perform a substitution on the stuff that you can find in a vo
mystified: in which way is this fact relevant to the discussion? (Not suggesting that it isn’t, but I’m missing the link)
It's relevant to the problem of having a library which relies on -R when you can have several relocated variants of that library.
so, to Michael’s feature request?
The use of -R allows to keep the name of the encompassing library implicit.
I don’t follow, but since this thread is not about
-V, I guess that’s fine.
@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.
Maybe we can have a breakout chat on this tomorrow (or now if you want).
Last updated: Jan 31 2023 at 14:03 UTC