Stream: Dune devs & users

Topic: coq.theory theories field

Ali Caglayan (Mar 26 2022 at 00:50):

I have just noticed that the coq.theory stanza has a theories field, however it passes as a -Q option. :S

Ali Caglayan (Mar 26 2022 at 00:50):

We should probably give the user some control between -Q and -R here

Ali Caglayan (Mar 26 2022 at 00:53):

or at least dune should be passing the correct -Q's

Li-yao (Mar 26 2022 at 01:30):

I remember complaining when it was -R :)

Paolo Giarrusso (Mar 26 2022 at 07:58):

Yeah, -Q makes sense for dependencies…

Paolo Giarrusso (Mar 26 2022 at 07:59):

And why “correct -Q”? What’s wrong with the current ones?

Ali Caglayan (Mar 27 2022 at 19:36):

If I have a theory with multiple nested folders, it might be difficult to list every single one of them out.

Ali Caglayan (Mar 27 2022 at 19:38):

Say 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?

Paolo Giarrusso (Mar 28 2022 at 01:40):

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!)

Paolo Giarrusso (Mar 28 2022 at 01:42):

but I certainly have seen sources that don't conform to dune's wishes, and indeed the porting is not necessarily trivial.

Paolo Giarrusso (Mar 28 2022 at 01:45):

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.

Karl Palmskog (Mar 28 2022 at 08:02):

I think Emilio has made clear before that he will only consider using -R

Gaëtan Gilbert (Mar 28 2022 at 08:08):

really?

Karl Palmskog (Mar 28 2022 at 08:12):

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

Ali Caglayan (Mar 28 2022 at 08:58):

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.

Gaëtan Gilbert (Mar 28 2022 at 09:06):

why would you do that instead of using -R?

Ali Caglayan (Mar 28 2022 at 10:07):

Good point that's completely pointless.

Paolo Giarrusso (Mar 28 2022 at 10:40):

IIUC, it's -R for the same library and -Q for other libraries?

Ali Caglayan (Mar 28 2022 at 10:56):

Experiment time:

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[1]: (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[2]: (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[3]: (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[4]: (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[5]: (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[6]: (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.

Paolo Giarrusso (Mar 28 2022 at 11:19):

The idea that Emilio explained is to have a dune file per “module”, so it makes sense to use -R internally but not externally.

Karl Palmskog (Mar 28 2022 at 11:20):

you mean per "theory", right? (which could have many modules in the Coq sense)

Paolo Giarrusso (Mar 28 2022 at 11:20):

No, I mean that theories are supposed to match meaningful software modules ^W components .

Paolo Giarrusso (Mar 28 2022 at 11:28):

@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?

Paolo Giarrusso (Mar 28 2022 at 11:29):

Either this is reasonable for the entire Coq ecosystem, or dune must become more flexible.

Ali Caglayan (Mar 28 2022 at 11:29):

Dune can easily be made more flexible

Paolo Giarrusso (Mar 28 2022 at 11:30):

I don’t get what you have in mind. Surely you’d need more info in dune files?

Ali Caglayan (Mar 28 2022 at 11:30):

Some Coq projects are not so modular

Ali Caglayan (Mar 28 2022 at 11:30):

We can have deeply nested folders which don't really work on their own

Ali Caglayan (Mar 28 2022 at 11:30):

So it makes sense to use -R

Ali Caglayan (Mar 28 2022 at 11:31):

when importing such theories it would be great to have the option to import as R

Karl Palmskog (Mar 28 2022 at 11:31):

@Paolo Giarrusso you mean, how painful is it in general to port a Coq project to use Dune?

Ali Caglayan (Mar 28 2022 at 11:32):

I feel that -Q behavior for importing should be optional and not the default

Paolo Giarrusso (Mar 28 2022 at 11:32):

@Ali Caglayan most others (me included) seem to agree -R for other libraries is a Coq misfeature?

Ali Caglayan (Mar 28 2022 at 11:33):

I suppose it really depends on how the project is set up.

Paolo Giarrusso (Mar 28 2022 at 11:33):

From … Require has a reasonable compromise.

Paolo Giarrusso (Mar 28 2022 at 11:34):

But without From and with -R, client imports will basically pick randomly across dependencies.

Karl Palmskog (Mar 28 2022 at 11:34):

my experience porting to Dune:

• plain Coq projects that use CoqMakefile without fancy stuff are easy
• any hackery in Makefiles make things a lot harder, sometimes near-impossible
• projects that span Coq and OCaml are mid-level hard, but also the ones where you get most bang for buck

Karl Palmskog (Mar 28 2022 at 11:36):

example of really hard-to-port-to-Dune Makefile: https://gitlab.inria.fr/fbesson/itauto/-/blob/master/Makefile (uses two different _CoqProject)

Ali Caglayan (Mar 28 2022 at 11:38):

@Paolo Giarrusso Are you suggesting that people are using -R to import multiple theories?

Ali Caglayan (Mar 28 2022 at 11:38):

I was talking about using -R to import the same theory.

Ali Caglayan (Mar 28 2022 at 11:38):

Take the HoTT library for example, use of -R is essential since there are many folders deeply nested.

Ali Caglayan (Mar 28 2022 at 11:38):

Writing dune files everywhere would be a waste of time IMO

Paolo Giarrusso (Mar 28 2022 at 11:38):

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"

Gaëtan Gilbert (Mar 28 2022 at 11:39):

-R and -Q are basically the same if you use From

Paolo Giarrusso (Mar 28 2022 at 11:40):

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.

Paolo Giarrusso (Mar 28 2022 at 11:41):

@Ali Caglayan There might be some confusion, why would you want more than 2 dune files?

Ali Caglayan (Mar 28 2022 at 11:41):

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.

Ali Caglayan (Mar 28 2022 at 11:43):

So if I have understood correctly, as long as I use From the fact that a theory was imported with Q should not matter?

Paolo Giarrusso (Mar 28 2022 at 11:43):

Yes, even From HoTT Require CRing would work (if unambiguous) and require https://github.com/HoTT/HoTT/blob/master/theories/Algebra/Rings/CRing.v

Paolo Giarrusso (Mar 28 2022 at 11:44):

Using -R would enable Require CRing to refer to that file. Or to any CRing in any other library available with -R.

Ali Caglayan (Mar 28 2022 at 11:45):

I was under the impression Coq could only look through the directories you give. I was not aware From was able to dig deeper.

Paolo Giarrusso (Mar 28 2022 at 11:45):

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.

Ali Caglayan (Mar 28 2022 at 11:46):

Cool, in which case everything I said about changing dunes default is irrelevant. Perhaps the only issue here is getting the point across :)

Paolo Giarrusso (Mar 28 2022 at 11:46):

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

Ali Caglayan (Mar 28 2022 at 11:47):

Yeah that is exactly what I ended up doing: https://github.com/HoTT/HoTT/pull/1634

Paolo Giarrusso (Mar 28 2022 at 11:48):

Passing -R by hand isn't exactly a supported use-case, no idea whether that already breaks today...
https://github.com/HoTT/HoTT/pull/1634/files#diff-ff412b610214bf91738cbefa48e34ee02af8e60a28e003514903c8142993a3c4R4

Paolo Giarrusso (Mar 28 2022 at 11:49):

does dune even pass those flags to coqdep?

Ali Caglayan (Mar 28 2022 at 11:50):

I can get rid of that now that I know -Q and From do the right thing

Paolo Giarrusso (Mar 28 2022 at 11:50):

but yes, if you don't want to move contrib to HoTT/Contrib (which is somewhat disruptive), you might need to use From HoTT Require even in contrib...

Paolo Giarrusso (Mar 28 2022 at 11:51):

oooh you have a cool idea there! You put both -R _build/default/theories HoTT and -R theories HoTT in _CoqProject!

Ali Caglayan (Mar 28 2022 at 11:51):

But I need to touch those files as there are a lot of complaints when it doesn't exist

Ali Caglayan (Mar 28 2022 at 11:52):

Also our _CoqProject is autogenerated

Ali Caglayan (Mar 28 2022 at 11:52):

Which meant that I had to use dune( 3.0?)'s (mode promote) to get it placed in the source tree

Paolo Giarrusso (Mar 28 2022 at 11:53):

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.

Paolo Giarrusso (Mar 28 2022 at 11:54):

oh, because you're building _CoqProject from dune not from a wrapper.

Paolo Giarrusso (Mar 28 2022 at 11:54):

(which is probably a good idea!)

Ali Caglayan (Mar 28 2022 at 11:55):

The script is etc/generate_coqproject.sh

Emilio Jesús Gallego Arias (Mar 28 2022 at 12:53):

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