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
that setup seems to work well, but does it make sense?
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
that's mainly useful for binaries that are private but would like to be setup in path locally
so you don't need to install it to make it available locally
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.
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.
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.
But present in this sense it means it will be installed as a public binary IIUC.
Submitted https://github.com/ocaml/dune/issues/4031 and https://github.com/ocaml/dune/pull/4032, but now I suspect
run should use
(or that I'm too hopelessly confused to try writing docs)
Very nice, thanks!
Indeed I got to know the meaning of these parts because I looked at the source code
and asked the devs, as I wanted to understand how
(run coqc ....) would work.
and indeed there are some hardcoded rules for
Last updated: Oct 16 2021 at 09:07 UTC