Stream: Dune devs & users

Topic: coq.theory theories field


view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 26 2022 at 00:50):

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

view this post on Zulip Ali Caglayan (Mar 26 2022 at 00:53):

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

view this post on Zulip Li-yao (Mar 26 2022 at 01:30):

I remember complaining when it was -R :)

view this post on Zulip Paolo Giarrusso (Mar 26 2022 at 07:58):

Yeah, -Q makes sense for dependencies…

view this post on Zulip Paolo Giarrusso (Mar 26 2022 at 07:59):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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!)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 28 2022 at 08:02):

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

view this post on Zulip Gaëtan Gilbert (Mar 28 2022 at 08:08):

really?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Mar 28 2022 at 09:06):

why would you do that instead of using -R?

view this post on Zulip Ali Caglayan (Mar 28 2022 at 10:07):

Good point that's completely pointless.

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 10:40):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 28 2022 at 11:20):

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

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 11:20):

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

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 11:29):

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

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:29):

Dune can easily be made more flexible

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:30):

Some Coq projects are not so modular

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:30):

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

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:30):

So it makes sense to use -R

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:31):

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

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:32):

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

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:33):

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

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 11:33):

From … Require has a reasonable compromise.

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 11:34):

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

view this post on Zulip Karl Palmskog (Mar 28 2022 at 11:34):

my experience porting to Dune:

view this post on Zulip 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)

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:38):

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

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:38):

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

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:38):

Writing dune files everywhere would be a waste of time IMO

view this post on Zulip 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"

view this post on Zulip Gaëtan Gilbert (Mar 28 2022 at 11:39):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 11:41):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:47):

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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 11:49):

does dune even pass those flags to coqdep?

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:52):

Also our _CoqProject is autogenerated

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 11:54):

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

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 11:54):

(which is probably a good idea!)

view this post on Zulip Ali Caglayan (Mar 28 2022 at 11:55):

The script is etc/generate_coqproject.sh

view this post on Zulip 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: Jan 30 2023 at 19:04 UTC