Dune-Coq: support transitive dependencies even for installed theories

[Blaisorblade]

In short, depending on a coq.theory should also make its dependencies available. This issue is known to experts (at least Emilio and Rodolphe) but I didn't find a bug-tracker entry, and at Bluerock we are interested in a solution, so I figured I would make one.

Desired Behavior

Assume we have (coq.theory (name foo.logical.prefix) (theories direct_deps)) and a client client. Let us write deps for direct_deps plus any theories they depend on.
When client's bar.v tries to Require foo.logical.prefix.some_module., any used module from deps must be in scope — so clients of theory foo.logical.prefix need to depend on theories in deps, and shouldn't have to list deps explicitly among their dependencies — that can even change when foo.logical.prefix evolves.

Dune usually supports this, except if foo.logical.prefix is installed and clients are using dune-coq >= 0.8: in that case:

1. deps are also installed, but
2. installed theories are not available implicitly (https://dune.readthedocs.io/en/stable/coq.html#coq-language-version), and
3. installing foo.logical.prefix doesn't even record that it depends on direct_deps.

Hence, we should

4. change 3 and record the dependencies direct_deps of theories when installing them
5. and make those dependencies deps (so, direct_deps and their dependencies) available to client.

Possible future extension:

If client requires on some modules from dep in deps explicitly, arguably client should depend on dep explicitly — to be more robust if foo.logical.prefix drops the dependency on dep. Emilio has mentioned this a few times. However, nowadays dependencies are either available or not, and supporting this extension would require distinguishing direct and indirect uses — either in Coq, or in separate linters. Thankfully, that does not affect point 4: all (transitive) dependencies deps of foo.logical.prefix would be available as indirect dependencies for client, and none as direct dependencies. Hence, I propose to leave discussion of this to future work.

Implementation ideas

IIRC, Rodolphe proposed to reuse findlib for this:
https://coq.zulipchat.com/#narrow/channel/240550-Dune-devs-.26-users/topic/.5Blaodpath.5D.20Coqdep.20vs.2E.20Coqmod/near/285853410

Other threads about this

https://coq.zulipchat.com/#narrow/channel/240550-Dune-devs-.26-users/topic/Dune-Coq.200.2E3.20dependency.20model
https://coq.zulipchat.com/#narrow/channel/240550-Dune-devs-.26-users/topic/Adding.20transitive.20deps.20into.20theories

Example

[SkySkimmer]

However, nowadays dependencies are either available or not, and supporting this extension would require distinguishing direct and indirect uses — either in Coq, or in separate linters.

Aren't they already distinguished? coqdep will mention direct deps and won't mention indirect deps.

[Blaisorblade]

I'm not sure if that would make a difference, but is that still true with coqdep -boot, which is what's used here?

IIUC, Dune just passes (to coqdep/coqc) -boot and a bunch of -Q/-R options for direct and indirect dependencies, and basically nothing else (minus maybe Init or Corelib) is on the COQPATH, for either coqdep or coqc? So how would coqdep be able to behave differently?

[SkySkimmer]

If you have Require foo, coqdep won't look in foo.vo or foo.v to see what it depends on, but coqc will look in foo.vo.

[Blaisorblade]

So, dune could pass direct dependencies to coqdep, and transitive dependencies to coqc/coqtop? Arguably it'd satisfy the basic requirements:

• if client/**/foo.v contains a Require some_dep.file statement, client's coq.theory stanza must depend on some_dep directly; otherwise coqdep would warn/fail
• indirect requires would still work since they're only processed in coqc.

I won't be surprised if there are problems — it's not clear to me if all of this behavior will stay the same.

As a future alternative, we could inform both coqdep and coqc of indirect dependencies via different options, and coqdep could use that info for more informative warning. Instead of "some_dep.file not found", it could say "some_dep.file is only an indirect dependency, make it a direct dependency to allow this Require statement" (up to bikeshedding). (This could even be a warning that defaults to an error — arguably, that's better for users since you can get later errors as well).

[SkySkimmer]

So, dune could pass direct dependencies to coqdep, and transitive dependencies to coqc/coqtop? Arguably it'd satisfy the basic requirements:

No, dune should pass the transitive -Q/-R flags to coqdep. coqdep will then return info on whether they are used directly.