Li-yao (Nov 30 2020 at 16:48): 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).
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?
Does it hardcode some behavior about standard extensions like .v?
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?
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
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
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)
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)
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
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.
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
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
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
Li-yao (Nov 30 2020 at 19:15):Emilio Jesús Gallego Arias said:
a kind of
*.vbut where the view of the filesystem includes generated files
That makes a lot of sense. Thanks for the responses!
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.
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).
Gregory Malecha (Dec 20 2020 at 15:07):What would be required to lift the restriction on is_target?
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.
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:24):@Gregory Malecha why is that a problem for your use case?
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.
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.
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.
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
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:36):That's fine, we were talking about targets.
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:36):Dynamic deps are fine.
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.
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.
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:38):In code:
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
}
That adds two rules:
foo.v -> foo.v.dfoo.v.d and does two sequential steps: building all the deps of foo.v, then building foo.vo 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
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:42):by arbitrary rule, but that's transparent
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
hopefully to be cleaned up in the future when coqdep has a -modules mode
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:43):coqc_rule only sets flags and just calls coqc
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
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
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"
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:51):but in this case you know statically
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:52):so things work, but you are not as parallel as you would like
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:52):tho some workarounds do exist
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:52):until we fix coqdep
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.
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:53):That's fine
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:53):nothing is special
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:53):just regular rules with deps and targets
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:54):that's fine, dune supports dynamic deps
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:54):dependencies for foo_hpp.v will be generated on-the-fly
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:54):when someone needs that file
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:55):the unfortunate thing today is that coqdep requires that file
Gregory Malecha (Dec 20 2020 at 15:55):Yes
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
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
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
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:56):however OCaml is easy as you cannot do open Foo.*.Bar
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:56):as in Coq
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:57):but that seems like a tricky / costly patch :)
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
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)
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:59):I'm not sure you need to do that tho
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:59):you should certianly not over-approximate anything
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:59):that's the job of dune
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:59):your job is just to output the rules
Emilio Jesús Gallego Arias (Dec 20 2020 at 15:59):then dune will figure out how to build them
Gregory Malecha (Dec 20 2020 at 16:00):Well, I need something to determine if I should rebuild a _hpp.v file
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:00):that's not your job, but dune's
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:00):yes, you need the rule for the file
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:01):which is of the form {deps} -[action]-> {targets}
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:01):as in Make
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:03):Indeed as long as the deps are "sound", you are fine
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:03):the rest you don't care
Gregory Malecha (Dec 20 2020 at 16:03):I will need to look at your rule above and see how it can work.
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:03):You can perfectly depend on something that does not exist
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:03):dune will look up for a rule to build it
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:03):etc...
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
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?
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:04):I'd start with the rules language
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:04):https://dune.readthedocs.io/en/stable/dune-files.html#rule
Gregory Malecha (Dec 20 2020 at 16:05):Thanks.
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:05):YW
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:05):You can go a long way just by writing dune files
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?"
Gregory Malecha (Dec 20 2020 at 16:06):But it is maybe just an interest, not a requirement
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:07):but intutitively makes a lot of things simpler
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:07):keep in mind the incremental nature / speed
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:07):it really helps rule processing to be able to determine targets statically
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...
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:08):or rules
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:10):and dynamic targets seem pretty rare
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
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
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:12):and moreover they tend to have bad properties
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:12):example for coq native
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:13):than a single rule for both , where targets depend on some build info
Emilio Jesús Gallego Arias (Dec 20 2020 at 16:13):you get much better parallelism I conjecture
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.
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 ...???..))
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.
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
Gregory Malecha (Dec 20 2020 at 18:12):Is there something that I am missing?
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
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
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 18:47):so the rule you propose is right
Emilio Jesús Gallego Arias (Dec 20 2020 at 18:47):what does cpp2v need
Emilio Jesús Gallego Arias (Dec 20 2020 at 18:47):not only the hpp file?
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
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...
Emilio Jesús Gallego Arias (Dec 20 2020 at 18:49):to get deps
Emilio Jesús Gallego Arias (Dec 20 2020 at 18:49):Then, once you have your (rule ...) dune can cache it
Emilio Jesús Gallego Arias (Dec 20 2020 at 18:50):as long as it is deterministic
Gregory Malecha (Dec 20 2020 at 19:09):cpp2v needs the c/c++ file and all transitive dependencies (for #include)
Gregory Malecha (Dec 20 2020 at 19:09):It is very similar to a compiler, but generates a .v rather than a .o
Gregory Malecha (Dec 20 2020 at 19:12):It seems like the limitation is in the language for specifying dependencies
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)
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
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
Emilio Jesús Gallego Arias (Dec 20 2020 at 19:37):[maybe try with a single .h fle]
Emilio Jesús Gallego Arias (Dec 20 2020 at 19:37):file
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.
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.
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.
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?
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)
Paolo Giarrusso (Dec 20 2020 at 20:26):to be clear, can dune parse the -MM syntax today?
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
Paolo Giarrusso (Dec 20 2020 at 20:28):but IIUC the rule for .deps could delegate to make.
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
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.
Rudi Grinberg (Dec 20 2020 at 20:35):Paolo Giarrusso said:
to be clear, can dune parse the
-MMsyntax today?
It doesn't. There hasn't been a need yet.
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 .))
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.
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
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.
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.
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.
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.
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.
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.
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
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.
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
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:
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.
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 :-)
Paolo Giarrusso (Dec 21 2020 at 18:55):(hm still some codegen needed).
Gregory Malecha (Dec 21 2020 at 18:56):There is a version that is public.
Gregory Malecha (Dec 21 2020 at 18:57):But I don't think that it has all of the interesting c++ stuff
Gregory Malecha (Dec 21 2020 at 18:57):github.com/bedrocksystems/cpp2v
Rudi Grinberg (Dec 21 2020 at 19:02):Do you use OCaml at all?
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)
Paolo Giarrusso (Dec 21 2020 at 19:45):also, that involves different stakeholders. So it's good that dune _can_ delegate to make :-)
Gregory Malecha (Dec 21 2020 at 22:52):We do use Ocaml. Currently we have two plugins in non-public repositories.
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 insidedepsyet. 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.
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
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?
Paolo Giarrusso (Jan 07 2021 at 18:44):Seems true; in fact, that rule doesn't have enough dependencies.
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.
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.
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.
Gregory Malecha (Jan 08 2021 at 02:51):Opened https://github.com/ocaml/dune/issues/4089
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
Thomas Letan (Jan 26 2021 at 12:04):Any hint?
Paolo Giarrusso (Jan 26 2021 at 12:21):(Wrong thread?)
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.
Thomas Letan (Jan 26 2021 at 12:49):(yes, sorry!)
Rudi Grinberg (Oct 21 2021 at 02:42):Quick update on the status of dune 3.0 with respect to some of the issues brought up in this thread:
(deps %{read:mydeps}) and go nuts.(include ./file-generated-by-rule). Dune can handle it internally, but we're still hammering out the user facing bits.None of this stuff was the priority for 3.0, so it's still a question if 2. will make it. Fortunately, other goals for 3.0 required us to increase the flexibility of dune's build model internally. This made it much easier to implement features of this sort.
Last updated: Oct 13 2024 at 01:02 UTC