Stream: Dune devs & users

Topic: menhir: .automaton file vanishes in rebuild

Michael Soegtrop (Dec 20 2022 at 08:24):

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?

Paolo Giarrusso (Dec 20 2022 at 08:39):

Dune is meant to clean up stale/stray outputs... But is there any syntax to inform dune of extra outputs in a stanza?

Paolo Giarrusso (Dec 20 2022 at 08:51):

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...

Paolo Giarrusso (Dec 20 2022 at 08:53):

Example wrapping coqc: https://gitlab.mpi-sws.org/iris/refinedc/-/blob/f737129161b2cf92e536f1c3a69795147c0fb6fc/dune#L2-8

Paolo Giarrusso (Dec 20 2022 at 08:54):

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

Paolo Giarrusso (Dec 20 2022 at 08:56):

Credits to Rodolphe Lepigre for teaching me this trick (but he's on vacation so not sure I should tag him?)

Emilio Jesús Gallego Arias (Dec 20 2022 at 10:20):

@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]

Emilio Jesús Gallego Arias (Dec 20 2022 at 10:23):

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: Oct 13 2024 at 01:02 UTC