`coq.theory` stanza should work on the transitive closure of the `plugins` field

[Alizter]

Coq uses findlib to find and dynlink to load plugins. However if an OCaml library depends on another, we do not pass this information to Coq and Coq isn't clever enough to figure out where things are. We should therefore take the transitive closure of the plugins field so that Coq doesn't get confused.

One option would be to fix this in Coq, but that is a can of worms that I am not willing to touch. I would rather adjust this from the Dune side and give users a better experience.

So if library A depends on library B, writing:

(coq.theory
 (plugins A)
 ...)

should pass -I A -I B tocoqc.

[ejgallego]

The rationale for this was that in the usual Coq context, implicit transitive deps off is usually the default.

Anyways, we should just fix coqdep upstream and remove legacy mode for 1.0 version of the language, I think that'd be more efficient.

[Alizter]

@ejgallego I don't understand how patching coqdep is the correct solution here? You have mentioned before that we intend to support building multiple Coq versions. This is not possible if we patch coqdep and rely on that behaviour.

[ejgallego]

@Alizter , if we fix coqdep we could remove the legacy mode, so that's what I meant; maybe not worth spending time on this if we are gonna remove the legacy mode.

Actually, the way we did things for 8.16 in the end (it was a lot of work), Dune doesn't care about the legacy mode too much.

Once we are in findlib mode, the -I flags are not needed at all.

[ejgallego]

So indeed at some point we should not emit them, there are several ways to teach dune about this.

Recall the reason findlib Coq loading doesn't work now is because coqdep emitting the wrong path to the meta file, so Dune gets confused.