search

ocaml / dune

A composable build system for OCaml.
https://dune.build/
MIT License
1.62k stars 401 forks source link

dune init should support Coq projects #7087

Open Alizter opened 1 year ago

Alizter commented 1 year ago

We should add two templates to dune init:

  1. A coq theory
  2. A coq plugin

Should be simple to do.

mihaicostin34 commented 1 month ago

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

nojb commented 1 month ago

Yes, it is. Have at it!

ejgallego commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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?