Generate "_CoqProject" files for Coq theories

[rlepigre]

This is a proof of concept for something @ejgallego and I discussed in the past as an alternative to using dune coq top for editors. We generate one _CoqProject file for each coq.theory stanza, which should allow good support across editors for stepping through Coq/Rocq source files.

This is incompatible with the following features, which I see as non-essential (i.e., could be removed IMO):

• Having more than one coq.theory stanza in a given directory.
• Using per-module flags in a coq.theory stanza.

If we want to push this through, we might want a way to disable generation of _CoqProject by supporting something like (project_file false) in the coq.theory stanza.

This feature is enabled by adding (generate_project_file) to the coq.theory stanza. When used in conjunction with (modules_flags ...) and error is given. No specific error is currently given in cases where several coq.theory stanzas in the same directory use the new flag, however this still errors in a reasonable way (multiple rules generating _CoqProject). This could be improved, but that is not essential for a first version.

[rlepigre]

@ejgallego any chance you could take a look at this?

[ejgallego]

Yes @rlepigre , I'm almost at the point I will resume work on Dune Rocq; thanks for your patience.

[ejgallego]

Looks pretty good to me, I have some minor comments, but I suggest to add a changelog and documentation, as I can fix the comments myself.

[rlepigre]

@ejgallego I added a changelog, but let's wait until we decide how to address the issues I raised in the description of the PR. I'd love to hear your take on these.

[SkySkimmer]

This is a proof of concept for something @ejgallego and I discussed in the past as an alternative to using dune coq top for editors.

I guess another alternative would be to have dune coq have some "tell me the flags in a machine readable way" subcommand and teach IDEs to use that.

[rlepigre]

I guess another alternative would be to have dune coq have some "tell me the flags in a machine readable way" subcommand and teach IDEs to use that.

That already exists: dune coq top (and its --toplevel argument). You can pass it a "fake toplevel" that spits out the arguments it receives in any format you like.

However, I never managed to get help to integrate support in editors, and in particular in PG (see here).

[SkySkimmer]

Having the "fake toplevel" builtin sounds like it would make it much easier to use for IDEs.

[rlepigre]

Having the "fake toplevel" builtin sounds like it would make it much easier to use for IDEs.

How so?

Editors would have to:

1. Run something like dune coq top --no-build --toplevel fake-toplevel path/to/file.v > /tmp/flags.
2. Run the appropriate toplevel using the flags of /tmp/flags.

The currently possible alternative is to just run dune coq top --no-build --toplevel whatever path/to/file.v.

[ejgallego]

@ejgallego I added a changelog, but let's wait until we decide how to address the issues I raised in the description of the PR. I'd love to hear your take on these.

I think it is fine to fail in both cases, tho we may want to have a better error message, right?

What's your take on those? The way I see this patch, it is mostly for backwards compatibility, at some point editors should try to understand dune files directly. I guess we should try to add dune-project support to coq-lsp soon.

Something that is not clear to me if we need to install _CoqProject files?

[SkySkimmer]

Some IDEs share the process between multiple files, so they do need to extract arguments and don't want to just start a fresh toplevel.

[rlepigre]

@Alizter @ejgallego I think this is now in a very reasonable state, since the feature is now opt-in. Hopefully we can get this in quickly.

[rlepigre]

CI failures look spurious.

[rlepigre]

Thanks @Alizter!