feat: Add support for user-defined builtins with Dune plugins
This patch adds support for model extensions in Dolmen_loop using a similar mechanism to typing extensions.
Model extensions and typing extensions are now loaded by the binary through Dune's plugin mechanism, and the existing bvconv extension is moved to use the plugin mechanism.
Fixes #203
the existing
bvconvextension is moved to use the plugin mechanism
In retrospect, I am not 100% sure this is a good idea. I did this initially to have an example of usage of the plugin mechanism, but ended up writing two example plugins (abs_real, abs_real_split) which I think is better for that purpose since. I am open to reverting this part of the change.
the existing
bvconvextension is moved to use the plugin mechanism
This was causing build failures on the CI so no longer part of the PR. Instead there is support for builtin extensions when loading them at the CLI level.
I did some late cleanup but this should be ready to review @Gbury
Made the requested changes + some others following (old) offline discussions:
-
Move code dealing with extensions out of the Options module and into a new Extensions module
-
Clean up examples (notably avoid an almost-empty plugin in abs_real_split by defining the builtin in the typing plugin; it does not make sense to use the model plugin without the typing plugin)
-
Load dune plugins lazily
-
Use a hash table to find binary extensions (but not typing extensions/model extensions)
-
Allow override of builtin extensions by dune plugins
@Gbury ping