Stream: jsCoq

Topic: Building Coq


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Jul 16 2021 at 12:58):

cool


Last updated: Jan 30 2023 at 17:03 UTC