feature(coq): generate plugin deps from plugins field in stanza

[Alizter]

We add the dependencies on plugins using the ones declared in the dune file.

Currently we require the user to add their ml libraries in the plugins field of the Coq stanza. Afterwards we add cmxs deps on files using the files declared by coqdep.

Since we have the full list of plugins, we might as well compute the cmxs deps (of the transitive closure) ourselves and add them to the Coq rules. Whether or not these files actually load these cmxs files is irrelevant but making them present is important.

[rgrinberg]

Could you add more description to the PR?

• What are the issues with the current approach?
• That this implementation is not yet complete (the cases where plugin_deps aren't calculated)

[rgrinberg]

This also means that plugins are compiled before coqdep is called which can have certain advantages.

That's incorrect. We introduce the dependencies without coqdep, but the plugins are compiled at the same time.

[rgrinberg]

Can you add extraction in this PR as well?

The coqtop stuff can be delayed until the deduplication is done.

[Alizter]

This also means that plugins are compiled before coqdep is called which can have certain advantages.

That's incorrect. We introduce the dependencies without coqdep, but the plugins are compiled at the same time.

Having a look at the tests that changed, the calls to coqdep moved after which is why I said this.

[rgrinberg]

Those changes just tell us that we've discovered the dependency edge before running coqdep. Has nothing to do with building plugins.

[rgrinberg]

Thinking about this a little more, I realize that this behavior isn't ideal either. We lose some build concurrency for no reason. Here's a more behaved implementation:

• Calculate the plugins closure set (we've done that)
• Use it to very that coqdep doesn't introduce .cmxs dependencies outside of this closure
• If coqdep introduces a cmxs dependency outside of this list, dune should error and say that this is invalid without depending on a plugin in the theory. Otherwise, the dependencies should be the subset selected by coqdep

The above describes the ideal behavior for both coqdep and coqmod.

Finally, could you add some tests for the cases described above? It's an important part to spec out.

[ejgallego]

Yes, only very few .v files do depend on the plugins, so adding a dependency on the plugins to all .v files is IMO wrong, and adds a lot of spurious build edges (and we make the build graph less concurrent)

What is the advantage of this approach? I can't see any. Morever, coqdep will keep emitting the .cmxs dep.

[ejgallego]

@rgrinberg coqdep will already not emit a dependency on a plugin if it can't be found.

[Alizter]

What is the advantage of this approach? I can't see any. Morever, coqdep will keep emitting the .cmxs dep.

I plan to make sure that the cmxs dep actually comes from the declared plugins, this will allow us to catch attempts to load plugins not declared in the dune file at the dune level rather than Coq failing.

[ejgallego]

I plan to make sure that the cmxs dep actually comes from the declared plugins, this will allow us to catch attempts to load plugins not declared in the dune file at the dune level rather than Coq failing.

I've never heard of this problem, and I can't see how this helps solving it. If you want to validate coqdep output more you can do so with what we have today.

Can you provide an example of the problem you are trying to solve, and Coq failing because of that?

How does adding all these spurious deps helps validating the plugin set?

[ejgallego]

Note that already the cmxs deps have to come from declared plugins, modulo some really weird stuff which could happen if two plugins have the same private name when using the legacy method.

[Alizter]

I've never heard of this problem, and I can't see how this helps solving it. If you want to validate coqdep output more you can do so with what we have today.

If Declare ML Module loads a plugin not declared in the dune file, then Coq will not be able to load the plugin and error. My validation suggestion is to let Dune catch this before that happens.

Can you provide an example of the problem you are trying to solve, and Coq failing because of that?

I am not solving a specific problem. I am trying to improve how plugins are handled by Dune.

[rgrinberg]

coqdep will already not emit a dependency on a plugin if it can't be found.

I think that's the problem basically. How does coqdep know whether a plugin can't be found or dune just hasn't built it yet?

[ejgallego]

coqdep will already not emit a dependency on a plugin if it can't be found.

I think that's the problem basically. How does coqdep know whether a plugin can't be found or dune just hasn't built it yet?

A .mllpack file has to be in the directory for the search path. That has changed in 8.16, when using the new method plugins are just findlib names.

[ejgallego]

If Declare ML Module loads a plugin not declared in the dune file, then Coq will not be able to load the plugin and error. My validation suggestion is to let Dune catch this before that happens.

I am not sure I understand how the validation is going to work, when using the legacy method that's quite tricky to do.

Is the validation implemented in this PR?

Can you provide an example of the problem you are trying to solve, and Coq failing because of that?

I am not solving a specific problem. I am trying to improve how plugins are handled by Dune.

Indeed the problem is that I don't see how this improves things, and on the contrary, significantly worsens the dep graph by adding ten of thousands of unneeded deps on for example the Coq Universe build.

[Alizter]

If Declare ML Module loads a plugin not declared in the dune file, then Coq will not be able to load the plugin and error. My validation suggestion is to let Dune catch this before that happens.

I am not sure I understand how the validation is going to work, when using the legacy method that's quite tricky to do.

You are correct that the validation is tricky to do for the legacy method and is probably not needed. For the new loading method it would be possible.

Is the validation implemented in this PR?

I have a patch that works validating the 8.16 plugin loading method. No validation is added in this PR.

Can you provide an example of the problem you are trying to solve, and Coq failing because of that?

I am not solving a specific problem. I am trying to improve how plugins are handled by Dune.

Indeed the problem is that I don't see how this improves things, and on the contrary, significantly worsens the dep graph by adding ten of thousands of unneeded deps on for example the Coq Universe build.

I have several other patches that are relying on this reorganization. The extra deps are unneeded, but a strongly believe that they are harmless.

In a future patch, we should be able to refine the dependencies further by associating which plugins a coq module depends on as some associated data. This would let plugin deps be resolved via the transitive closure of the coq theories depended on etc. This is more of a sketch of an idea I have had about this.

[ejgallego]

I have several other patches that are relying on this reorganization. The extra deps are unneeded, but a strongly believe that they are harmless.

Adding a lot of spurious deps doesn't meet my definition of harmless as for sure will eat memory and increase overhead due to the longer build graph.

In a future patch, we should be able to refine the dependencies further by associating which plugins a coq module depends on as some associated data. This would let plugin deps be resolved via the transitive closure of the coq theories depended on etc. This is more of a sketch of an idea I have had about this.

I am lost here. The current way we compute deps w.r.t. plugins is optimal, so why do we need this? I am still unsure what problem you are trying to solve with this PR, as far as I can see it is purely a regression.

[Alizter]

Summary: patch is crap can do better