Shachar Itzhaky (Jul 15 2021 at 10:47): Shachar Itzhaky (Jul 15 2021 at 10:47):@Gaëtan Gilbert helpfully pointed out that it is not advisable to run ./configure if one is planning to build with Dune. So we can probably remove it, but it raises the question -- how would we disable the native and bytecode compilers, that were previously set as configure options. Come to think about it, it is possible that already today our Dune build compiles everything and the compilation features are only turned off at runtime (on init). Idk if that's a terrible size overhead, but perhaps we can shave off some.
Emilio Jesús Gallego Arias (Jul 16 2021 at 12:39):@Gaëtan Gilbert advice is incorrect, dune makes running configure _optional_ , and will provide some defaults for developers; however, configure must still be run in many cases and dune does handle and support that case
Emilio Jesús Gallego Arias (Jul 16 2021 at 12:39):Said otherwise, what dune avoids is for many developers to have to do a ./configure -profile devel after a clean
Shachar Itzhaky (Jul 16 2021 at 12:58):cool
Last updated: Apr 18 2024 at 02:01 UTC