Stream: Dune devs & users

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


view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 02:11):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 15:57):

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

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 20:27):

oh cool

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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>

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 23:05):

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 14 2020 at 00:30):

Very nice, thanks!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 14 2020 at 00:32):

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


Last updated: Oct 16 2021 at 09:07 UTC