Is there any general consensus on when your project should use a _CoqProject file vs when it should use dune?
Dune support for Coq is still experimental, so most Dune users still provide both build methods.
There are a few examples in https://github.com/coq-community.
@Théo Zimmermann Are there even IDEs that support developing with a reasonable structure and without a _CoqProject file? I guess ProofGeneral doesn't understand dune setups, does it?
Indeed, you are correct to highlight that even when using Dune to build, you still need to provide a hackish
_CoqProject so that IDEs will work reasonably.
OK cool, thanks!
Last updated: Jan 29 2023 at 01:02 UTC