[coq] auto-infer plugins field

[Alizter]

From Coq 8.16 onwards, the plugins field of the coq.theory stanza could be auto-inferred.

1. We find any .v files that do "Declare ML Module".
2. We parse the public_name of the library that is declared.
3. We add this automatically to the list of plugins.

This is only possible from 8.16 onwards as we started using findlib to load plugins. Older versions will not have the plugin names so we need to stay at the current behaviour for those.

This is only about inferring the plugins in the coq.theory stanza and not inferring the plugins in any dependencies. As of writing, Dune is not able to infer the plugins needed from dependencies and this is a bug #7893. The behaviour I am describing here means that a user only has to include a "Declare ML Module" in a .v file rather than having to write them out in the stanza.

We should also work out how we want this to interact with dune coq top. I am not sure we are going to be able to interactively build plugins when they are loaded and these declare statements will have to live in existing .v files. This could be annoying.

It should still be possible for users to declare a plugins field however and we have to work out if this should override or complement the inferred plugins.

[ejgallego]

The workings of this are a bit more subtle tho, a few comments:

• Having to parse .v files is not good for us, we should use coqdep to find this information.
• As of today, coqdep does require the plugins to be in place, so we'd need coqdep -modules as to implement this effectively

As of writing, Dune is not able to infer the plugins needed from dependencies and this is a bug https://github.com/ocaml/dune/issues/7893.

Not sure how that bug is related to this issue. Dune is able to infer the plugins from deps, it is just that the code making the list of such plugins was buggy.

We should also work out how we want this to interact with dune coq top. I am not sure we are going to be able to interactively build plugins when they are loaded and these declare statements will have to live in existing .v files. This could be annoying.

What problem do you anticipate? dune coq top uses the regular dep analysis so that shouldn't be an issue I think.

[Alizter]

• Having to parse .v files is not good for us, we should use coqdep to find this information.

We don't have to parse all .v files. Only the ones which report a cmxs in coqdep.

Not sure how that bug is related to this issue. Dune is able to infer the plugins from deps, it is just that the code making the list of such plugins was buggy.

Right, I am just making sure to describe the current behaviour precisely.

What problem do you anticipate? dune coq top uses the regular dep analysis so that shouldn't be an issue I think.

If I write Declare ML Module into dune coq top, I am unsure if it will be able to load a plugin since those a determined when we parse the stanzas.

[ejgallego]

We don't have to parse all .v files. Only the ones which report a cmxs in coqdep.

That's already too late as coqdep won't work without the plugin command line flags being in place, as it will try to resolve the cmxs. Thus you need coqdep -modules to implement this.

Parsing .v files in Dune is a no go I'm afraid.

Right, I am just making sure to describe the current behaviour precisely.

Well that bug will be fixed today so I'm unsure how it is related. Current behavior is pretty easy to describe:

• coqdep / coqc need to have the right META files and -I flags in place to locate plugins
• Dune will read the (plugin ) field and set these flags, and ensure that the right files (META or legacy .mlpack) files are up to date before the coqdep call.

If I write Declare ML Module into dune coq top, I am unsure if it will be able to load a plugin since those a determined when we parse the stanzas.

That's the same if you write Require Import Foo, dune can't see thru the interactive session. coq-lsp can.