Paolo Giarrusso (Apr 30 2021 at 20:54): Paolo Giarrusso (Apr 30 2021 at 20:54):I understand that -p enables --release which can change settings... but when looking at logs, little seems changed. On the smallest example, I only see -w -native-compiler-disabled -native-compiler ondemand passed in the normal build but not in the release build...
Paolo Giarrusso (Apr 30 2021 at 20:56):maybe I should just stick to dune install foo --prefix=..., and not use -p on my dev machine
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:56):Release uses a different set of optimizations flags, in particular it enables OCaml's inter-module optimizations, which makes incremental builds much slower as due to inlining etc... if you change a module implementation now you have to rebuild all of the things that depend _on the interface_
Paolo Giarrusso (Apr 30 2021 at 20:56):but for pure Coq code?
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:57):Coq code needs to be rebuilt as coqc is different
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:57):for pure Coq code does nothing ATM
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:57):we use the same flags, tho in release we allow to enable native for example
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:57):dev skips native compilation explictly
Paolo Giarrusso (Apr 30 2021 at 20:57):wait wait, I'm not building coq
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:57):Oh, I see what you mean
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:58):indeed the rebuild seems like a bug
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:58):I agree
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:58):Dune is rebuilding as the flags are different
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:58):but I think there is not reason to have them different in your case indeed, can you open a bug in dune upstream so I keep track of this for 2.9?
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:59):When analyzing what should be rebuilt
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:59):Dune keeps track not only of the deps, but also of the rule
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:59):so in this case we changed the rule [due to the flags] hence the rebuild
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:59):does it make sense @Paolo Giarrusso ?
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:59):thanks for reporting this
Paolo Giarrusso (Apr 30 2021 at 20:59):we agree and I'm filing that bug
Emilio Jesús Gallego Arias (Apr 30 2021 at 20:59):By the way, the question of what dev / release etc... could mean for Coq is open
Emilio Jesús Gallego Arias (Apr 30 2021 at 21:00):so if you have any suggestion
Emilio Jesús Gallego Arias (Apr 30 2021 at 21:00):.v -> .vio -> .vo is usually slower than going to .vo directly
Emilio Jesús Gallego Arias (Apr 30 2021 at 21:00):vos / vok seem like a too radical thing
Emilio Jesús Gallego Arias (Apr 30 2021 at 21:01):so we will add it's own target, not profile
Paolo Giarrusso (Apr 30 2021 at 21:06):filed https://github.com/ocaml/dune/issues/4553
Paolo Giarrusso (Apr 30 2021 at 21:07):vio/vos/vok + caching would be great; I thought that vio was deprecated, but IIUC the problem was only about the build system so maybe you can recover it with dune?
Paolo Giarrusso (Apr 30 2021 at 21:11):but I'm not sure even vio relates to releases?
Emilio Jesús Gallego Arias (Apr 30 2021 at 21:13):I dunno about vio, it is not widely used as it produces files quadratic in size w.r.t. to the document + some other stuff
Paolo Giarrusso (Apr 30 2021 at 21:14):ah I see — the idea's that dev mode could use some of those modes to speed up those builds
Emilio Jesús Gallego Arias (Apr 30 2021 at 21:14):Yeah, we have these modes [and we could have even more]
Last updated: Jun 04 2023 at 23:30 UTC