Laurent Théry (Feb 13 2023 at 13:07): 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
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)
Pierre Roux (Feb 13 2023 at 13:14):There is also multinomials that is dune exclusive (but I think it also has a _CoqProject)
Laurent Théry (Feb 13 2023 at 13:15):you mean most have both to have user-interface works ok?
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.
Laurent Théry (Feb 13 2023 at 13:17):Thanks
Notification Bot (Feb 13 2023 at 13:17):Laurent Théry has marked this topic as resolved.
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.
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.
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 03 2023 at 15:31 UTC