Dune + Coq + Menhir

[liyishuai]

Desired Behavior

Allow generating Parser.v from Parser.vy, and using it in the (coq.theory) stanza.

Example

(coq.theory
 (name JSON)
 (package coq-json)
 (synopsis "JSON in Coq"))

(menhir
 (modules Parser)
 (flags --coq)
)

Currently:

Error: I can't determine what library/executable the files produced by this stanza are part of.

File "./theories/Lexer.v", line 1, characters 0-37: Error: Cannot find a physical path bound to logical path Parser with prefix JSON.

[ejgallego]

Hi @liyishuai , this should be pretty easy to add.

The problem is that the menhir stanza doesn't recognize the --coq flag, and in particular it doesn't know that a .v file will be producded.

In order to fix this, go to src/dune_rules/menhir/menhir_rules.ml, and add next to both calls of

    let* explain_flags = explain_flags base stanza in

a Coq version coq_flags that will detect if the --coq flag has passed, then add to the target list the .v file generated.

I'd be happy to do a seed PR, but I'd like help to write the test case(s).

[liyishuai]

I have an active repo https://github.com/liyishuai/coq-json that can serve as the test case (feel free to move everything under theories/).

[ejgallego]

Thanks @liyishuai , unfortunately that repos is too heavy for Dune's CI.

In order to add a test case to Dune, we should do something self-contained (that can work with coq-stdlib).

[liyishuai]

Official example, currently Makefile-based: https://github.com/LexiFi/menhir/tree/master/demos/coq-minicalc

[Shark-with-Blue-Shoes]

@liyishuai @ejgallego

This issue has been open for quite some time, if you don't intend to solve it, I found a workaround.

You can do something like ->

(rule
 (target Parser.v)
 (deps items.vy expr.vy program.vy stmt.vy tokens.vy types.vy)
 (action
  (run menhir --coq --coq-no-version-check --base program %{deps})))

This should compile multiple files into one target, but you can remove --base program to only do one

(rule
 (target Parser.v)
 (deps items.vy expr.vy program.vy stmt.vy tokens.vy types.vy)
 (action
  (run menhir --coq --coq-no-version-check %{deps})))