We just noticed that one of Frama-C’s tutorials, which tells users to try bogue on a simple plug-in, is broken due to the lack of threads in the libraries section of our dune file.
Frama-C uses dynamic linking for its plug-ins, so when a plug-in requires threads, such as bogue does, if we haven’t thought of it beforehand, it’s too late for the users. They need to recompile everything. Which kind of defeats the purpose of allowing so much extensibility via dynamic linking.
While adding threads seems mostly harmless (does not seem to impact compilation time, nor execution time), we are worried about unintended consequences. If it is “sort of standard”, why isn’t it enabled by default? Do we risk something by just adding it everywhere in our dune files? And, most importantly, are there other similar libraries which we should be linking by default, “just in case” some user may want to write their own (dynamically-loaded) plug-in which will require it?