dune init should support Coq projects

[Alizter]

We should add two templates to dune init:

1. A coq theory
2. A coq plugin

Should be simple to do.

[mihaicostin34]

Hello! Is this issue still open? I would like have a try at this

[nojb]

Yes, it is. Have at it!

[ejgallego]

Hi @mihaicostin34 , yes, indeed it is open, don't hesitate to let us know if we can be of help.

In addition to the OCaml-related channels, Coq-related Dune development is usually coordinated using Coq's Zulip, Dune channel https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users feel free to stop by if you have any question.

[mihaicostin34]

Just making sure I understood correctly : a new command should be added (like dune coq init or dune init coq, with arguments to specify wether a theory or a plugin is wanted) which should create a basic coq project, something similar to what is shown here: https://dune.readthedocs.io/en/stable/coq.html#examples Is that correct?

[mihaicostin34]

Hi @mihaicostin34 , yes, indeed it is open, don't hesitate to let us know if we can be of help.

In addition to the OCaml-related channels, Coq-related Dune development is usually coordinated using Coq's Zulip, Dune channel https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users feel free to stop by if you have any question.

Thank you!

[ejgallego]

Just making sure I understood correctly : a new command should be added (like dune coq init or dune init coq, with arguments to specify wether a theory or a plugin is wanted) which should create a basic coq project, something similar to what is shown here: https://dune.readthedocs.io/en/stable/coq.html#examples Is that correct?

It seems right to me! I'm not sure if dune coq init is preferred to dune init coq, but this should be easy to tweak once a PR has been submitted.

[mihaicostin34]

Hello! I've been having some trouble figuring out how the Stanza and Encoder modules tie together for the creation of stanzas as csts. Could anyone provide some more explanations/clarifications please?