Stream: Coq users

Topic: When to use _CoqProject vs dune?

view this post on Zulip Shea Levy (Oct 09 2020 at 09:11):

Is there any general consensus on when your project should use a _CoqProject file vs when it should use dune?

view this post on Zulip Théo Zimmermann (Oct 09 2020 at 09:47):

Dune support for Coq is still experimental, so most Dune users still provide both build methods.

view this post on Zulip Théo Zimmermann (Oct 09 2020 at 09:48):

There are a few examples in https://github.com/coq-community.

view this post on Zulip Christian Doczkal (Oct 09 2020 at 09:50):

@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?

view this post on Zulip Théo Zimmermann (Oct 09 2020 at 09:51):

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.

view this post on Zulip Shea Levy (Oct 09 2020 at 09:51):

OK cool, thanks!

Last updated: Oct 08 2024 at 15:02 UTC