_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.
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
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
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
I mean, if one finds useful to separate files in directories, why would he want the opposite w.r.t. module paths?
If you have the same file (name) in two directories, you get a gratuitous clash for example.
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
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
That should not happen. Coq is deterministic with respect to the ordering of the various loadpath commands.
cool. so even in the
-R case, the
"" namespace isn't optimal?
sure, Coq loading is deterministic, but people think they are loading a file they want, when they are really not
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.
-Q), "" is optimal if the given directory contains independent libraries.
well, "independent" seems to be stretching it in the example reference:
-Q . "" -Q ../hs-spec "" -Q ../../../base "" -Q ../../../base-thy Proofs -Q ../../containers/lib ""
But this specific example is not meant to be installed and used by other people, is it?
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
the example reference doesn't use
-R at all. What do you mean independent libraries?
What I mean is that there is no fundamental difference between
If you think it makes sense for
-R to use "", then it makes the exact same sense for
As for independent libraries, the canonical example is Coq itself, as it does
-Q path/to/user-contrib "".
I've been assuming that if
-R means recursive than
-Q is incapable of descending into a directory structure and creating a qualified
Both of them are recursive; they give you access to all the subdirectories. The difference lies in how you
Require the files.
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
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.
-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.
disjoint paths across libraries are probably a safer default.
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...
IIRC there is a warning if there is no clear "root"
Which suggests using INSTALLDEFAULTROOT. OTOH, there's not even an option to deny that warning (= use -warn-error on it) :upside_down:
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)
I don't see anything mentioning INSTALLDEFAULTROOT except some old logs in the test suite
see also https://github.com/coq/coq/commit/cc924e68f3704f9bf6f0277844d1269c6c3ab577
Great! I wasn't aware of the removal (only in 8.15, which is why).
Quinn has marked this topic as resolved.
Last updated: Oct 03 2023 at 04:02 UTC