Stream: Coq users

Topic: -Q vs -R


view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 20:07):

I thought-R was a universally agreed upon legacy setting. Emilio seems to disagree for dune.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 20:08):

What’s the best practice?

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 16:22):

so, I must keep using -Q/-R for the high-level behavior of Require.

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 16:25):

It does contain the library name, but it is in theory easy to relocate.

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 16:26):

same question, now for “library name”

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 16:26):

WDYM?

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 16:26):

does coq/theories/Lists/List.vo contain coq.Lists.List or List or sth in between?

view this post on Zulip Gaëtan Gilbert (Dec 01 2020 at 16:26):

Coq.Lists.List

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 16:26):

it contains Coq.Lists.List.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 16:30):

so, to Michael’s feature request?

view this post on Zulip Paolo Giarrusso (Dec 01 2020 at 16:30):

fair

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 16:31):

The use of -R allows to keep the name of the encompassing library implicit.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jan 31 2023 at 14:03 UTC