Using dune to build a package of a verifiied programming language

[DasNaCl]

Suppose I want to build a programming language where parts of its tooling and whatnot are verified.
Naturally, I'd use menhir to build a parser and make use of the (menhir ...) stanza to generate the parser.
However, given the verification nature, I want to invoke menhir --coq, so the output file of menhir ends with v instead of ml. Then, by means of Coq's extraction mechanism, I want to actually build the ml file of the parser and use it in a minimal ocaml project that just invokes the extracted Coq functions.

(coq.theory
  (name MiniCalc)
  (package coq-minicalc)
  (theories MenhirLib)
  )
(executable
  (name minicc)
  (libraries MiniCalc.Parser)
  )
(menhir
  (modules MiniCalc.Parser)
  (flags (:standard --coq --coq-no-complete))
  )
(coq.extraction
  (prelude MiniCalc)
  (extracted_modules MiniCalc.Parser)
  )
(include_subdirs qualified)

Here is an example repo: https://codeberg.org/dasnacl/MiniCalc

[Alizter]

So this is a feature request for a menhir like stanza for the Coq mode. I guess we could design a coq.menhir stanza which acts very much like menhir but for using menhir in Coq mode. We (the Coq part of the Dune team) don't currently have any plans to do so, but I don't see any reason it shouldn't be possible.

[DasNaCl]

Thanks for the reply!
I didn't know that this wasn't implemented. Can't the menhir stanza be given an option to switch between .ml and .v files as targets?
I tried to implement a coq.menhir stanza by mostly copy-pasting the menhir stuff, but I got some internal exception in dune and given that I don't feel qualified to contribute at all, it'd be nice to either get some guidance for such a contribution (I guess this also warrants more discussion on how the stanza should look) or to know that this will become part of the plan the dune team responsible for Coq has.
Thanks again for the reply! :)

[Alizter]

If you like, you can open a draft PR with your changes and I can give you some (async) pointers about how to modify the code.

[ejgallego]

Maybe you could write the menhir call as a (rule ...) . IMHO that would be a first good step towards extending Menhir mode to produce Coq output.