_CoqProject file for editors

[ju-sh]

How would a _CoqProject file using this plugin look like?

I couldn't make it work.

[palmskog]

Since Dune is the build system of Coq, the point of this repo is to highlight using Dune to build plugins. To my knowledge, _CoqProject/coq_makefile can't be made to work in the same way without serious hacks. So we don't plan to support _CoqProject/make builds here.

[ejgallego]

Indeed while it is true that we cannot support _CoqProject files reliably, many users do depend on them to be able to run their plugins with PG / CoqIDE / Vscoq.

So maybe we could add a _CoqProject file, with the above disclaimers, but having the right config for the example so Coq Editors do work, something like:

# Disclaimer about _CoqProject and dune
-R theories MyPlugin

[palmskog]

OK, I'm fine with adding a _CoqProject only for editor purposes.

[ejgallego]

Ok, then let's reopen this. It is sad we have to do it, but it has become quite of a FAQ.

[palmskog]

Fine by me to reopen, but the original issue was sort of an X/Y problem since you can have coq_makefile builds without _CoqProject.

[ejgallego]

Yes, I fully agree. Thanks for the clarification, while we know the difference, it is important we are quite explicit for people that may not fully understand the different roles on the build ecosystem.

[StamesJames]

I had the same issue for using the template in vscode with vscoq.
A _CoqProject file with:
-R ./_build/default/theories/ MyPlugin
-I ./_build/default/src/
in the root folder or adding:
"vscoq.args": [
"-R" ,"./_build/default/theories/", "MyPlugin",
"-I" ,"./_build/default/src/"
]
to the settings.json did the trick.