Stream: Coq users

Topic: ✔ `-Q . ""`


view this post on Zulip Quinn (Nov 02 2021 at 10:19):

Consider a _CoqProject file such as this one. I understand -R dir "", it recursively accepts dir and changes the dir/foo/bar/ subdirectories to dir.foo.bar paths in Require/Import commands in coq. I understand -Q . ModName, it maps the directory (in this case pwd) (I assume nonrecursively) to the name ModName for importing or requiring like Require ModName. or Import ModName.. I do not understand what -Q dir "" means.

view this post on Zulip Karl Palmskog (Nov 02 2021 at 10:22):

my understanding is that they want to use the empty namespace as root, so their files can use Require Import <Filename-without-.v> instead of Require Import <namespace>.<Filename-without-.v>, even by projects outside of their project

view this post on Zulip Karl Palmskog (Nov 02 2021 at 10:23):

this is not recommended when providing a library for use in other code, and because of this I don't think it's easy to use hs-to-coq as a regular dependency like one does with external Coq libraries

view this post on Zulip Enrico Tassi (Nov 02 2021 at 10:23):

Indeed. I would not consider this a super nice practice, since we have From whatever Require Things so flattening the "module space" is a bit gratuitous IMO

view this post on Zulip Enrico Tassi (Nov 02 2021 at 10:24):

I mean, if one finds useful to separate files in directories, why would he want the opposite w.r.t. module paths?

view this post on Zulip Enrico Tassi (Nov 02 2021 at 10:25):

If you have the same file (name) in two directories, you get a gratuitous clash for example.

view this post on Zulip Karl Palmskog (Nov 02 2021 at 10:26):

well, it's a very subtle crash, I think one will get "shadowing", i.e., one might load another file than the intended one in different contexts

view this post on Zulip Karl Palmskog (Nov 02 2021 at 10:27):

I completely understand that people want a different virtual Coq path layout than their physical one though, but I think they should at least not pollute the global namespace

view this post on Zulip Guillaume Melquiond (Nov 02 2021 at 10:27):

That should not happen. Coq is deterministic with respect to the ordering of the various loadpath commands.

view this post on Zulip Quinn (Nov 02 2021 at 10:27):

cool. so even in the -R case, the "" namespace isn't optimal?

view this post on Zulip Karl Palmskog (Nov 02 2021 at 10:27):

sure, Coq loading is deterministic, but people think they are loading a file they want, when they are really not

view this post on Zulip Quinn (Nov 02 2021 at 10:28):

Karl Palmskog: this is not recommended when providing a library for use in other code, and because of this I don't think it's easy to use hs-to-coq as a regular dependency like one does with external Coq libraries

well it's not a question of the tool but a question of how the user incorporates output from the tool into a project, in this case.

view this post on Zulip Guillaume Melquiond (Nov 02 2021 at 10:29):

For -R (and -Q), "" is optimal if the given directory contains independent libraries.

view this post on Zulip Karl Palmskog (Nov 02 2021 at 10:30):

well, "independent" seems to be stretching it in the example reference:

-Q . ""
-Q ../hs-spec ""
-Q ../../../base ""
-Q ../../../base-thy  Proofs
-Q ../../containers/lib ""

view this post on Zulip Guillaume Melquiond (Nov 02 2021 at 10:31):

But this specific example is not meant to be installed and used by other people, is it?

view this post on Zulip Karl Palmskog (Nov 02 2021 at 10:32):

I guess not, but it's the only way to use/compile hs-to-coq currently, to my knowledge. It's the same all over the codebase: https://github.com/plclub/hs-to-coq/blob/master/base/_CoqProject#L1

view this post on Zulip Quinn (Nov 02 2021 at 10:35):

the example reference doesn't use -R at all. What do you mean independent libraries?

view this post on Zulip Guillaume Melquiond (Nov 02 2021 at 10:36):

What I mean is that there is no fundamental difference between -R and -Q.

view this post on Zulip Guillaume Melquiond (Nov 02 2021 at 10:38):

If you think it makes sense for -R to use "", then it makes the exact same sense for -Q.

view this post on Zulip Guillaume Melquiond (Nov 02 2021 at 10:39):

As for independent libraries, the canonical example is Coq itself, as it does -Q path/to/user-contrib "".

view this post on Zulip Quinn (Nov 02 2021 at 10:40):

I've been assuming that if -R means recursive than -Q is incapable of descending into a directory structure and creating a qualified . path

view this post on Zulip Guillaume Melquiond (Nov 02 2021 at 10:41):

Both of them are recursive; they give you access to all the subdirectories. The difference lies in how you Require the files.

view this post on Zulip Karl Palmskog (Nov 02 2021 at 10:42):

right, some people use -Q mostly because it forces their project to consistently use "fully qualified" Requires, as in Require Import MyProject.Stuff. instead of Require Import Stuff. (the latter would lead to build error with -Q)

view this post on Zulip Guillaume Melquiond (Nov 02 2021 at 10:46):

Whether you do -R path Foo or -Q path Foo, file path/a/b/c.vo will provide the module Foo.a.b.c. But with -R, you can type Require c, while with -Q, you have to type From Foo Require c.

view this post on Zulip Quinn (Nov 02 2021 at 10:53):

great, thanks

view this post on Zulip Paolo Giarrusso (Nov 02 2021 at 12:12):

FWIW, -Q …. “” wouldn’t be expressible in dune AFAIK. For build tooling like separationg logic, aliasing between logical paths complicates reasoning (here, runtime reasoning), including eg uninstalling.

view this post on Zulip Paolo Giarrusso (Nov 02 2021 at 12:13):

disjoint paths across libraries are probably a safer default.

view this post on Zulip Karl Palmskog (Nov 02 2021 at 12:14):

I think coq_makefile actually allows putting .vo files directly in the user-contrib root? Or there might be some error message. Dune should be harder to trick into doing that, though...

view this post on Zulip Enrico Tassi (Nov 02 2021 at 12:33):

IIRC there is a warning if there is no clear "root"

view this post on Zulip Paolo Giarrusso (Nov 02 2021 at 14:49):

Which suggests using INSTALLDEFAULTROOT. OTOH, there's not even an option to deny that warning (= use -warn-error on it) :upside_down:

view this post on Zulip Théo Zimmermann (Nov 02 2021 at 15:10):

And the warning is not documented anywhere and I don't know how to set INSTALLDEFAULTROOT (as I raised in the last Coq Call, I think)

view this post on Zulip Gaëtan Gilbert (Nov 02 2021 at 15:15):

I don't see anything mentioning INSTALLDEFAULTROOT except some old logs in the test suite

view this post on Zulip Gaëtan Gilbert (Nov 02 2021 at 15:15):

see also https://github.com/coq/coq/commit/cc924e68f3704f9bf6f0277844d1269c6c3ab577

view this post on Zulip Théo Zimmermann (Nov 02 2021 at 15:23):

Great! I wasn't aware of the removal (only in 8.15, which is why).

view this post on Zulip Notification Bot (Nov 08 2021 at 04:05):

Quinn has marked this topic as resolved.


Last updated: Feb 06 2023 at 13:03 UTC