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.
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.
For -R
(and -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 -R
and -Q
.
If you think it makes sense for -R
to use "", then it makes the exact same sense for -Q
.
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 .
path
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" Require
s, as in Require Import MyProject.Stuff.
instead of Require Import Stuff.
(the latter would lead to build error with -Q
)
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
.
great, thanks
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.
disjoint paths across libraries are probably a safer default.
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...
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 13 2024 at 01:02 UTC