@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.
@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
Said otherwise, what dune avoids is for many developers to have to do a
./configure -profile devel after a clean
Last updated: May 31 2023 at 02:31 UTC