Stream: Dune devs & users

Topic: Generated files dependency


view this post on Zulip Li-yao (Nov 30 2020 at 16:48):

I have a project where some .v files are generated, using a custom rule. I'm curious how exactly dune figures out that the .v file is part of a library, so that it generates that file before building the Coq code (in particular, I'm guessing it needs to run coqdep after generating the Coq file).

  1. Does it simply execute rules before doing anything else? But then how would it handle rules that depend on products of the standard build process so they need to run after it, e.g., .vo files, or worse, if you need to look at a .vo to generate another .v down the line?

  2. Does it hardcode some behavior about standard extensions like .v?

  3. Or is it a fluke that things build in my case and is there a stanza to explain how the generated files relate to the overall library?

view this post on Zulip Paolo Giarrusso (Nov 30 2020 at 17:05):

I looked into this setup, and IIUC, what matters is that the rules specify the output name

view this post on Zulip Paolo Giarrusso (Nov 30 2020 at 17:05):

and (I assume) having a rule producing a .v file should have the same effect as having the actual .v file there

view this post on Zulip Paolo Giarrusso (Nov 30 2020 at 17:06):

(so dune doesn't need to run all rules first, and that doesn't work in general)

view this post on Zulip Paolo Giarrusso (Nov 30 2020 at 17:09):

and IIUC, point 2. holds — the theories stanza knows to find all .v files under the given folder (or sth similar)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 30 2020 at 19:06):

@Li-yao , Dune can compute the targets of the rules statically without having to run them, this is akin to static analysis and is described in the paper "Selective Applicative Functors" https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf

view this post on Zulip Emilio Jesús Gallego Arias (Nov 30 2020 at 19:07):

Indeed, for a (coq.theory ...) , the standard means all .v files generated under the directory scope.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 30 2020 at 19:08):

a kind of *.v but where the view of the filesystem includes generated files

view this post on Zulip Emilio Jesús Gallego Arias (Nov 30 2020 at 19:09):

So rules are run twice, first, as a static analysis to compute targets, second, the actual run on-demand

view this post on Zulip Emilio Jesús Gallego Arias (Nov 30 2020 at 19:09):

Knowing targets is pretty important for a few reasons, in particular to have sound _incremental_ builds in the presence of deletions

view this post on Zulip Li-yao (Nov 30 2020 at 19:15):

Emilio Jesús Gallego Arias said:

a kind of *.v but where the view of the filesystem includes generated files

That makes a lot of sense. Thanks for the responses!

view this post on Zulip Li-yao (Nov 30 2020 at 19:26):

Does dune support situations where such analysis cannot be done statically, say, where you might want a custom script to compute dependencies? Just idly wondering about a very dynamic but completely hypothetical metaprogramming scenario.

view this post on Zulip Rudi Grinberg (Nov 30 2020 at 19:42):

Li-yao said:

Does dune support situations where such analysis cannot be done statically, say, where you might want a custom script to compute dependencies? Just idly wondering about a very dynamic but completely hypothetical metaprogramming scenario.

Computing dynamic dependencies is fully supported. The mental model we should use is that dune must decide val is_target : Path.t -> bool without executing any build rules. However, val deps_of : Path.t -> deps will require building (exactly when dynamic dependencies are present).

view this post on Zulip Gregory Malecha (Dec 20 2020 at 15:07):

What would be required to lift the restriction on is_target?

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

I guess allowing it to call build rules, not expert enough tho as to evaluate impact on the codebase.

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

@Gregory Malecha why is that a problem for your use case?

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

For Coq / OCaml we can compute the set of targets without having to do any build, usually from the configuration parameters / flags.

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

Actually I'm not sure how far we can go with flags, as flags may require building.

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

@Li-yao deps are fine, as Rudi notes, targets is where the restrictions are, that is to say, objects produced.

view this post on Zulip Gregory Malecha (Dec 20 2020 at 15:28):

You might not know what your dependencies are until you start computing dependencies. I guess if it really is a function, I could just make it a constant function to true and rely on laziness to not try to computer it all

view this post on Zulip Gregory Malecha (Dec 20 2020 at 15:30):

I guess concretely, foo.v depends on foo_hpp.v which is generated from foo.hpp and depends on any file that is included by foo.hpp

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

That's fine, we were talking about targets.

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

Dynamic deps are fine.

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

Dynamic targets are not supported, and that's a limitation in some cases. But indeed, there are totally different concepts.

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

Your case is fine today, if we were not able to do this, nothing would work in the first place, as even for a simple .v file we have to compute foo.v.d using coqdep, and that requires building. Then we parse that file to compute the deps for foo.v.

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

In code:

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

  let coqdep_rule = coqdep_rule cctx ~source_rule ~file_flags coq_module in

  (* Process coqdep and generate rules *)
  let deps_of = deps_of ~dir:cctx.dir ~boot_type:cctx.boot_type coq_module in

  (* Rules for the files *)
  { Module_rule.coqdep = coqdep_rule
  ; coqc =
      Build.with_no_targets deps_of >>> coqc_rule cctx ~file_flags coq_module
  }

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

That adds two rules:

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

Note that the first rule has additional dependencies, as coqdep must be called with all the relevant source files present, which can be indeed generated

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

by arbitrary rule, but that's transparent

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

That's the code for coqdep_rule:

  Build.with_no_targets cctx.mlpack_rule
  >>> Build.with_no_targets source_rule
  >>> Command.run ~dir:(Path.build cctx.dir) ~stdout_to cctx.coqdep file_flags

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

hopefully to be cleaned up in the future when coqdep has a -modules mode

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

coqc_rule only sets flags and just calls coqc

view this post on Zulip Gregory Malecha (Dec 20 2020 at 15:49):

I guess I was figuring that I didn't know about foo_hpp.v until I read it from the dependencies of foo.v since it probably doesn't exist on the file system yet

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

That's fine, as long as there is a rule to generate foo_hpp.v dune will know it may exist

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

that's actually one of the reasons that target are important to be known "statically"

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

but in this case you know statically

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

tho for example the current coqdep pitfall will have dune generate foo_hpp.v before the coqdep call

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

so things work, but you are not as parallel as you would like

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

tho some workarounds do exist

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

until we fix coqdep

view this post on Zulip Gregory Malecha (Dec 20 2020 at 15:52):

I'm wondering about the case where foo_hpp.v might have additional dependencies that we don't know about.

view this post on Zulip Gregory Malecha (Dec 20 2020 at 15:53):

It sounds like I could get dune to do this for me, by trying to statically compute the graph

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

That's fine

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

nothing is special

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

just regular rules with deps and targets

view this post on Zulip Gregory Malecha (Dec 20 2020 at 15:54):

But I can't run coqdep on foo_hpp.v because it doesn't exist until the build phase

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

that's fine, dune supports dynamic deps

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

dependencies for foo_hpp.v will be generated on-the-fly

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

when someone needs that file

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

the unfortunate thing today is that coqdep requires that file

view this post on Zulip Gregory Malecha (Dec 20 2020 at 15:55):

Yes

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

so build too much, but if that's a problem you can use some workarounds we have discussed with Paolo

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

fixing coqdep is planned, but it is not easy due to the semantics of require requiring the whole set of .v files to be present in the file system

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

but Abishek patch should land sometime soon, tho it is far from a general solution

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

OCaml was in the same situation, but if I am not mistaken -modules was implemented precisely for dune

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

however OCaml is easy as you cannot do open Foo.*.Bar

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

as in Coq

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

Well once could imagine having coqdep output that kind of deps, and Dune could indeed match as it knows the resulting filesystem layout without having to run the build rules

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

but that seems like a tricky / costly patch :)

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

I'd dare to say that using the split workaround we discussed you would still max out a reasonable number of cores

view this post on Zulip Gregory Malecha (Dec 20 2020 at 15:58):

You have convinced me that dune can be made to do what I want. I just need to build a closed world by pre-conputing a bunch of rules before invoking dune, and maybe do all of my coq generation during that phase (or over-approximate the dependencies of the generated files)

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

I'm not sure you need to do that tho

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

you should certianly not over-approximate anything

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

that's the job of dune

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

your job is just to output the rules

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

then dune will figure out how to build them

view this post on Zulip Gregory Malecha (Dec 20 2020 at 16:00):

Well, I need something to determine if I should rebuild a _hpp.v file

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

that's not your job, but dune's

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

yes, you need the rule for the file

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:01):

which is of the form {deps} -[action]-> {targets}

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:01):

as in Make

view this post on Zulip Gregory Malecha (Dec 20 2020 at 16:02):

So as long as every file that is #included in that file is listed as a build target, I should be ok

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:03):

Indeed as long as the deps are "sound", you are fine

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:03):

the rest you don't care

view this post on Zulip Gregory Malecha (Dec 20 2020 at 16:03):

I will need to look at your rule above and see how it can work.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:03):

You can perfectly depend on something that does not exist

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:03):

dune will look up for a rule to build it

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:03):

etc...

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:03):

it is nicer than make as if rules are inconsistent you directly get an error

view this post on Zulip Gregory Malecha (Dec 20 2020 at 16:03):

It looks like ocaml. Does that mean that I need to modify the dune sources? Or is there another way to hook into the system?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:04):

I'd start with the rules language

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:04):

https://dune.readthedocs.io/en/stable/dune-files.html#rule

view this post on Zulip Gregory Malecha (Dec 20 2020 at 16:05):

Thanks.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:05):

YW

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:05):

You can go a long way just by writing dune files

view this post on Zulip Gregory Malecha (Dec 20 2020 at 16:06):

I can't look at it in depth right now, but I will try to look at it later. I'm still interested in the original question "why not support dynamic targets?"

view this post on Zulip Gregory Malecha (Dec 20 2020 at 16:06):

But it is maybe just an interest, not a requirement

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:06):

Core dune devs can answer this more accurately, but I understand it is just a limitation of the implementation as of today that will be lifted

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:07):

but intutitively makes a lot of things simpler

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:07):

keep in mind the incremental nature / speed

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:07):

it really helps rule processing to be able to determine targets statically

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:08):

I am writing some notes how the build engine works, so that should give a better pic, the question is pretty technical. For example, you have some heuristic that asks if targets in a directory have changed, etc...

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:08):

or rules

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:08):

the idea is to be able to skip as much work as posssible in an incremental build

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:10):

and dynamic targets seem pretty rare

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:10):

usually a rule knows what is going to generate without having to run anything

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:11):

more details on this paper https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:11):

rules of the from "do some build, based on the result generate foo.vo or else bar.vo" are pretty rare

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:12):

and moreover they tend to have bad properties

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:12):

example for coq native

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 16:12):

it is much better to have two rules , one for cmxs and one for vo

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

than a single rule for both , where targets depend on some build info

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

you get much better parallelism I conjecture

view this post on Zulip Gregory Malecha (Dec 20 2020 at 16:42):

I am not advocating for rules that might generate one target or another. That seems unnecessary. I am asking about determining dynamically what is a target. As I mentioned above, making is_target _ = true would be fine.

view this post on Zulip Gregory Malecha (Dec 20 2020 at 18:12):

So, I just need to generate a rule for each file. It will look like (rule (target foo_hpp.v) (action "cpp2v ...") (deps ...???..))

view this post on Zulip Gregory Malecha (Dec 20 2020 at 18:12):

It seems like I need to invoke gcc to get the dependencies to deal with transitive #include.

view this post on Zulip Gregory Malecha (Dec 20 2020 at 18:12):

And I might need to update these rules each time that I build to make sure that the deps line is up-to-date

view this post on Zulip Gregory Malecha (Dec 20 2020 at 18:12):

Is there something that I am missing?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 18:46):

Yup, dune knows about C files so maybe you don't need to do that

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 18:46):

Indeed, there is support for generating that rules, that's how first implemented Coq's dune support, once we were happy we wrote them in ML

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 18:47):

Dune can already build C and C++ stuff as it is very often needed for OCaml

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 18:47):

so the rule you propose is right

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 18:47):

what does cpp2v need

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 18:47):

not only the hpp file?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 18:48):

dune supports rule sandboxing, that is, it will call each rule on a restricted setup where only the deps are present, that's useful for debugging

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 18:49):

If what you need in terms of C / C++ support is already not there I'd be surprised it can't be added easily, as dune knows already how to call cpp etc...

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 18:49):

to get deps

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 18:49):

Then, once you have your (rule ...) dune can cache it

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 18:50):

as long as it is deterministic

view this post on Zulip Gregory Malecha (Dec 20 2020 at 19:09):

cpp2v needs the c/c++ file and all transitive dependencies (for #include)

view this post on Zulip Gregory Malecha (Dec 20 2020 at 19:09):

It is very similar to a compiler, but generates a .v rather than a .o

view this post on Zulip Gregory Malecha (Dec 20 2020 at 19:12):

It seems like the limitation is in the language for specifying dependencies

view this post on Zulip Gregory Malecha (Dec 20 2020 at 19:14):

E.g. if I could write (deps (c_deps_of foo.hpp)), that would solve the problem (of course I would need to specify all of the proper command-line options, but that would be fine)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 19:36):

Indeed, but I'm not sure how the rule for foo.hpp looks currently [I'm unfamiliar with that part of the code] , maybe it already pulls these deps

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 19:37):

what does dune rules say if you add the hpp file as a dep

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 19:37):

[maybe try with a single .h fle]

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 19:37):

file

view this post on Zulip Rudi Grinberg (Dec 20 2020 at 19:41):

Gregory Malecha said:

I can't look at it in depth right now, but I will try to look at it later. I'm still interested in the original question "why not support dynamic targets?"

We'll support them eventually. The reason for not supporting them now is completely practical. Currently our rule generation functions rely on various functions of the form:

(** Returns the set of targets in the given directory. *)
val targets_of : dir:Path.t -> Path.Set.t

To make it possible for such functions be dynamic, they need to run inside our concurrency monad used for executing rules. But that will require changing every single rule generation function we have to use the damned concurrency monad. In summary, it's just a massive, but mostly mechanical change.

view this post on Zulip Rudi Grinberg (Dec 20 2020 at 19:52):

Gregory Malecha said:

E.g. if I could write (deps (c_deps_of foo.hpp)), that would solve the problem (of course I would need to specify all of the proper command-line options, but that would be fine)

As far as I understand, you need something like:

(rule
 (deps (glob_files *.cpp *.hpp))
 (action (with-stdout-to foo.cxx.deps (gcc -MM foo.cpp))))

(rule
 (targets foo.v)
 (deps foo.cxx (:include foo.cxx.deps))
 (action (run cpp2v foo.cxx -o %{targets})))

The only catch is that (:include ..) isn't supported inside deps yet. There's no problem with adding support for that. We already have this feature, we just simply haven't exposed supported for it in the frontend.

view this post on Zulip Rudi Grinberg (Dec 20 2020 at 19:57):

Emilio Jesús Gallego Arias said:

Yup, dune knows about C files so maybe you don't need to do that

Dune knows how to build C sources, but the rules are naive. It just assumes that any .o target depends on the corresponding .cpp target along with all header files dune knows about. The right way is to use gcc -MM to get actual dependencies. The janestreet folks might be working on this since they have some more complex C/C++ builds they need to port to dune.

view this post on Zulip Gregory Malecha (Dec 20 2020 at 20:03):

@Rudi Grinberg can you not use naive liftings into the concurrency monad? Something like liftM? (This is a very naive statement)

Thanks for the suggestions. It seems like :include would be great for this purpose. With richer primitives like this, can you do more in the rule language and less in ocaml?

view this post on Zulip Rudi Grinberg (Dec 20 2020 at 20:16):

can you not use naive liftings into the concurrency monad? Something like liftM? (This is a very naive statement)

I tried that already, but it's not so simple. We have some folds of the form:

val fold : file_tree -> f:('a -> 'acc -> 'acc) -> 'acc - >'acc

That would need to be called with 'a -> 'acc -> 'acc Monad.t now. So now we need to rewrite a bunch of these folds as well. The monads end up contaminating quite a bit of code this way. In any case, we'll try to get this limitation lifted in 2021. It's getting in the way of improving a lot of things in dune.

Thanks for the suggestions. It seems like :include would be great for this purpose. With richer primitives like this, can you do more in the rule language and less in ocaml?

Yes, that's the goal.

Though we are actually leaning towards providing more OCaml api's where possible. For example, we have an action plugin: https://dune.readthedocs.io/en/stable/dune-libs.html#experimental-dune-action-plugin. It allows you to discover dependencies as you're running a custom action:
https://github.com/ocaml/dune/blob/master/otherlibs/action-plugin/src/dune_action_plugin.mli
You'll need to write your action in OCaml, but it will be more natural for you to handle dependencies. E.g. you could just call read_file inside cpp2v instead of having a separate dependency discovery command. (Limitations on targets still apply)

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

to be clear, can dune parse the -MM syntax today?

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

OTOH, I think the rule for foo.cxx.deps can't be written in dune for _different_ reasons — you need the right compiler flags, which are specified in a different build system

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

but IIUC the rule for .deps could delegate to make.

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

And in fact, since cpp2v needs the same flags, we'd probably do the same to call cpp2v foo.cxx

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

I'm unsure how to force dune to always call make; (deps (universe)) _might_ do that, based on https://dune.readthedocs.io/en/stable/dune-files.html#rule and https://dune.readthedocs.io/en/stable/concepts.html#deps-field, but I'd need to try — it might not work, depending on the formal semantics of:

In any case, this is only for dependencies in the installed world, you must still specify all dependencies that come from the workspace.

view this post on Zulip Rudi Grinberg (Dec 20 2020 at 20:35):

Paolo Giarrusso said:

to be clear, can dune parse the -MM syntax today?

It doesn't. There hasn't been a need yet.

view this post on Zulip Rudi Grinberg (Dec 20 2020 at 20:36):

Paolo Giarrusso said:

I'm unsure how to force dune to always call make; (deps (universe)) _might_ do that, based on https://dune.readthedocs.io/en/stable/dune-files.html#rule and https://dune.readthedocs.io/en/stable/concepts.html#deps-field, but I'd need to try — it might not work, depending on the formal semantics of:

In any case, this is only for dependencies in the installed world, you must still specify all dependencies that come from the workspace.

Or you could just over-approximate the deps and depend on the entire source of the make build (deps (source_tree .))

view this post on Zulip Rudi Grinberg (Dec 20 2020 at 20:38):

Wrapping some existing build script written in make is something that is quite common in dune by the way. There are many examples around and you shouldn't shy away from it.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2020 at 21:46):

flags can be handled with include , at the end you have a set of rules and most of them should fit into dune's definition of rule so things should work

view this post on Zulip Paolo Giarrusso (Dec 20 2020 at 23:08):

since dune doesn't understand make and the logic for flags isn't trivial, I'd rather not duplicate it.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 21 2020 at 10:37):

I mean that you can have the flags generated into a file that is shared by both dune and Make, indeed, it should not be duplicated.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 21 2020 at 10:39):

All this discussion made me think that a bit of more documentation on how dune works and the engine vs rules is could be helpful.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 21 2020 at 10:40):

Indeed it seems that people strongly associate dune to something OCaml-specific, however the underlying build engine is fairly generic [with some choices that could matter in some other use cases], in fact this is already captured reasonably in the structure of the code with dune_engine and dune_rules directories.

view this post on Zulip Gregory Malecha (Dec 21 2020 at 12:20):

The reason that I associate it with Ocaml is because the rule language does not currently seem powerful enough to do anything deep (discussion above, though maybe I simply don't understand it), and the only language support in the code base is for Coq and Ocaml. There is great support for both, but if you want to add anything else, your options are limited.

Comparing only the rules language (which seems to be the public API), dune seems less expressive than make since it doesn't have pattern rules. It seems kind of like making windows calc the interface to a super-computer.

view this post on Zulip Gregory Malecha (Dec 21 2020 at 12:31):

@Rudi Grinberg Are there any examples of the action plugin in use? From what you linked, it isn't even clear the type of the function that I need to implement, what it should do, or how to make it accessible to dune.

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

Indeed, the rule language is more like rule assembler and pretty declarative [which brings other advantages] , so you have to do some generation. As I commented on SO, at first we implemented dune support in Coq generating dune files, that was pretty easy tho. I like that dune language is more declarative and less expressive, that brings some interesting advantages and elegance. I think Bazel / Ninja have similar concepts right?

See https://github.com/ocaml/dune/tree/master/otherlibs/action-plugin for exapmles / tests

view this post on Zulip Rudi Grinberg (Dec 21 2020 at 17:21):

@Gregory Malecha That's a fair assessment. Dune aims to be a first class build system for OCaml, Coq, and C/C++. Being a good general purpose build system is a secondary goal.

view this post on Zulip Notification Bot (Dec 21 2020 at 18:27):

This topic was moved here from #Coq devs & plugin devs > Debugging CI issue with output redirect by Théo Zimmermann

view this post on Zulip Gregory Malecha (Dec 21 2020 at 18:45):

@Rudi Grinberg it achieves its goals very well. I just wish I could use it more :smiley:

view this post on Zulip Rudi Grinberg (Dec 21 2020 at 18:50):

Out of curiosity, Is the project where you're looking for a build system public? I'd like to see how complex it is.

view this post on Zulip Paolo Giarrusso (Dec 21 2020 at 18:52):

Bazel doesn't require code generation and allows abstracting over rules (https://docs.bazel.build/versions/3.7.0/skylark/macros.html)...

OTOH, the action plugin might be what we need :-)

view this post on Zulip Paolo Giarrusso (Dec 21 2020 at 18:55):

(hm still some codegen needed).

view this post on Zulip Gregory Malecha (Dec 21 2020 at 18:56):

There is a version that is public.

view this post on Zulip Gregory Malecha (Dec 21 2020 at 18:57):

But I don't think that it has all of the interesting c++ stuff

view this post on Zulip Gregory Malecha (Dec 21 2020 at 18:57):

github.com/bedrocksystems/cpp2v

view this post on Zulip Rudi Grinberg (Dec 21 2020 at 19:02):

Do you use OCaml at all?

view this post on Zulip Paolo Giarrusso (Dec 21 2020 at 19:26):

Some of our C++ code is also public. Here's a link to some of the flag-setting code https://github.com/bedrocksystems/NOVA/blob/b438f903323e557e66055d5e26ca0b8d8786149e/Makefile#L84-L131 (fixed)

view this post on Zulip Paolo Giarrusso (Dec 21 2020 at 19:45):

also, that involves different stakeholders. So it's good that dune _can_ delegate to make :-)

view this post on Zulip Gregory Malecha (Dec 21 2020 at 22:52):

We do use Ocaml. Currently we have two plugins in non-public repositories.

view this post on Zulip Gregory Malecha (Jan 07 2021 at 02:21):

Rudi Grinberg said:

Gregory Malecha said:

E.g. if I could write (deps (c_deps_of foo.hpp)), that would solve the problem (of course I would need to specify all of the proper command-line options, but that would be fine)

As far as I understand, you need something like:

(rule
 (deps (glob_files *.cpp *.hpp))
 (action (with-stdout-to foo.cxx.deps (gcc -MM foo.cpp))))

(rule
 (targets foo.v)
 (deps foo.cxx (:include foo.cxx.deps))
 (action (run cpp2v foo.cxx -o %{targets})))

The only catch is that (:include ..) isn't supported inside deps yet. There's no problem with adding support for that. We already have this feature, we just simply haven't exposed supported for it in the frontend.

How difficult would this be to add? I could try to hack on it if it wasn't too much work, but I know nothing of the internals of dune, so there would be some learning curve.

view this post on Zulip Rudi Grinberg (Jan 07 2021 at 02:41):

@Gregory Malecha I'd just make a ticket on the bug tracker. Then I can bring it up in the dune dev meeting

view this post on Zulip Gregory Malecha (Jan 07 2021 at 04:40):

Looking at what you wrote again, it seems like it will re-compute the dependency files on every invocation of dune where any cpp or hpp file changed. Is this true?

view this post on Zulip Paolo Giarrusso (Jan 07 2021 at 18:44):

Seems true; in fact, that rule doesn't have enough dependencies.

view this post on Zulip Paolo Giarrusso (Jan 07 2021 at 18:45):

IIRC, the real rule is that the .cxxdeps files should depend on all the included headers, after the first run; gcc's output might account for that, as long as you use make.

view this post on Zulip Rudi Grinberg (Jan 07 2021 at 23:44):

Gregory Malecha said:

Looking at what you wrote again, it seems like it will re-compute the dependency files on every invocation of dune where any cpp or hpp file changed. Is this true?

Yes, that seems wrong. Don't know what i was thinking, I think it should only depend on foo.cpp.

view this post on Zulip Rudi Grinberg (Jan 08 2021 at 00:46):

Paolo Giarrusso said:

IIRC, the real rule is that the .cxxdeps files should depend on all the included headers, after the first run; gcc's output might account for that, as long as you use make.

This is similar to what we do with ocamldep. It's possible to express this dependency using the following make pseaudo syntax:

%.cxx.deps: %.cxx
%.cxx.transitive-deps: %.cxx.deps
  # the action will read the direct deps and then discover more

In any case, if you make the issue I think the team will just decide to add 1st class support for C/C++ then making you go through all this low level hackery.

view this post on Zulip Gregory Malecha (Jan 08 2021 at 02:51):

Opened https://github.com/ocaml/dune/issues/4089

view this post on Zulip Thomas Letan (Jan 26 2021 at 12:03):

Hi! I can’t find the changelog for the 0.3 version of coq language in Dune

view this post on Zulip Thomas Letan (Jan 26 2021 at 12:04):

Any hint?

view this post on Zulip Paolo Giarrusso (Jan 26 2021 at 12:21):

(Wrong thread?)

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2021 at 12:47):

@Thomas Letan there is a basic attempt to a changelog here https://dune.readthedocs.io/en/stable/dune-files.html#coq-theory , which is badly rendered by the way. We should improve it.

view this post on Zulip Thomas Letan (Jan 26 2021 at 12:49):

(yes, sorry!)


Last updated: Oct 16 2021 at 07:02 UTC