Stream: Dune devs & users

Topic: Generating .v files with non-ocaml in-repo executable

Paolo Giarrusso (Dec 13 2020 at 02:10):

Just wrote my first code-generation rule... it seems the action can just be (run cpp2v ...) as long as the cpp2v binary is either in the PATH or declared with e.g. (install (section bin) (files cpp2v) (package coq-cpp2v-bin)) elsewhere in the same workspace

Paolo Giarrusso (Dec 13 2020 at 02:11):

that setup seems to work well, but does it make sense?

Emilio Jesús Gallego Arias (Dec 13 2020 at 15:56):

Yes, binaries are resolved like libraries, following a set of rules that hierarchical in nature, if the binary is present in the workspace dune will resolve it to the local copy. There are more advanced setups using (env ...) , see https://dune.readthedocs.io/en/stable/dune-files.html#env

Emilio Jesús Gallego Arias (Dec 13 2020 at 15:57):

that's mainly useful for binaries that are private but would like to be setup in path locally

Emilio Jesús Gallego Arias (Dec 13 2020 at 15:57):

so you don't need to install it to make it available locally

Paolo Giarrusso (Dec 13 2020 at 20:27):

oh cool

Paolo Giarrusso (Dec 13 2020 at 20:28):

but "binary is present in the workspace" cannot be correct if a "workspace" refers to a part of the filesystem. I can't see where the docs define it otherwise.

Paolo Giarrusso (Dec 13 2020 at 20:30):

let's just say: that the "workspace" is not a filesystem part is not obvious from https://dune.readthedocs.io/en/stable/overview.html#terminology.

Emilio Jesús Gallego Arias (Dec 13 2020 at 21:59):

Indeed, please open issues / suggest improvements, last Dune dev meeting was very focused on the documentation and all devs agree that there is a problem with it.

Emilio Jesús Gallego Arias (Dec 13 2020 at 21:59):

But present in this sense it means it will be installed as a public binary IIUC.

Paolo Giarrusso (Dec 13 2020 at 23:04):

Submitted https://github.com/ocaml/dune/issues/4031 and https://github.com/ocaml/dune/pull/4032, but now I suspect run should use exe:<prog> not bin:<prog>

Paolo Giarrusso (Dec 13 2020 at 23:05):

(or that I'm too hopelessly confused to try writing docs)

Emilio Jesús Gallego Arias (Dec 14 2020 at 00:30):

Very nice, thanks!

Emilio Jesús Gallego Arias (Dec 14 2020 at 00:31):

Indeed I got to know the meaning of these parts because I looked at the source code

Emilio Jesús Gallego Arias (Dec 14 2020 at 00:31):

and asked the devs, as I wanted to understand how (run coqc ....) would work.

Emilio Jesús Gallego Arias (Dec 14 2020 at 00:32):

and indeed there are some hardcoded rules for .opt .exe etc....

Last updated: Jun 04 2023 at 23:30 UTC