I have just noticed that the coq.theory stanza has a theories field, however it passes as a -Q option. :S
We should probably give the user some control between -Q and -R here
or at least dune should be passing the correct -Q's
I remember complaining when it was
Yeah, -Q makes sense for dependencies…
And why “correct -Q”? What’s wrong with the current ones?
If I have a theory with multiple nested folders, it might be difficult to list every single one of them out.
A/a.v B/b.v c.v and I want to reference a theory at the level of c.v, how am I supposed to do this without passing
-Q for each folder?
You could pass the whole folder with
-Q prefix folder (that is, a
dune file in there), then
From prefix Require a b c. will load your three modules... (if I understand the question!)
but I certainly have seen sources that don't conform to
dune's wishes, and indeed the porting is not necessarily trivial.
for instance, I have a project that passes multiple
-Qs for separate folders even if they're part of the same "module", and even if the folders have mutual dependencies.
coqdep is happy, I expect dune will not be.
I think Emilio has made clear before that he will only consider using
well, we will have to ping @Emilio Jesús Gallego Arias to confirm about
-R-only in Dune (and no plans to change this), but this is my recollection
Wouldn't it just be simpler to support both? Or as I suggested, turn an -R into multiple -Qs which is something I'm sure dune can do.
why would you do that instead of using -R?
Good point that's completely pointless.
-R for the same library and
-Q for other libraries?
A ├── AA │ └── aa.v ├── AB │ └── ab.v └── dune B ├── b.v └── dune
$ cat A/dune (include_subdirs qualified) (coq.theory (name A))
$ cat B/dune (coq.theory (name B) (theories A))
Running: (cd _build/default/B && /mnt/sdd1/.opam/coq.dev/bin/coqdep -Q ../A A -R . B -dyndep opt b.v) > _build/default/B/b.v.d Running: (cd _build/default/A && /mnt/sdd1/.opam/coq.dev/bin/coqdep -R . A -dyndep opt AA/aa.v) > _build/default/A/AA/aa.v.d Running: (cd _build/default/A && /mnt/sdd1/.opam/coq.dev/bin/coqdep -R . A -dyndep opt AB/ab.v) > _build/default/A/AB/ab.v.d Running: (cd _build/default && /mnt/sdd1/.opam/coq.dev/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R A A A/AA/aa.v) Running: (cd _build/default && /mnt/sdd1/.opam/coq.dev/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R A A A/AB/ab.v) Running: (cd _build/default && /mnt/sdd1/.opam/coq.dev/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -Q A A -R B B B/b.v)
@Paolo Giarrusso looks like you are correct. -R for the same library and -Q for other libraries. I even made B not have
(include_subdirs qualified) and it still uses -R. This behavior is a little strange. We should have a clear way to ask for both.
The idea that Emilio explained is to have a dune file per “module”, so it makes sense to use -R internally but not externally.
you mean per "theory", right? (which could have many modules in the Coq sense)
No, I mean that theories are supposed to match meaningful software modules ^W components .
@Karl Palmskog surely some code must be reorganized to fit dune’s wishes, and you’ve done lots of such work, how painful is it?
Either this is reasonable for the entire Coq ecosystem, or dune must become more flexible.
Dune can easily be made more flexible
I don’t get what you have in mind. Surely you’d need more info in dune files?
Some Coq projects are not so modular
We can have deeply nested folders which don't really work on their own
So it makes sense to use -R
when importing such theories it would be great to have the option to import as R
@Paolo Giarrusso you mean, how painful is it in general to port a Coq project to use Dune?
I feel that -Q behavior for importing should be optional and not the default
@Ali Caglayan most others (me included) seem to agree -R for other libraries is a Coq misfeature?
I suppose it really depends on how the project is set up.
From … Require has a reasonable compromise.
But without From and with -R, client imports will basically pick randomly across dependencies.
my experience porting to Dune:
example of really hard-to-port-to-Dune Makefile: https://gitlab.inria.fr/fbesson/itauto/-/blob/master/Makefile (uses two different
@Paolo Giarrusso Are you suggesting that people are using -R to import multiple theories?
I was talking about using -R to import the same theory.
Take the HoTT library for example, use of -R is essential since there are many folders deeply nested.
Writing dune files everywhere would be a waste of time IMO
I'm not sure what you mean, but you wrote "when importing such theories it would be great to have the option to import as R"
-R and -Q are basically the same if you use From
to me that reads "clients should be able to request
-R for theories they depend on", but it's hard to pin down what you mean... so let me look at HoTT.
@Ali Caglayan There might be some confusion, why would you want more than 2
Sorry for not being clearer. I meant to say it like this: Say I had a project that depends on HoTT. If I don't mention the HoTT library using -R how can I import the files deeply in there, without specifying everything using -Q? But it seems Gaëtan's post indicates that From solves this.
So if I have understood correctly, as long as I use
From the fact that a theory was imported with Q should not matter?
From HoTT Require CRing would work (if unambiguous) and require https://github.com/HoTT/HoTT/blob/master/theories/Algebra/Rings/CRing.v
-R would enable
Require CRing to refer to that file. Or to any
CRing in any other library available with
I was under the impression Coq could only look through the directories you give. I was not aware From was able to dig deeper.
With Coq 8.15, ambiguous requires become errors, so if somebody else added
CRing.v that way you'd go from "random behavior" to "hard error", but
-R remains unnecessary here.
Cool, in which case everything I said about changing dunes default is irrelevant. Perhaps the only issue here is getting the point across :)
it also seems you'd need only 2
dune files, since
dune covers a whole directory — at least IIUC https://github.com/HoTT/HoTT/blob/master/etc/generate_coqproject.sh#L24 as using
-R theories HoTT -Q contrib HoTT.Contrib
Yeah that is exactly what I ended up doing: https://github.com/HoTT/HoTT/pull/1634
-R by hand isn't exactly a supported use-case, no idea whether that already breaks today...
does dune even pass those flags to
I can get rid of that now that I know -Q and From do the right thing
but yes, if you don't want to move
HoTT/Contrib (which is somewhat disruptive), you might need to use
From HoTT Require even in
oooh you have a cool idea there! You put both
-R _build/default/theories HoTT and
-R theories HoTT in
But I need to touch those files as there are a lot of complaints when it doesn't exist
Also our _CoqProject is autogenerated
Which meant that I had to use dune( 3.0?)'s (mode promote) to get it placed in the source tree
I usually _choose_ which prefix to put, and switch manually, but that's annoying...
mkdir might silence the warnings but might have other side effects.
oh, because you're building
_CoqProject from dune not from a wrapper.
(which is probably a good idea!)
The script is etc/generate_coqproject.sh
I guess we need to rethink the whole thing here, certainly
-R for non-local libs is a huge misfeature and will create lots of pain if you happen to have two files named
List.v for example.
From being recursive means way more complex implementation for external module resolution, such as coqdep etc... have to do [and they need for example to scan the whole filesystem to be able to resolve that].
So I dunno. Regarding
_CoqProject I'm gonna merge @Rodolphe Lepigre
dune coqtop hopefully today or tomorrow so that'll help with many IDEs.
Last updated: Jun 03 2023 at 15:31 UTC