Stream: coq-community devs & users

Topic: ✔ Project and dune


view this post on Zulip Laurent Théry (Feb 13 2023 at 13:07):

Where can I find a small example of a coq project that is using dune for its build (no _CoqProject)?
Thanks

view this post on Zulip Karl Palmskog (Feb 13 2023 at 13:12):

you mean a project that only has a Dune build? In Coq-community, many projects support both Dune and coq_makefile, but to my knowledge none are Dune exclusive for the pure Coq projects. The only one I know that is Dune-exclusive is: https://github.com/jasmin-lang/coqword

But even that project has a _CoqProject to work with ProofGeneral (but it contains no file list)

view this post on Zulip Pierre Roux (Feb 13 2023 at 13:14):

There is also multinomials that is dune exclusive (but I think it also has a _CoqProject)

view this post on Zulip Laurent Théry (Feb 13 2023 at 13:15):

you mean most have both to have user-interface works ok?

view this post on Zulip Karl Palmskog (Feb 13 2023 at 13:16):

yes, they use the usual trick in _CoqProject:

-R _build/default/src CoqWord

... which effectively rules out compatibility with coq_makefile.

view this post on Zulip Laurent Théry (Feb 13 2023 at 13:17):

Thanks

view this post on Zulip Notification Bot (Feb 13 2023 at 13:17):

Laurent Théry has marked this topic as resolved.

view this post on Zulip Ali Caglayan (Feb 13 2023 at 15:09):

Also https://github.com/ejgallego/coq-universe for a list of Dune coq projects that we are currently playing with. Includes a lot of math comp.

view this post on Zulip Ali Caglayan (Feb 13 2023 at 17:13):

Btw you shouldn't need _CoqProject hacks if you want to use a user-interface. The better way is to use dune coq top to wrap your coq exec in your UI.

view this post on Zulip Karl Palmskog (Feb 13 2023 at 17:18):

I think this enquiry was related to this recent discussion over Dune support in VsCoq.


Last updated: Jun 23 2024 at 23:01 UTC