I am using menhir with dune with this stanza:
(menhir (modules parser) (flags ("--dump" "--explain")))
It works all fine, except that the
.automaton file created cause of the
--dump option vanishes after a rebuild. If I do
dune clean; dune build it is there. If I do another
dune build it is gone. Is this a bug or do I have to tell in the stanza that extra files are generated?
Dune is meant to clean up stale/stray outputs... But is there any syntax to inform dune of extra outputs in a stanza?
But it's somewhat easy to tell dune to use a different menhir binary, say a shell script wrapping the real thing; that could move the extra output in a tmp folder and print the path. Let me find an example...
Example wrapping coqc: https://gitlab.mpi-sws.org/iris/refinedc/-/blob/f737129161b2cf92e536f1c3a69795147c0fb6fc/dune#L2-8
The script is placed on the PATH as coqc, so it uses opam exec to find the real binary: https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/tools/coqc_timing.sh
Credits to Rodolphe Lepigre for teaching me this trick (but he's on vacation so not sure I should tag him?)
@Michael Soegtrop , this is a bug in Dune, issue https://github.com/ocaml/dune/issues/3284 is related. I'd suggest you open an issue about it.
The bug is that indeed Dune should understand Menhir's flags and then keep
.automaton as an output. As it does not, it cleans up stray outputs [which is needed for soundness of incremental builds in general]
Of course you could write your own rule to call menhir, built-in rules just call menhir:
(run /home/egallego/.opam/dev-coq-lsp/bin/menhir src/parser.mly --base src/parser --infer-write-query src/parser__mock.ml.mock))))
Last updated: Jun 03 2023 at 18:01 UTC